J. Slaney, E. Lusk, and W. McCune, "SCOTT: Semantically Constrained OTTER System Description," The International Conference on Automated Deduction (CADE-12), Lecture Notes in Computer Science, Springer, vol. 814, Nancy France, 1994, 1969, pp. 764-768, . [pdf]
This is the announcement of SCOTT 1.0 from the proceedings of CADE-12. SCOTT combines OTTER and FINDER into a new theorem prover.