op(400, xfx, [/]).  % infix operators

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).

assign(pick_given_ratio, 4).
assign(max_mem, 20000).

set(knuth_bendix).

set(hyper_res).
set(order_history).
set(unit_deletion).
set(para_from_units_only).
set(para_into_units_only).

assign(max_weight, 45).
  
weight_list(pick_and_purge).
weight(x/ (((y/y)/y)/ ((y/y)/y))=x,2).
weight((((x/x)/x)/ ((x/x)/x))/ (((y/y)/y)/ (((y/z)/ (y/z))/ (y/z)))=z,2).
weight((((x/x)/x)/ (((x/ (y/z))/ (x/ (y/z)))/ (x/ (y/z))))/ ((y/y)/y)=z,2).
weight(((x/x)/x)/ ((x/x)/x)= ((y/y)/y)/ ((y/y)/y),2).
weight((((x/x)/x)/ ((x/x)/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((y/y)/y))= (y/y)/y,2).
weight((((x/x)/x)/ ((x/x)/x))/ ((((y/y)/ (y/y))/ (y/y))/ ((((z/z)/z)/ ((z/z)/z))/ ((y/y)/y)))=y,2).
weight(x/ (((((y/y)/y)/ ((y/y)/y))/ ((z/z)/z))/ ((((z/z)/z)/ ((z/z)/z))/ ((z/z)/z)))=x,2).
weight(((x/x)/x)/ (((x/y)/ (x/y))/ (x/y))= ((z/z)/z)/ (((z/y)/ (z/y))/ (z/y)),2).
weight((((x/x)/x)/ ((x/x)/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((z/z)/z))= (z/z)/z,2).
weight((((x/x)/ (x/x))/ (x/x))/ ((((y/y)/y)/ ((y/y)/y))/ ((x/x)/x))= (x/x)/x,2).
weight((((x/x)/x)/ ((x/x)/x))/ ((y/y)/y)=y,2).
weight(x/ (y/y)=x,2).
weight(((x/x)/x)/ (((x/y)/ (x/y))/ (x/y))= (y/y)/y,2).
weight((((x/x)/y)/ ((x/x)/y))/ ((x/x)/y)=y,2).
weight((x/x)/y= (y/y)/y,2).
weight(x/x=y/y,2).
end_of_list.

list(usable).
x = x.
end_of_list.

list(sos).
x / y != z / u  |  y / (((z / z) / z) / ((x / x) / x)) = u.
end_of_list.

list(passive).
A / A != B / B.
end_of_list.