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 prove this, we extend the lower bounds on the depth of
monotone circuits of Raz and McKenzie (FOCS 97) to monotone real
circuits.

In the case of resolution, we further improve this result by giving an
exponential separation of tree-like resolution from (dag-like) regular
resolution proofs. In fact, the refutation provided to give the upper
bound respects the stronger restriction of being a Davis-Putnam
resolution proof. This extends the corresponding superpolynomial
separation of Urquhart (BSL 1995).

Finally, we prove an exponential separation between Davis-Putnam
resolution and unrestricted resolution proofs; only a superpolynomial
separation was previously known (Goerdt, Ann. Math. AI 1992).