Admissible 
making a context unifier admissible

Bound 
iterative deepening bound

Config 
configuration for a derivation

Const 
global constants

Context 
context with operations

Context_unifier 
basic types for and operations on context unifiers

Context_unifier_check 
context unifier validity check

Context_unifier_search 
search for context unifiers

Context_unifier_space 
a problem clause

Counter 
int counter

Darwin 
proof procedure

Discrimination_tree 
term indexing with a discrimination tree

Equality 
equality by axiomatization

Finite_domain 
finite domain model finding

Flags 
command line evaluation

Heap 
heap structures

Jumping 
random jumps within the search space

Lemma 
lemma learning

Lemma_grounded 
grounded lemma generation

Lemma_lifted 
lifted lemma learning

Lemma_propositional 
propositional 'lemma' generation

Log 
derivation log

Preprocessing_equality 
simplifications based on equality

Preprocessing_pure 
removes pure clauses

Preprocessing_resolution 
computes short resolvents

Preprocessing_split_ground 
splitting of variable disjoint clause parts

Preprocessing_split_nonground 
splitting of clause parts

Preprocessing_unit 
unit subsumption and resolution

common print functions and constants used in ouput
 
Problem 
a problem clause set

Problem_literals 
checking of problem literals against new context literals

Read_darwin 
reads files in darwin's format

Read_tme 
reads tme files

Read_tptp 
reads tptp files

Selection 
selection of a split or assert literal

Selection_assert 
selection of assert candidates

Selection_lookahead 
Close lookahead for candidates

Selection_split 
selection of split candidates

Selection_types 
common types for selection modules

Sort_inference 
infers sorts based on a clause set

Stack 
imperative stack

State 
choice point (decision level) management

State_backtrack 
backtracking of module
State

Statistic 
derivation statistic

Subst 
a substitution

Symbol 
constant and function symbols

Term 
terms, literals, clauses

Term_attributes 
computation and comparison of term attributes

Term_indexing 
term indexing

Tools 
general functions

Unification 
term unification

Var 
universal and parameteric variables

Zip_wrapper 
wrapper for reading zipped files
