% -----------------------------
% Theorem 3.  Original version.
% -----------------------------

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

set(paramodulation).
set(hyper_resolution).

formulas(assumptions).

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

% gL clauses
z * x0 != z * y0 | w * x0 = w * y0 # label("gL").
(z * x0) * x1 != (z * y0) * y1 | (w * x0) * x1 = (w * y0) * y1 # label("gL").
x0 * (z * x1) != y0 * (z * y1) | x0 * (w * x1) = y0 * (w * y1) # label("gL").
(z * x0) + x1 != (z * y0) + y1 | (w * x0) + x1 = (w * y0) + y1 # label("gL").
x0 + (z * x1) != y0 + (z * y1) | x0 + (w * x1) = y0 + (w * y1) # label("gL").
x0 * z != y0 * z | x0 * w = y0 * w # label("gL").
(x0 * z) * x1 != (y0 * z) * y1 | (x0 * w) * x1 = (y0 * w) * y1 # label("gL").
x0 * (x1 * z) != y0 * (y1 * z) | x0 * (x1 * w) = y0 * (y1 * w) # label("gL").
(x0 * z) + x1 != (y0 * z) + y1 | (x0 * w) + x1 = (y0 * w) + y1 # label("gL").
x0 + (x1 * z) != y0 + (y1 * z) | x0 + (x1 * w) = y0 + (y1 * w) # label("gL").
z + x0 != z + y0 | w + x0 = w + y0 # label("gL").
(z + x0) * x1 != (z + y0) * y1 | (w + x0) * x1 = (w + y0) * y1 # label("gL").
x0 * (z + x1) != y0 * (z + y1) | x0 * (w + x1) = y0 * (w + y1) # label("gL").
(z + x0) + x1 != (z + y0) + y1 | (w + x0) + x1 = (w + y0) + y1 # label("gL").
x0 + (z + x1) != y0 + (z + y1) | x0 + (w + x1) = y0 + (w + y1) # label("gL").
x0 + z != y0 + z | x0 + w = y0 + w # label("gL").
(x0 + z) * x1 != (y0 + z) * y1 | (x0 + w) * x1 = (y0 + w) * y1 # label("gL").
x0 * (x1 + z) != y0 * (y1 + z) | x0 * (x1 + w) = y0 * (y1 + w) # label("gL").
(x0 + z) + x1 != (y0 + z) + y1 | (x0 + w) + x1 = (y0 + w) + y1 # label("gL").
x0 + (x1 + z) != y0 + (y1 + z) | x0 + (x1 + w) = y0 + (y1 + 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.
