Argonne National Laboratory has been a center of research in automated theorem proving for nearly thirty years. In that time Argonne scientists and collaborators have developed a long series of theorem-proving systems with which to explore this fascinating field. Since the first systems of the mid-sixties, many features have changed of course, but others, perhaps the most fundamental, have remained the same. We survey here some of the history of those theorem-proving programs from the earliest to the most current, focusing in particular on the fundamental approach that has remained basically unchanged as a framework for the implementation of new ideas as they have come along. We will also try to identify the strengths and weaknesses of each of the systems by describing some of the problems that each could solve and could not solve, thus motivating the ideas for the next, system.