% ----------------------------------------------------
% Theorem 3.  Final version that appears in the paper.
% ----------------------------------------------------

clear(auto).

assign(order,kbo).
set(lex_order_vars).

set(paramodulation).
set(hyper_resolution).

clear(back_demod).
set(para_from_small).
set(para_units_only).

formulas(assumptions).

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

% selected gL clause
(x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL").

% denial of all 4 goals
(a * b) * e != a + b
   | a + (a * e) != e
   | a + b != b + a
   | a + (b + c) != (a + b) + c.

end_of_list.

% --------------------------------------------
% hints extracted from previously found proofs
% --------------------------------------------

formulas(hints).

x + (x * e) = e.
x * (y * x) = y.
x * y = y * x.
e * e = e.
x + e = x.
e + x = x.
c6 + (c6 * e) != e.
c6 + (e * c6) != e.
x * (x * y) = y.
x = (y * x) * y.
x = (x * y) * y.
x = y * (x * y).
(x + y) * (z + u) = (x + u) * (z + y).
x * (y + z) = (x + z) * (y + e).
x * (y + z) = (x + z) * y.
x * (y + z) = y * (x + z).
x * (y + z) = (e + z) * (y + x).
x * (y + z) = z * (y + x).
x * (y + z) = y * (z + x).
x * (y + z) = z * (x + y).
(x + y) * z = (x + z) * (e + y).
z * (x + y) = (x + z) * (e + y).
x * (z + y) = (x + z) * (e + y).
x * (z + y) = (x + z) * y.
x * (z + y) = y * (x + z).
x * (y + z) = x * (z + y).
x * (y * (x + z)) = z + y.
x * (x * (z + y)) = z + y.
x * (x * (y + z)) = z + y.
x + y = y + x.
(x + y) * (y * (z + x)) = z.
(x + y) * (y * (x + z)) = z.
(x + y) * (x * (z + y)) = z.
(x + y) * (x * (y + z)) = z.
(x + y) * (x * y) = e.
(x * y) * (x + y) = e.
y * ((x * y) + x) = e.
y * (x + (x * y)) = e.
x * ((x * y) + y) = e.
x * (y + (x * y)) = e.
x * e = y + (x * y).
x + (y * x) = y * e.
e * e != e.
e != e.
x + y = (x * y) * e.
x + (x * y) = y * e.
x + y = e * (x * y).
e * (x * y) = x + y.
x + (y + z) = (x + y) + z.
(x + y) + z = (x * (y + z)) * e.
z + (x + y) = (x * (y + z)) * e.
z + (x + y) = e * (x * (y + z)).
z + (x + y) = x + (y + z).
x + (y + z) = z + (x + y).
end_of_list.

formulas(hints).
x6 + (x6 * e) = e.
x6 + (e * x6) = e.
(x1 * x2) * e = x1 + x2.
e * (x1 * x2) = x1 + x2.
(x3 + x4) + x5 = x3 + (x4 + x5).
x5 + (x3 + x4) = x3 + (x4 + x5).
end_of_list.
