Contents of Otter FTP directory
                  ===============================

This directory is out of date.  Our software and papers are
available directly from various web pages.

CURRENT SOFTWARE
----------------
otter-3.0.5.tar.Z    First-order theorem prover (February 19, 1998).
otter.tar.Z          A symbolic link to the current version of Otter.
Otter-Changelog      Recent changes in Otter.

DOSOT304.EXE         Otter 3.0.4 for DOS (August 16, 1995).
DOSOT304.TXT         Introduction to Otter 3.0.4 for DOS.

MACOT304.HQX         Otter 3.0.4 for Macintosh (September 20, 1995).
MACOT304.TXT         Introduction to Otter 3.0.4 for Macintosh.

mace-1.2.0.tar.Z     First-order model searcher (August 16, 1995).
mace.tar.Z           A symbolic link to the current version of MACE.

OLD SOFTWARE (directory old_stuff)
------------
otter-3.0.4.tar.Z    (August 16, 1995)
otter-3.0.3.tar.Z    (August 27, 1994)
otter-3.0.2.tar.Z    (June 16, 1994)
otter-3.0.0.tar.Z    (January 24, 1994)

anldp-1.0.0.tar.Z -- Program (now called MACE) to serach for models.

DOSOT301.TXT -- Introduction to DOSOT301.EXE.   (Feb 21, 1994).

DOSOT301.EXE -- Self-extracting (LHA) archive of DOS version of Otter 3.0.1.
                (Feb 21, 1994).

Macintosh - Otter 3.0.0 for Mac (not well organized).

BOBOT301.EXE -- Otter (.EXE only) that allows 250 variables; otherwise,
	the same as the otter .exe in DOSOT301.  (Aug 1, 1994).

PROTOTYPE SOFTWARE
------------------
otterface-0.1.tar.Z -- Prototype GUI (in tcl/tk) for Otter.

prf_disp.tar.Z -- Prototype proof display (in tcl/tk) for Otter proofs.
                  (doesn't work for recent versions of Otter)

QED/check-4.tar.gz - a proof checker for Otter proofs (requires Nqthm).

OTHER STUFF
-----------

Papers -- some papers related to Otter.

index.tar.Z -- Term sets used for "Experiments with Discrimination Tree
	Indexing and Path Indexing for Term Retrieval".

otter_jobs.tar.Z -- Input files and Otter output files for experiments
	presented in "Experiments with ROO, a Parallel Automated
	deduction system", by Lusk and McCune.

LT-WAL -- a directory of input files and proofs related to the paper
	"Single Identities for Lattice Theory and for Weakly Associative
	Lattices", by W. McCune and R. Padmanabhan.

*******************************************************************************
*  DON'T FORGET TO USE BINARY MODE WHEN FTPing .Z, .exe, OR EXECUTABLE FILES. *
*******************************************************************************

After you have fetched a compressed tar file, say file.tar.Z,
you can unpack it in the usual way with the following UNIX commands.

   uncompress file.tar.Z
   tar xvf file.tar