formula_list(usable).

( all x y z ( i(k(r(x),x),I) -> ( k(x,r(n(y,z)))=n(k(x,r(y)),k(x,r(z))) ) )).

( all x y z ( r(k(x,r(n(y,z)))) = k(n(y,z),r(x)) ) ).

( all x y z ( r(n(k(x,r(y)),k(x,r(z)))) = n(k(y,r(x)),k(z,r(x))) ) ).

end_of_list.