Ivy is a preprocessor and proof checker for resolution/paramodulation theorem provers. It is coded in ACL2 and proved sound for finite interpretations.
Ivy is distributed with ACL2, in the directory books/workshops/1999/ivy. Check the main ACL2 page for information on how to obtain and intall ACL2 and the separate workshop file. Or, obtain a separate version of Ivy from the ACL2 site here.
Or, you can take the version that we sent to the ACL2 maintainers (April 12, 2000). This contains everything: the Ivy source and theorems (ACL2 books), full distributions of Otter-3.0.6 and MACE-1.3.4, examples, and exercises. (Some of the README files and makefiles are different.)