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