formula_list(usable). ( all x y z ( i(k(x,d(y,z)),d(k(x,y),z)) ) ). % (xviii) end_of_list.