a2/src/3a.prvr9

   1 formulas(assumptions).
   2 all x all y all z (x*(y*z)=(x*y)*z).
   3 all x (x*I=x).
   4 all x (x*inv(x)=I).
   5 end_of_list.
   6 formulas(goals).
   7 %I*x=x.
   8 %inv(inv(x))=x.
   9 %inv(x)*x=I.
  10 all x all y (x*y=y*x).
  11 end_of_list.