include("ortholattice-header").

% BA_SS basis: { A_SS, CUT_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,f(y,y)),f(x,y)) = x.                       % CUT_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,f(B,B)),f(A,B)) != A.                      % denial of CUT_SS


end_of_list.