More Search Prep

set(expand_relational_defs).
clear(expand_relational_defs).    % default clear

If this flag is set, Prover9 looks for relational definitions in the assumptions and uses them to rewrite all occurrences of the defined relations elsewhere in the input, before the start of the search. The expansion steps are detailed in the output file and appear in proofs with the justification expand_def.
Relational definitions must be closed formulas for example,
formulas(assumptions).
  all x all y all z (A(x,y,z) <-> ((x <= y & y <= z) | (z <= y & y <= x))).
end_of_list.
If there are circular definitions, Prover9 will immediately exit with a fatal error.
This flag eliminates predicate symbols, and its effects overlap somewhat with the flag predicate_elim.
Here is a trivial example, using the transitivity-of-subset problem.
prover9 -f subset_trans_expand.in > subset_trans_expand.out
For more examples using this flag, see the problem set "Ternary Relations in Lattices", which is available from the Prover9 Web page.

set(predicate_elim).    % default set
clear(predicate_elim).

If this flag is set, Prover9 applies a procedure that attempts to eliminate predicate symbols from the problem before the start of the search. The eliminations occur by resolution, and those steps show up as ordinary resolution inferences in any proofs that are found. The procedure works by selecting an eliminable predicate symbol, say P, then doing some set of resolution inferences on P, then removing all clauses that contain P. The procedure is intended to preserve the existence of proofs; however, if there are multiple goals, predicate elimination may prevent multiple proofs.
The effects of this flag overlap somewhat with expand_relational_defs, which also eliminates predicate symbols.

assign(fold_denial_max, n).  % default n=0, range [-1 .. INT_MAX]

This parameter applies to negated ground input equalities in which neither side is a constant, say f(a,b) != f(b,a). If the left-hand side has fewer than n symbols, a new constant is introduced and set equal to the left-hand side. This operation is applied to at most one clause in the input sos list.

set(sort_initial_sos).
clear(sort_initial_sos).    % default clear

If this flag is set, the sos list is sorted just before the start of the search. The order (somewhat arbitrary) is

positive clauses < negative clauses < mixed clauses;
fewer symbols < more symbols;
fewer literals < more literals;
shallower < deeper.

set(process_initial_sos).    % default set
clear(process_initial_sos).

If this flag is set, clauses in the initial sos list will be handled (with a few exceptions) as if they were inferred. For example, demodulation, subsumption, and the check for unit conflict will be applied. The exceptions are that none of max_weight, max_vars, max_depth, or max_literals will be applied. (These four parameters are never applied before the first given clause is selected.)
This flag should be cleared only in very rare circumstances.

Next Section: Search Limits