The LISP-like language of the SMT Library as defined at http://combination.cs.uiowa.edu/smtlib/ Formal proofs in a logical calculus. Informal proofs, e.g., in mathematical vernecular. ND The OMDoc language as described at http://www.mathweb.org/omdoc/ NI A resolution calculus that uses only the rules Binary resolution, Factoring and Paramodulation. The TSTP language as defined at http://www.cs.miami.edu/~tptp/TSTP/ CPU and/or wallclock time (in secs) available to solve a given problem, or perform a certain task. CPU and wallclock time (in msecs) that was needed to generate a problem, result, etc. The CPU time of the time resource in seconds. The wall clock time of the CPU of a time resource in seconds. The format of the TSTP proving problem, either FOF (first-order-formula) or CNF (clause normal form). A URL pointing to a twelf document defining the logic. The TPTP language as defined at http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html Problem is in CNF and only consists of horn clauses. Horn HRN equality EQU super feature of all other equality features. NEQ Problem contains no equality at all. noEquality SAT sat Problem is known as satisfiable. Classical first-order predicate logic with equality as described in ... Problem is in TSTP CNF format, contains only equality atoms and they all occur in unit clauses. unitPureEquality UEQ Problem contains some equality atoms. SEQ someEquality Problem is in TSTP CNF format and contains only equality atoms but some of them occur in non-unit clauses. nonUnitPureEquality NUE The OpenMath language as described at http://www.openmath.org/cocoon/openmath/standard/index.html FOF Problem is in TSTP FOF format. fofForm Neumann, Bernays, Goedel set theory. Problem is known as a theorem. theorem THM PEQ pureEquality Problem contains only equality atoms. only for testing afasfdafd Problem is essentially propositional, e.g., it doesn't contain any variables. EPR essentiallyProp Closed quantifier-free formulas built over an arbitrary expansion of the empty signature with free sort, function and predicate symbols. Note that the formulas can contain term (resp., formula) variables as long as they are bound by a let (resp., flet) construct. Also, formulas in ite terms must be themselves quantifier-free. notHorn Problem does not only contain Horn clauses. NHN test_fof_problem input_formula(foo,conjecture,(equal(bar,bar))). Zermelo Fraenkel set theory. like in Isabelle/HOL