%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM128+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:59:47 AM UTC 2026
% Result : Theorem 127.49s 22.96s
% Output : CNFRefutation 127.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM128+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n014.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sat Sep 26 23:32:21 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.38 % Process 175490 was started by sandbox on n014,
% 0.11/5.38 % Sat Sep 26 23:32:21 2026
% 0.11/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/5.68
% 0.15/5.68 % From the command line: assign(max_seconds, 300).
% 127.49/22.96
% 127.49/22.96 % given #500 (I,wt=58): 1006 vreduce(A) != B | vvar(f42(A,B)) = A | vabs(f43(A,B),f44(A,B),f45(A,B)) = A | vsomeExp(vapp(vabs(f47(A,B),f48(A,B),f49(A,B)),vgetSomeExp(f50(A,B)))) = B | defn_20(A,B) | defn_30(A,B) | visSomeExp(f62(A,B)) | vreduce(f65(A,B)) = f66(A,B) # tptp_name(reduce-INV). [clausify(49)].
% 127.49/22.96
% 127.49/22.96 % given #1000 (I,wt=61): 1788 vsubst(A,B,C) != D | f12(A,B,C,D) = D | f15(A,B,C,D) != f14(A,B,C,D) | f18(A,B,C,D) = B | f20(A,B,C,D) = B | defn_10(A,B,C,D) | vabs(f28(A,B,C,D),f27(A,B,C,D),f30(A,B,C,D)) = C. [copy(1787),flip(b)].
% 127.49/22.96
% 127.49/22.96 % given #1500 (I,wt=102): 2752 vsubst(A,B,C) != D | f11(A,B,C,D) = f10(A,B,C,D) | vvar(f15(A,B,C,D)) = D | vapp(f16(A,B,C,D),f19(A,B,C,D)) = C | vabs(f22(A,B,C,D),f23(A,B,C,D),f24(A,B,C,D)) = D | defn_10(A,B,C,D) | vsubst(f25(A,B,C,D),f26(A,B,C,D),vabs(f29(A,B,C,D),f27(A,B,C,D),vsubst(f28(A,B,C,D),vvar(f29(A,B,C,D)),f30(A,B,C,D)))) = D. [resolve(180,f,69,a)].
% 127.49/22.96
% 127.49/22.96 % given #2000 (I,wt=58): 3252 vsubst(A,B,C) != D | f11(A,B,C,D) = f10(A,B,C,D) | f13(A,B,C,D) = B | f17(A,B,C,D) = A | f22(A,B,C,D) = f21(A,B,C,D) | defn_10(A,B,C,D) | f28(A,B,C,D) != f25(A,B,C,D). [resolve(251,f,72,a)].
% 127.49/22.96
% 127.49/22.96 % given #2500 (I,wt=65): 3752 vsubst(A,B,C) != D | vvar(f11(A,B,C,D)) = C | vvar(f15(A,B,C,D)) = C | vapp(f16(A,B,C,D),f19(A,B,C,D)) = C | vabs(f22(A,B,C,D),f23(A,B,C,D),f24(A,B,C,D)) = C | defn_10(A,B,C,D) | f25(A,B,C,D) = A. [resolve(322,f,75,a)].
% 127.49/22.96
% 127.49/22.96 % given #3000 (I,wt=51): 4252 vsubst(A,B,C) != D | f12(A,B,C,D) = B | vvar(f15(A,B,C,D)) = D | f17(A,B,C,D) = A | f21(A,B,C,D) = A | defn_10(A,B,C,D) | visFreeVar(f28(A,B,C,D),f26(A,B,C,D)). [resolve(394,f,71,a)].
% 127.49/22.96
% 127.49/22.96 % given #3500 (I,wt=57): 4752 vsubst(A,B,C) != D | f12(A,B,C,D) = B | f14(A,B,C,D) = A | f18(A,B,C,D) = B | vabs(f22(A,B,C,D),f23(A,B,C,D),f24(A,B,C,D)) = D | defn_10(A,B,C,D) | f26(A,B,C,D) = B. [resolve(465,f,74,a)].
% 127.49/22.96
% 127.49/22.96 % SZS status Theorem for theBenchmark
% 127.49/22.96
% 127.49/22.96 % Proof 1 at 16.63 (+ 0.55) seconds.
% 127.49/22.96 % Length of proof is 41.
% 127.49/22.96 % Level of proof is 11.
% 127.49/22.96 % Maximum clause weight is 41.000.
% 127.49/22.96 % Given clauses 3762.
% 127.49/22.96
% 127.49/22.96 % SZS output start CNFRefutation for theBenchmark
% 127.49/22.96 fof(isFreeVar0, axiom, ! [VVar0,VExp0,Vx,Vv] : ((VVar0 = Vv & VExp0 = vvar(Vx)) => ((Vx = Vv => visFreeVar(VVar0,VExp0)) & (visFreeVar(VVar0,VExp0) => Vx = Vv))), file('theBenchmark.p',isFreeVar0)).
% 127.49/22.96 fof(isFreeVar2, axiom, ! [VVar0,VExp0,Ve1,Vv,Ve2] : ((VVar0 = Vv & VExp0 = vapp(Ve1,Ve2)) => (((visFreeVar(Vv,Ve1) | visFreeVar(Vv,Ve2)) => visFreeVar(VVar0,VExp0)) & (visFreeVar(VVar0,VExp0) => (visFreeVar(Vv,Ve1) | visFreeVar(Vv,Ve2))))), file('theBenchmark.p',isFreeVar2)).
% 127.49/22.96 fof(DIFF-empty-bind, axiom, ! [VVar0,VTyp0,VCtx0] : ~ (vempty = vbind(VVar0,VTyp0,VCtx0)), file('theBenchmark.p',DIFF-empty-bind)).
% 127.49/22.96 fof(getSomeType0, axiom, ! [VOptTyp0,RESULT,Ve] : (VOptTyp0 = vsomeType(Ve) => (RESULT = vgetSomeType(VOptTyp0) => RESULT = Ve)), file('theBenchmark.p',getSomeType0)).
% 127.49/22.96 fof(lookup0, axiom, ! [Vx,VVar0,VCtx0,RESULT] : ((VVar0 = Vx & VCtx0 = vempty) => (RESULT = vlookup(VVar0,VCtx0) => RESULT = vnoType)), file('theBenchmark.p',lookup0)).
% 127.49/22.96 fof(lookup-INV, axiom, ! [VVar0,VCtx0,RESULT] : (vlookup(VVar0,VCtx0) = RESULT => (? [Vx] : (VVar0 = Vx & VCtx0 = vempty & RESULT = vnoType) | ? [VC,Vx,Vy,VTy] : (VVar0 = Vx & VCtx0 = vbind(Vy,VTy,VC) & Vx = Vy & RESULT = vsomeType(VTy)) | ? [VTy,Vy,Vx,VC] : (VVar0 = Vx & VCtx0 = vbind(Vy,VTy,VC) & ~ (Vx = Vy) & RESULT = vlookup(Vx,VC)))), file('theBenchmark.p',lookup-INV)).
% 127.49/22.96 fof(gensym-is-fresh, axiom, ! [Vv,Ve] : (vgensym(Ve) = Vv => ~ (visFreeVar(Vv,Ve))), file('theBenchmark.p',gensym-is-fresh)).
% 127.49/22.96 fof(subst0, axiom, ! [Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve] : ((VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy)) => (Vx = Vy => (RESULT = vsubst(VVar0,VExp0,VExp1) => RESULT = Ve))), file('theBenchmark.p',subst0)).
% 127.49/22.96 fof(getSomeExp0, axiom, ! [VOptExp0,RESULT,Ve] : (VOptExp0 = vsomeExp(Ve) => (RESULT = vgetSomeExp(VOptExp0) => RESULT = Ve)), file('theBenchmark.p',getSomeExp0)).
% 127.49/22.96 fof(fresh-unequal-var-3, conjecture, ! [Ve,Ve1,Vx,Vfresh] : (Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) => ~ (Vx = Vfresh)), file('theBenchmark.p',fresh-unequal-var-3)).
% 127.49/22.96 fof(fresh-unequal-var-3_neg, negated_conjecture, ~(! [Ve,Ve1,Vx,Vfresh] : (Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) => ~ (Vx = Vfresh))), inference(assume_negation, [status(cth)], [fresh-unequal-var-3])).
% 127.49/22.96 cnf(c_893, plain, vsomeExp(A) != B | vgetSomeExp(B) != C | C = A, inference(clausify, [status(thm)], [getSomeExp0])).
% 127.49/22.96 fof(nnf_65, plain, ? [Ve,Ve1,Vx,Vfresh] : (vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) = Vfresh & Vfresh = Vx), inference(fof_nnf, [status(thm)], [fresh-unequal-var-3_neg])).
% 127.49/22.96 fof(sk_fresh-unequal-var-3_neg, plain, (vgensym(vapp(vapp(sK0,sK1),vvar(sK2))) = sK3 & sK3 = sK2), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3]), skolemize(Ve,sK0), skolemize(Ve1,sK1), skolemize(Vx,sK2), skolemize(Vfresh,sK3)], [nnf_65])).
% 127.49/22.96 cnf(c_1081, negated_conjecture, vgensym(vapp(vapp(sK0,sK1),vvar(sK2))) = sK3, inference(split_conjunct, [status(thm)], [sk_fresh-unequal-var-3_neg])).
% 127.49/22.96 cnf(c_1082, negated_conjecture, sK3 = sK2, inference(split_conjunct, [status(thm)], [sk_fresh-unequal-var-3_neg])).
% 127.49/22.96 cnf(c_1193, plain, A != B | C != D | vvar(E) != F | E != A | vsubst(B,D,F) != V6 | V6 = C, inference(clausify, [status(thm)], [subst0])).
% 127.49/22.96 cnf(c_1194, plain, vgensym(A) != B | ~visFreeVar(B,A), inference(clausify, [status(thm)], [gensym-is-fresh])).
% 127.49/22.96 fof(nnf_25, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | ? [X0] : (X0 = VVar0 & VCtx0 = vempty & RESULT = vnoType) | ? [X1,X2,X3,X4] : (X2 = VVar0 & vbind(X3,X4,X1) = VCtx0 & X3 = X2 & vsomeType(X4) = RESULT) | ? [VTy,Vy,Vx,VC] : (Vx = VVar0 & vbind(Vy,VTy,VC) = VCtx0 & ~ (Vy = Vx) & vlookup(Vx,VC) = RESULT)), inference(fof_nnf, [status(thm)], [lookup-INV])).
% 127.49/22.96 fof(sk_lookup-INV_sk, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | (sK4(VVar0,VCtx0,RESULT) = VVar0 & VCtx0 = vempty & RESULT = vnoType) | (sK11(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK5(VVar0,VCtx0,RESULT),sK6(VVar0,VCtx0,RESULT),sK7(VVar0,VCtx0,RESULT)) = VCtx0 & sK5(VVar0,VCtx0,RESULT) = sK11(VVar0,VCtx0,RESULT) & vsomeType(sK6(VVar0,VCtx0,RESULT)) = RESULT) | (sK12(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK8(VVar0,VCtx0,RESULT),sK9(VVar0,VCtx0,RESULT),sK10(VVar0,VCtx0,RESULT)) = VCtx0 & ~ (sK8(VVar0,VCtx0,RESULT) = sK12(VVar0,VCtx0,RESULT)) & vlookup(sK12(VVar0,VCtx0,RESULT),sK10(VVar0,VCtx0,RESULT)) = RESULT)), inference(skolemize, [status(esa), new_symbols(skolem, [sK4,sK11,sK5,sK6,sK7,sK12,sK8,sK9,sK10]), skolemize(X0,sK4(VVar0,VCtx0,RESULT)), skolemize(X1,sK7(VVar0,VCtx0,RESULT)), skolemize(X2,sK11(VVar0,VCtx0,RESULT)), skolemize(X3,sK5(VVar0,VCtx0,RESULT)), skolemize(X4,sK6(VVar0,VCtx0,RESULT)), skolemize(VTy,sK9(VVar0,VCtx0,RESULT)), skolemize(Vy,sK8(VVar0,VCtx0,RESULT)), skolemize(Vx,sK12(VVar0,VCtx0,RESULT)), skolemize(VC,sK10(VVar0,VCtx0,RESULT))], [nnf_25])).
% 127.49/22.96 fof(sk_lookup-INV, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK4(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK11(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK5(VAR_0,VAR_1,VAR_2),sK6(VAR_0,VAR_1,VAR_2),sK7(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK5(VAR_0,VAR_1,VAR_2) = sK11(VAR_0,VAR_1,VAR_2) | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK12(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK8(VAR_0,VAR_1,VAR_2),sK9(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK8(VAR_0,VAR_1,VAR_2) = sK12(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK6(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK12(VAR_0,VAR_1,VAR_2),sK10(VAR_0,VAR_1,VAR_2)) = VAR_2)), inference(cnf_transformation, [status(thm)], [sk_lookup-INV_sk])).
% 127.49/22.96 cnf(c_1274, plain, vlookup(A,B) != C | sK4(A,B,C) = A | vbind(sK5(A,B,C),sK6(A,B,C),sK7(A,B,C)) = B | vbind(sK8(A,B,C),sK9(A,B,C),sK10(A,B,C)) = B, inference(split_conjunct, [status(thm)], [sk_lookup-INV])).
% 127.49/22.96 cnf(c_1283, plain, A != B | C != vempty | vlookup(B,C) != D | D = vnoType, inference(clausify, [status(thm)], [lookup0])).
% 127.49/22.96 cnf(c_8346, plain, A != B | vempty != C | vlookup(B,C) != D | D = vnoType,
% 127.49/22.96 inference(copy, [status(thm)], [c_1283])).
% 127.49/22.96 cnf(c_8347, plain, A != B | vempty != C | vlookup(B,C) != D | vnoType = D,
% 127.49/22.96 inference(copy, [status(thm)], [c_8346])).
% 127.49/22.96 cnf(c_1284, plain, vempty != A | vlookup(B,A) != C | vnoType = C,
% 127.49/22.96 inference(copy, [status(thm)], [c_8347])).
% 127.49/22.96 cnf(c_1285, plain, vsomeType(A) != B | vgetSomeType(B) != C | C = A, inference(clausify, [status(thm)], [getSomeType0])).
% 127.49/22.96 cnf(c_1287, plain, vbind(A,B,C) != vempty, inference(clausify, [status(thm)], [DIFF-empty-bind])).
% 127.49/22.96 cnf(c_1295, plain, A != B | vapp(C,D) != E | ~visFreeVar(A,D) | visFreeVar(B,E), inference(clausify, [status(thm)], [isFreeVar2])).
% 127.49/22.96 cnf(c_1301, plain, A != B | vvar(C) != D | A != C | visFreeVar(B,D), inference(clausify, [status(thm)], [isFreeVar0])).
% 127.49/22.96 cnf(c_4815, negated_conjecture, vgensym(vapp(vapp(sK0,sK1),vvar(sK2))) = sK2,
% 127.49/22.96 inference(paramod, [status(thm)], [c_1082, c_1081])).
% 127.49/22.96 cnf(c_5137, plain, vgetSomeExp(vsomeExp(A)) != B | B = A,
% 127.49/22.96 inference(xxres, [status(thm)], [c_893])).
% 127.49/22.96 cnf(c_5361, plain, A != B | C != D | E != A | vsubst(B,D,vvar(E)) != F | F = C,
% 127.49/22.96 inference(xxres, [status(thm)], [c_1193])).
% 127.49/22.96 cnf(c_5376, plain, A != B | C != A | vsubst(B,B,vvar(C)) != D | D = A,
% 127.49/22.96 inference(factor, [status(thm)], [c_5361])).
% 127.49/22.96 cnf(c_8348, plain, A != A | vsubst(A,A,vvar(A)) != B | B = A,
% 127.49/22.96 inference(factor, [status(thm)], [c_5376])).
% 127.49/22.96 cnf(c_5388, plain, vsubst(A,A,vvar(A)) != B | B = A,
% 127.49/22.96 inference(copy, [status(thm)], [c_8348])).
% 127.49/22.96 cnf(c_8349, plain, vempty != A | vnoType = vlookup(B,A),
% 127.49/22.96 inference(xxres, [status(thm)], [c_1284])).
% 127.49/22.96 cnf(c_5449, plain, vempty != A | vlookup(B,A) = vnoType,
% 127.49/22.96 inference(copy, [status(thm)], [c_8349])).
% 127.49/22.96 cnf(c_5450, plain, vgetSomeType(vsomeType(A)) != B | B = A,
% 127.49/22.96 inference(xxres, [status(thm)], [c_1285])).
% 127.49/22.96 cnf(c_5466, plain, A != B | A != C | visFreeVar(B,vvar(C)),
% 127.49/22.96 inference(xxres, [status(thm)], [c_1301])).
% 127.49/22.96 cnf(c_8350, plain, A != B | visFreeVar(B,vvar(B)),
% 127.49/22.96 inference(factor, [status(thm)], [c_5466])).
% 127.49/22.96 cnf(c_5470, plain, visFreeVar(A,vvar(A)),
% 127.49/22.96 inference(copy, [status(thm)], [c_8350])).
% 127.49/22.96 cnf(c_6568, plain, A != B | vapp(C,vvar(A)) != D | visFreeVar(B,D),
% 127.49/22.96 inference(resolve, [status(thm)], [c_5470, c_1295])).
% 127.49/22.96 cnf(c_6572, plain, vgetSomeExp(vsomeExp(A)) = A,
% 127.49/22.96 inference(xxres, [status(thm)], [c_5137])).
% 127.49/22.96 cnf(c_8351, plain, A = vgetSomeExp(vsomeExp(A)),
% 127.49/22.96 inference(copy, [status(thm)], [c_6572])).
% 127.49/22.96 cnf(c_8352, plain, vlookup(A,vgetSomeExp(vsomeExp(vempty))) = vnoType,
% 127.49/22.96 inference(resolve, [status(thm)], [c_5449, c_8351])).
% 127.49/22.96 cnf(c_6611, plain, vlookup(A,vempty) = vnoType,
% 127.49/22.96 inference(paramod, [status(thm)], [c_6572, c_8352])).
% 127.49/22.96 cnf(c_8353, plain, sK4(A,vempty,vnoType) = A | vbind(sK5(A,vempty,vnoType),sK6(A,vempty,vnoType),sK7(A,vempty,vnoType)) = vempty | vbind(sK8(A,vempty,vnoType),sK9(A,vempty,vnoType),sK10(A,vempty,vnoType)) = vempty,
% 127.49/22.96 inference(resolve, [status(thm)], [c_6611, c_1274])).
% 127.49/22.96 cnf(c_8354, plain, sK4(A,vempty,vnoType) = A | vbind(sK8(A,vempty,vnoType),sK9(A,vempty,vnoType),sK10(A,vempty,vnoType)) = vempty,
% 127.49/22.96 inference(resolve, [status(thm)], [c_1287, c_8353])).
% 127.49/22.96 cnf(c_6628, plain, sK4(A,vempty,vnoType) = A,
% 127.49/22.96 inference(resolve, [status(thm)], [c_1287, c_8354])).
% 127.49/22.96 cnf(c_8355, plain, A = sK4(A,vempty,vnoType),
% 127.49/22.96 inference(copy, [status(thm)], [c_6628])).
% 127.49/22.96 cnf(c_8356, plain, sK4(vgetSomeType(vsomeType(A)),vempty,vnoType) = A,
% 127.49/22.96 inference(resolve, [status(thm)], [c_5450, c_8355])).
% 127.49/22.96 cnf(c_6644, plain, vgetSomeType(vsomeType(A)) = A,
% 127.49/22.96 inference(paramod, [status(thm)], [c_6628, c_8356])).
% 127.49/22.96 cnf(c_8357, plain, A = vgetSomeType(vsomeType(A)),
% 127.49/22.96 inference(copy, [status(thm)], [c_6644])).
% 127.49/22.96 cnf(c_8358, plain, vgetSomeType(vsomeType(vsubst(A,A,vvar(A)))) = A,
% 127.49/22.96 inference(resolve, [status(thm)], [c_5388, c_8357])).
% 127.49/22.96 cnf(c_6659, plain, vsubst(A,A,vvar(A)) = A,
% 127.49/22.96 inference(paramod, [status(thm)], [c_6644, c_8358])).
% 127.49/22.96 cnf(c_8359, plain, vapp(A,vvar(vsubst(B,B,vvar(B)))) != C | visFreeVar(B,C),
% 127.49/22.96 inference(resolve, [status(thm)], [c_6568, c_6659])).
% 127.49/22.96 cnf(c_8332, plain, vapp(A,vvar(B)) != C | visFreeVar(B,C),
% 127.49/22.96 inference(paramod, [status(thm)], [c_6659, c_8359])).
% 127.49/22.96 cnf(c_8360, plain, A = vsubst(A,A,vvar(A)),
% 127.49/22.96 inference(copy, [status(thm)], [c_6659])).
% 127.49/22.96 cnf(c_8361, plain, visFreeVar(A,vsubst(vapp(B,vvar(A)),vapp(B,vvar(A)),vvar(vapp(B,vvar(A))))),
% 127.49/22.96 inference(resolve, [status(thm)], [c_8332, c_8360])).
% 127.49/22.96 cnf(c_8334, plain, visFreeVar(A,vapp(B,vvar(A))),
% 127.49/22.96 inference(paramod, [status(thm)], [c_6659, c_8361])).
% 127.49/22.96 cnf(c_8344, plain, vgensym(vapp(A,vvar(B))) != B,
% 127.49/22.96 inference(resolve, [status(thm)], [c_8334, c_1194])).
% 127.49/22.96 cnf(c_8345, plain, $false,
% 127.49/22.96 inference(resolve, [status(thm)], [c_8344, c_4815])).
% 127.49/22.96 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------