op(400, infix, ^).
op(400, infix, v).

lex([C, B, A, x v x, c(x), x ^ x, f(x,x)]).  % rewrite to join/complement

set(anl_eq).

assign(pick_given_ratio, 4).
assign(max_weight, 40).
set(discard_commutativity_consequences).
 
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).

clear(sigint_interact).
clear(detailed_history).

list(usable).
x = x.
end_of_list.

list(sos).

f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x.  % OML_Sh

x v y = f(f(x,x),f(y,y)).   % DEF_J
x ^ y = f(f(x,y),f(x,y)).   % DEF_M
c(x) = f(x,x).              % DEF_C

end_of_list.

assign(max_proofs, 5).

list(passive).

%  A v (A ^ B) != A | $Ans(B1).
%  A v (c(A) ^ (A v B)) != A v B | $Ans(OM).

A v (B v C) != B v (A v C) | $Ans(AJ).
A v c(c(A) v B) != A | $Ans(B1_rewritten).
A ^ B != c(c(A) v c(B)) | $Ans(DM).
A v c(A v c(A v B)) != A v B | $Ans(OM_rewritten).
f(A,B) != c(A) v c(B) | $Ans(DEF_SS).


end_of_list.
