assign(report_stderr, 2).
set(ignore_option_dependencies). % GUI handles dependencies

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

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

formulas(assumptions).

% lattice theory

%L2v
x v y = y v x.
%L3v
(x v y) v z = x v (y v z).
%L2^
x ^ y = y ^ x.
%L3^
(x ^ y) ^ z = x^ (y ^ z).
%L4^
x ^ (x v y) = x.
%L4v
x v (x ^ y) = x.

%Boundedness
%L5v
0 v x = x.
%L6v
1 v x = 1.

% ---------------------------
% ---------------------------
%representable
% ---------------------------

%Orthocomplementation
%O1'
x'' = x.
%O2'
x v x' = 1.
%O3
x ^ y = (x' v y')'.

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

%Stonean
pc(pc(x v y)) = pc(pc(x)) v pc(pc(y)).

% ---------------------------
% ---------------------------
% Contact relation
% ---------------------------

%C.0
-C(0,x).
%C.1
x!=0 -> C(x,x).
%C(x,x).

%C.2
C(x,y) -> C(y,x).
%C.3
x ^ y = x -> (all z (C(x,z) -> C(y,z))).

end_of_list.

formulas(goals).

x ^ y != 0 -> (all w ( w ^ (x ^ y) = w <-> ( w ^ x = w & w ^ y = w ) )).

end_of_list.

