Unrestricted resolution versus N-resolution

AbstractAn N-resolution proof is a resolution proof in which the resolution rule is restricted: one clause to which it is applied must only consist of negative literals. N-resolution is complete (Schöning (1987), p. 109, Stickel (1985), p. 86). We construct an infinite family of propositional formulas and show: These formulas have unrestricted resolution proofs whose length is polynomially bounded in their size. All N-resolution proofs of these formulas are of superpolynomial length