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.outThe 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.)