% File ex6.in:  Example input processing, encoding the group theory problem
% from ex01.in with a first-order formula instead of clauses.

formulas(assumptions).

(
   exists w
   (
      % identity
      (all x (x * w = x & w * x = x))

      % inverse
      & (all x exists y (x * y = w & y * x = w))

      % associativity
      & (all x all y all z ((x * y) * x = x * (y * z)))

      % denial of the theorem
      & -((all x (x * x = w)) -> (all x all y (x * y = y * x)))
   )
).

end_of_list.
