Ivy is a system that checks Otter proofs and MACE models.
Ivy is coded in ACL2 and many soundness metatheorems have
been proved about the various programs in Ivy.  See 

       http://www.mcs.anl.gov/~mccune/acl2/ivy

Ivy-2 is the current version.  Otter-3.0.6 and MACE-1.3.4
come bundled with Ivy-2.  If you wish to have Ivy-2 call Otter-3.3
and MACE-2. instead, you can do so by updating 2 Ivy files (after
configuring Ivy):

ivy-v2/ivy-sources/util/otter-mace.lisp

    Change the line 
        (defvar mace-parms "6 60 -m1 -I -c")
    to
        (defvar mace-parms "-N6 -t60 -I")

ivy-v2/ivy-sources/util/ivy

    Change the lines that begin

        set otter_binary=
        set mace_binary=

    so that they refer to the Otter-3.3 and MACE-2.1 binaries, for example,

        set otter_binary=/homes/mccune/bin-linux/otter33
        set mace_binary=/homes/mccune/bin-linux/mace21