On bounded depth proofs for Tseitin formulas on the grid; revisited

Johan Håstad, Kilian Risse

We study Frege proofs using depth-$d$ Boolean formulas for the Tseitin contradiction on $n\times n$ grids. We prove that if each line in the proof is of size $M$ then the number o…