Prover9 Manual Version 2009-02A

Prover9 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_process).    % default set
clear(auto_process).
set(auto_setup).    % default set
clear(auto_setup).
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]
set(raw).
clear(raw).    % default clear

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]

From Page More Search Prep

set(expand_relational_defs).
clear(expand_relational_defs).    % default clear
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(process_initial_sos).    % default set
clear(process_initial_sos).

From Page Search Limits

assign(sos_limit, n).  % default n=20000, 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]
assign(max_minutes, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_hours, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_days, 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(weight_part, n).  % default n=0, range [0 .. INT_MAX]
assign(false_part, n).   % default n=4, range [0 .. INT_MAX]
assign(true_part, n).    % default n=4, range [0 .. INT_MAX]
assign(random_part, n).  % default n=0, range [0 .. INT_MAX]
assign(hints_part, n).   % default n=INT_MAX, range [0 .. INT_MAX]
set(default_parts).      % default set
clear(default_parts).
assign(pick_given_ratio, n).  % default n=0, range [0 .. INT_MAX]
set(lightest_first).
clear(lightest_first).    % default clear
set(breadth_first).
clear(breadth_first).    % default clear
set(random_given).
clear(random_given).    % default clear
assign(random_seed, n).  % default n=0, range [-1 .. INT_MAX]
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
set(ordered_res).    % default set
clear(ordered_res).
set(check_res_instances).
clear(check_res_instances).    % default clear
assign(literal_selection, string).  % default string=max_negative, range [max_negative, all_negative, none]
set(pos_hyper_resolution).
clear(pos_hyper_resolution).    % default clear
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(ordered_para).    % default set
clear(ordered_para).
set(check_para_instances).
clear(check_para_instances).    % default clear
set(para_from_vars).    % default set
clear(para_from_vars).
assign(para_lit_limit, n).  % default n=-1, range [-1 .. INT_MAX]
set(para_units_only).
clear(para_units_only).    % default clear
set(basic_paramodulation).
clear(basic_paramodulation).    % default clear

From Page Processing Inferred Clauses

set(lex_order_vars).
clear(lex_order_vars).    % default clear
assign(demod_step_limit, n).  % default n=1000, range [-1 .. INT_MAX]
assign(demod_increase_limit, n).  % default n=1000, range [-1 .. INT_MAX]
set(back_demod).      % default set
clear(back_demod).
set(lex_dep_demod).    % default set
clear(lex_dep_demod).
assign(lex_dep_demod_lim, n).  % default n=11, range [-1 .. INT_MAX]
set(lex_dep_demod_sane).    % default set
clear(lex_dep_demod_sane).
set(unit_deletion).
clear(unit_deletion).    % default clear
set(cac_redundancy).    % default set
clear(cac_redundancy).
assign(max_literals, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_depth, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_vars, n).  % default n=-1, range [-1 .. INT_MAX]
assign(max_weight, n).  % default n=100, range [INT_MIN .. INT_MAX]
set(safe_unit_conflict).
clear(safe_unit_conflict).    % default clear
set(factor).
clear(factor).    % default clear
assign(new_constants, n).  % default n=0, range [-1 .. INT_MAX]
set(back_subsume).    % default set
clear(back_subsume).
assign(backsub_check, n).  % default n=500, 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_clause_properties).
clear(print_clause_properties).    % 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
set(bell).    % default set
clear(bell).

From Page Weighting

assign(constant_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]
assign(sk_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(depth_penalty, n).  % default n=0, range [INT_MIN .. INT_MAX]
assign(var_penalty, n).  % default n=0, range [INT_MIN .. INT_MAX]
assign(default_weight, n).  % default n=INT_MAX, range [INT_MIN .. INT_MAX]

From Page Goals and Denials

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

From Page Hints

set(breadth_first_hints).
clear(breadth_first_hints).    % default clear
set(degrade_hints).    % default set
clear(degrade_hints).
set(limit_hint_matchers).
clear(limit_hint_matchers).    % default clear
set(back_demod_hints).    % default set
clear(back_demod_hints).
set(collect_hint_labels).
clear(collect_hint_labels).    % default clear

From Page Semantic Guidance

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

Next Section: Glossary