formula_list(usable).



( all x y z w (n(n(x,y),n(z,w)) = n(n(x,w),n(z,y))   )).



end_of_list.