The following paragraphs describe the command-line interface of mkbTT. The call
$ ./mkbtt <file> <options>
invokes mkbTT on the given file. Supported formats for input problems are Possible options include the following:
The global time limit is given by -t <seconds> . To control the output, use -st, -ct and -p to obtain some statistics, the completed system, and a proof of the saturation, respectively. The flag -h displays the list of possible options and -v <n> controls the verbosity, where <n> is a value between 0 and 3. Using -ch <file>, a rewrite system can be supplied to check whether it is complete and joins the input equalities. The settings for the required termination check have to be specified as described below.
mkbTT can output XML proofs in CPF which can be certified by CeTA. To this end, the script callcertify needs to be modified to output a certifiable termination proof. To obtain a certifiable completion proof, one can call mkbTT with option -cert as follows:
$ ./mkbtt input/kb/slothrop_equiv_proofs_or.trs -cert > proof.xml
$ ceta proof.xml

In ordered completion mode, mkbTT can produce certifiable entailment (dis)proofs using -cert and -p format, where format is one of cpfconv (for conversions), cpfsub (for subsumption proofs with history), or cpftree (for equational proof trees):
$ ./mkbtt -o -cert -p cpfsub input/easy/GRP022-2.tptp > proof.xml
$ ceta proof.xml
The format of disproofs is ndependent of the choice of <format>, e.g. in
$ ./mkbtt -o -cert -p cpfsub input/easy/BOO027-1.tptp > proof.xml
$ ceta proof.xml

mkbTT has also some very basic theorem proving feature in normalized completion mode. For instance, CeTA certifies the following entailment proof:
$ ./mkbtt -n -cert -p cpfsub input/certification/groups0.tptp -s acrpo > proof.xml
$ ceta proof.xml
Please note that certification of entailment proofs requires CeTA ≥ 2.18.

Termination checks
By default, termination checks are performed internally using TTT2. The applied termination techniques can be controlled by using -s <strategy> and specifying a strategy in the TTT2 language. Alternatively, termination can be checked externally if an appropriate script is supplied using the option -tp <script>. The script is supposed to be executable from the current directory and it has to be compatible with the following minimal interface:
<script> <file> <timeout> is supposed to check termination of the given system in TPDB format and print YES on the first line of standard output if termination could be established. The parameter <timeout> specifies a time limit in seconds for a termination check (if it is ignored mkbTT just kills the process). Here are examples for such scripts calling AProVe and μterm.
With both internal and external termination, the time limit for each termination check is specified by -T <seconds> .
Node selection
To control the selection of nodes, the option -ss <strategy> allows to supply a selection strategy in mkbTT's strategy language. Predefined strategies are max, slothrop and sum. The max strategy is used by default.
Term indexing
The term indexing technique used for variant and encompassment retrievals in rewrite inferences can be specified via -ix <technique>, where nv denotes naive indexing, pi denotes path indexing, dt specifies discrimination trees and ct abbreviates code trees, the latter is applied by default. Besides, the option -ui <technique> allows to select an indexing technique for the retrieval of unifiable terms in deduce steps.
Critical pair criteria
By adding the flag -cp <cpc> a critical pair criterion can be selected, where <cpc> can be none or have one of the values prime, blocked, connected or all denoting the criteria PCP, BCP, CCP and all as outlined in the paper.
The option -is <iso> is used to control process isomorphisms, where <iso> may take the values rename or rename+ to incorporate checking for renamings, perm or perm+ to check for argument permutations, none to suppress isomorphism checks or auto to heuristically choose a possibly applicable isomorphism at the beginning of a run (the latter is used by default). A trailing + indicates that checks are repeatedly performed in every iteration, and not just when a process is split.
Special features
mkbTT now (experimentally) supports pre-orientation of equations. For this purpose, please create a file in TPDB format describing a relative termination problem. For all strict rules the given orientation is kept, while all weak rules are considered as equations and treated as usual input equalities. Note that mkbTT fails if termination of preoriented equations cannot be shown with the selected termination tool or strategy. For example, in this problem associativity is pre-oriented while all other axioms are treated as equations.