formula_list(usable).

( all x y ( n(k(x,U),k(y,U))=Z -> k(r(x),y)=Z )).

end_of_list.