@misc{cogprints414,
           month = {July},
           title = {A Tough Nut for Proof Procedures},
          author = {John McCarthy},
            year = {1964},
             url = {http://cogprints.org/414/},
        abstract = {It is well known to be impossible to tile with dominoes a checkerboard with two opposite corners deleted. This fact is readily stated in the first order predicate calculus, but the usual proof which involves a parity and counting argument does not readily translate into predicate calculus. We conjecture that this problem will be very difficult for programmed proof procedures,.}
}

<script src="//archive-bar.soton.ac.uk/archive-bar.js"></script>