%%%%%%%%%%% Start of MACE input file

op(400, xfx, [^,v]).  % infix operators

list(sos).

% Axioms for an ortholattice.

x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).

x v y = y v x.
(x v y) v z = x v (y v z).

c(c(x)) = x.
x v (y v c(y)) = y v c(y).
x v (x ^ y) = x.
x ^ y = c(c(x) v c(y)).

% Ortholattice lemmas.

x ^ x = x.
x v x = x.
c(x) v x = 1.
c(x) ^ x = 0.

1 v x = 1.
x v 1 = 1.
1 ^ x = x.
x ^ 1 = x.

0 ^ x = 0.
x ^ 0 = 0.
0 v x = x.
x v 0 = x.

end_of_list.

list(sos).

% The original denial:
%
% c((A ^ c(B)) v c(A)) v ((A ^ c(B)) v ((c(A) ^ ((A v c(B)) ^
% (A v B))) v (c(A) ^ c((A v c(B)) ^ (A v B))))) != A v c(A).

% An equivalent denial that names subterms:  (This is necessary, because
% MACE cannot handle big equations.)

A ^ c(B) = D1.
A v c(B) = D2.
A v B = D3.
c(A) = D4.
D2 ^ D3 = D5.
D4 ^ c(D5) = D6.
D4 ^ D5 = D7.
D7 v D6 = D8.

c(D1 v D4) v (D1 v D8) != 1.

end_of_list.

%%%%%%%%%%% End of MACE input file.