We prove an exponential lower bound for tree-like Cutting Planes
refutations of a set of clauses which has polynomial size resolution
refutations. This implies an exponential separation between tree-like
and dag-like proofs for both Cutting Planes and resolution; in both
cases only superpolynomial separations were known before.
In order to ... more >>>

This paper gives two distinct proofs of an exponential separation
between regular resolution and unrestricted resolution.
The previous best known separation between these systems was
quasi-polynomial.