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

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

assign(pick_given_ratio, 2).
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, 18).
  
weight_list(pick_and_purge).
%  Following are 16 positive steps from McCune's 20-step proof, from shorten2.out.
weight(x/e=x,2).
weight(e/ ((e/x)/ (e/ (x/y)))=y,2).
weight(((e/x)/ (e/ (x/ (y/z))))/ (e/y)=z,2).
weight((e/x)/ (e/ (x/y))=e/ (e/ (e/y)),2).
weight(e/ (e/x)=x,2).
weight((e/ (x/y))/ (e/x)=y,2).
weight((e/x)/ ((e/y)/ (x/ (y/z)))=z,2).
weight((e/x)/ (y/x)=e/y,2).
weight((x/y)/ (e/y)=x,2).
weight(x/ (y/ (e/x))=e/y,2).
weight(e/x=y/ (x/ (e/y)),2).
weight(x/y=e/ (y/x),2).
weight(e/ (x/y)=y/x,2).
weight(x/ ((y/z)/ (e/x))=z/y,2).
weight((x/y)/ (z/ (y/ (e/z)))=x,2).
weight((e/ (x/y))/ ((e/z)/x)=y/ (e/z),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.

x / x = e.

(A / ((((A / A) / B) / C) / (((A / A) / A) / C))) != B.
end_of_list.

list(passive).
end_of_list.