OTTER (Organized Techniques for Theorem-proving and Effective Research) is a resolution-style theorem-proving program for first-order logic with equality. OTTER includes the inference rules binary resolution, hyperresolution, UR-resolution, and binary paramodulation. Some of its other abilities and features are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, evaluable functions and predicates, and Knuth-Bendix completion. OTTER is coded in C, is free, and is portable to many different kinds of computer.

This document reports on the work done by the Separations Science and Technology Programs of the Chemical Technology Division, Argonne National Laboratory, in the period October 1991-March 1992. This effort is mainly concerned with developing the TRUEX process for removing and concentrating actinides from acidic waste streams contaminated with transuranic (TRU) elements. The objectives of TRUEX processing are to recover valuable TRU elements and to lower disposal costs for the nonTRU waste product of the process.