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

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

list(sos).

% Axioms for an ortholattice.

x ^ y = y ^ x.              % dependent on other axioms
% (x ^ y) ^ z = x ^ (y ^ z).  % dependent on other axioms

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).  % follows from lemmas below
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(usable).

c(A) = d2.
B v d2 = d3.
B ^ d2 = d4.
c(d3) = d5.
d2 ^ c(B) = d8.
d3 ^ A = d9.
d8 v d4 = d10.
d10 v d9 = d11.
d11 ^ d2 = d12.
d11 v d2 = d13.
c(d11) ^ d2 = d14.
d13 ^ A = d16.
d14 v d12 = d17.
d17 v d16 = d18.
d5 ^ d18 = d19.
c(d18) ^ d5 = d20.
d18 v d5 = d21.
d21 ^ d3 = d22.
d19 v d22 = d23.
d23 v d20 != 1.

end_of_list.

% list(usable).
%     ( ( c( c(A) v B ) ^ ( ( ( c(A) ^ ( ( ( c(A) ^ B
%     ) v ( c(A) ^ c(B) ) ) v ( A ^ ( c(A) v B ) ) ) ) v ( c(A)
%     ^ c( ( ( c(A) ^ B ) v ( c(A) ^ c(B) ) ) v ( A ^ ( c(A) v
%     B ) ) ) ) ) v ( A ^ ( c(A) v ( ( ( c(A) ^ B ) v ( c(A) ^
%     c(B) ) ) v ( A ^ ( c(A) v B ) ) ) ) ) ) ) v ( c( c(A) v B
%     ) ^ c( ( ( c(A) ^ ( ( ( c(A) ^ B ) v ( c(A) ^ c(B) ) ) v
%     ( A ^ ( c(A) v B ) ) ) ) v ( c(A) ^ c( ( ( c(A) ^ B ) v
%     ( c(A) ^ c(B) ) ) v ( A ^ ( c(A) v B ) ) ) ) ) v ( A ^ (
%     c(A) v ( ( ( c(A) ^ B ) v ( c(A) ^ c(B) ) ) v ( A ^ ( c(A)
%     v B ) ) ) ) ) ) ) ) v ( ( c(A) v B ) ^ ( c( c(A) v B )
%     v ( ( ( c(A) ^ ( ( ( c(A) ^ B ) v ( c(A) ^ c(B) ) ) v ( A
%     ^ ( c(A) v B ) ) ) ) v ( c(A) ^ c( ( ( c(A) ^ B ) v ( c(A)
%     ^ c(B) ) ) v ( A ^ ( c(A) v B ) ) ) ) ) v ( A ^ ( c(A)
%     v ( ( ( c(A) ^ B ) v ( c(A) ^ c(B) ) ) v ( A ^ ( c(A) v B
%     ) ) ) ) ) ) ) ) = 1.
% end_of_list.

list(passive).

assign(2 ^ 3, 0).
assign(2 ^ 4, 0).
assign(2 ^ 5, 2).
assign(2 ^ 6, 0).
assign(2 ^ 7, 7).
assign(2 ^ 8, 0).
assign(2 ^ 9, 7).

assign(3 ^ 4, 4).
assign(3 ^ 5, 0).
assign(3 ^ 6, 3).
assign(3 ^ 7, 0).
assign(3 ^ 8, 0).
assign(3 ^ 9, 4).

assign(4 ^ 5, 0).
assign(4 ^ 6, 4).
assign(4 ^ 7, 0).
assign(4 ^ 8, 0).
assign(4 ^ 9, 4).

assign(5 ^ 6, 8).
assign(5 ^ 7, 7).
assign(5 ^ 8, 8).
assign(5 ^ 9, 7).

assign(6 ^ 7, 0).
assign(6 ^ 8, 8).
assign(6 ^ 9, 4).

assign(7 ^ 8, 0).
assign(7 ^ 9, 7).

assign(8 ^ 9, 0).

end_of_list.