formula_list(usable).

(	all x ( k(x,Z) = Z ) ).	% (xiii)_4

(	all x ( k(Z,x) = Z ) ).	% (xiii)_3

(	all x ( d(x,U) = U ) ).	% (xiii)_2

(	all x ( d(U,x) = U ) ).	% (xiii)_1

end_of_list.