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.