In 1971, Overbeek came to Northern Illinois University, not far from Argonne, met Wos, and redesigned FTP in order to merge the two lines of development represented by RW1 and FTP. The new system was called WOS1. It contained all the features of both of its predecessors, thus starting another tradition of the Argonne family, that (for the most part) each new system would not be a small system designed to illustrate or validate a single idea, but rather the union of all that had gone before, in order to accumulate a really powerful system. Thus WOS1 had function symbols and paramodulation, hyperresolution and weighting, and was based on the closure algorithm. Its implementation, particularly the sophisticated indexing method (FPA lists) that made the speed of the unification algorithm largely irrelevant, is described in [21].
This system was used for an extensive set of experiments, on all the problems that the group could assemble, and the results published, along with the precise statements of the problems[13]. This paper has served as a model for subsequent collections of problems. It represents a snapshot of the capabilities of the Argonne system of the early seventies. The paper was presented at the Argonne Workshop on Automated Theorem Proving, which was retroactively named CADE-1. The system ran on the supercomputer of its day, the IBM 360/195, and was written in 40,000 lines of assembly language. Its capabilities and limitations are precisely documented in [13].
It was thought by some that the power of this system came primarily from its implementation in assembly language. This was not true. Assembly language provided the most convenient method of the time to implement sophisticated data structures, which provided the ``secret'' of the system's performance. High performance without redundancy control just makes the combinatorial explosion occur faster. It was the use of the closure algorithm and data structures to support fast subsumption and resolution that underlay the capabilities of that system.