NAME

       mace4 - searches for finite countermodels of first-order statements

SYNOPSIS

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

DESCRIPTION

       This manual page documents briefly the mace4 command.

       The  program  mace4  searches  for finite structures satisfying first-order and equational
       statements, the same kind of statement that prover9(1) accepts. If the  statement  is  the
       denial  of  some  conjecture,  any  structures  found  by mace4 are counterexamples to the
       conjecture.  mace4 can be a valuable complement to prover9(1), looking for counterexamples
       before  (or  at  the  same time as) using prover9(1) to search for a proof. It can also be
       used to help debug input clauses and formulas for prover9(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.

       -help  This tells mace4 to print a summary of these command-line options.

       -n n   This  gives the starting domain size for the search. The default value is 2. If you
              also give an -N option, mace4 will iterate domain sizes up through  the  -N  value,
              using an increment given by the -I value. Otherwise, mace4 will search only for the
              -n value.

       -N n   This gives the ending domain size for the search. The default is 10.

       -i n   This gives the domain size increment for the search. The default is 1.

       -q n   This flag overrides the parameter iterate. It says to try the sizes that are  prime
              numbers, from -n up through -N.

       -m n   Stop searching when the nth structure has been found.  The default is 1.

       -t n   Stop searching after n seconds.

       -s n   Allow  at  most n seconds for each domain size. The parameter can be used (together
              with -t) to give an overall time limit.

       -b n   Stop searching when (about) n megabytes of memory have been used.

       -V n   A 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 `_'.

       -P n   If  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 as  isofilter(1)
              and interpformat(1).

       -p n   If  this flag is set, and if -P is clear, all structures that are found are printed
              in a tabular form.

       -R n   If 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.

       -v n   If  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.)

       -T n   If  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 original mace4 manual.

SEE ALSO

       prover9(1).
       Full  documentation  for mace4 is found in the prover9 manual, available on Debian systems
       in the prover9-doc package at /usr/share/doc/prover9-doc/manual/index.html.
       The     original     mace4     manual,      which      can      be      downloaded      at
       http://www.cs.unm.edu/~mccune/prover9/mace4.pdf

AUTHOR

       mace4 was 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)