formula_list(usable).

(	all x y z ( d(x,n(y,z)) = n(d(x,y),d(x,z)) )).	 % (vi)_1

(	all x y z ( d(n(x,y),z) = n(d(x,z),d(y,z)) )).	 % (vi)_2

end_of_list.