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))
)