@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,.}
}