Resolution lower bounds for the weak pigeonhole principle. - Raz, R. (Journal of the ACM)
We prove that any Resolution proof for the weak pigeonhole principle, with n holes and any number of pigeons, is of length Ω(2nε), (for some global constant ε > 0). One corollary is that a certain propositional formulation of the statement NP ⊄ P/poly does not have short Resolution proofs.