Alexander Razborov

We show that every resolution proof of the {\em functional} version

$FPHP^m_n$ of the pigeonhole principle (in which one pigeon may not split

between several holes) must have size $\exp\of{\Omega\of{\frac n{(\log

m)^2}}}$. This implies an $\exp\of{\Omega(n^{1/3})}$ bound when the number

of pigeons $m$ is arbitrary.