% -----------------------------
% Theorem 4.  Original version.
% -----------------------------

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

set(paramodulation).
set(hyper_resolution).

set(para_units_only).
set(para_from_small).

formulas(assumptions).

f(e, e, e) = e.
f(x, y, z) = f(x, z, y).
f(x, y, f(x, y, z) ) = z.
x + e = x.
e + x = x.

% extra assumption
f(x, y, z) = f(y, z, x).   

% gL clauses
f(z,x0,x1) != f(z,y0,y1) | f(w,x0,x1) = f(w,y0,y1) # label("gL").
f(f(z,x0,x1),x2,x3) != f(f(z,y0,y1),y2,y3) | f(f(w,x0,x1),x2,x3) = f(f(w,y0,y1),y2,y3) # label("gL").
f(x0,f(z,x1,x2),x3) != f(y0,f(z,y1,y2),y3) | f(x0,f(w,x1,x2),x3) = f(y0,f(w,y1,y2),y3) # label("gL").
f(x0,x1,f(z,x2,x3)) != f(y0,y1,f(z,y2,y3)) | f(x0,x1,f(w,x2,x3)) = f(y0,y1,f(w,y2,y3)) # label("gL").
f(z,x0,x1) + x2 != f(z,y0,y1) + y2 | f(w,x0,x1) + x2 = f(w,y0,y1) + y2 # label("gL").
x0 + f(z,x1,x2) != y0 + f(z,y1,y2) | x0 + f(w,x1,x2) = y0 + f(w,y1,y2) # label("gL").
f(x0,z,x1) != f(y0,z,y1) | f(x0,w,x1) = f(y0,w,y1) # label("gL").
f(f(x0,z,x1),x2,x3) != f(f(y0,z,y1),y2,y3) | f(f(x0,w,x1),x2,x3) = f(f(y0,w,y1),y2,y3) # label("gL").
f(x0,f(x1,z,x2),x3) != f(y0,f(y1,z,y2),y3) | f(x0,f(x1,w,x2),x3) = f(y0,f(y1,w,y2),y3) # label("gL").
f(x0,x1,f(x2,z,x3)) != f(y0,y1,f(y2,z,y3)) | f(x0,x1,f(x2,w,x3)) = f(y0,y1,f(y2,w,y3)) # label("gL").
f(x0,z,x1) + x2 != f(y0,z,y1) + y2 | f(x0,w,x1) + x2 = f(y0,w,y1) + y2 # label("gL").
x0 + f(x1,z,x2) != y0 + f(y1,z,y2) | x0 + f(x1,w,x2) = y0 + f(y1,w,y2) # label("gL").
f(x0,x1,z) != f(y0,y1,z) | f(x0,x1,w) = f(y0,y1,w) # label("gL").
f(f(x0,x1,z),x2,x3) != f(f(y0,y1,z),y2,y3) | f(f(x0,x1,w),x2,x3) = f(f(y0,y1,w),y2,y3) # label("gL").
f(x0,f(x1,x2,z),x3) != f(y0,f(y1,y2,z),y3) | f(x0,f(x1,x2,w),x3) = f(y0,f(y1,y2,w),y3) # label("gL").
f(x0,x1,f(x2,x3,z)) != f(y0,y1,f(y2,y3,z)) | f(x0,x1,f(x2,x3,w)) = f(y0,y1,f(y2,y3,w)) # label("gL").
f(x0,x1,z) + x2 != f(y0,y1,z) + y2 | f(x0,x1,w) + x2 = f(y0,y1,w) + y2 # label("gL").
x0 + f(x1,x2,z) != y0 + f(y1,y2,z) | x0 + f(x1,x2,w) = y0 + f(y1,y2,w) # label("gL").
z + x0 != z + y0 | w + x0 = w + y0 # label("gL").
f(z + x0,x1,x2) != f(z + y0,y1,y2) | f(w + x0,x1,x2) = f(w + y0,y1,y2) # label("gL").
f(x0,z + x1,x2) != f(y0,z + y1,y2) | f(x0,w + x1,x2) = f(y0,w + y1,y2) # label("gL").
f(x0,x1,z + x2) != f(y0,y1,z + y2) | f(x0,x1,w + x2) = f(y0,y1,w + y2) # 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").
f(x0 + z,x1,x2) != f(y0 + z,y1,y2) | f(x0 + w,x1,x2) = f(y0 + w,y1,y2) # label("gL").
f(x0,x1 + z,x2) != f(y0,y1 + z,y2) | f(x0,x1 + w,x2) = f(y0,y1 + w,y2) # label("gL").
f(x0,x1,x2 + z) != f(y0,y1,y2 + z) | f(x0,x1,x2 + w) = f(y0,y1,y2 + 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 goal for inverse
A + x != e.

end_of_list.
