formula_list(usable). ( all x y ( ( k(x,r(y)) = Z ) -> ( n(k(U,x),k(U,y)) = Z ) ) ). ( all x y ( ( n(k(U,x),k(U,y)) = Z ) -> ( k(x,r(y)) = Z ) ) ). ( all x y ( ( u(d(Z,x),d(Z,y)) = U ) -> ( d(x,r(y)) = U ) ) ). ( all x y ( ( d(x,r(y)) = U ) -> ( u(d(Z,x),d(Z,y)) = U ) ) ). end_of_list.