1        ------------------
2        Otter, Version 3.3    Search for Proofs
3        ------------------
4        ------------------
5        Mace,  Version 2.2    Search for Countermodels
6        ------------------
7
8(Also see index.html in this directory.)
9
10----------------
11OTTER HIGHLIGHTS
12----------------
13
14Over the years we've added many experimental features to Otter,
15but the basic functions haven't changed much in the past
16ten years.
17
18The Otter package now includes Mace 2 (as a separate program).
19
20----------------
21Mace2 HIGHLIGHTS
22----------------
23
24Mace2 is now in independent program.  It no longer calls Otter
25to parse the input.  It still accepts the same inputs as Otter.
26Performance is sometimes better than in previous versions
27(see mace2/README.22).
28
29----------------
30DOCUMENTS
31----------------
32
33The documents directory contains a (newly updated) Otter 3.3
34manual and a Mace 2.0 manual.  See documents/README.
35
36----------------
37FETCHING
38----------------
39
40Download Otter 3.3 and Mace 2.2 from the Otter Web page:
41
42  http://www.mcs.anl.gov/AR/otter/
43
44----------------
45INSTALLING AND TESTING (for unix-like systems)
46----------------
47
48Unpack the package with a command something like
49
50  % gunzip -c otter-3.3.tar.gz | tar xvf -
51
52Then
53
54  % cd otter-3.3
55
56If you are on a recent linux or Macintosh system, try
57
58  % make install      (this just copies pre-compiled binaries to ./bin/)
59  % make test-otter
60  % make test-mace2
61
62Macintosh users:  If you see "make: Command not found.", it means
63you don't have the developer's tools (compliers, etc.) installed.
64The good news is that you don't need them.  Instead, run the commands
65"./make-install", "./make-test-otter", and "./make-test-mace2".
66
67If test-otter gives a proof and test-mace2 gives a model, everything is
68probably okay.  The binaries should be in the directory bin/.
69
70If something goes wrong, try
71
72  % make all
73
74THEN
75
76  % make test-otter
77  % make test-mace2
78
79If any of that fails, see README.make.
80
81To run the Otter test suite, "cd examples; ./Run_all".
82To run the Mace2 test suite, "cd examples-mace; ./Run_all".
83
84The Otter web page is http://www.mcs.anl.gov/AR/otter/
85
86  W. McCune   (otter@mcs.anl.gov)
87  Argonne National Laboratory
88  August, 2003 (updated August 2004)
89