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

lex([C, B, A, x v x, c(x), x ^ x, f(x,x)]).  % rewrite to ^,c when possible

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(x,f(f(y,y),y)),z))) = x.  % OL_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, 6).

list(passive).

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

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).
c(c(A)) != A | $Ans(CC).
A v c(A) != B v c(B) | $Ans(ONE).
f(A,B) != c(A) v c(B) | $Ans(DEF_SS).

end_of_list.