Prover9 Manual |  | Version 2009-02A

# Prover9 Options

There are three kinds of 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

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