% Saved by Prover9-Mace4 Version 0.5, December 2007.

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
  assign(max_seconds, 60).
end_if.

if(Mace4).   % Options for Mace4
  assign(max_seconds, 60).
end_if.

formulas(assumptions).

%L2^
x ^ y = y ^ x.
%L3^
x ^ (y ^ z) = (x ^ y) ^ z.

%L4'^
(x' ^ y')' ^ x = x.

%L6^
1 ^ x = x.

%Orthocomplementation
%OC1'
x'' = x.
%OC2'
x ^ x' = 0.
%OC3'
x v y = (x' ^ y')'.

%Pseudocomplementation
%PC1
x ^ pc(x ^ y) = x ^ pc(y).  
%PC2'
pc(0) = 1.
%PC2''
pc(1) = 0.

%S1'
pc(x ^ y) = ( (pc(x))' ^ (pc(y))' )'.

end_of_list.

formulas(goals).

%L1^
x = x ^ x.

%L1v
x = x v x.

%L2v
x v y = y v x.

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

%L4^
x ^ (x v y) = x.

%L4v
x v (x ^ y) = x.

%L5^
0 ^ x = 0.

%L5v
0 v x = x.

%L6v
1 v x = 1.

%PC2
x ^ 0' = x.

%PC3
0''=0.

%OC1
x v (y v z) = (z' ^ y')' v x.

%OC2
x ^ (x v y)=x.

%OC3
x v (y ^ y') = x.

%S1
pc(x ^ y) = pc(x) v pc(y).

end_of_list.

