include("ortholattice-header").

% OML_SS basis: { A_SS, B_SS, OM_SS }
% OML basis:    { AJ, B1, DM, OM }

list(sos).

f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))).  % A_SS
f(f(x,x),f(x,y)) = x.                           % B_SS
f(x,f(x,f(x,y))) = f(x,y).                      % OM_SS

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 (B v C) != B v (A v C)     | $Ans(AJ).
  A v (A ^ B) != A               | $Ans(B1).
  A ^ B != c(c(A) v c(B))        | $Ans(DM).
% A v (c(A) ^ (A v B)) != A v B  | $Ans(OM).
  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.