set(anl_eq).

assign(pick_given_ratio, 3).
assign(neg_weight, -11).
assign(max_weight, 33).

set(discard_commutativity_consequences).

weight_list(pick_and_purge).
weight(1, 5).
end_of_list.

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

clear(sigint_interact).
clear(detailed_history).

list(usable).
x = x.
end_of_list.

list(sos).

f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))).  % A_SS
f(f(x,x),f(x,y)) = x.                           % B_SS
f(x,f(x,x)) = f(y,f(y,y)).                      % ONE_SS
f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))).  % MOD_SS

f(x,f(x,x)) = 1.                                % ONEa_SS
% f(x,y) = f(y,x).     % lemma

f(f(B,A),f(f(f(A,A),C),f(f(f(f(f(A,B),C),C),A),f(A,D)))) != A | $Ans(MOL_Sh).  % denial of MOL_Sh

end_of_list.

