%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM130+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:48 AM UTC 2026
% Result : Theorem 143.04s 29.96s
% Output : CNFRefutation 143.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM130+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.39 % Computer : n016.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Sat Sep 26 23:37:43 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.40 % Process 2011145 was started by sandbox2 on n016,
% 0.10/10.40 % Sat Sep 26 23:37:43 2026
% 0.10/10.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/10.70
% 0.14/10.70 % From the command line: assign(max_seconds, 300).
% 143.04/29.96
% 143.04/29.96 % given #500 (I,wt=58): 1001 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)) | f65(A,B) != vabs(C,D,E). [copy(1000),flip(h)].
% 143.04/29.96
% 143.04/29.96 % given #1000 (I,wt=84): 1787 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 | f21(A,B,C,D) = A | 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. [copy(1786),flip(b)].
% 143.04/29.96
% 143.04/29.96 % given #1500 (I,wt=72): 2748 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) | f28(A,B,C,D) != f25(A,B,C,D). [resolve(174,f,66,a)].
% 143.04/29.96
% 143.04/29.96 % given #2000 (I,wt=54): 3248 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) | f25(A,B,C,D) = A. [resolve(245,f,69,a)].
% 143.04/29.96
% 143.04/29.96 % given #2500 (I,wt=58): 3748 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 | f20(A,B,C,D) = B | defn_10(A,B,C,D) | visFreeVar(f28(A,B,C,D),f26(A,B,C,D)). [resolve(317,f,65,a)].
% 143.04/29.96
% 143.04/29.96 % given #3000 (I,wt=47): 4248 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) | f26(A,B,C,D) = B. [resolve(388,f,68,a)].
% 143.04/29.96
% 143.04/29.96 % given #3500 (I,wt=68): 4748 vsubst(A,B,C) != D | f12(A,B,C,D) = B | f14(A,B,C,D) = A | f18(A,B,C,D) = B | f22(A,B,C,D) = f21(A,B,C,D) | defn_10(A,B,C,D) | vgensym(vapp(vapp(f26(A,B,C,D),f30(A,B,C,D)),vvar(f25(A,B,C,D)))) = f29(A,B,C,D). [resolve(460,f,64,a)].
% 143.04/29.96
% 143.04/29.96 % SZS status Theorem for theBenchmark
% 143.04/29.96
% 143.04/29.96 % Proof 1 at 17.98 (+ 0.78) seconds.
% 143.04/29.96 % Length of proof is 72.
% 143.04/29.96 % Level of proof is 17.
% 143.04/29.96 % Maximum clause weight is 41.000.
% 143.04/29.96 % Given clauses 3843.
% 143.04/29.96
% 143.04/29.96 % SZS output start CNFRefutation for theBenchmark
% 143.04/29.96 fof(DIFF-var-abs, axiom, ! [VVar0,VVar1,VTyp0,VExp0] : ~ (vvar(VVar0) = vabs(VVar1,VTyp0,VExp0)), file('theBenchmark.p',DIFF-var-abs)).
% 143.04/29.96 fof(DIFF-var-app, axiom, ! [VVar0,VExp0,VExp1] : ~ (vvar(VVar0) = vapp(VExp0,VExp1)), file('theBenchmark.p',DIFF-var-app)).
% 143.04/29.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)).
% 143.04/29.96 fof(isFreeVar1, axiom, ! [VT,VVar0,VExp0,Vx,Vv,Ve] : ((VVar0 = Vv & VExp0 = vabs(Vx,VT,Ve)) => (((~ (Vx = Vv) & visFreeVar(Vv,Ve)) => visFreeVar(VVar0,VExp0)) & (visFreeVar(VVar0,VExp0) => (~ (Vx = Vv) & visFreeVar(Vv,Ve))))), file('theBenchmark.p',isFreeVar1)).
% 143.04/29.96 fof(DIFF-empty-bind, axiom, ! [VVar0,VTyp0,VCtx0] : ~ (vempty = vbind(VVar0,VTyp0,VCtx0)), file('theBenchmark.p',DIFF-empty-bind)).
% 143.04/29.96 fof(getSomeType0, axiom, ! [VOptTyp0,RESULT,Ve] : (VOptTyp0 = vsomeType(Ve) => (RESULT = vgetSomeType(VOptTyp0) => RESULT = Ve)), file('theBenchmark.p',getSomeType0)).
% 143.04/29.96 fof(lookup0, axiom, ! [Vx,VVar0,VCtx0,RESULT] : ((VVar0 = Vx & VCtx0 = vempty) => (RESULT = vlookup(VVar0,VCtx0) => RESULT = vnoType)), file('theBenchmark.p',lookup0)).
% 143.04/29.96 fof(lookup1, axiom, ! [VC,Vx,Vy,VVar0,VCtx0,RESULT,VTy] : ((VVar0 = Vx & VCtx0 = vbind(Vy,VTy,VC)) => (Vx = Vy => (RESULT = vlookup(VVar0,VCtx0) => RESULT = vsomeType(VTy)))), file('theBenchmark.p',lookup1)).
% 143.04/29.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)).
% 143.04/29.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)).
% 143.04/29.96 fof(subst3, axiom, ! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1] : ((VVar0 = Vx & VExp0 = Ve & VExp1 = vabs(Vy,VT,Ve1)) => (Vx = Vy => (RESULT = vsubst(VVar0,VExp0,VExp1) => RESULT = vabs(Vy,VT,Ve1)))), file('theBenchmark.p',subst3)).
% 143.04/29.96 fof(getSomeExp0, axiom, ! [VOptExp0,RESULT,Ve] : (VOptExp0 = vsomeExp(Ve) => (RESULT = vgetSomeExp(VOptExp0) => RESULT = Ve)), file('theBenchmark.p',getSomeExp0)).
% 143.04/29.96 fof(T-var, axiom, ! [VC,Vx,VT] : (vlookup(Vx,VC) = vsomeType(VT) => vtcheck(VC,vvar(Vx),VT)), file('theBenchmark.p',T-var)).
% 143.04/29.96 fof(T-inv, axiom, ! [Ve,VT,VC] : (vtcheck(VC,Ve,VT) => (? [Vx] : (Ve = vvar(Vx) & vlookup(Vx,VC) = vsomeType(VT)) | ? [Vx,Ve2,VT1,VT2] : (Ve = vabs(Vx,VT1,Ve2) & VT = varrow(VT1,VT2) & vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)) | ? [Ve1,Ve2,VS] : (Ve = vapp(Ve1,Ve2) & vtcheck(VC,Ve1,varrow(VS,VT)) & vtcheck(VC,Ve2,VS)))), file('theBenchmark.p',T-inv)).
% 143.04/29.96 fof(T-Strong, axiom, ! [Vx,VS,VC,Ve,VT] : ((~ (visFreeVar(Vx,Ve)) & vtcheck(vbind(Vx,VS,VC),Ve,VT)) => vtcheck(VC,Ve,VT)), file('theBenchmark.p',T-Strong)).
% 143.04/29.96 fof(T-subst-abs-1, conjecture, ! [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] : ((Vx = Vy & vtcheck(VC,Ve,VT) & vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)) => vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2)), file('theBenchmark.p',T-subst-abs-1)).
% 143.04/29.96 fof(T-subst-abs-1_neg, negated_conjecture, ~(! [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] : ((Vx = Vy & vtcheck(VC,Ve,VT) & vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)) => vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2))), inference(assume_negation, [status(cth)], [T-subst-abs-1])).
% 143.04/29.96 cnf(c_889, plain, vsomeExp(A) != B | vgetSomeExp(B) != C | C = A, inference(clausify, [status(thm)], [getSomeExp0])).
% 143.04/29.96 cnf(c_1046, plain, vlookup(A,B) != vsomeType(C) | vtcheck(B,vvar(A),C), inference(clausify, [status(thm)], [T-var])).
% 143.04/29.96 fof(nnf_54, plain, ! [Ve,VT,VC] : (~ (vtcheck(VC,Ve,VT)) | ? [X0] : (vvar(X0) = Ve & vlookup(X0,VC) = vsomeType(VT)) | ? [Vx,X1,VT1,VT2] : (vabs(Vx,VT1,X1) = Ve & varrow(VT1,VT2) = VT & vtcheck(vbind(Vx,VT1,VC),X1,VT2)) | ? [Ve1,Ve2,VS] : (vapp(Ve1,Ve2) = Ve & vtcheck(VC,Ve1,varrow(VS,VT)) & vtcheck(VC,Ve2,VS))), inference(fof_nnf, [status(thm)], [T-inv])).
% 143.04/29.96 fof(sk_T-inv_sk, plain, ! [Ve,VT,VC] : (~ (vtcheck(VC,Ve,VT)) | (vvar(sK0(Ve,VT,VC)) = Ve & vlookup(sK0(Ve,VT,VC),VC) = vsomeType(VT)) | (vabs(sK1(Ve,VT,VC),sK2(Ve,VT,VC),sK3(Ve,VT,VC)) = Ve & varrow(sK2(Ve,VT,VC),sK21(Ve,VT,VC)) = VT & vtcheck(vbind(sK1(Ve,VT,VC),sK2(Ve,VT,VC),VC),sK3(Ve,VT,VC),sK21(Ve,VT,VC))) | (vapp(sK4(Ve,VT,VC),sK5(Ve,VT,VC)) = Ve & vtcheck(VC,sK4(Ve,VT,VC),varrow(sK22(Ve,VT,VC),VT)) & vtcheck(VC,sK5(Ve,VT,VC),sK22(Ve,VT,VC)))), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3,sK21,sK4,sK5,sK22]), skolemize(X0,sK0(Ve,VT,VC)), skolemize(Vx,sK1(Ve,VT,VC)), skolemize(X1,sK3(Ve,VT,VC)), skolemize(VT1,sK2(Ve,VT,VC)), skolemize(VT2,sK21(Ve,VT,VC)), skolemize(Ve1,sK4(Ve,VT,VC)), skolemize(Ve2,sK5(Ve,VT,VC)), skolemize(VS,sK22(Ve,VT,VC))], [nnf_54])).
% 143.04/29.96 fof(sk_T-inv, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK22(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK2(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) = VAR_2 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK2(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK22(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK2(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK22(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK0(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK22(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),sK3(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK2(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) = VAR_2 | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK2(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK22(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK2(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) | vapp(sK4(VAR_1,VAR_2,VAR_0),sK5(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK22(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK0(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK1(VAR_1,VAR_2,VAR_0),sK2(VAR_1,VAR_2,VAR_0),VAR_0),sK3(VAR_1,VAR_2,VAR_0),sK21(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0)))), inference(cnf_transformation, [status(thm)], [sk_T-inv_sk])).
% 143.04/29.96 cnf(c_1049, plain, ~vtcheck(A,B,C) | vvar(sK0(B,C,A)) = B | vabs(sK1(B,C,A),sK2(B,C,A),sK3(B,C,A)) = B | vapp(sK4(B,C,A),sK5(B,C,A)) = B, inference(split_conjunct, [status(thm)], [sk_T-inv])).
% 143.04/29.96 cnf(c_1068, plain, visFreeVar(A,B) | ~vtcheck(vbind(A,C,D),B,E) | vtcheck(D,B,E), inference(clausify, [status(thm)], [T-Strong])).
% 143.04/29.96 fof(nnf_59, plain, ? [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] : (Vy = Vx & vtcheck(VC,Ve,VT) & vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2) & ~ (vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2))), inference(fof_nnf, [status(thm)], [T-subst-abs-1_neg])).
% 143.04/29.96 fof(sk_T-subst-abs-1_neg, plain, (sK6 = sK7 & vtcheck(sK9,sK13,sK8) & vtcheck(vbind(sK7,sK8,sK9),vabs(sK6,sK10,sK11),sK12) & ~ (vtcheck(sK9,vsubst(sK7,sK13,vabs(sK6,sK10,sK11)),sK12))), inference(skolemize, [status(esa), new_symbols(skolem, [sK6,sK7,sK9,sK13,sK8,sK10,sK11,sK12]), skolemize(VT,sK8), skolemize(VC,sK9), skolemize(Vx,sK7), skolemize(Ve,sK13), skolemize(Vy,sK6), skolemize(VS,sK10), skolemize(Ve1,sK11), skolemize(VT2,sK12)], [nnf_59])).
% 143.04/29.96 cnf(c_1071, negated_conjecture, sK6 = sK7, inference(split_conjunct, [status(thm)], [sk_T-subst-abs-1_neg])).
% 143.04/29.96 cnf(c_1073, negated_conjecture, vtcheck(vbind(sK7,sK8,sK9),vabs(sK6,sK10,sK11),sK12), inference(split_conjunct, [status(thm)], [sk_T-subst-abs-1_neg])).
% 143.04/29.96 cnf(c_1074, negated_conjecture, vtcheck(vbind(sK7,sK8,sK9),vabs(sK7,sK10,sK11),sK12),
% 143.04/29.96 inference(paramod, [status(thm)], [c_1071, c_1073])).
% 143.04/29.96 cnf(c_1075, negated_conjecture, ~vtcheck(sK9,vsubst(sK7,sK13,vabs(sK6,sK10,sK11)),sK12), inference(split_conjunct, [status(thm)], [sk_T-subst-abs-1_neg])).
% 143.04/29.96 cnf(c_1076, negated_conjecture, ~vtcheck(sK9,vsubst(sK7,sK13,vabs(sK7,sK10,sK11)),sK12),
% 143.04/29.96 inference(paramod, [status(thm)], [c_1071, c_1075])).
% 143.04/29.96 cnf(c_1181, plain, A != B | C != D | vabs(E,F,V6) != V7 | E != A | vsubst(B,D,V7) != V8 | vabs(E,F,V6) = V8, inference(clausify, [status(thm)], [subst3])).
% 143.04/29.96 cnf(c_1182, plain, A != B | vabs(C,D,E) != F | C != A | vsubst(B,V6,F) != V7 | vabs(C,D,E) = V7,
% 143.04/29.96 inference(copy, [status(thm)], [c_1181])).
% 143.04/29.96 cnf(c_1186, plain, A != B | C != D | vvar(E) != F | E != A | vsubst(B,D,F) != V6 | V6 = C, inference(clausify, [status(thm)], [subst0])).
% 143.04/29.96 fof(nnf_25, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | ? [X2] : (X2 = VVar0 & VCtx0 = vempty & RESULT = vnoType) | ? [X1,X0,X3,X4] : (X0 = VVar0 & vbind(X3,X4,X1) = VCtx0 & X3 = X0 & 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])).
% 143.04/29.96 fof(sk_lookup-INV_sk, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | (sK14(VVar0,VCtx0,RESULT) = VVar0 & VCtx0 = vempty & RESULT = vnoType) | (sK23(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK15(VVar0,VCtx0,RESULT),sK16(VVar0,VCtx0,RESULT),sK17(VVar0,VCtx0,RESULT)) = VCtx0 & sK15(VVar0,VCtx0,RESULT) = sK23(VVar0,VCtx0,RESULT) & vsomeType(sK16(VVar0,VCtx0,RESULT)) = RESULT) | (sK24(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK18(VVar0,VCtx0,RESULT),sK19(VVar0,VCtx0,RESULT),sK20(VVar0,VCtx0,RESULT)) = VCtx0 & ~ (sK18(VVar0,VCtx0,RESULT) = sK24(VVar0,VCtx0,RESULT)) & vlookup(sK24(VVar0,VCtx0,RESULT),sK20(VVar0,VCtx0,RESULT)) = RESULT)), inference(skolemize, [status(esa), new_symbols(skolem, [sK14,sK23,sK15,sK16,sK17,sK24,sK18,sK19,sK20]), skolemize(X2,sK14(VVar0,VCtx0,RESULT)), skolemize(X1,sK17(VVar0,VCtx0,RESULT)), skolemize(X0,sK23(VVar0,VCtx0,RESULT)), skolemize(X3,sK15(VVar0,VCtx0,RESULT)), skolemize(X4,sK16(VVar0,VCtx0,RESULT)), skolemize(VTy,sK19(VVar0,VCtx0,RESULT)), skolemize(Vy,sK18(VVar0,VCtx0,RESULT)), skolemize(Vx,sK24(VVar0,VCtx0,RESULT)), skolemize(VC,sK20(VVar0,VCtx0,RESULT))], [nnf_25])).
% 143.04/29.96 fof(sk_lookup-INV, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK14(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(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(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK24(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(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(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(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(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(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK24(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(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(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(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK23(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(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(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK24(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(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(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(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2),sK17(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | sK24(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK15(VAR_0,VAR_1,VAR_2) = sK23(VAR_0,VAR_1,VAR_2) | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(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(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK24(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(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK18(VAR_0,VAR_1,VAR_2),sK19(VAR_0,VAR_1,VAR_2),sK20(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(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK18(VAR_0,VAR_1,VAR_2) = sK24(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK16(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK24(VAR_0,VAR_1,VAR_2),sK20(VAR_0,VAR_1,VAR_2)) = VAR_2)), inference(cnf_transformation, [status(thm)], [sk_lookup-INV_sk])).
% 143.04/29.96 cnf(c_1267, plain, vlookup(A,B) != C | sK14(A,B,C) = A | vbind(sK15(A,B,C),sK16(A,B,C),sK17(A,B,C)) = B | vbind(sK18(A,B,C),sK19(A,B,C),sK20(A,B,C)) = B, inference(split_conjunct, [status(thm)], [sk_lookup-INV])).
% 143.04/29.96 cnf(c_1275, plain, A != B | vbind(C,D,E) != F | C != A | vlookup(B,F) != V6 | vsomeType(D) = V6, inference(clausify, [status(thm)], [lookup1])).
% 143.04/29.96 cnf(c_1276, plain, A != B | C != vempty | vlookup(B,C) != D | D = vnoType, inference(clausify, [status(thm)], [lookup0])).
% 143.04/29.96 cnf(c_10369, plain, A != B | vempty != C | vlookup(B,C) != D | D = vnoType,
% 143.04/29.96 inference(copy, [status(thm)], [c_1276])).
% 143.04/29.96 cnf(c_10370, plain, A != B | vempty != C | vlookup(B,C) != D | vnoType = D,
% 143.04/29.96 inference(copy, [status(thm)], [c_10369])).
% 143.04/29.96 cnf(c_1277, plain, vempty != A | vlookup(B,A) != C | vnoType = C,
% 143.04/29.96 inference(copy, [status(thm)], [c_10370])).
% 143.04/29.96 cnf(c_1278, plain, vsomeType(A) != B | vgetSomeType(B) != C | C = A, inference(clausify, [status(thm)], [getSomeType0])).
% 143.04/29.96 cnf(c_1280, plain, vbind(A,B,C) != vempty, inference(clausify, [status(thm)], [DIFF-empty-bind])).
% 143.04/29.96 cnf(c_1291, plain, A != B | vabs(C,D,E) != F | ~visFreeVar(B,F) | A != C, inference(clausify, [status(thm)], [isFreeVar1])).
% 143.04/29.96 cnf(c_1293, plain, A != B | vvar(C) != D | ~visFreeVar(B,D) | A = C, inference(clausify, [status(thm)], [isFreeVar0])).
% 143.04/29.96 cnf(c_1294, plain, A != B | vvar(C) != D | A != C | visFreeVar(B,D), inference(clausify, [status(thm)], [isFreeVar0])).
% 143.04/29.96 cnf(c_1299, plain, vapp(A,B) != vvar(C), inference(clausify, [status(thm)], [DIFF-var-app])).
% 143.04/29.96 cnf(c_1300, plain, vabs(A,B,C) != vvar(D), inference(clausify, [status(thm)], [DIFF-var-abs])).
% 143.04/29.96 cnf(c_10371, plain, A != B | vabs(B,C,D) != E | ~visFreeVar(B,E),
% 143.04/29.96 inference(factor, [status(thm)], [c_1291])).
% 143.04/29.96 cnf(c_4859, plain, vabs(A,B,C) != D | ~visFreeVar(A,D),
% 143.04/29.96 inference(copy, [status(thm)], [c_10371])).
% 143.04/29.96 cnf(c_5137, plain, vgetSomeExp(vsomeExp(A)) != B | B = A,
% 143.04/29.96 inference(xxres, [status(thm)], [c_889])).
% 143.04/29.96 cnf(c_5255, plain, visFreeVar(sK7,vabs(sK7,sK10,sK11)) | vtcheck(sK9,vabs(sK7,sK10,sK11),sK12),
% 143.04/29.96 inference(resolve, [status(thm)], [c_1074, c_1068])).
% 143.04/29.96 cnf(c_5361, plain, A != B | C != A | vsubst(B,D,vabs(C,E,F)) != V6 | vabs(C,E,F) = V6,
% 143.04/29.96 inference(xxres, [status(thm)], [c_1182])).
% 143.04/29.96 cnf(c_10372, plain, A != A | vsubst(A,B,vabs(A,C,D)) != E | vabs(A,C,D) = E,
% 143.04/29.96 inference(factor, [status(thm)], [c_5361])).
% 143.04/29.96 cnf(c_5364, plain, vsubst(A,B,vabs(A,C,D)) != E | vabs(A,C,D) = E,
% 143.04/29.96 inference(copy, [status(thm)], [c_10372])).
% 143.04/29.96 cnf(c_5401, plain, A != B | vvar(C) != D | C != A | vsubst(B,E,D) != F | F = E,
% 143.04/29.96 inference(xxres, [status(thm)], [c_1186])).
% 143.04/29.96 cnf(c_5402, plain, A != B | C != D | E != A | vsubst(B,D,vvar(E)) != F | F = C,
% 143.04/29.96 inference(xxres, [status(thm)], [c_1186])).
% 143.04/29.96 cnf(c_10373, plain, A != A | vvar(A) != B | vsubst(A,C,B) != D | D = C,
% 143.04/29.96 inference(factor, [status(thm)], [c_5401])).
% 143.04/29.96 cnf(c_5414, plain, vvar(A) != B | vsubst(A,C,B) != D | D = C,
% 143.04/29.96 inference(copy, [status(thm)], [c_10373])).
% 143.04/29.96 cnf(c_5417, plain, A != B | C != A | vsubst(B,B,vvar(C)) != D | D = A,
% 143.04/29.96 inference(factor, [status(thm)], [c_5402])).
% 143.04/29.96 cnf(c_10374, plain, A != A | vsubst(A,A,vvar(A)) != B | B = A,
% 143.04/29.96 inference(factor, [status(thm)], [c_5417])).
% 143.04/29.96 cnf(c_5429, plain, vsubst(A,A,vvar(A)) != B | B = A,
% 143.04/29.96 inference(copy, [status(thm)], [c_10374])).
% 143.04/29.96 cnf(c_5483, plain, A != B | C != A | vlookup(B,vbind(C,D,E)) != F | vsomeType(D) = F,
% 143.04/29.96 inference(xxres, [status(thm)], [c_1275])).
% 143.04/29.96 cnf(c_10375, plain, A != A | vlookup(A,vbind(A,B,C)) != D | vsomeType(B) = D,
% 143.04/29.96 inference(factor, [status(thm)], [c_5483])).
% 143.04/29.96 cnf(c_5486, plain, vlookup(A,vbind(A,B,C)) != D | vsomeType(B) = D,
% 143.04/29.96 inference(copy, [status(thm)], [c_10375])).
% 143.04/29.96 cnf(c_10376, plain, vempty != A | vnoType = vlookup(B,A),
% 143.04/29.96 inference(xxres, [status(thm)], [c_1277])).
% 143.04/29.96 cnf(c_5490, plain, vempty != A | vlookup(B,A) = vnoType,
% 143.04/29.96 inference(copy, [status(thm)], [c_10376])).
% 143.04/29.96 cnf(c_5491, plain, vgetSomeType(vsomeType(A)) != B | B = A,
% 143.04/29.96 inference(xxres, [status(thm)], [c_1278])).
% 143.04/29.96 cnf(c_5507, plain, A != B | A != C | visFreeVar(B,vvar(C)),
% 143.04/29.96 inference(xxres, [status(thm)], [c_1294])).
% 143.04/29.96 cnf(c_10377, plain, A != B | visFreeVar(B,vvar(B)),
% 143.04/29.96 inference(factor, [status(thm)], [c_5507])).
% 143.04/29.96 cnf(c_5511, plain, visFreeVar(A,vvar(A)),
% 143.04/29.96 inference(copy, [status(thm)], [c_10377])).
% 143.04/29.96 cnf(c_6611, plain, A != B | vvar(C) != vvar(B) | A = C,
% 143.04/29.96 inference(resolve, [status(thm)], [c_5511, c_1293])).
% 143.04/29.96 cnf(c_6618, plain, vgetSomeExp(vsomeExp(A)) = A,
% 143.04/29.96 inference(xxres, [status(thm)], [c_5137])).
% 143.04/29.96 cnf(c_10378, plain, A = vgetSomeExp(vsomeExp(A)),
% 143.04/29.96 inference(copy, [status(thm)], [c_6618])).
% 143.04/29.96 cnf(c_10379, plain, vlookup(A,vgetSomeExp(vsomeExp(vempty))) = vnoType,
% 143.04/29.96 inference(resolve, [status(thm)], [c_5490, c_10378])).
% 143.04/29.96 cnf(c_6657, plain, vlookup(A,vempty) = vnoType,
% 143.04/29.96 inference(paramod, [status(thm)], [c_6618, c_10379])).
% 143.04/29.96 cnf(c_10380, plain, sK14(A,vempty,vnoType) = A | vbind(sK15(A,vempty,vnoType),sK16(A,vempty,vnoType),sK17(A,vempty,vnoType)) = vempty | vbind(sK18(A,vempty,vnoType),sK19(A,vempty,vnoType),sK20(A,vempty,vnoType)) = vempty,
% 143.04/29.96 inference(resolve, [status(thm)], [c_6657, c_1267])).
% 143.04/29.96 cnf(c_10381, plain, sK14(A,vempty,vnoType) = A | vbind(sK18(A,vempty,vnoType),sK19(A,vempty,vnoType),sK20(A,vempty,vnoType)) = vempty,
% 143.04/29.96 inference(resolve, [status(thm)], [c_1280, c_10380])).
% 143.04/29.96 cnf(c_6674, plain, sK14(A,vempty,vnoType) = A,
% 143.04/29.96 inference(resolve, [status(thm)], [c_1280, c_10381])).
% 143.04/29.96 cnf(c_10382, plain, A = sK14(A,vempty,vnoType),
% 143.04/29.96 inference(copy, [status(thm)], [c_6674])).
% 143.04/29.96 cnf(c_10383, plain, sK14(vgetSomeType(vsomeType(A)),vempty,vnoType) = A,
% 143.04/29.96 inference(resolve, [status(thm)], [c_5491, c_10382])).
% 143.04/29.96 cnf(c_6690, plain, vgetSomeType(vsomeType(A)) = A,
% 143.04/29.96 inference(paramod, [status(thm)], [c_6674, c_10383])).
% 143.04/29.96 cnf(c_10384, plain, A = vgetSomeType(vsomeType(A)),
% 143.04/29.96 inference(copy, [status(thm)], [c_6690])).
% 143.04/29.96 cnf(c_10385, plain, vgetSomeType(vsomeType(vsubst(A,A,vvar(A)))) = A,
% 143.04/29.96 inference(resolve, [status(thm)], [c_5429, c_10384])).
% 143.04/29.96 cnf(c_6729, plain, vsubst(A,A,vvar(A)) = A,
% 143.04/29.96 inference(paramod, [status(thm)], [c_6690, c_10385])).
% 143.04/29.96 cnf(c_10386, plain, vvar(A) != vvar(B) | vsubst(B,B,vvar(B)) = A,
% 143.04/29.96 inference(resolve, [status(thm)], [c_6611, c_6729])).
% 143.04/29.96 cnf(c_8242, plain, vvar(A) != vvar(B) | B = A,
% 143.04/29.96 inference(paramod, [status(thm)], [c_6729, c_10386])).
% 143.04/29.96 cnf(c_10387, plain, A = vsubst(A,A,vvar(A)),
% 143.04/29.96 inference(copy, [status(thm)], [c_6729])).
% 143.04/29.96 cnf(c_10388, plain, vsomeType(A) = vsubst(vlookup(B,vbind(B,A,C)),vlookup(B,vbind(B,A,C)),vvar(vlookup(B,vbind(B,A,C)))),
% 143.04/29.96 inference(resolve, [status(thm)], [c_5486, c_10387])).
% 143.04/29.96 cnf(c_10389, plain, vsomeType(A) = vlookup(B,vbind(B,A,C)),
% 143.04/29.96 inference(paramod, [status(thm)], [c_6729, c_10388])).
% 143.04/29.96 cnf(c_8270, plain, vlookup(A,vbind(A,B,C)) = vsomeType(B),
% 143.04/29.96 inference(copy, [status(thm)], [c_10389])).
% 143.04/29.96 cnf(c_8320, plain, vtcheck(vbind(A,B,C),vvar(A),B),
% 143.04/29.96 inference(resolve, [status(thm)], [c_8270, c_1046])).
% 143.04/29.96 cnf(c_10390, plain, vvar(sK0(vvar(A),B,vbind(A,B,C))) = vvar(A) | vabs(sK1(vvar(A),B,vbind(A,B,C)),sK2(vvar(A),B,vbind(A,B,C)),sK3(vvar(A),B,vbind(A,B,C))) = vvar(A) | vapp(sK4(vvar(A),B,vbind(A,B,C)),sK5(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 143.04/29.96 inference(resolve, [status(thm)], [c_8320, c_1049])).
% 143.04/29.96 cnf(c_10391, plain, vvar(sK0(vvar(A),B,vbind(A,B,C))) = vvar(A) | vapp(sK4(vvar(A),B,vbind(A,B,C)),sK5(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 143.04/29.96 inference(resolve, [status(thm)], [c_1300, c_10390])).
% 143.04/29.96 cnf(c_8376, plain, vvar(sK0(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 143.04/29.96 inference(resolve, [status(thm)], [c_1299, c_10391])).
% 143.04/29.96 cnf(c_10392, plain, A = sK0(vvar(A),B,vbind(A,B,C)),
% 143.04/29.96 inference(resolve, [status(thm)], [c_8376, c_8242])).
% 143.04/29.96 cnf(c_8517, plain, sK0(vvar(A),B,vbind(A,B,C)) = A,
% 143.04/29.96 inference(copy, [status(thm)], [c_10392])).
% 143.04/29.96 cnf(c_10393, plain, A = sK0(vvar(A),B,vbind(A,B,C)),
% 143.04/29.96 inference(copy, [status(thm)], [c_8517])).
% 143.04/29.96 cnf(c_10394, plain, vvar(A) != B | sK0(vvar(vsubst(A,C,B)),D,vbind(vsubst(A,C,B),D,E)) = C,
% 143.04/29.96 inference(resolve, [status(thm)], [c_5414, c_10393])).
% 143.04/29.96 cnf(c_9391, plain, vvar(A) != B | vsubst(A,C,B) = C,
% 143.04/29.96 inference(paramod, [status(thm)], [c_8517, c_10394])).
% 143.04/29.96 cnf(c_10395, plain, A = sK0(vvar(A),B,vbind(A,B,C)),
% 143.04/29.96 inference(copy, [status(thm)], [c_8517])).
% 143.04/29.96 cnf(c_10396, plain, vsubst(A,B,sK0(vvar(vvar(A)),C,vbind(vvar(A),C,D))) = B,
% 143.04/29.96 inference(resolve, [status(thm)], [c_9391, c_10395])).
% 143.04/29.96 cnf(c_9392, plain, vsubst(A,B,vvar(A)) = B,
% 143.04/29.96 inference(paramod, [status(thm)], [c_8517, c_10396])).
% 143.04/29.96 cnf(c_10397, plain, B = vsubst(A,B,vvar(A)),
% 143.04/29.96 inference(copy, [status(thm)], [c_9392])).
% 143.04/29.96 cnf(c_10398, plain, vabs(A,B,C) = vsubst(D,vsubst(A,E,vabs(A,B,C)),vvar(D)),
% 143.04/29.96 inference(resolve, [status(thm)], [c_5364, c_10397])).
% 143.04/29.96 cnf(c_10399, plain, vabs(A,B,C) = vsubst(A,E,vabs(A,B,C)),
% 143.04/29.96 inference(paramod, [status(thm)], [c_9392, c_10398])).
% 143.04/29.96 cnf(c_10362, plain, vsubst(A,B,vabs(A,C,D)) = vabs(A,C,D),
% 143.04/29.96 inference(copy, [status(thm)], [c_10399])).
% 143.04/29.96 cnf(c_10363, negated_conjecture, ~vtcheck(sK9,vabs(sK7,sK10,sK11),sK12),
% 143.04/29.96 inference(paramod, [status(thm)], [c_10362, c_1076])).
% 143.04/29.96 cnf(c_10364, negated_conjecture, visFreeVar(sK7,vabs(sK7,sK10,sK11)),
% 143.04/29.96 inference(resolve, [status(thm)], [c_10363, c_5255])).
% 143.04/29.96 cnf(c_10400, plain, vabs(sK7,A,B) != vabs(sK7,sK10,sK11),
% 143.04/29.96 inference(resolve, [status(thm)], [c_10364, c_4859])).
% 143.04/29.96 cnf(c_10401, plain, vabs(sK7,sK10,sK11) != vabs(sK7,A,B),
% 143.04/29.96 inference(copy, [status(thm)], [c_10400])).
% 143.04/29.96 cnf(c_10368, plain, $false,
% 143.04/29.96 inference(copy, [status(thm)], [c_10401])).
% 143.04/29.96 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------