assign(iterate_up_to, 12).

set(verbose).

% This list of formulas specifies a noncommutative group.
%
% Normally we would write the group axioms with clauses
% (as in the example ncg-48.in).  Here we use quantified
% formulas.

formulas(theory).

% Associativity

all x all y all z ((x * y) * z = x * (y * z)).

% There is a left identity element, and every element has a left inverse.

exists e ((all x (e * x = x)) &
          (all x exists y (y * x = e))).

% So far, we have group theory.  Now, state that
% there are two noncommuting elements.

exists a exists b (a * b != b * a).

end_of_list.