formulas(sos). (x*(y*z)=(x*y)*z). (x*I=x). (x*inv(x)=I). end_of_list. formulas(goals). all x all y (x*y=y*x). end_of_list.