include("ortholattice-header").

% OL_SS basis: { A_SS, B_SS, ONE_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,x)) = f(y,f(y,y)).                       % ONE_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,A)) != f(B,f(B,B)).                      % denial of ONE_SS

end_of_list.