op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators

lrpo_multiset_status([m(_,_,_)]).  % This allows a direct proof.

set(knuth_bendix).
set(hyper_res).

set(para_from_units_only).
set(para_into_units_only).

assign(pick_given_ratio, 3).

list(usable).
x = x.
end_of_list.

list(sos).

m(x,y,z) != m(x,u,v) | m(w,y,z) = m(w,u,v).

m(x,y,y) = x.

m(x,y,z) = m(z,y,x).

end_of_list.

list(passive).
m(A,B,m(C,D,E)) != m(m(A,B,C),D,E).

end_of_list.