s/prolog_style_variables<\/tt>/prolog_style_variables<\/b><\/tt><\/a>/ s/auto<\/tt>/auto<\/b><\/tt><\/a>/ s/auto_inference<\/tt>/auto_inference<\/b><\/tt><\/a>/ s/auto_process<\/tt>/auto_process<\/b><\/tt><\/a>/ s/auto_setup<\/tt>/auto_setup<\/b><\/tt><\/a>/ s/auto_limits<\/tt>/auto_limits<\/b><\/tt><\/a>/ s/auto2<\/tt>/auto2<\/b><\/tt><\/a>/ s/lrs_ticks<\/tt>/lrs_ticks<\/b><\/tt><\/a>/ s/lrs_interval<\/tt>/lrs_interval<\/b><\/tt><\/a>/ s/min_sos_limit<\/tt>/min_sos_limit<\/b><\/tt><\/a>/ s/auto2<\/tt>/auto2<\/b><\/tt><\/a>/ s/order<\/tt>/order<\/b><\/tt><\/a>/ s/inverse_order<\/tt>/inverse_order<\/b><\/tt><\/a>/ s/eq_defs<\/tt>/eq_defs<\/b><\/tt><\/a>/ s/expand_relational_defs<\/tt>/expand_relational_defs<\/b><\/tt><\/a>/ s/predicate_elim<\/tt>/predicate_elim<\/b><\/tt><\/a>/ s/fold_denial_max<\/tt>/fold_denial_max<\/b><\/tt><\/a>/ s/sort_initial_sos<\/tt>/sort_initial_sos<\/b><\/tt><\/a>/ s/process_initial_sos<\/tt>/process_initial_sos<\/b><\/tt><\/a>/ s/sos_limit<\/tt>/sos_limit<\/b><\/tt><\/a>/ s/max_given<\/tt>/max_given<\/b><\/tt><\/a>/ s/max_kept<\/tt>/max_kept<\/b><\/tt><\/a>/ s/max_megs<\/tt>/max_megs<\/b><\/tt><\/a>/ s/max_seconds<\/tt>/max_seconds<\/b><\/tt><\/a>/ s/max_minutes<\/tt>/max_minutes<\/b><\/tt><\/a>/ s/max_hours<\/tt>/max_hours<\/b><\/tt><\/a>/ s/max_days<\/tt>/max_days<\/b><\/tt><\/a>/ s/age_part<\/tt>/age_part<\/b><\/tt><\/a>/ s/weight_part<\/tt>/weight_part<\/b><\/tt><\/a>/ s/false_part<\/tt>/false_part<\/b><\/tt><\/a>/ s/true_part<\/tt>/true_part<\/b><\/tt><\/a>/ s/random_part<\/tt>/random_part<\/b><\/tt><\/a>/ s/hints_part<\/tt>/hints_part<\/b><\/tt><\/a>/ s/default_parts<\/tt>/default_parts<\/b><\/tt><\/a>/ s/pick_given_ratio<\/tt>/pick_given_ratio<\/b><\/tt><\/a>/ s/lightest_first<\/tt>/lightest_first<\/b><\/tt><\/a>/ s/breadth_first<\/tt>/breadth_first<\/b><\/tt><\/a>/ s/random_given<\/tt>/random_given<\/b><\/tt><\/a>/ s/random_seed<\/tt>/random_seed<\/b><\/tt><\/a>/ s/input_sos_first<\/tt>/input_sos_first<\/b><\/tt><\/a>/ s/binary_resolution<\/tt>/binary_resolution<\/b><\/tt><\/a>/ s/neg_binary_resolution<\/tt>/neg_binary_resolution<\/b><\/tt><\/a>/ s/ordered_res<\/tt>/ordered_res<\/b><\/tt><\/a>/ s/check_res_instances<\/tt>/check_res_instances<\/b><\/tt><\/a>/ s/literal_selection<\/tt>/literal_selection<\/b><\/tt><\/a>/ s/pos_hyper_resolution<\/tt>/pos_hyper_resolution<\/b><\/tt><\/a>/ s/hyper_resolution<\/tt>/hyper_resolution<\/b><\/tt><\/a>/ s/neg_hyper_resolution<\/tt>/neg_hyper_resolution<\/b><\/tt><\/a>/ s/ur_resolution<\/tt>/ur_resolution<\/b><\/tt><\/a>/ s/pos_ur_resolution<\/tt>/pos_ur_resolution<\/b><\/tt><\/a>/ s/neg_ur_resolution<\/tt>/neg_ur_resolution<\/b><\/tt><\/a>/ s/initial_nuclei<\/tt>/initial_nuclei<\/b><\/tt><\/a>/ s/nucleus_limit<\/tt>/nucleus_limit<\/b><\/tt><\/a>/ s/paramodulation<\/tt>/paramodulation<\/b><\/tt><\/a>/ s/ordered_para<\/tt>/ordered_para<\/b><\/tt><\/a>/ s/check_para_instances<\/tt>/check_para_instances<\/b><\/tt><\/a>/ s/para_from_vars<\/tt>/para_from_vars<\/b><\/tt><\/a>/ s/para_lit_limit<\/tt>/para_lit_limit<\/b><\/tt><\/a>/ s/para_units_only<\/tt>/para_units_only<\/b><\/tt><\/a>/ s/basic_paramodulation<\/tt>/basic_paramodulation<\/b><\/tt><\/a>/ s/lex_order_vars<\/tt>/lex_order_vars<\/b><\/tt><\/a>/ s/demod_step_limit<\/tt>/demod_step_limit<\/b><\/tt><\/a>/ s/demod_size_limit<\/tt>/demod_size_limit<\/b><\/tt><\/a>/ s/back_demod<\/tt>/back_demod<\/b><\/tt><\/a>/ s/lex_dep_demod<\/tt>/lex_dep_demod<\/b><\/tt><\/a>/ s/lex_dep_demod_lim<\/tt>/lex_dep_demod_lim<\/b><\/tt><\/a>/ s/lex_dep_demod_sane<\/tt>/lex_dep_demod_sane<\/b><\/tt><\/a>/ s/unit_deletion<\/tt>/unit_deletion<\/b><\/tt><\/a>/ s/cac_redundancy<\/tt>/cac_redundancy<\/b><\/tt><\/a>/ s/max_literals<\/tt>/max_literals<\/b><\/tt><\/a>/ s/max_literals<\/tt>/max_literals<\/b><\/tt><\/a>/ s/max_vars<\/tt>/max_vars<\/b><\/tt><\/a>/ s/max_weight<\/tt>/max_weight<\/b><\/tt><\/a>/ s/safe_unit_conflict<\/tt>/safe_unit_conflict<\/b><\/tt><\/a>/ s/factor<\/tt>/factor<\/b><\/tt><\/a>/ s/new_constants<\/tt>/new_constants<\/b><\/tt><\/a>/ s/back_subsume<\/tt>/back_subsume<\/b><\/tt><\/a>/ s/backsub_check<\/tt>/backsub_check<\/b><\/tt><\/a>/ s/echo_input<\/tt>/echo_input<\/b><\/tt><\/a>/ s/quiet<\/tt>/quiet<\/b><\/tt><\/a>/ s/print_initial_clauses<\/tt>/print_initial_clauses<\/b><\/tt><\/a>/ s/print_given<\/tt>/print_given<\/b><\/tt><\/a>/ s/print_gen<\/tt>/print_gen<\/b><\/tt><\/a>/ s/print_kept<\/tt>/print_kept<\/b><\/tt><\/a>/ s/print_labeled<\/tt>/print_labeled<\/b><\/tt><\/a>/ s/print_clause_properties<\/tt>/print_clause_properties<\/b><\/tt><\/a>/ s/print_proofs<\/tt>/print_proofs<\/b><\/tt><\/a>/ s/default_output<\/tt>/default_output<\/b><\/tt><\/a>/ s/report<\/tt>/report<\/b><\/tt><\/a>/ s/stats<\/tt>/stats<\/b><\/tt><\/a>/ s/clocks<\/tt>/clocks<\/b><\/tt><\/a>/ s/bell<\/tt>/bell<\/b><\/tt><\/a>/ s/constant_weight<\/tt>/constant_weight<\/b><\/tt><\/a>/ s/constant_weight<\/tt>/constant_weight<\/b><\/tt><\/a>/ s/variable_weight<\/tt>/variable_weight<\/b><\/tt><\/a>/ s/not_weight<\/tt>/not_weight<\/b><\/tt><\/a>/ s/or_weight<\/tt>/or_weight<\/b><\/tt><\/a>/ s/prop_atom_weight<\/tt>/prop_atom_weight<\/b><\/tt><\/a>/ s/nest_penalty<\/tt>/nest_penalty<\/b><\/tt><\/a>/ s/skolem_penalty<\/tt>/skolem_penalty<\/b><\/tt><\/a>/ s/depth_penalty<\/tt>/depth_penalty<\/b><\/tt><\/a>/ s/var_penalty<\/tt>/var_penalty<\/b><\/tt><\/a>/ s/default_weight<\/tt>/default_weight<\/b><\/tt><\/a>/ s/max_proofs<\/tt>/max_proofs<\/b><\/tt><\/a>/ s/reuse_denials<\/tt>/reuse_denials<\/b><\/tt><\/a>/ s/auto_denials<\/tt>/auto_denials<\/b><\/tt><\/a>/ s/restrict_denials<\/tt>/restrict_denials<\/b><\/tt><\/a>/ s/breadth_first_hints<\/tt>/breadth_first_hints<\/b><\/tt><\/a>/ s/degrade_hints<\/tt>/degrade_hints<\/b><\/tt><\/a>/ s/limit_hint_matchers<\/tt>/limit_hint_matchers<\/b><\/tt><\/a>/ s/back_demod_hints<\/tt>/back_demod_hints<\/b><\/tt><\/a>/ s/collect_hint_labels<\/tt>/collect_hint_labels<\/b><\/tt><\/a>/ s/order<\/tt>/order<\/b><\/tt><\/a>/ s/eval_limit<\/tt>/eval_limit<\/b><\/tt><\/a>/