"Planar" tautologies hard for resolution

We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a 2^Ω(n) lower bound for any resolution proof of the mutilated chessboard problem on a 2n×2n chessboard as well as for the Tseitin tautology (G. Tseitin, 1968) based on the n×n rectangular grid graph. The former result answers a 35 year old conjecture by J. McCarthy (1964).