Here is a list of all documented variables with links to the class documentation for each member:

- a -

• action : StackProver
• actions : StackItem
• all_names_added : VariableIndex

- b -

• backtrack : StackProver
• backtrack_points : SubstitutionStack, VariableIndex
• bt_restriction_index : StackItem

- c -

• c : Clause
• C : ProofChecker
• c : StackItem
• C_2 : InferenceItem
• choice : ERWA, EXP3, UCB
• choose_next : ERWA, EXP3, UCB
• clause_roles : Matrix
• clauses : Matrix
• clauses_copy : Matrix
• cnf_only : StackProver
• comment_blocks : TPTPParser
• conjecture_false : StackProver
• conjecture_missing : StackProver
• conjecture_true : StackProver
• copy_saved : Matrix
• current_depth : StackProver
• current_depth_limit : StackProver

- d -

• d : Clause, Matrix
• depth : StackItem
• depth_limit_reached : StackProver

- e -

• end_time : StackProver
• extensions_tried : StackProver

- f -

• file_contents : TPTPParser
• fip : TPTPParser
• first_anon_variable : VariableIndex
• fof_has_axioms : StackProver
• fun_index : FOF, StackProver
• funs : FunctionIndex

- h -

• highest_anon_variable : VariableIndex

- i -

• index : Matrix
• index_in_lemmata : InferenceItem
• index_in_path : InferenceItem
• item_type : StackItem

- l -

• L : InferenceItem
• l : StackItem
• Lem : ProofChecker
• lemmata : StackProver
• lemmata_tried : StackProver
• Lindex : InferenceItem
• Lprime : InferenceItem
• ls : Lemmata

- m -

• matrix : ProofChecker, StackProver, TPTPParser

- n -

• name_index : FunctionIndex, PredicateIndex, VariableIndex
• negated_conjecture_removed : StackProver
• negative_clauses : Matrix
• new_C : StackProver
• next_definitional_id : PredicateIndex
• next_index : FunctionIndex, PredicateIndex, SubstitutionStack, VariableIndex
• next_unique_index : VariableIndex
• num_equals : Matrix
• num_preds : StackProver
• num_subs : ProofChecker

- o -

• output_interval : StackProver

- p -

• P : ProofChecker
• p : ProofPrinter, StackItem
• path : SimplePath, StackProver
• pip : TPTPParser
• positive_clauses : Matrix
• pred : FOF
• pred_index : FOF, StackProver
• preds : PredicateIndex
• problem_path : StackProver
• proof : ProofChecker
• proof_count : StackProver
• proof_printer : StackProver

- r -

• r_stack : ProofChecker
• random_generator : ERWA, EXP3, UCB
• reductions_tried : StackProver
• results : StackProver
• right_branch_stack : StackProver
• right_branches_started : StackProver
• roles_copy : Matrix

- s -

• s : Unifier
• schedule : schedule::Schedule
• schedule_step_number : schedule::Schedule
• show : StackProver
• si : StackProver
• sigma : InferenceItem
• simplified_fof_has_axioms : StackProver
• skolem_function_number : FunctionIndex
• stack : StackProver, SubstitutionStack
• status : StackProver
• sub : StackItem, Substitution
• sub_formulas : FOF
• sub_stack : StackProver

- t -

• T : InferenceItem
• term_index : FOF, StackProver
• term_pointers : TermIndex
• this_action : StackItem
• ti : ProofChecker
• times : schedule::Schedule
• tip : TPTPParser
• to_do : Unifier
• tptp_conversion_string : StackProver, TPTPParser
• type : FOF

- u -

• u : ProofChecker, StackProver
• use_timeout : StackProver

- v -

• var : FOF
• var_index : FOF, StackProver
• vars : VariableIndex
• vi : ProofChecker
• vip : TPTPParser