clauses(theory).
f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))).  % MOD_SS
end_of_list.