formula_list(usable).

(	all x y w v ( i( k(n(x,w),n(y,v)), k(x,y) ) )). % 4

(	all x y w v ( i( k(n(x,w),n(y,v)), k(w,v) ) )). % 5

end_of_list.