On the Comparative Complexity of Resolution and the Connection Method

Quadratic proofs of the pigeonhole formulas are presented using the connection method proof techniques. For this class of formulas exponential lower bounds are known for the length-of-resolution refutations. This indicates a significant difference in the power of these two proof techniques. While short proofs of these formulas are known using extended resolution, this particular proof technique, in contrast to both the connection method and resolution, seems not suitable for the actual proof search.