% File ex1.in:  Basic (minimal) input file that proves a simple thoerem
% in group theory.

formulas(assumptions).

   % identity
   e * x = x.
   x * e = x.

   % inverse
   x' * x = e.
   x * x' = e.

   % associativity
   (x * y) * z = x * (y * z).

   % denial of the theorem
   x * x = e.
   b * a != a * b.

end_of_list.
