============================== Prover9 =============================== Prover9 (64) version 2009-02A, February 2009. Process 20021 was started by veroff on proof, Fri Dec 7 16:29:09 2012 The command was "prover9 -f thm4_final.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file thm4_final.in assign(order,kbo). set(lex_order_vars). set(paramodulation). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). 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. 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"). 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. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(e,e,e) = e. [assumption]. f(x,y,z) = f(x,z,y). [assumption]. f(x,y,f(x,y,z)) = z. [assumption]. x + e = x. [assumption]. e + x = x. [assumption]. f(x,y,z) != f(x,u,w) | f(v5,y,z) = f(v5,u,w) # label("gL"). [assumption]. 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"). [assumption]. f(x,f(y,z,u),w) != f(v5,f(y,v6,v7),v8) | f(x,f(v9,z,u),w) = f(v5,f(v9,v6,v7),v8) # label("gL"). [assumption]. f(x,y,f(z,u,w)) != f(v5,v6,f(z,v7,v8)) | f(x,y,f(v9,u,w)) = f(v5,v6,f(v9,v7,v8)) # label("gL"). [assumption]. f(x,y,z) + u != f(x,w,v5) + v6 | f(v7,y,z) + u = f(v7,w,v5) + v6 # label("gL"). [assumption]. x + f(y,z,u) != w + f(y,v5,v6) | x + f(v7,z,u) = w + f(v7,v5,v6) # label("gL"). [assumption]. f(x,y,z) != f(u,y,w) | f(x,v5,z) = f(u,v5,w) # label("gL"). [assumption]. f(f(x,y,z),u,w) != f(f(v5,y,v6),v7,v8) | f(f(x,v9,z),u,w) = f(f(v5,v9,v6),v7,v8) # label("gL"). [assumption]. f(x,f(y,z,u),w) != f(v5,f(v6,z,v7),v8) | f(x,f(y,v9,u),w) = f(v5,f(v6,v9,v7),v8) # label("gL"). [assumption]. f(x,y,f(z,u,w)) != f(v5,v6,f(v7,u,v8)) | f(x,y,f(z,v9,w)) = f(v5,v6,f(v7,v9,v8)) # label("gL"). [assumption]. f(x,y,z) + u != f(w,y,v5) + v6 | f(x,v7,z) + u = f(w,v7,v5) + v6 # label("gL"). [assumption]. x + f(y,z,u) != w + f(v5,z,v6) | x + f(y,v7,u) = w + f(v5,v7,v6) # label("gL"). [assumption]. f(x,y,z) != f(u,w,z) | f(x,y,v5) = f(u,w,v5) # label("gL"). [assumption]. f(f(x,y,z),u,w) != f(f(v5,v6,z),v7,v8) | f(f(x,y,v9),u,w) = f(f(v5,v6,v9),v7,v8) # label("gL"). [assumption]. f(x,f(y,z,u),w) != f(v5,f(v6,v7,u),v8) | f(x,f(y,z,v9),w) = f(v5,f(v6,v7,v9),v8) # label("gL"). [assumption]. f(x,y,f(z,u,w)) != f(v5,v6,f(v7,v8,w)) | f(x,y,f(z,u,v9)) = f(v5,v6,f(v7,v8,v9)) # label("gL"). [assumption]. f(x,y,z) + u != f(w,v5,z) + v6 | f(x,y,v7) + u = f(w,v5,v7) + v6 # label("gL"). [assumption]. x + f(y,z,u) != w + f(v5,v6,u) | x + f(y,z,v7) = w + f(v5,v6,v7) # label("gL"). [assumption]. x + y != x + z | u + y = u + z # label("gL"). [assumption]. f(x + y,z,u) != f(x + w,v5,v6) | f(v7 + y,z,u) = f(v7 + w,v5,v6) # label("gL"). [assumption]. f(x,y + z,u) != f(w,y + v5,v6) | f(x,v7 + z,u) = f(w,v7 + v5,v6) # label("gL"). [assumption]. f(x,y,z + u) != f(w,v5,z + v6) | f(x,y,v7 + u) = f(w,v5,v7 + v6) # label("gL"). [assumption]. (x + y) + z != (x + u) + w | (v5 + y) + z = (v5 + u) + w # label("gL"). [assumption]. x + (y + z) != u + (y + w) | x + (v5 + z) = u + (v5 + w) # label("gL"). [assumption]. x + y != z + y | x + u = z + u # label("gL"). [assumption]. f(x + y,z,u) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6) # label("gL"). [assumption]. f(x,y + z,u) != f(w,v5 + z,v6) | f(x,y + v7,u) = f(w,v5 + v7,v6) # label("gL"). [assumption]. f(x,y,z + u) != f(w,v5,v6 + u) | f(x,y,z + v7) = f(w,v5,v6 + v7) # label("gL"). [assumption]. (x + y) + z != (u + y) + w | (x + v5) + z = (u + v5) + w # label("gL"). [assumption]. x + (y + z) != u + (w + z) | x + (y + v5) = u + (w + v5) # label("gL"). [assumption]. A + x != e # answer(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 187 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Function symbol KB weights: e=1. A=1. +=1. f=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ e, A, +, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) Auto_process settings: (no changes). kept: 1 f(e,e,e) = e. [assumption]. kept: 2 f(x,y,z) = f(x,z,y). [assumption]. kept: 3 f(x,y,f(x,y,z)) = z. [assumption]. kept: 4 x + e = x. [assumption]. kept: 5 e + x = x. [assumption]. kept: 6 f(x,y,z) != f(x,u,w) | f(v5,y,z) = f(v5,u,w) # label("gL"). [assumption]. kept: 7 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"). [assumption]. kept: 8 f(x,f(y,z,u),w) != f(v5,f(y,v6,v7),v8) | f(x,f(v9,z,u),w) = f(v5,f(v9,v6,v7),v8) # label("gL"). [assumption]. kept: 9 f(x,y,f(z,u,w)) != f(v5,v6,f(z,v7,v8)) | f(x,y,f(v9,u,w)) = f(v5,v6,f(v9,v7,v8)) # label("gL"). [assumption]. kept: 10 f(x,y,z) + u != f(x,w,v5) + v6 | f(v7,y,z) + u = f(v7,w,v5) + v6 # label("gL"). [assumption]. kept: 11 x + f(y,z,u) != w + f(y,v5,v6) | x + f(v7,z,u) = w + f(v7,v5,v6) # label("gL"). [assumption]. kept: 12 f(x,y,z) != f(u,y,w) | f(x,v5,z) = f(u,v5,w) # label("gL"). [assumption]. kept: 13 f(f(x,y,z),u,w) != f(f(v5,y,v6),v7,v8) | f(f(x,v9,z),u,w) = f(f(v5,v9,v6),v7,v8) # label("gL"). [assumption]. kept: 14 f(x,f(y,z,u),w) != f(v5,f(v6,z,v7),v8) | f(x,f(y,v9,u),w) = f(v5,f(v6,v9,v7),v8) # label("gL"). [assumption]. kept: 15 f(x,y,f(z,u,w)) != f(v5,v6,f(v7,u,v8)) | f(x,y,f(z,v9,w)) = f(v5,v6,f(v7,v9,v8)) # label("gL"). [assumption]. kept: 16 f(x,y,z) + u != f(w,y,v5) + v6 | f(x,v7,z) + u = f(w,v7,v5) + v6 # label("gL"). [assumption]. kept: 17 x + f(y,z,u) != w + f(v5,z,v6) | x + f(y,v7,u) = w + f(v5,v7,v6) # label("gL"). [assumption]. kept: 18 f(x,y,z) != f(u,w,z) | f(x,y,v5) = f(u,w,v5) # label("gL"). [assumption]. kept: 19 f(f(x,y,z),u,w) != f(f(v5,v6,z),v7,v8) | f(f(x,y,v9),u,w) = f(f(v5,v6,v9),v7,v8) # label("gL"). [assumption]. kept: 20 f(x,f(y,z,u),w) != f(v5,f(v6,v7,u),v8) | f(x,f(y,z,v9),w) = f(v5,f(v6,v7,v9),v8) # label("gL"). [assumption]. kept: 21 f(x,y,f(z,u,w)) != f(v5,v6,f(v7,v8,w)) | f(x,y,f(z,u,v9)) = f(v5,v6,f(v7,v8,v9)) # label("gL"). [assumption]. kept: 22 f(x,y,z) + u != f(w,v5,z) + v6 | f(x,y,v7) + u = f(w,v5,v7) + v6 # label("gL"). [assumption]. kept: 23 x + f(y,z,u) != w + f(v5,v6,u) | x + f(y,z,v7) = w + f(v5,v6,v7) # label("gL"). [assumption]. kept: 24 x + y != x + z | u + y = u + z # label("gL"). [assumption]. kept: 25 f(x + y,z,u) != f(x + w,v5,v6) | f(v7 + y,z,u) = f(v7 + w,v5,v6) # label("gL"). [assumption]. kept: 26 f(x,y + z,u) != f(w,y + v5,v6) | f(x,v7 + z,u) = f(w,v7 + v5,v6) # label("gL"). [assumption]. kept: 27 f(x,y,z + u) != f(w,v5,z + v6) | f(x,y,v7 + u) = f(w,v5,v7 + v6) # label("gL"). [assumption]. kept: 28 (x + y) + z != (x + u) + w | (v5 + y) + z = (v5 + u) + w # label("gL"). [assumption]. kept: 29 x + (y + z) != u + (y + w) | x + (v5 + z) = u + (v5 + w) # label("gL"). [assumption]. kept: 30 x + y != z + y | x + u = z + u # label("gL"). [assumption]. kept: 31 f(x + y,z,u) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6) # label("gL"). [assumption]. kept: 32 f(x,y + z,u) != f(w,v5 + z,v6) | f(x,y + v7,u) = f(w,v5 + v7,v6) # label("gL"). [assumption]. kept: 33 f(x,y,z + u) != f(w,v5,v6 + u) | f(x,y,z + v7) = f(w,v5,v6 + v7) # label("gL"). [assumption]. kept: 34 (x + y) + z != (u + y) + w | (x + v5) + z = (u + v5) + w # label("gL"). [assumption]. kept: 35 x + (y + z) != u + (w + z) | x + (y + v5) = u + (w + v5) # label("gL"). [assumption]. kept: 36 A + x != e # answer(x). [assumption]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 36 A + x != e # answer(x). [assumption]. end_of_list. formulas(sos). 1 f(e,e,e) = e. [assumption]. 2 f(x,y,z) = f(x,z,y). [assumption]. 3 f(x,y,f(x,y,z)) = z. [assumption]. 4 x + e = x. [assumption]. 5 e + x = x. [assumption]. 6 f(x,y,z) != f(x,u,w) | f(v5,y,z) = f(v5,u,w) # label("gL"). [assumption]. 7 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"). [assumption]. 8 f(x,f(y,z,u),w) != f(v5,f(y,v6,v7),v8) | f(x,f(v9,z,u),w) = f(v5,f(v9,v6,v7),v8) # label("gL"). [assumption]. 9 f(x,y,f(z,u,w)) != f(v5,v6,f(z,v7,v8)) | f(x,y,f(v9,u,w)) = f(v5,v6,f(v9,v7,v8)) # label("gL"). [assumption]. 10 f(x,y,z) + u != f(x,w,v5) + v6 | f(v7,y,z) + u = f(v7,w,v5) + v6 # label("gL"). [assumption]. 11 x + f(y,z,u) != w + f(y,v5,v6) | x + f(v7,z,u) = w + f(v7,v5,v6) # label("gL"). [assumption]. 12 f(x,y,z) != f(u,y,w) | f(x,v5,z) = f(u,v5,w) # label("gL"). [assumption]. 13 f(f(x,y,z),u,w) != f(f(v5,y,v6),v7,v8) | f(f(x,v9,z),u,w) = f(f(v5,v9,v6),v7,v8) # label("gL"). [assumption]. 14 f(x,f(y,z,u),w) != f(v5,f(v6,z,v7),v8) | f(x,f(y,v9,u),w) = f(v5,f(v6,v9,v7),v8) # label("gL"). [assumption]. 15 f(x,y,f(z,u,w)) != f(v5,v6,f(v7,u,v8)) | f(x,y,f(z,v9,w)) = f(v5,v6,f(v7,v9,v8)) # label("gL"). [assumption]. 16 f(x,y,z) + u != f(w,y,v5) + v6 | f(x,v7,z) + u = f(w,v7,v5) + v6 # label("gL"). [assumption]. 17 x + f(y,z,u) != w + f(v5,z,v6) | x + f(y,v7,u) = w + f(v5,v7,v6) # label("gL"). [assumption]. 18 f(x,y,z) != f(u,w,z) | f(x,y,v5) = f(u,w,v5) # label("gL"). [assumption]. 19 f(f(x,y,z),u,w) != f(f(v5,v6,z),v7,v8) | f(f(x,y,v9),u,w) = f(f(v5,v6,v9),v7,v8) # label("gL"). [assumption]. 20 f(x,f(y,z,u),w) != f(v5,f(v6,v7,u),v8) | f(x,f(y,z,v9),w) = f(v5,f(v6,v7,v9),v8) # label("gL"). [assumption]. 21 f(x,y,f(z,u,w)) != f(v5,v6,f(v7,v8,w)) | f(x,y,f(z,u,v9)) = f(v5,v6,f(v7,v8,v9)) # label("gL"). [assumption]. 22 f(x,y,z) + u != f(w,v5,z) + v6 | f(x,y,v7) + u = f(w,v5,v7) + v6 # label("gL"). [assumption]. 23 x + f(y,z,u) != w + f(v5,v6,u) | x + f(y,z,v7) = w + f(v5,v6,v7) # label("gL"). [assumption]. 24 x + y != x + z | u + y = u + z # label("gL"). [assumption]. 25 f(x + y,z,u) != f(x + w,v5,v6) | f(v7 + y,z,u) = f(v7 + w,v5,v6) # label("gL"). [assumption]. 26 f(x,y + z,u) != f(w,y + v5,v6) | f(x,v7 + z,u) = f(w,v7 + v5,v6) # label("gL"). [assumption]. 27 f(x,y,z + u) != f(w,v5,z + v6) | f(x,y,v7 + u) = f(w,v5,v7 + v6) # label("gL"). [assumption]. 28 (x + y) + z != (x + u) + w | (v5 + y) + z = (v5 + u) + w # label("gL"). [assumption]. 29 x + (y + z) != u + (y + w) | x + (v5 + z) = u + (v5 + w) # label("gL"). [assumption]. 30 x + y != z + y | x + u = z + u # label("gL"). [assumption]. 31 f(x + y,z,u) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6) # label("gL"). [assumption]. 32 f(x,y + z,u) != f(w,v5 + z,v6) | f(x,y + v7,u) = f(w,v5 + v7,v6) # label("gL"). [assumption]. 33 f(x,y,z + u) != f(w,v5,v6 + u) | f(x,y,z + v7) = f(w,v5,v6 + v7) # label("gL"). [assumption]. 34 (x + y) + z != (u + y) + w | (x + v5) + z = (u + v5) + w # label("gL"). [assumption]. 35 x + (y + z) != u + (w + z) | x + (y + v5) = u + (w + v5) # label("gL"). [assumption]. end_of_list. formulas(demodulators). end_of_list. % 170 hints (187 processed, 17 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=6): 1 f(e,e,e) = e. [assumption]. given #2 (I,wt=9): 2 f(x,y,z) = f(x,z,y). [assumption]. given #3 (I,wt=9): 3 f(x,y,f(x,y,z)) = z. [assumption]. given #4 (I,wt=5): 4 x + e = x. [assumption]. given #5 (I,wt=5): 5 e + x = x. [assumption]. given #6 (I,wt=18): 6 f(x,y,z) != f(x,u,w) | f(v5,y,z) = f(v5,u,w) # label("gL"). [assumption]. given #7 (I,wt=30): 7 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"). [assumption]. given #8 (I,wt=30): 8 f(x,f(y,z,u),w) != f(v5,f(y,v6,v7),v8) | f(x,f(v9,z,u),w) = f(v5,f(v9,v6,v7),v8) # label("gL"). [assumption]. given #9 (I,wt=30): 9 f(x,y,f(z,u,w)) != f(v5,v6,f(z,v7,v8)) | f(x,y,f(v9,u,w)) = f(v5,v6,f(v9,v7,v8)) # label("gL"). [assumption]. given #10 (I,wt=26): 10 f(x,y,z) + u != f(x,w,v5) + v6 | f(v7,y,z) + u = f(v7,w,v5) + v6 # label("gL"). [assumption]. given #11 (I,wt=26): 11 x + f(y,z,u) != w + f(y,v5,v6) | x + f(v7,z,u) = w + f(v7,v5,v6) # label("gL"). [assumption]. given #12 (I,wt=18): 12 f(x,y,z) != f(u,y,w) | f(x,v5,z) = f(u,v5,w) # label("gL"). [assumption]. given #13 (I,wt=30): 13 f(f(x,y,z),u,w) != f(f(v5,y,v6),v7,v8) | f(f(x,v9,z),u,w) = f(f(v5,v9,v6),v7,v8) # label("gL"). [assumption]. given #14 (I,wt=30): 14 f(x,f(y,z,u),w) != f(v5,f(v6,z,v7),v8) | f(x,f(y,v9,u),w) = f(v5,f(v6,v9,v7),v8) # label("gL"). [assumption]. given #15 (I,wt=30): 15 f(x,y,f(z,u,w)) != f(v5,v6,f(v7,u,v8)) | f(x,y,f(z,v9,w)) = f(v5,v6,f(v7,v9,v8)) # label("gL"). [assumption]. given #16 (I,wt=26): 16 f(x,y,z) + u != f(w,y,v5) + v6 | f(x,v7,z) + u = f(w,v7,v5) + v6 # label("gL"). [assumption]. given #17 (I,wt=26): 17 x + f(y,z,u) != w + f(v5,z,v6) | x + f(y,v7,u) = w + f(v5,v7,v6) # label("gL"). [assumption]. given #18 (I,wt=18): 18 f(x,y,z) != f(u,w,z) | f(x,y,v5) = f(u,w,v5) # label("gL"). [assumption]. given #19 (I,wt=30): 19 f(f(x,y,z),u,w) != f(f(v5,v6,z),v7,v8) | f(f(x,y,v9),u,w) = f(f(v5,v6,v9),v7,v8) # label("gL"). [assumption]. given #20 (I,wt=30): 20 f(x,f(y,z,u),w) != f(v5,f(v6,v7,u),v8) | f(x,f(y,z,v9),w) = f(v5,f(v6,v7,v9),v8) # label("gL"). [assumption]. given #21 (I,wt=30): 21 f(x,y,f(z,u,w)) != f(v5,v6,f(v7,v8,w)) | f(x,y,f(z,u,v9)) = f(v5,v6,f(v7,v8,v9)) # label("gL"). [assumption]. given #22 (I,wt=26): 22 f(x,y,z) + u != f(w,v5,z) + v6 | f(x,y,v7) + u = f(w,v5,v7) + v6 # label("gL"). [assumption]. given #23 (I,wt=26): 23 x + f(y,z,u) != w + f(v5,v6,u) | x + f(y,z,v7) = w + f(v5,v6,v7) # label("gL"). [assumption]. given #24 (I,wt=14): 24 x + y != x + z | u + y = u + z # label("gL"). [assumption]. given #25 (I,wt=26): 25 f(x + y,z,u) != f(x + w,v5,v6) | f(v7 + y,z,u) = f(v7 + w,v5,v6) # label("gL"). [assumption]. given #26 (I,wt=26): 26 f(x,y + z,u) != f(w,y + v5,v6) | f(x,v7 + z,u) = f(w,v7 + v5,v6) # label("gL"). [assumption]. given #27 (I,wt=26): 27 f(x,y,z + u) != f(w,v5,z + v6) | f(x,y,v7 + u) = f(w,v5,v7 + v6) # label("gL"). [assumption]. given #28 (I,wt=22): 28 (x + y) + z != (x + u) + w | (v5 + y) + z = (v5 + u) + w # label("gL"). [assumption]. given #29 (I,wt=22): 29 x + (y + z) != u + (y + w) | x + (v5 + z) = u + (v5 + w) # label("gL"). [assumption]. given #30 (I,wt=14): 30 x + y != z + y | x + u = z + u # label("gL"). [assumption]. given #31 (I,wt=26): 31 f(x + y,z,u) != f(w + y,v5,v6) | f(x + v7,z,u) = f(w + v7,v5,v6) # label("gL"). [assumption]. given #32 (I,wt=26): 32 f(x,y + z,u) != f(w,v5 + z,v6) | f(x,y + v7,u) = f(w,v5 + v7,v6) # label("gL"). [assumption]. given #33 (I,wt=26): 33 f(x,y,z + u) != f(w,v5,v6 + u) | f(x,y,z + v7) = f(w,v5,v6 + v7) # label("gL"). [assumption]. given #34 (I,wt=22): 34 (x + y) + z != (u + y) + w | (x + v5) + z = (u + v5) + w # label("gL"). [assumption]. given #35 (I,wt=22): 35 x + (y + z) != u + (w + z) | x + (y + v5) = u + (w + v5) # label("gL"). [assumption]. given #36 (H,wt=9): 44 f(x,f(x,y,z),y) = z. [para(3(a,1),2(a,1)),flip(a)]. given #37 (H,wt=9): 46 f(x,y,f(x,z,y)) = z. [para(2(a,1),3(a,1,3))]. given #38 (H,wt=9): 112 f(x,f(x,y,z),z) = y. [para(2(a,1),44(a,1,2))]. given #39 (H,wt=13): 86 e + (x + (y + z)) = y + (x + z). [hyper(29,a,5,a)]. given #40 (H,wt=11): 207 x + (y + z) = y + (x + z). [para(86(a,1),5(a,1))]. given #41 (H,wt=9): 234 x + (y + e) = y + x. [para(4(a,1),207(a,1,2)),flip(a)]. % Operation + is commutative; C redundancy checks enabled. given #42 (H,wt=7): 256 x + y = y + x. [para(4(a,1),234(a,1,2))]. given #43 (H,wt=17): 90 f(x,y + z,u + w) = f(x,u + z,y + w). [hyper(32,a,2,a)]. given #44 (H,wt=15): 298 f(x,y + z,e + u) = f(x,z,y + u). [para(5(a,1),90(a,1,2)),flip(a)]. given #45 (H,wt=15): 380 f(x,y + z,e + u) = f(x,y,z + u). [para(256(a,1),298(a,1,2))]. given #46 (H,wt=13): 401 f(x,y + z,u) = f(x,y,z + u). [para(5(a,1),380(a,1,3))]. given #47 (H,wt=11): 458 f(x,e,y + z) = f(x,y,z). [para(5(a,1),401(a,1,2)),flip(a)]. given #48 (H,wt=11): 498 f(x,e,f(x,y,z)) = y + z. [para(458(a,1),3(a,1,3))]. given #49 (H,wt=11): 511 f(x,y + z,f(x,y,z)) = e. [para(458(a,1),46(a,1,3))]. given #50 (H,wt=13): 447 f(x,y,z + u) = f(x,u,y + z). [para(401(a,1),2(a,1))]. given #51 (H,wt=15): 440 f(x,y + z,u + e) = f(x,y,z + u). [para(256(a,1),380(a,1,3))]. given #52 (H,wt=17): 321 f(x,y + z,u + w) = f(x,u + y,z + w). [para(256(a,1),90(a,1,2))]. given #53 (H,wt=21): 78 f(x,y,f(x,z,f(u,w,f(v5,y,v6)))) = f(u,w,f(v5,z,v6)). [hyper(15,a,3,a)]. given #54 (H,wt=18): 842 f(x,e,f(x,y,f(z,u,e))) = f(z,u,f(e,y,e)). [para(1(a,1),78(a,1,3,3,3))]. given #55 (H,wt=18): 977 f(x,e,f(x,y,f(z,u,e))) = f(z,u,f(e,e,y)). [para(2(a,1),842(a,2,3))]. given #56 (H,wt=21): 849 f(x,y,f(x,z,f(u,w,f(v5,y,v6)))) = f(u,w,f(v5,v6,z)). [para(2(a,1),78(a,2,3))]. given #57 (H,wt=1021): 846 f(x,y,f(x,z,f(u,w,f(v5,v6,y)))) = f(u,w,f(v5,z,v6)). [para(2(a,1),78(a,1,3,3,3))]. given #58 (H,wt=1021): 1199 f(x,y,f(x,z,f(u,w,f(v5,v6,y)))) = f(u,w,f(v5,v6,z)). [para(2(a,1),849(a,1,3,3,3))]. given #59 (A,wt=9): 37 f(f(e,e,e),e,e) = e. [para(1(a,2),1(a,1,1))]. given #60 (T,wt=7): 59 x + (e + e) = x. [para(4(a,2),4(a,1,2))]. given #61 (T,wt=7): 60 (x + e) + e = x. [para(4(a,2),4(a,1))]. given #62 (T,wt=7): 66 e + (x + e) = x. [para(5(a,2),4(a,1))]. given #63 (T,wt=7): 67 (e + e) + x = x. [para(4(a,2),5(a,1,1))]. given #64 (A,wt=12): 39 f(f(x,y,f(x,y,e)),e,e) = e. [para(3(a,2),1(a,1,1))]. given #65 (T,wt=7): 68 e + (e + x) = x. [para(5(a,2),5(a,1))]. given #66 (T,wt=7): 1996 (e + x) + e = x. [para(256(a,1),60(a,1,1))]. given #67 (T,wt=8): 49 f(e + e,e,e) = e. [para(4(a,2),1(a,1,1))]. given #68 (T,wt=8): 50 f(e,e + e,e) = e. [para(4(a,2),1(a,1,2))]. given #69 (A,wt=12): 40 f(e,f(x,y,f(x,y,e)),e) = e. [para(3(a,2),1(a,1,2))]. given #70 (T,wt=8): 51 f(e,e,e + e) = e. [para(4(a,2),1(a,1,3))]. given #71 (T,wt=8): 53 f(e,e,e) = e + e. [para(4(a,2),1(a,2))]. given #72 (T,wt=8): 54 x + f(e,e,e) = x. [para(1(a,2),4(a,1,2))]. given #73 (T,wt=8): 61 f(e,e,e) + x = x. [para(1(a,2),5(a,1,1))]. given #74 (A,wt=12): 41 f(e,e,f(x,y,f(x,y,e))) = e. [para(3(a,2),1(a,1,3))]. -------- Proof 1 -------- f(e,A,e). ============================== PROOF ================================= % Proof 1 at 0.11 (+ 0.01) seconds: f(e,A,e). % Length of proof is 21. % Level of proof is 10. % Maximum clause weight is 26. % Given clauses 74. 1 f(e,e,e) = e. [assumption]. 2 f(x,y,z) = f(x,z,y). [assumption]. 3 f(x,y,f(x,y,z)) = z. [assumption]. 4 x + e = x. [assumption]. 5 e + x = x. [assumption]. 29 x + (y + z) != u + (y + w) | x + (v5 + z) = u + (v5 + w) # label("gL"). [assumption]. 32 f(x,y + z,u) != f(w,v5 + z,v6) | f(x,y + v7,u) = f(w,v5 + v7,v6) # label("gL"). [assumption]. 36 A + x != e # answer(x). [assumption]. 41 f(e,e,f(x,y,f(x,y,e))) = e. [para(3(a,2),1(a,1,3))]. 86 e + (x + (y + z)) = y + (x + z). [hyper(29,a,5,a)]. 90 f(x,y + z,u + w) = f(x,u + z,y + w). [hyper(32,a,2,a)]. 207 x + (y + z) = y + (x + z). [para(86(a,1),5(a,1))]. 234 x + (y + e) = y + x. [para(4(a,1),207(a,1,2)),flip(a)]. 256 x + y = y + x. [para(4(a,1),234(a,1,2))]. 298 f(x,y + z,e + u) = f(x,z,y + u). [para(5(a,1),90(a,1,2)),flip(a)]. 380 f(x,y + z,e + u) = f(x,y,z + u). [para(256(a,1),298(a,1,2))]. 401 f(x,y + z,u) = f(x,y,z + u). [para(5(a,1),380(a,1,3))]. 458 f(x,e,y + z) = f(x,y,z). [para(5(a,1),401(a,1,2)),flip(a)]. 498 f(x,e,f(x,y,z)) = y + z. [para(458(a,1),3(a,1,3))]. 3788 x + f(e,x,e) = e. [para(41(a,1),498(a,1)),flip(a)]. 3789 $F # answer(f(e,A,e)). [resolve(3788,a,36,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=74. Generated=6038. Kept=3788. proofs=1. Usable=75. Sos=3653. Demods=0. Limbo=29, Disabled=66. Hints=187. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=2250. Back_subsumed=30. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=139. Nonunit_bsub_feature_tests=511. Megabytes=4.88. User_CPU=0.11, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 20021 exit (max_proofs) ------  Process 20021 exit (max_proofs) Fri Dec 7 16:29:09 2012