formula_list(usable).

	( all x y z ( i(x,u(y,z)) -> i(n(x,c(z)),y) )). % 1

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

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

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

end_of_list.