The LISP-like language of the SMT Library as defined at http://combination.cs.uiowa.edu/smtlib/
Informal proofs, e.g., in mathematical vernecular.
The OMDoc language as described at http://www.mathweb.org/omdoc/
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.
super feature of all other equality features.
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.
Problem is in TSTP CNF format and contains only equality atoms but some of them occur in non-unit clauses.
The OpenMath language as described at http://www.openmath.org/cocoon/openmath/standard/index.html
Problem is essentially propositional, e.g., it doesn't contain any variables.
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.
Problem does not only contain Horn clauses.