  We consider sets $\Gamma(n,s,k)$ of narrow clauses expressing that no
definition of a size $s$ circuit with $n$ inputs is refutable in resolution R
in $k$ steps. We show that every CNF shortly refutable in Extended R, ER, can
be easily reduced to an instance of $\Gamma(0,s,k)$ (with $s,k$ depending on
the size of the ER-refutation) and, in particular, that $\Gamma(0,s,k)$ when
interpreted as a relativized NP search problem is complete among all such
problems provably total in bounded arithmetic theory $V^1_1$.
  We use the ideas of implicit proofs to define from $\Gamma(0,s,k)$ a
non-relativized NP search problem $i\Gamma$ and we show that it is complete
among all such problems provably total in bounded arithmetic theory $V^1_2$.
The reductions are definable in $S^1_2$.
  We indicate how similar results can be proved for some other propositional
proof systems and bounded arithmetic theories and how the construction can be
used to define specific random unsatisfiable formulas, and we formulate two
open problems about them.

Logic;Logic in Computer Science