Egly answers a question raised by Urquhart in a 1995 paper [1], where he proves that resolution with limited extension (Rle), a Gentzen system G based on the biconditional ( as the only connective, and G extended by the analytic cut rule (Gacut) can polynomially simulate (p-simulate) each other.

The justification for these p-simulations is that an application of an analytic cut rule can be simulated by the rules for ( and by limited extensions. The question answered in the paper is whether such a p-simulation extends to a Gentzen system with all the usual connectives. The author shows that a p-simulation only exists between Gacut and Rle and that there are no p-simulations between G and Gacut or between G and Rle.

The second section familiarizes readers with the definitions and notations used throughout the paper. The author uses a variant of a sequent calculus, where the form of the proof is not restricted to tree form and the logical axioms are not restricted to the form A+ A for an atom.

The third section presents the proof of the main result.

The paper is well written and concise. The result supplements previous work in the propositional calculus.