include("ortholattice-header").

% Modify the basic strategy.

lex([A, B, C, D, 0, 1, x v x, x ^ x, c(x), f(x,x)]).
assign(max_proofs, 2).

% BA basis: { AJ, DM, ONE, CUT }

list(sos).

x v (y v z) = y v (x v z).  % AJ
x ^ y = c(c(x) v c(y)).     % DM
x v c(x) = y v c(y).        % ONE
(x v c(y)) ^ (x v y) = x.   % CUT

% Axiom ONE allows us to name the constant.  Also name its complement.

x v c(x) = 1.   % ONEa
c(1) = 0.

end_of_list.

list(passive).

A v (A ^ B) != A | $Ans(B1).   % denial of B1
c(c(A)) != A | $Ans(CC).       % denial of CC

end_of_list.
