formula_list(usable). ( all x z ( (i(x,I) & i(z,I)) -> (k(x,z)=n(x,z)) )). end_of_list.