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

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).
assign(max_weight, 19).

% Note that for this style of proof, where the goals are in the passive list,
% the denials must be in canonical form.  Because of the symbol ordering
% in the lex command, the canonical form is all in terms of join and complement.
% Therefore we rewrite denials that contain the meet operation.

list(passive).

  A v (B v C) != B v (A v C)      | $Ans(AJ).
  A ^ B != c(c(A) v c(B))         | $Ans(DM).
  A v c(A) != B v c(B)            | $Ans(ONE).

% (A v c(B)) ^ (A v B) != A       | $Ans(CUT).
  c(c(A v c(B)) v c(A v B)) != A  | $Ans(CUT_rewritten).

  f(A,B) != c(A) v c(B)      | $Ans(DEF_SS).

end_of_list.