include("ortholattice-header").

% OL    basis: { AJ, B1, DM, CC, ONE }
% OL_SS basis: { A_SS, B_SS, ONE_SS }

list(sos).

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

f(x,y) = c(x) v c(y).        % DEF_SS

end_of_list.

% The following command orders the relevant operations as f < v < c < ^
% so that everything is rewritten in terms of f whenever possible.

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

assign(max_proofs, 6).

list(passive).

f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C))) | $Ans(A_SS).  % denial of A_SS
f(f(A,A),f(A,B)) != A | $Ans(B_SS).                           % denial of B_SS
f(A,f(A,A)) != f(B,f(B,B)) | $Ans(ONE_SS).                    % denial of ONE_SS

A v B != f(f(A,A),f(B,B)) | $Ans(DEF_J).        % DEF_J
A ^ B != f(f(A,B),f(A,B)) | $Ans(DEF_M).        % DEF_M
c(A) != f(A,A) | $Ans(DEF_C).                   % DEF_C

end_of_list.