Axioms Axioms can either be supplied in TRS format (see or in
TPTP3 format (see for details). Here is an example in TPTP format:
cnf(transformation1, axiom,
  ( t(c(a(t(X)))) = t(X))).
cnf(transformation2, axiom,
  ( g(a(g(X))) = a(g(X)))).
cnf(transformation3, axiom,
  ( c(t(c(X))) = t(c(X)))).
cnf(transformation4, axiom,
  ( a(g(t(a(X)))) = a(X))).
cnf(transformation5, axiom,
  ( t(a(t(X))) = c(t(X)))).
Equality Please supply the goal equality in the format term=term using uppercase identifiers for variables, like
t(a(g(c(t(a(g(c(t(a(g(c(t(X))))))))))))) = c(t(g(a(c(t(g(a(c(t(X))))))))))
Timeout in seconds
use shortest path corresponding to rewrite sequence