A natural question to ask about a proof system \(\mathcal{P}\) is thus whether it is possible to identify classes of tautologies \(H\) which are ‘hard’ in the sense that any \(\mathcal{P}\)-proof demonstrating that \(\phi \in H\) is valid must be infeasibly long relative to the size of \(\phi\). A positive answer was obtained by Haken (1985) for the system known as resolution on which many automated theorem-provers are based. Haken’s proof made use of Cook and Reckhow’s (1979) observation that we may formulate the Pigeon Hole Principle (PHP) – i.e. the statement that any assignment of \(n+1\) pigeons to \(n\) holes must assign two pigeons to some hole – in propositional logic by using the atomic letter \(P_{ij}\) to express that pigeon \(i\) gets placed in hole \(j\). The formula