---
name: "mace2"
section: "1"
platform: "linux"
package: "mace2"
version: "3.3f-1.1"
release: "Debian 8 (Jessie)"
platforms: ["linux"]
url: "https://new.carta.tech/mace2"
---

# mace2(1)

searches for finite countermodels of first-order statements

## NAME

mace2 - searches for finite countermodels of first-order statements

## 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)](/otter/1.md), 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.*

## SEE ALSO

[**anldp**(1)](/anldp/1.md), [**formed**(1)](/formed/1.md), [**otter**(1)](/otter/1.md), [**pl**(1)](/pl/1.md).\
 *Full documentation for* **mace2** *is found in /usr/share/doc/mace2/mace2.{html,ps.gz}.*

## AUTHOR

**mace2** *ws written by William McCune \<otter@mcs.anl.gov\>*

*This manual page was written by Peter Collingbourne \<pcc03@doc.ic.ac.uk\>,* *for the Debian project (but may be used by others).*