Prover9 Manual Version June-2006

Options

There are three kinds of options:

Option Dependencies

Several of the flags and parameters cause other flags and parameters to be changed. In some cases, that is the only direct effect they have. For example, if you clear(auto), you will see the following in the output.
clear(auto).
    % clear(auto) -> clear(auto_inference).
    % clear(auto_inference) -> clear(predicate_elim).
    % clear(auto_inference) -> assign(eq_defs, pass).
    % clear(auto) -> clear(auto_limits).
    % clear(auto_limits) -> assign(max_weight, 2147483647).
    % clear(auto_limits) -> assign(sos_limit, -1).
The lines starting with "%" are the dependent options that are changed in behalf of clear(auto). Note the sub-dependencies in this example.

The option dependencies can be undone by simply changing the dependent option afterward, as in the following example input.

clear(auto).
set(predicate_elim).

Option Listing

The option names below are links to the sections containing the descriptions.

From Page Clauses and Formulas

set(prolog_style_variables).
clear(prolog_style_variables).    % default clear

From Page Automatic Modes

set(auto).    % default set
clear(auto).
set(auto_inference).    % default set
clear(auto_inference).
set(auto_limits).    % default set
clear(auto_limits).
set(auto2).
clear(auto2).    % default clear
assign(lrs_ticks, n).  % default n=-1, range [-1 .. INT_MAX]
assign(lrs_interval, n).  % default n=50, range [1 .. INT_MAX]
assign(min_sos_limit, n).  % default n=0, range [0 .. INT_MAX]

From Page Term Ordering

assign(order, string).  % default string=lpo, range [lpo,rpo,kbo]
set(inverse_order).    % default set
clear(inverse_order).
assign(eq_defs, string).  % default string=unfold, range [unfold,fold,pass]
set(dont_flip_input).
clear(dont_flip_input).    % default clear

From Page More Search Prep

set(predicate_elim).    % default set
clear(predicate_elim).
assign(fold_denial_max, n).  % default n=0, range [-1 .. INT_MAX]
set(sort_initial_sos).
clear(sort_initial_sos).    % default clear
set(hands_off_options).
clear(hands_off_options).    % default clear
set(process_initial_sos).    % default set
clear(process_initial_sos).

From Page Search Limits

assign(sos_limit, n).  % default n=10000, range [-1 .. INT_MAX]
assign(max_given, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_kept, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_megs, n).  % default n=200, range [-1 .. INT_MAX]
assign(max_seconds, n).  % default n=-1, range [-1 .. INT_MAX]

From Page Selecting the Given Clause

assign(age_part, n).    % default n=1, range [0 .. INT_MAX]
assign(true_part, n).   % default n=2, range [0 .. INT_MAX]
assign(false_part, n).  % default n=2, range [0 .. INT_MAX]
assign(pick_given_ratio, n).  % default n=0, range [0 .. INT_MAX]
set(breadth_first).
clear(breadth_first).    % default clear
set(input_sos_first).    % default set
clear(input_sos_first).

From Page Inference Rules

set(binary_resolution).
clear(binary_resolution).    % default clear
set(neg_binary_resolution).
clear(neg_binary_resolution).    % default clear
assign(literal_selection, string).  % default string=maximal, range [maximal, first_maximal, all, first]
set(hyper_resolution).
clear(hyper_resolution).    % default clear
set(neg_hyper_resolution).
clear(neg_hyper_resolution).    % default clear
set(ur_resolution).
clear(ur_resolution).    % default clear
set(pos_ur_resolution).
clear(pos_ur_resolution).    % default clear
set(neg_ur_resolution).
clear(neg_ur_resolution).    % default clear
set(initial_nuclei).
clear(initial_nuclei).    % default clear
assign(ur_nucleus_limit, n).  % default n=-1, range [-1 .. INT_MAX]
set(paramodulation).
clear(paramodulation).    % default clear
set(basic_paramodulation).
clear(basic_paramodulation).    % default clear
set(para_units_only).
clear(para_units_only).    % default clear
assign(para_lit_limit, n).  % default n=-1, range [-1 .. INT_MAX]
set(ordered_inference).    % default set
clear(ordered_inference).
set(ordered_instance).
clear(ordered_instance).    % default clear

From Page Processing Inferred Clauses

assign(max_weight, n).  % default n=100, range [INT_MIN .. INT_MAX]
assign(max_literals, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_vars, n).  % default n=-1, range [-1 .. INT_MAX]
set(back_demod).
clear(back_demod).    % default clear
set(lex_dep_demod).    % default set
clear(lex_dep_demod).
set(lex_dep_demod_sane).    % default set
clear(lex_dep_demod_sane).
set(lex_order_vars).
clear(lex_order_vars).    % default clear
assign(demod_step_limit, n).  % default n=1000, range [-1 .. INT_MAX]
assign(demod_size_limit, n).  % default n=1000, range [-1 .. INT_MAX]
set(safe_unit_conflict).
clear(safe_unit_conflict).    % default clear
set(back_subsume).    % default set
clear(back_subsume).
set(cac_redundancy).    % default set
clear(cac_redundancy).
set(unit_deletion).
clear(unit_deletion).    % default clear
set(back_unit_deletion).
clear(back_unit_deletion).    % default clear
set(factor).
clear(factor).    % default clear
assign(new_constants, n).  % default n=0, range [-1 .. INT_MAX]

From Page Output Files

set(echo_input).    % default set
clear(echo_input).
set(quiet).
clear(quiet).    % default clear
set(print_initial_clauses).    % default set
clear(print_initial_clauses).
set(print_given).    % default set
clear(print_given).
set(print_gen).
clear(print_gen).    % default clear
set(print_kept).
clear(print_kept).    % default clear
set(print_labeled).
clear(print_labeled).    % default clear
set(print_proofs).    % default set
clear(print_proofs).
set(default_output).    % default set
clear(default_output).
assign(report, n).  % default n=-1, range [-1 .. INT_MAX]
assign(stats, string).  % default string=lots, range [none,some,lots,all]
set(clocks).
clear(clocks).    % default clear

From Page Weighting

assign(constant_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]
assign(variable_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]
assign(not_weight, n).  % default n=0, range [INT_MIN .. INT_MAX]
assign(or_weight, n).  % default n=0, range [INT_MIN .. INT_MAX]
assign(prop_atom_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]
assign(nest_penalty, n).  % default n=0, range [0 .. INT_MAX]
assign(skolem_penalty, n).  % default n=1, range [0 .. INT_MAX]
assign(default_weight, n).  % default n=INT_MAX, range [INT_MIN .. INT_MAX]

From Page FOF Reduction

set(fof_reduction).
clear(fof_reduction).    % default clear
set(print_subproblems).    % default set
clear(print_subproblems).

From Page Goals

set(restrict_denials).
clear(restrict_denials).    % default clear
assign(max_proofs, n).  % default n=1, range [-1 .. INT_MAX]
set(reuse_denials).
clear(reuse_denials).    % default clear

From Page Hints

assign(bsub_hint_wt, n).  % default n=INT_MAX, range [INT_MIN .. INT_MAX]
assign(bsub_hint_add_wt, n).  % default n=-1000, range [INT_MIN .. INT_MAX]
set(degrade_hints).    % default set
clear(degrade_hints).
set(collect_hint_labels).
clear(collect_hint_labels).    % default clear

From Page Semantic Guidance

assign(eval_limit, n).  % default n=1024, range [-1 .. INT_MAX]