formula_list(usable). ( all x y z ( i(n(k(x,y),z), k(n(k(z,r(y)),x),y)) )). % (xv)_2 end_of_list.