formulas(assumptions).

  (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.
