include("ortholattice-header").

% OML basis:    { AJ, B1, DM, OM }
% OML_SS basis: { A_SS, B_SS, OM_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
x v (c(x) ^ (x v y)) = x v y.  % OM

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([D, C, B, A, 0, 1, f(x,x), x v x, c(x), x ^ x]).

assign(max_proofs, 6).
assign(max_weight, 21).
assign(pick_given_ratio, 4).

list(passive).

f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C)))  | $Ans(A_SS).
f(f(A,A),f(A,B)) != A                           | $Ans(B_SS).
f(A,f(A,f(A,B))) != f(A,B)                      | $Ans(OM_SS).

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

end_of_list.