formula_list(usable). % inclusion laws ( all x y ( ( i(x,y) & i(y,x) ) -> x = y )). % 13 end_of_list.