On the complexity of regular resolution and the Davis-Putnam procedure

For infinitely many n > 0 we construct contradictory formulas α_n in conjunctive form with n literals such that every regular proof tree which proves the contradiction must contain 2^cn distinct clauses for some c > 0. This implies a 2^cn lower bound for the number of distinct clauses which are generated by the Davis-Putnam procedure applied to α_n using any order of variable elimination.