formula_list(usable). ( all x y w v ( i( k(n(x,w),n(y,v)), n(k(x,y),k(w,v)) ) )). % (viii) end_of_list.