Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Record()
axiom()
cond()
define()
lemma()
BaseSolver
EProverTHFSolver
LeoIIISolver
MultiSolver
NanoCopISolver
SATSolver
TweeSolver
VampireSolver
VampireTHFSolver
ZipperpositionSolver
binpath()
collect_decls()
collect_sorts()
expr_to_smtlib()
expr_to_tptp()
funcdecl_smtlib()
install_solvers()
mangle_decl()
mangle_decl_smtlib()
run()
smtlib_datatypes()
sort_to_tptp()
run_aprove()