formula_list(usable). ( all x y z ( d(Z,u(d(x,y),z)) = d(Z,u(d(r(x),z),y)) )). % (xvi)_2 end_of_list.