formula_list(usable). % inclusion laws

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

end_of_list.