include("gt_header").

% These weight templates cause cluases that contain matching
% terms to be deleted.

weight_list(pick_and_purge).
weight($(0) @ $(0) * ($(0) @ $(0)), 100).
weight($(0) * ($(0) @ $(0)) @ $(0), 100).
weight($(0) @ ($(0) @ $(0)) * $(0), 100).
weight(($(0) @ $(0)) * $(0) @ $(0), 100).
weight($(0) @ ($(0) @ ($(0) @ $(0))), 100).
weight($(0) @ $(0) * $(0) * $(0), 100).
weight($(0) * $(0) * $(0) @ $(0), 100).
end_of_list.

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.
