On a Solution of the mutilated Checkerboard Problem Using the Theorema Set Theory Prover

The Mutilated Checkerboard Problem has some tradition as a benchmark problem for automated theorem proving systems. Informally speaking, it states that an 8 by 8 checkerboard with the two opposite corners removed cannot be covered by dominoes. Various solutions using different approaches have been presented since its original statement by John McCarthy in 1964. An elegant four-line proof has been given on paper by McCarthy himself in 1995, which is based on a formulation of the original problem in set theory. Since then, the checkerboard problem stands as a benchmark problem in particular also for automated set theory provers. In this paper, we are going to present a complete proof of the checkerboard problem using the {\itshape Theorema} {\itshape Set Theory prover}.