formula_list(usable).


% variant of (viii):

( all x y z ( i(k(n(x,y),z), n(k(x,z),k(y,z))) )).





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





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



end_of_list.