We prove lower bounds of the form exp\left(n^{\epsilon_d}\right),
\epsilon_d>0, on the length of proofs of an explicit sequence of
tautologies, based on the Pigeonhole Principle, in proof systems
using formulas of depth d, for any constant d. This is the
largest lower bound for the strongest proof system, for which any
superpolynomial lower bounds are known.