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.