## SYNOPSIS

**mace2**[

*options*] <

*input-file*>

*output-file*

## DESCRIPTION

This manual page documents briefly the**mace2**command.

**mace2** is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland-Logeman procedure decides the propositional problem, and any models found are translated to first-order models. **mace2** is a useful complement to the theorem prover
**otter**(1),
with **otter** searching for proofs and **mace2** looking for countermodels.

## OPTIONS

A summary of options is included below.**-n***n*-
This gives the starting domain size for the search. The default value is 2. If you also give an
**-N**option, MACE will iterate domain sizes up through the**-N**value. Otherwise,**mace2**will search only for the**-n**value. **-N***n*-
This gives the ending domain size for the search. The default is the value of the
**-n**option. **-c**-
This says that constants in the input should be assigned unique elements of the domain. If the number of constants in the input is greater than the domain size
*n*, the first*n*constants are given values, and the rest are unconstrained. This is a useful option because it eliminates lots of isomorphism from the search. But it can block all models, especially when used with other constraints. **-p**-
This option tells
**mace2**to print models in a nice tabular form as they are found. This format is meant for human consumption. **-P**-
This option tells
**mace2**to print models in an easily parsable form. This format has an**otter**-like syntax and can be read by most Prolog systems. **-I**-
This option tells
**mace2**to print models in IVY form. This format is a Lisp S-expression and is meant to be read by IVY, our proof and model checker. **-m***n*-
This tells
**mace2**to stop after finding*n*models. The default is 1. **-t***n*-
This tells
**mace2**to stop after about n seconds. The default is unlimited.**mace2***ignores any assign(max_seconds, n) commands that might be in the input file. Such commands are used by***otter***only.* **-k***n*-
This tells
**mace2**to stop if it tries to allocate more than*n*kilobytes of memory. The default is 48000 (about 48 megabytes).**mace2***ignores any assign(max_mem, n) commands that might be in the input file. Such commands are used by***otter***only.* **-x**-
This is a special-purpose constraint designed to reduce isomorphism in quasigroup problems. It applies only to binary function
*f*. **-h**-
This tells
**mace2**to print a summary of these command-line options.

## AUTHOR

**mace2**ws written by William McCune <[email protected]>

This manual page was written by Peter Collingbourne <[email protected]>, for the Debian project (but may be used by others).