formula_list(usable). ( all x y z ( i(n(k(x,z),c(k(y,z))), k(n(x,c(y)),z)) ) ). % (x)_1 end_of_list.