Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
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()
install_solvers2()
mangle_decl()
mangle_decl_smtlib()
run()
smt2tptp()
smtlib_datatypes()
sort_to_tptp()
tptp2smt()
all_pairs()
basic()
huet()
huet_smt2_file()
is_trivial()
orient()
simplify()
deduce all possible critical pairs from R