For each $k \geq 1$, we give a famiily of unsatisfiable sets of
clauses which have polynomial size ${\mbox{Res}}(k+1)$ refutations, but which
require ${\mbox{Res}}(k)$ refutations of $2^{n^{\epsilon_k}}$. This improves
the superpolynomial- separation between resolution and ${\mbox{Res}}(2)$ given
by Bonet and Galesi to exponential. As a corollary, we obtain an exponential
separation between depth 0 Frege and depth 1 Frege, improving upon the
superpolynomial separation given by the weak pigeonhole principle.
Pre-2018 CSE ID: CS2002-0697