After Bill McCune joined Argonne in 1984, he undertook a complete rewrite of the system during 1987-1988 in order to recapture the speed of the early systems and provide a tool that could absorb new theory and new implementation techniques he wanted to experiment with. This system became OTTER[14], still the system most used at Argonne, and also in use by many others around the world.
OTTER discarded many of the LMA features designed for flexibility in order to be a small, fast system. It is currently a batch-only system, and it imposes limits on term sizes, etc., although it is easy to change these at compile time. It is written in C. Two notable features are indexing via discrimination trees for forward subsumption (See [16] for a full discussion of indexing issues.) and the use of lexical recursive path ordering for rewrite rule manipulation.
OTTER has been used in a number of investigations that have led to the solutions of open problems, particularly in the areas of combinatory logic[19] and axiom systems for groups[17,15]. It was also used by Overbeek in the solution of open questions posed in Smullyan's To Mock a Mockingbird. In fact, for a time OTTER was installed in such a way that it could answer email that asked it to solve certain problems about combinatory logic. OTTER's speed has been put to good use as many of the single axiom problems required submitting thousands of OTTER runs in an automated way. OTTER is very widely distributed, being available both by anonymous ftp and on a diskette bound into the book [28]. It runs on IBM-compatible personal computers and Macintoshes as well as on most Unix machines. Very recent enhancements include a graphics-based tool for manipulating formulas[2] and a customizable Prolog-style operator input language extension[18].