-------------------------------------------------------------------------------
   MAEDMAX
-------------------------------------------------------------------------------

Welcome to maedmax! Maedmax implements ordered completion, extending the
powerful completion tool Maxcomp [0].

Besides OCaml, camlp4, ocamlfind, and Ocamlbuild [1], it requires Yices1 [2],
the OCamlYices [3] bindings for OCaml, and the json library Yojson [4] as well
as xml-light [5] for output.

Using OCamlbuild, the Maedmax executable can be created by executing
 $ make
in this directory.

-------------------------------------------------------------------------------
   USAGE
-------------------------------------------------------------------------------

The usage of Maedmax is as follows:
 $ ./maedmax <options> <input>

where the input file can be in TPTP [6] or trs format [7].
In case you are happy with the default options, you can simply e.g. call
 $ ./maedmax examples/RNG042-2.tptp

A TPTP proof is produced when using the flag -P tstp:
 $ ./maedmax -P tstp examples/GRP696-1.p

-------------------------------------------------------------------------------
   OPTIONS
-------------------------------------------------------------------------------

You can also specify a number options, as for instance in the calls
 $ ./maedmax --xsig examples/MN90_Ex4_5_ACgroups_exp2.tptp
 $ ./maedmax --cpf examples/GRP154-1.tptp
 $ ./maedmax -T 5 -M olpo -K 2 -N 10 examples/RNG042-2.tptp

Here is what these (and all other) options mean:
 - A timeout in seconds can be specified using option -T.
 - The termination strategy can be controlled with the option -M, which takes an
   additional string specifying the strategy.  Possible values for -M are olpo
   for LPO, okbo for KBO, or olpokbo for a combination (which is the default).
 - Ground joinability is attempted to be proven over an extended signature, i.e.
   the signature extended by infinitely many constants when using option --xsig.
 - The tool attempts to produce a proof in the certifiable CPF format when
   called with option --cpf.
 - The tool can also be run in standard completion mode using option --kb. In
   this mode it closely resembles maxcomp.
 - A number of options allows to control parameters of the maximal completion
   procedure and the ground confluence checks. All of the following require to
   specify a natural number.
   - Option -K controls the number of TRSs selected in every iteration.
   - Option -N controls how many passive equations are added to the set of
     active facts, per selected TRS.
   - The instantiation depth of ground joinability checks is controlled by -I 
     (cf. the number of repetitions in the strategy given on p.9 of the paper). 
 - The remaining options are mainly there for analyzing input problems and
   debugging.
   - Option --term performs a termination check of the input system, considering
     the rules to be oriented as given.
   - Option --analyze prints problem properties, including recognized theories.
   - Debugging output is triggered by the option -D. 


-------------------------------------------------------------------------------
   WHAT'S MORE ...
-------------------------------------------------------------------------------

Some further information may be found on
  http://cl-informatik.uibk.ac.at/software/maedmax

If you have come across any questions or problems, please do not hesitate to
contact sarah.winkler@uibk.ac.at.


[0] http://www.jaist.ac.jp/project/maxcomp/
[1] https://github.com/ocaml/ocamlbuild/blob/master/manual/manual.adoc
[2] http://yices.csl.sri.com/
[3] https://github.com/polazarus/ocamlyices
[4] http://mjambon.com/yojson.html
[5] https://opam.ocaml.org/packages/xml-light/
[6] http://www.cs.miami.edu/~tptp/
[7] https://www.lri.fr/~marche/tpdb/format.html
[8] http://cl-informatik.uibk.ac.at/software/cpf/
[9] http://cl-informatik.uibk.ac.at/software/ceta/