Hard examples for resolution
Alasdair Urquhart · Journal of the ACM · 1987
Exponential lower bounds are proved for the length-of-resolution refutations of sets of disjunctions constructed from expander graphs, using the method of Tseitin. Since these sets of clauses encode biconditionals, they have short (polynomial-length) refutations in a standard axiomatic formulation of propositional calculus.