formulas(assumptions).
-x*(y*z)=(x*y)*z.
-x*I=x.
-x*inv(x)=I.
+all x all y all z (x*(y*z)=(x*y)*z).
+all x (x*I=x).
+all x (x*inv(x)=I).
end_of_list.
formulas(goals).
%I*x=x.
%inv(inv(x))=x.
%inv(x)*x=I.
-x*y=y*x.
+all x all y (x*y=y*x).
end_of_list.