formula_list(usable).

	( all x ( u(x,x) = x )). % 17

	( all x y z ( ( u(x,y)=y & u(y,z)=z ) -> u(x,z) = z )). % 18

	( all x y ( u(x,y)=y -> u(c(y),c(x))=c(x) )). % 19

end_of_list.