Special flags for the "fotl-translate" tool:

Argument Name Description
--debug / -d Display more details for the different transformation steps
--regroupnext Formulae of the form \next φ <op> \next ψ, with <op> = &,|, are transformed into \next(φ <op> ψ)
--extendedstepclauses Step clauses in the transformation result are allowed to contain more than one literal on each side
--singleeventuality For a propositional problem multiple eventualities will be transformed into a single one
--measuretime Measure the CPU time used for the whole transformation process and print it out to the standard error output stream

Special flags for TSPASS:

Argument Name Possible Values Description
-LoopSearchTest 0 Perform loop tests using logical equivalence
1 Perform loop tests using subsumption (default)
-SequentialLoopSearch For a given eventuality L a loop search clause s^L_i ^ C => D is only selected if the set of usable clauses does not contain a loop search clause s^L_j ^ E => F with j < i.
-LoopSearchIterations 1,... Specify the number of iterations of the regular clause inference / reduction scheme after which a loop search is performed
-PDiffMark Print out the occurrences of loop search clauses that contain at least two different loop search markers during the reduction steps
-PLoopCand Print out the loop search candidate clauses for the loop search test
-SeqLoopSearchIterations 1,... Controls after how many sequential selections of loop search clauses an arbitrary loop search clause is selected
-ModelConstruction Construct a model for satisfiable propositional problems
-PModelConstructionSteps Print out more information during model construction
-ModelConstructionType 0 Perform model construction using ordered resolution (default)
1 Perform model construction using unordered resolution
-EliminateRedundantCycles Eliminate redundant cycles during model construction (switched on by default)