formula_list(usable).

	( all x y ( i(n(x,y),y) )).                     % 4

	( all x y z ( i(n(x,u(y,z)), u(y,n(x,z))) )).   % 5

	( all x y ( x = u(n(x,y),n(x,c(y))) )).         % 6

	( all x y z ( i(x,y) -> i(u(z,x),u(z,y)) )).    % 7

	( all x y z ( i(x,y) -> i(n(z,x),n(z,y)) )).    % 8

end_of_list.