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

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

set(paramodulation).
set(hyper_resolution).

set(para_units_only).
set(para_from_small).

clear(back_demod).
set(restrict_denials).

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.

% 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 # answer(x).

end_of_list.

formulas(hints).

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.
f(x,y,z) = f(y,z,x).
f(x,y,z) = f(y,x,z).
f(x,y,z) != f(x,u,w) | f(v5,y,z) = f(v5,u,w) # label("gL").
f(x,y,z) != f(x,u,w) | f(y,v5,z) = f(v5,u,w).
f(x,y,z) != f(x,u,w) | f(y,z,v5) = f(v5,u,w).
f(x,y,z) != f(x,u,w) | f(y,z,v5) = f(u,v5,w).
f(x,y,z) != f(x,u,w) | f(y,z,v5) = f(u,w,v5).
f(f(x,y,z),u,w) != f(f(x,v5,v6),v7,v8) | f(f(v9,y,z),u,w) = f(f(v9,v5,v6),v7,v8) # label("gL").
f(u,f(x,y,z),w) != f(f(x,v5,v6),v7,v8) | f(f(v9,y,z),u,w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(f(x,v5,v6),v7,v8) | f(f(v9,y,z),u,w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,f(x,v5,v6),v8) | f(f(v9,y,z),u,w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(f(v9,y,z),u,w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(f(y,v9,z),u,w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(f(y,z,v9),u,w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(u,f(y,z,v9),w) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(u,w,f(y,z,v9)) = f(f(v9,v5,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(u,w,f(y,z,v9)) = f(f(v5,v9,v6),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(u,w,f(y,z,v9)) = f(f(v5,v6,v9),v7,v8).
f(u,w,f(x,y,z)) != f(v7,v8,f(x,v5,v6)) | f(u,w,f(y,z,v9)) = f(v7,f(v5,v6,v9),v8).
f(x,y,f(z,u,w)) != f(v5,v6,f(z,v7,v8)) | f(x,y,f(u,w,v9)) = f(v5,v6,f(v7,v8,v9)).
f(x,y,z) != f(u,y,w) | f(x,v5,z) = f(u,v5,w) # label("gL").
f(x,y,z) != f(y,u,w) | f(x,v5,z) = f(u,v5,w).
f(x,y,z) != f(y,u,w) | f(x,z,v5) = f(u,v5,w).
f(x,y,z) != f(y,u,w) | f(x,z,v5) = f(u,w,v5).
f(y,u,w) != f(x,y,z) | f(x,z,v5) = f(u,w,v5).
f(x,y,z) != f(x,u,w) | f(u,w,v5) = f(y,z,v5).
f(x,y,z) + u != f(w,y,v5) + v6 | f(x,v7,z) + u = f(w,v7,v5) + v6 # label("gL").
f(x,y,z) + u != f(y,w,v5) + v6 | f(x,v7,z) + u = f(w,v7,v5) + v6.
f(x,y,z) + u != f(y,w,v5) + v6 | f(x,z,v7) + u = f(w,v7,v5) + v6.
f(x,y,z) + u != f(y,w,v5) + v6 | f(x,z,v7) + u = f(w,v5,v7) + v6.
f(y,w,v5) + v6 != f(x,y,z) + u | f(x,z,v7) + u = f(w,v5,v7) + v6.
f(x,y,z) + u != f(x,w,v5) + v6 | f(w,v5,v7) + v6 = f(y,z,v7) + u.
x + (y + z) != u + (y + w) | x + (v5 + z) = u + (v5 + w) # label("gL").
f(x + y,z,u) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6) # label("gL").
f(z,x + y,u) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6).
f(z,u,x + y) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6).
f(z,u,x + y) != f(v5,w + y,v6) | f(x + v7,z,u) = f(w + v7,v5,v6).
f(z,u,x + y) != f(v5,v6,w + y) | f(x + v7,z,u) = f(w + v7,v5,v6).
f(z,u,x + y) != f(v5,v6,w + y) | f(z,x + v7,u) = f(w + v7,v5,v6).
f(z,u,x + y) != f(v5,v6,w + y) | f(z,u,x + v7) = f(w + v7,v5,v6).
f(z,u,x + y) != f(v5,v6,w + y) | f(z,u,x + v7) = f(v5,w + v7,v6).
f(x,y,z + u) != f(w,v5,v6 + u) | f(x,y,z + v7) = f(w,v5,v6 + v7).
A + x != e.
x = f(y,f(y,z,x),z).
x = f(y,f(y,x,z),z).
x = f(y,f(x,y,z),z).
x = f(y,z,f(x,y,z)).
f(x,y,f(z,x,y)) = z.
f(x,f(y,x,f(y,z,u)),w) = f(z,u,w).
f(x,f(x,y,f(y,z,u)),w) = f(z,u,w).
f(x,y,f(x,z,f(z,u,w))) = f(u,w,y).
f(x,y,f(y,f(z,u,f(x,w,v5)),v6)) = f(z,u,f(w,v5,v6)).
f(x,y,f(y,z,f(u,w,f(x,v5,v6)))) = f(u,w,f(v5,v6,z)).
f(x,f(y,z,u),f(w,v5,v6)) = f(x,f(y,w,v5),f(z,u,v6)).
f(x,y,f(z,u,w)) = f(v5,v6,f(v6,f(x,y,f(v5,z,u)),w)).
f(x,y,f(z,u,w)) = f(v5,v6,f(v6,f(x,y,f(z,v5,u)),w)).
f(x,y,f(z,u,w)) = f(v5,v6,f(v6,f(x,y,f(z,u,v5)),w)).
f(x,y,f(z,u,w)) = f(v5,v6,f(v6,w,f(x,y,f(z,u,v5)))).
f(x,y,f(z,u,w)) = f(v5,v6,f(w,v6,f(x,y,f(z,u,v5)))).
f(x,y,f(z,y,f(u,w,f(v5,v6,x)))) = f(u,w,f(v5,v6,z)).
e + (x + (y + z)) = y + (x + z).
x + (y + z) = y + (x + z).
f(x,y + z,u + w) = f(x,u + z,y + w).
f(x,f(y,x,z),z) = y.
f(x,f(x,y,z),z) = y.
f(x,y,f(x,z,y)) = z.
f(x,y,z) + (f(u,w,v5) + v6) = f(w,v5,z) + (f(u,x,y) + v6).
f(x,y,z) + (f(u,w,v5) + v6) = f(w,z,v5) + (f(u,x,y) + v6).
f(x,y,z) + (f(u,w,v5) + v6) = f(z,w,v5) + (f(u,x,y) + v6).
f(x,y,z) + (f(u,w,v5) + v6) = f(z,w,v5) + (f(x,u,y) + v6).
f(x,y,z) + (f(u,w,v5) + v6) = f(z,w,v5) + (f(x,y,u) + v6).
f(x,y,z) + (f(u,w,v5) + v6) = f(u,w,x) + (f(v5,y,z) + v6).
x + y = y + (x + e).
x + y = y + x.
x + (A + y) != e.
x + (y + A) != e.
f(x,y,z) + (v6 + f(u,w,v5)) = f(u,w,x) + (f(v5,y,z) + v6).
v6 + (f(x,y,z) + f(u,w,v5)) = f(u,w,x) + (f(v5,y,z) + v6).
v6 + (f(x,y,z) + f(u,w,v5)) = f(u,x,w) + (f(v5,y,z) + v6).
v6 + (f(x,y,z) + f(u,w,v5)) = f(x,u,w) + (f(v5,y,z) + v6).
v6 + (f(x,y,z) + f(u,w,v5)) = f(x,u,w) + (f(y,v5,z) + v6).
v6 + (f(x,y,z) + f(u,w,v5)) = f(x,u,w) + (f(y,z,v5) + v6).
v6 + (f(x,y,z) + f(u,w,v5)) = f(x,u,w) + (v6 + f(y,z,v5)).
x + (f(y,z,u) + f(w,v5,v6)) = x + (f(y,w,v5) + f(z,u,v6)).
f(x,y + z,u + w) = f(x,z + u,y + w).
f(x,y + z,u + w) = f(x,u + y,z + w).
f(x,y,f(x,e,e)) = f(e,e,y).
f(x,y,f(x,e,e)) = f(e,y,e).
f(x,y,f(x,e,e)) = f(y,e,e).
f(e,e,x) = f(y,f(y,e,e),x).
f(e,x,e) = f(y,f(y,e,e),x).
f(x,e,e) = f(y,f(y,e,e),x).
f(x,e,e) = f(y,x,f(y,e,e)).
f(x,e,e) = f(x,y,f(y,e,e)).
f(x,y,f(y,e,e)) = f(x,e,e).
f(x,f(x,e,e),f(y,e,e)) = y.
f(x,f(x,e,e),f(y + z,e,e)) = z + y.
f(x,f(x,e,e),f(e,y + z,e)) = z + y.
f(x,f(x,e,e),f(e,e,y + z)) = z + y.
f(x,f(x,e,e),f(e,e,y + z)) = y + z.
x + (y + f(z,f(z,e,e),f(A,e,e))) != e.
x + (y + f(z,f(z,e,e),f(e,A,e))) != e.
x + (y + f(z,f(z,e,e),f(e,e,A))) != e.
f(e,x,f(x,y,f(z,u,e))) = f(z,u,f(e,e,y)).
f(x,e,f(x,y,f(z,u,e))) = f(z,u,f(e,e,y)).
f(x,e,f(x,y,f(z,u,e))) = f(z,u,f(e,y,e)).
f(x,e,f(x,y,f(z,u,e))) = f(z,u,f(y,e,e)).
f(x,f(y,x,e),f(z,u,e)) = f(f(y,z,u),e,e).
f(x,f(x,y,e),f(z,u,e)) = f(f(y,z,u),e,e).
f(x,f(x,y,e),f(z,u,e)) = f(e,f(y,z,u),e).
f(x,f(x,y,e),f(z,u,e)) = f(e,e,f(y,z,u)).
f(e,x,f(y,x,f(z,u,f(w,v5,f(w,e,e))))) = f(z,u,f(v5,e,y)).
f(e,x,f(y,x,f(z,u,f(v5,e,e)))) = f(z,u,f(v5,e,y)).
f(e,x,f(x,y,f(z,u,f(v5,e,e)))) = f(z,u,f(v5,e,y)).
f(x,e,f(x,y,f(z,u,f(v5,e,e)))) = f(z,u,f(v5,e,y)).
f(x,e,f(x,y,f(z,u,f(v5,e,e)))) = f(z,u,f(v5,y,e)).
f(x,e,f(x,y,f(z,u,f(w,e,e)))) = f(z,u,f(y,w,e)).
x + (f(y,z,u) + f(w,v5,f(z,u,v6))) = x + (f(y,w,v5) + v6).
x + (f(y,z,u) + f(w,v5,f(z,u,v6))) = x + (v6 + f(y,w,v5)).
x + (f(y,e,e) + f(z,u,w)) = x + (f(v5,z,u) + f(y,f(v5,e,e),w)).
x + (f(y,e,e) + f(z,u,w)) = x + (f(z,v5,u) + f(y,f(v5,e,e),w)).
x + (f(y,e,e) + f(z,u,w)) = x + (f(z,u,v5) + f(y,f(v5,e,e),w)).
x + (f(y,e,e) + f(z,u,w)) = x + (f(z,u,v5) + f(y,w,f(v5,e,e))).
x + (f(y,z,u) + f(w,v5,f(u,e,e))) = x + (f(w,e,e) + f(y,z,v5)).
x + (f(y,z,f(z,e,e)) + f(u,w,f(e,e,A))) != e.
x + (f(y,e,e) + f(u,w,f(e,e,A))) != e.
x + (A + f(y,z,u)) != e.
x + (A + (f(y,z,u) + e)) != e.
x + (A + (e + f(y,z,u))) != e.
x + (e + (A + f(y,z,u))) != e.
f(x,y,z + u) = f(x,z + y,e + u).
f(x,y,z + u) = f(x,y + z,e + u).
f(x,y,z + u) = f(x,y + z,u + e).
f(x,y,z + u) = f(x,y + z,u).
f(x,y,z + u) = f(x,u,y + z).
f(x,y,z) = f(x,e,y + z).
f(x,e,y + z) = f(x,y,z).
f(x,f(x,e,e),f(e,y,z)) = y + z.
f(x,f(x,e,e),f(y,e,z)) = y + z.
f(x,f(x,e,e),f(y,z,e)) = y + z.
f(e,e,f(e,y,z)) = y + z.
f(e,e,f(y,e,z)) = y + z.
f(e,e,f(x,y,e)) = x + y.
f(x,e,f(x,y,z)) = y + z.
f(x,y + z,f(x,y,z)) = e.
x + f(y,z,f(u,e,e)) = f(y,z,f(x,u,e)).
y + f(z,u,e) = f(z,u,f(y,e,e)).
f(x,y,f(z,e,e)) = z + f(x,y,e).
x + (f(y,z,u) + (u + f(w,v5,e))) = x + (f(w,e,e) + f(y,z,v5)).
x + (y + (f(z,u,y) + f(w,v5,e))) = x + (f(w,e,e) + f(z,u,v5)).
x + (y + f(z,u,e)) = f(z,u,f(x,y,e)).
x + (y + (f(z,y,u) + f(w,v5,e))) = x + (f(w,e,e) + f(z,u,v5)).
x + (y + (f(y,z,u) + f(w,v5,e))) = x + (f(w,e,e) + f(z,u,v5)).
x + f(w,v5,f(y,f(y,z,u),e)) = x + (f(w,e,e) + f(z,u,v5)).
x + f(w,v5,f(y,e,f(y,z,u))) = x + (f(w,e,e) + f(z,u,v5)).
x + f(w,v5,z + u) = x + (f(w,e,e) + f(z,u,v5)).
x + (f(y,e,e) + f(z,u,w)) = x + f(y,w,z + u).
f(e,x,f(x,y,f(z,u,w + v5))) = f(z,u,f(e,f(w,v5,e),y)).
f(x,e,f(x,y,f(z,u,w + v5))) = f(z,u,f(e,f(w,v5,e),y)).
y + f(z,u,w + v5) = f(z,u,f(e,f(w,v5,e),y)).
y + f(z,u,w + v5) = f(z,u,f(e,y,f(w,v5,e))).
y + f(z,u,w + v5) = f(z,u,f(y,e,f(w,v5,e))).
f(x,y,f(z,e,f(u,w,e))) = z + f(x,y,u + w).
f(x,y + z,f(u,w,v5)) = f(x,f(e,u,w),f(e,f(y,z,e),v5)).
f(x,y + z,f(u,w,v5)) = f(x,f(u,e,w),f(e,f(y,z,e),v5)).
f(x,y + z,f(u,w,v5)) = f(x,f(u,w,e),f(e,f(y,z,e),v5)).
f(x,y + z,f(u,w,v5)) = f(x,f(u,w,e),f(e,v5,f(y,z,e))).
f(x,y + z,f(u,w,v5)) = f(x,f(u,w,e),f(v5,e,f(y,z,e))).
f(x,y + z,f(u,w,v5)) = v5 + f(x,f(u,w,e),y + z).
x + f(y,f(z,u,e),w + v5) = f(y,w + v5,f(z,u,x)).
x + (f(y,z,u) + (w + v5)) = x + (f(y,e,e) + f(z,u,f(w,v5,e))).
x + (w + (f(y,z,u) + v5)) = x + (f(y,e,e) + f(z,u,f(w,v5,e))).
x + (w + (v5 + f(y,z,u))) = x + (f(y,e,e) + f(z,u,f(w,v5,e))).
x + (w + (v5 + f(y,z,u))) = x + f(y,f(w,v5,e),z + u).
x + (w + (v5 + f(y,z,u))) = f(y,z + u,f(w,v5,x)).
x + (w + (v5 + f(y,z,u))) = f(y,z + u,f(w,x,v5)).
x + (y + (z + f(u,w,v5))) = f(u,w + v5,f(x,y,z)).
x + (e + f(e,e,f(A,f(y,z,u),e))) != e.
x + (e + f(e,e,f(A,e,f(y,z,u)))) != e.
x + (e + f(e,e,f(e,A,f(y,z,u)))) != e.
f(x,y + z,f(u,e,A)) != e.
$F.
end_of_list.
