We prove that every property of 3CNF formulas that implies
unsatisfiability and is expressible in Datalog
has asymptotic probability zero when formulas are
randomly generated by taking $6n$ non-trivial clauses
of exactly three literals uniformly and independently.
Our result is a consequence of designing a winning
strategy for Duplicator in the existential $k$-pebble game
on the structure that encodes the 3CNF formula and
a fixed template structure encoding a satisfiable formula.
The winning strategy makes use of certain extension
axioms that we introduce and hold almost surely on
a random 3CNF formula. An interesting feature of our
result is that it brings the fields of Propositional
Proof Complexity and Finite Model Theory together.
To make this connection more explicit, we show that
Duplicator wins the existential pebble game on
the structure encoding the Pigeonhole Principle
and the template structure above. Moreover, we also prove
that there exists a $2k$-Datalog program expressing that
an input 3CNF formula has a Resolution refutation of
width $k$. As a consequence to our result and the known
size-width relationship in Resolution, we obtain
new proofs of the exponential lower bounds for Resolution
refutations of random 3CNF formulas and the Pigeonhole