Prover9 Options

• Flags are Boolean-valued options which can be changed with the set and clear commands, e.g.,
  set(clocks).
  set(print_given).
  
• Parms are integer-valued options which can be changed with the assign command, e.g.,
  assign(max_weight, 30).
• Stringparms are string-valued options which can be changed with the assign command, e.g.,
  assign(order, kbo).

Option Dependencies

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 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

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]