% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).

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).

%%%% +:= join *:= meet 

x + x = x. 

x + y = y + x. 

x + (y + z) = (x + y) + z. 

x * x = x. 

x * y = y * x. 

x * (y * z) = (x * y) * z. 

%x + (y * z) = (x + y) * (x * z).

(x')' = x.

(x + y)' = x' * y'.

(x * y)' = x' + y'. 

%x * (x' + y) = x * y.

%x * (x + x') = x.

x * (x' + y) = x * y. 

0 + x = x. 

1 = 0'.

%%%% linearly ordered 

x + x' = x & y + y' = y -> (x + y = y | y + x = x).

end_of_list.

formulas(goals).

%x = y.

end_of_list.

