Provided by: prover9_0.0.200911a-2.1build1_amd64

**NAME**

mace4 - searches for finite countermodels of first-order statements

**SYNOPSIS**

mace4[options] <input-file>output-file

**DESCRIPTION**

This manual page documents briefly themace4command. The programmace4searches for finite structures satisfying first-order and equational statements, the same kind of statement thatprover9(1) accepts. If the statement is the denial of some conjecture, any structures found bymace4are counterexamples to the conjecture.mace4can be a valuable complement toprover9(1), looking for counterexamples before (or at the same time as) usingprover9(1) to search for a proof. It can also be used to help debug input clauses and formulas forprover9(1).

**OPTIONS**

A summary of options is included below. Options override the equivalent settings given in the input file. To set or clear a flag, you must give 1 or 0 as the value.-helpThis tellsmace4to print a summary of these command-line options.-nnThis gives the starting domain size for the search. The default value is 2. If you also give an-Noption,mace4will iterate domain sizes up through the-Nvalue, using an increment given by the-Ivalue. Otherwise,mace4will search only for the-nvalue.-NnThis gives the ending domain size for the search. The default is 10.-inThis gives the domain size increment for the search. The default is 1.-qnThis flag overrides the parameter iterate. It says to try the sizes that are prime numbers, from-nup through-N.-mnStop searching when thenth structure has been found. The default is 1.-tnStop searching afternseconds.-snAllow at mostnseconds for each domain size. The parameter can be used (together with-t) to give an overall time limit.-bnStop searching when (about)nmegabytes of memory have been used.-VnA rule is needed for distinguishing variables from constants in clauses and formulas with free variables. If this flag is clear, variables start with (lower case) `u' through `z'. If this flag is set, variables in clauses start with (upper case) `A' through `Z' or `_'.-PnIf this flag is set, all structures that are found are printed in `standard' form, which means they are suitable as input to other LADR programs such asisofilter(1) andinterpformat(1).-pnIf this flag is set, and if-Pis clear, all structures that are found are printed in a tabular form.-RnIf this flag is set, a ring structure is is applied to the search. The operations {+,-,*} are assumed to be the ring of integers (mod domain_size). This method puts a tight constraint on the search, allowing much larger structures to be investigated.-vnIf this flag is set, the output file receives information about the search, including the initial partial model (the part of the model that can be determined before backtracking starts) and timing and other statistics for each domain size. (It does not give a trace of the backtracking, so it does not consume a lot of file space.)-TnIf the trace flag is set, detailed information about the search, including a trace of all assignments and backtracking, is printed to the standard output. This flag causes a lot of output, so it should be used only on small searches. There also exist a number of advanced options, which are used for experimentation with search methods. They can be ignored by nearly all users. For descriptions of these options, see the originalmace4manual.

**SEE** **ALSO**

prover9(1). Full documentation formace4is found in theprover9manual, available on Debian systems in theprover9-docpackage at/usr/share/doc/prover9-doc/manual/index.html. The originalmace4manual, which can be downloaded at http://www.cs.unm.edu/~mccune/prover9/mace4.pdf

**AUTHOR**

mace4was written by William McCune <mccune@cs.unm.edu> This manual page was written by Peter Collingbourne <peter@pcc.me.uk>, for the Debian project (but may be used by others). August 12, 2007 MACE4(1)