Prover9 Manual Version June-2006

Mace4

The program Mace4 [McCune-Mace4] searches for finite models of first-order and equational statements, the same kind of statement that Prover9 accepts. If the statement is the denial of some conjecture, any models found by Mace4 are counterexamples to the conjecture.

Mace4 can be a valuable complement to Prover9, looking for counterexamples before (or at the same time as) using Prover9 to search for a proof. It can also be used to help debug input clauses and formulas for Prover9.

For the most part, Mace4 accepts the same input files as Prover9. If the input file contains commands that Mace4 does not understand, then the argument "-c" must be given to tell Mace4 to ignore those commands.

For example, say you've just invented group theory, and you're wondering if all groups are commutative. You can run the following two jobs in parallel, with Prover9 looking for a proof, and Mace4 looking for a counterexample.

prover9  -f x2.in > x2.prover9.out
mace4 -c -N10 -f x2.in > x2.mace4.out
The following command is helpful.

mace4 -help

The models in Mace4 output files can be transformed in various ways with the program Interpformat. Here are examples.

interpformat portable -f x2.mace4.out > x2.portable
interpformat portable2 -f x2.mace4.out > x2.portable2
interpformat tabular -f x2.mace4.out > x2.tabular
interpformat raw -f x2.mace4.out > x2.raw
interpformat cooked -f x2.mace4.out > x2.cooked
interpformat xml -f x2.mace4.out > x2.xml
interpformat tex -f x2.mace4.out > x2.tex

For further information see the Mace4 Web page. (The PDF manual on the Mace4 Web page is somewhat out of date.)