mkbTT online

Input Input can either be supplied in both the old or the new TPDB
format or in TPTP format. Please check
for details about the respective format.

Here is an example (CGE2) in TRS format:

(VAR x y z)
*(e,x) -> x
*(i(x),x) -> e
*(*(x,y),z) -> *(x,*(y,z))
f(*(x,y)) -> *(f(x),f(y))
g(*(x,y)) -> *(g(x),g(y))
*(f(x),g(y)) -> *(g(y),f(x))
standard completion    ordered completion    normalized completion
completed TRS    statistics    proof
Expert Mode