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), 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), formed(1), otter(1), pl(1).
       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).

                                                November  5, 2006                                       MACE2(1)