-- changed the interface of functions vampire_oracle and eprover_oracle.

-- terms are fully typed. -- only the top-level boolean terms are predicates.

-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.

-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.

-- added combinator reduction axioms (typed and untyped) for HOL goals. -- combined make_nnf functions for HOL and FOL goals. -- hypothesis of goals are now also skolemized by inference.

-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).