% File ex3.in: Illustrate more features (clause labels, goals, hints).

formulas(assumptions).

   e * x = x                  # label("left identity").
   x * e = x                  # label("right identity").

   x' * x = e                 # label("left inverse").
   x * x' = e                 # label("right inverse").

   (x * y) * z = x * (y * z)  # label(associativity).

   % theorem hypothesis
   x * x = e                  # label("idempotence").

end_of_list.

formulas(goals).

   x * y = y * x              # label("commutativity").

end_of_list.

formulas(hints).

   x * (y * (x * y)) = e.

end_of_list.
