Haken showed that any resolution proof of \(\text{PHP}_n\) must have size at least exponential in \(n\). From this it follows that resolution is not polynomially bounded. However, it was later shown by Buss (1987) that the system \(\mathcal{P}_1\) (and hence also systems like \(\mathcal{P}_2\), \(\mathcal{P}_3\) which can be shown to efficiently simulate \(\mathcal{P}_1\)) do admit proofs of \(\text{PHP}_n\) which are of size polynomial in \(n\). One subsequent direction of research in proof co