  We prove logarithmic depth lower bounds in Stabbing Planes for the classes of
combinatorial principles known as the Pigeonhole principle and the Tseitin
contradictions. The depth lower bounds are new, obtained by giving almost
linear length lower bounds which do not depend on the bit-size of the
inequalities and in the case of the Pigeonhole principle are tight.
  The technique known so far to prove depth lower bounds for Stabbing Planes is
a generalization of that used for the Cutting Planes proof system. In this work
we introduce two new approaches to prove length/depth lower bounds in Stabbing
Planes: one relying on Sperner's Theorem which works for the Pigeonhole
principle and Tseitin contradictions over the complete graph; a second proving
the lower bound for Tseitin contradictions over a grid graph, which uses a
result on essential coverings of the boolean cube by linear polynomials, which
in turn relies on Alon's combinatorial Nullenstellensatz.
