formula_list(usable). ( all x y ( ( i(k(r(x),x),I) & i(k(r(y),y),I) ) -> i(k(r(k(x,y)),k(x,y)),I) )). % (xxvi) end_of_list.