formula_list(usable). % two of Huntington's axioms (1933) for Boolean algebra all x y ( u(x,y) = u(y,x) ). % BI all x y z ( u(x,u(y,z)) = u(u(x,y),z) ). % BII end_of_list.