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 complexity has been to identify additional proof systems for which PHP or related combinatorial principles are also hard.  See, e.g., Buss (2012), Segerlind (2007).