# MACE4 Model Searcher

MACE4 searches for finite models of first-order statements.

MACE4 is an entirely different program from MACE-2.0 which is distributed with Otter-3, and the input languages are different. MACE-2.0 is usually better for problems with many multiliteral clauses, and MACE4 is usually better for equational problems.

An early version of MACE4 was entered (under the name ICGNS) in the first-order satisfiability division of the 2002 CASC theorem proving competition. Here is the abstract that accompanied the entry, and here are the results of the competition.

## Examples

- You can browse the sample problems in the distribution package.
- Here is an example of a Perl program that calls MACE4.

## Documentation

- The MACE4 manual in PDF
- The MACE4 manual in PostScript

William McCune
Mathematics and Computer Science Division
Argonne National Laboratory