formula_list(usable).

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

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

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

end_of_list.