Online Otter-λ

Settings:

• Inference Rules
• binary_res
• hyper_res
• neg_hyper_res
• ur_res
• para_into
• para_from
• demod_inf
• geometric_rule
• Paramodulation
• para_from_left
• para_from_right
• para_into_left
• para_into_right
• para_from_vars
• para_into_vars
• para_from_units_only
• para_into_units_only
• para_skip_skolem
• para_ones_rule
• para_all
• Output
• very_verbose
• print_given
• print_kept
• print_back_sub
• print_new_demod
• print_back_demod
• print_proofs
• print_lists_at_end
• echo_included_files
• build_proof_object
• Process Generated Clauses
• unit_deletion
• delete_identical_nested_skolem
• sort_literals
• for_sub
• back_sub
• ancestor_subsume
• factor
• geometric_rewrite
• max_literals 
• max_weight 
• max_distinct_vars 
• change_limit_after 
• new_max_weight 
• History
• detailed_history
• order_history
• demod_history
• Stopping The Search
• max_seconds 
• max_gen 
• max_kept 
• max_given 
• max_mem 
• max_proofs 
• Demodulation
• demod_linear
• demod_out_in
• dynamic_demod
• dynamic_demod_all
• back_demod
• demod_limit 
• Ordering
• knuth_bendix
• order_eq
• eq_units_both_ways
• dynamic_demod_lex_dep
• lrpo
• lex_order_vars
• symbol_elim
• order_hyper
• Miscellany
• auto
• simplify_fol
• process_input
• propositional
• report 
• stats_level 
• min_bit_width 
• Given Clauses
• sos_queue
• sos_stack
• input_sos_first
• interactive_given
• pick_given_ratio 
• geo_given_ratio 
• interrupt_given 
• Language
• prolog_style_variables
• display_terms
• check_arity
• input_sequent
• output_sequent
• bird_print
• pretty_print
• pretty_print_indent 
• Memory
• control_memory
• really_delete_clauses
• free_all_mem
• Indexing
• index_for_back_demod
• for_sub_fpa
• no_fapl
• no_fanl
• fpa_literals 
• fpa_terms 
• Hot List
• heat 
• dynamic_heat_weight 
• Weighting
• atom_wt_max_args
• term_wt_max_args
• neg_weight 
• Otter-λ Settings
• Second Order Inference
• lambda
• induction
• cases
• External Simplification
• bignums
• simplify
• solve
• complex
• More Settings

Lists:

• usable
• sos
• demodulators
• passive
• hot
• other