Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
collect_sorts()
BaseSolver
EProverSolver
EProverTHFSolver
LeanSolver
LeoIIISolver
MultiSolver
NanoCopISolver
SATSolver
TweeSolver
VampireSolver
VampireTHFSolver
ZipperpositionSolver
binpath()
collect_decls()
download()
install_solvers()
install_solvers2()
run()
smt2tptp()
tptp2smt()
set[SortRef]