formula_list(usable). ( all x y ( ( i(k(r(x),x),I) & i(k(r(y),y),I) & (n(k(x,U),k(y,U))=Z) ) -> i(k(r(u(x,y)),u(x,y)),I) )). % (xxxi) end_of_list.