include("ortholattice-header").

% OML_SS basis: { A_SS, B_SS, OM_SS }

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

% f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C))).  % denial of A_SS
% f(f(A,A),f(A,B)) != A.                           % denial of B_SS
  f(A,f(A,f(A,B))) != f(A,B).                      % denial of OM_SS

end_of_list.