op(400, xfx, [*,+,^,v,/,\,#]). % infix operators lrpo_multiset_status([_*_]). % This allows a direct proof. set(knuth_bendix). set(hyper_res). set(para_from_units_only). set(para_into_units_only). clear(print_kept). list(usable). x = x. end_of_list. list(sos). x * (y * x) = y. x * y = y * x. (x * y) * z != (x * u) * v | (w * y) * z = (w * u) * v. end_of_list. list(passive). % ((A * B) * C) * D != ((D * B) * C) * A. % ((A * B) * C) * D != B * (C * (A * D)). % (A * B) * (C * D) != (A * C) * (B * D). ((A * B) * C) * D != ((D * B) * C) * A. end_of_list.