  We study Frege proofs for the one-to-one graph Pigeon Hole Principle defined
on the $n\times n$ grid where $n$ is odd. We are interested in the case where
each formula in the proof is a depth $d$ formula in the basis given by $\land$,
$\lor$, and $\neg$. We prove that in this situation the proof needs to be of
size exponential in $n^{\Omega (1/d)}$. If we restrict the size of each line in
the proof to be of size $M$ then the number of lines needed is exponential in
$n/(\log M)^{O(d)}$. The main technical component of the proofs is to design a
new family of random restrictions and to prove the appropriate switching
lemmas.
