clauses(theory).

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

f(f(x,x),f(x,x)) = x.   % OL property

f(A,B) != f(B,A).       % denial of commutativity

end_of_list.