set(anl_eq).

assign(pick_given_ratio, 1).
assign(max_weight, 41).

set(discard_commutativity_consequences).

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(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x.  % MOL_Sh
end_of_list.

% assign(max_proofs, 4).

list(passive).

% MOL 4-basis: { A_SS, B_SS, ONE_SS, MOD_SS }

f(A,f(A,A)) != f(f(B,B),B) | $Ans(ONE_SS).

end_of_list.

