摘要：One of the earliest proposed hard problems for theorem provers is a propositional version of the Mutilated Chessboard problem. It is well known from recreational mathematics: Given a chessboard having two diagonally opposite squares removed, prove that it cannot be covered with dominoes. In Proof Complexity, we consider not ordinary, but 2n * 2n mutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution.
