clauses(theory).

f(f(f(y,x),x),f(f(f(z,x),f(y,x)),f(f(y,y),z))) = x.

end_of_list.

formulas(theory).

all x all y exists z (f(x,z) = y).
all x all y exists z (f(z,x) = y).

end_of_list.