omkbTT

omkbTT online

Input Input can either be supplied in TRS format (see http://www.lri.fr/~marche/tpdb/format.html) or in
TPTP format (see http://www.cs.miami.edu/~tptp for details).

Here is an example (CGE2) in TRS format:

(VAR x y z)
(RULES
*(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))
)
(example)  
 
Output
output completed TRS    provide statistics
Expert Mode