formula_list(usable).



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



% trivial from the preceding statement:

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



end_of_list.