Meeting the challenge of fifty years of logic

In this article, we tell a story of good fortune. The good fortune concerns the discovery of a systematic approach to compress 50 years of excellent research in logic into a single day's use of an automated reasoning program. The discovery resulted from a colleague's experiment with a new representation and a new use of the weighting strategy. The experiment focused on an attempt—which I knew would fail—to prove one of the benchmark theorems that had eluded us for years. Fortunately, I was wrong; my colleague's attempt was successful, and a proof was found. The proof led to proving in one day 13 theorems, theorems that resulted from 50 years of excellent research in logic. We present these theorems as intriguing problems to test the power of a reasoning program or to evaluate the effectiveness of a new idea. In addition to the challenge problems, we discuss a possible approach to finding short proofs and the results achieved with it.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.