formula_list(usable).

( all x y z ( i(n(k(z,x),c(k(z,y))), k(z,n(x,c(y)))) ) ).  % (x)_2

end_of_list.