Axioms can either be supplied in TRS format
(see http://www.lri.fr/~marche/tpdb/format.html) or in

TPTP3 format (see http://www.cs.miami.edu/~tptp 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)))).