formula_list(usable).

(	all x ( i(k(x,U),k(n(k(x,r(x)),I),U)) )).

(       all x ( i(k(n(k(x,r(x)),I),U),k(x,U)) )).

(	all x ( k(x,U) = k(n(k(x,r(x)),I),U)  )).

end_of_list.