formula_list(usable).

(	all x ( k(U,x) = d(Z,k(U,x)) ) ).	% (xiv)_1

(	all x ( k(x,U) = d(k(x,U),Z) ) ).	% (xiv)_2

(	all x ( d(Z,x) = k(U,d(Z,x)) ) ).	% (xiv)_3

(	all x ( d(x,Z) = k(d(x,Z),U) ) ).	% (xiv)_4

end_of_list.