include("cs_header").

assign(max_seconds, 7200).

list(sos).
(x @ y) @ z = x @ (y @ z).                % (A2) commutator is associative
end_of_list.

list(sos).
  ((A @ B) @ C) != (D @ (F @ G))         | $Ans(A).
% (A @ B) * C != C * (A @ B)             | $Ans(N).
% (A @ C) * (B @ C) != ((A * B) @ C)     | $Ans(D).
% A * B * C * B * A != B * A * C * A * B | $Ans(E).
end_of_list.
