@article{GALIL197723,
    Abstract = {For infinitely many n > 0 we construct contradictory formulas {$\alpha$}n in conjunctive form with n literals such that every regular proof tree which proves the contradiction must contain 2cn distinct clauses for some c > 0. This implies a 2cn lower bound for the number of distinct clauses which are generated by the Davis-Putnam procedure applied to {$\alpha$}n using any order of variable elimination.},
    Author = {Galil, Zvi},
    File = {On the complexity of regular resolution and the Davis-Putnam procedure - 1-s2.0-0304397577900548-main.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Number = {1},
    Pages = {23-46},
    Title = {On the complexity of regular resolution and the Davis-Putnam procedure},
    URL = {https://www.sciencedirect.com/science/article/pii/0304397577900548},
    Volume = {4},
    Year = {1977},
    bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/0304397577900548},
    bdsk-url-2 = {https://doi.org/10.1016/0304-3975(77)90054-8},
    date-added = {2021-08-04 12:27:08 +0200},
    date-modified = {2021-08-04 12:27:08 +0200},
    doi = {10.1016/0304-3975(77)90054-8}
}

@article{GALIL197723, Abstract = {For infinitely many n > 0 we construct contradictory formulas {$\alpha$}n in conjunctive form with n literals such that every regular proof tree which proves the contradiction must contain 2cn distinct clauses for some c > 0. This implies a 2cn lower bound for the number of distinct clauses which are generated by the Davis-Putnam procedure applied to {$\alpha$}n using any order of variable elimination.}, Author = {Galil, Zvi}, File = {On the complexity of regular resolution and the Davis-Putnam procedure - 1-s2.0-0304397577900548-main.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Number = {1}, Pages = {23-46}, Title = {On the complexity of regular resolution and the Davis-Putnam procedure}, URL = {https://www.sciencedirect.com/science/article/pii/0304397577900548}, Volume = {4}, Year = {1977}, bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/0304397577900548}, bdsk-url-2 = {https://doi.org/10.1016/0304-3975(77)90054-8}, date-added = {2021-08-04 12:27:08 +0200}, date-modified = {2021-08-04 12:27:08 +0200}, doi = {10.1016/0304-3975(77)90054-8} }