% Goodearl's Separativity Conjecture
%
% This is an equivalent form of the conjecture
% suitable for an automated deduction attack
%
% Source: Fred Wehrung

op(450,infix_right,"*").

if(Prover9).
assign(max_megs,500).

assign(order,kbo).
%set(lex_order_vars). % because of +
function_order([0,1,A0,B0,A1,B1,U,C,D,E,F,*,',+,-]).

end_if.

formulas(assumptions).

% ring axioms
0 + x = x. x + 0 = x.
-x + x = 0. x + -x = 0. -(-x) = x.
(x + y) + z = x + (y + z).
x + y = y + x.

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

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

% Von Neumann regular (' is an inverse)
x * x' * x = x .
x' * x * x' = x'.

% A0, A1, B0, B1 are pairwise orthogonal idempotents
% which resolve the identity element.

A0 + (A1 + (B0 + B1)) = 1.

% idempotents
A0 * A0 = A0.
A1 * A1 = A1.
B0 * B0 = B0.
B1 * B1 = B1.

% orthogonality relations
A0 * A1 = 0. A1 * A0 = 0.
A0 * B0 = 0. B0 * A0 = 0.
A0 * B1 = 0. B1 * A0 = 0.
A1 * B0 = 0. B0 * A1 = 0.
A1 * B1 = 0. B1 * A1 = 0.
B0 * B1 = 0. B1 * B0 = 0.

% properties of idempotent U 
U * U = 1.
U * A0 * U = A1.
U * B0 * U = B1.

% (A0 + A1) ~ (A1 + B0) via C, D
A0 + A1 = C * D. A1 + B0 = D * C.
C = (A0 + A1) * C * (A1 + B0).
D = (A1 + B0) * D * (A0 + A1).

% (A1 + B0) ~ (B0 + B1) via E, F
A1 + B0 = E * F. B0 + B1 = F * E.
E = (A1 + B0) * E * (B0 + B1).
F = (B0 + B1) * F * (A1 + B0).

% Goal: A0 ~ B0
x * y != A0 | y * x != B0.

end_of_list.