%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM129+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 : n006.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 106.44s 15.23s
% Output : CNFRefutation 106.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM129+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/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 23:31:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 2387272 was started by sandbox on n006,
% 0.11/0.37 % Sat Sep 26 23:31:40 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.40/0.67
% 0.40/0.67 % From the command line: assign(max_seconds, 300).
% 106.44/15.23
% 106.44/15.23 % given #500 (I,wt=65): 919 vsubst(A,B,C) != D | f12(A,B,C,D) = B | f15(A,B,C,D) != f14(A,B,C,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_00(A,B,C,D) | defn_10(A,B,C,D) # tptp_name(subst-INV). [clausify(35)].
% 106.44/15.23
% 106.44/15.23 % given #1000 (I,wt=54): 1692 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) | visFreeVar(f28(A,B,C,D),f26(A,B,C,D)). [copy(1691),flip(b)].
% 106.44/15.23
% 106.44/15.23 % given #1500 (I,wt=79): 2658 vsubst(A,B,C) != D | f11(A,B,C,D) = f10(A,B,C,D) | vvar(f15(A,B,C,D)) = D | vapp(vsubst(f17(A,B,C,D),f18(A,B,C,D),f16(A,B,C,D)),vsubst(f17(A,B,C,D),f18(A,B,C,D),f19(A,B,C,D))) = D | f21(A,B,C,D) = A | defn_10(A,B,C,D) | f26(A,B,C,D) = B. [resolve(180,f,75,a)].
% 106.44/15.23
% 106.44/15.23 % given #2000 (I,wt=72): 3158 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) | 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(252,f,71,a)].
% 106.44/15.23
% 106.44/15.23 % given #2500 (I,wt=76): 3658 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) | vabs(f28(A,B,C,D),f27(A,B,C,D),f30(A,B,C,D)) = C. [resolve(323,f,74,a)].
% 106.44/15.23
% 106.44/15.23 % given #3000 (F,wt=12): 4726 c3 != A | vabs(B,C,D) != c4 | A != B. [resolve(1206,c,896,a),flip(a)].
% 106.44/15.23
% 106.44/15.23 % SZS status Theorem for theBenchmark
% 106.44/15.23
% 106.44/15.23 % Proof 1 at 13.65 (+ 0.63) seconds.
% 106.44/15.23 % Length of proof is 67.
% 106.44/15.23 % Level of proof is 17.
% 106.44/15.23 % Maximum clause weight is 41.000.
% 106.44/15.23 % Given clauses 3166.
% 106.44/15.23
% 106.44/15.23 % SZS output start CNFRefutation for theBenchmark
% 106.44/15.23 fof(DIFF-var-abs, axiom, ! [VVar0,VVar1,VTyp0,VExp0] : ~ (vvar(VVar0) = vabs(VVar1,VTyp0,VExp0)), file('theBenchmark.p',DIFF-var-abs)).
% 106.44/15.23 fof(DIFF-var-app, axiom, ! [VVar0,VExp0,VExp1] : ~ (vvar(VVar0) = vapp(VExp0,VExp1)), file('theBenchmark.p',DIFF-var-app)).
% 106.44/15.23 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)).
% 106.44/15.23 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)).
% 106.44/15.23 fof(DIFF-empty-bind, axiom, ! [VVar0,VTyp0,VCtx0] : ~ (vempty = vbind(VVar0,VTyp0,VCtx0)), file('theBenchmark.p',DIFF-empty-bind)).
% 106.44/15.23 fof(getSomeType0, axiom, ! [VOptTyp0,RESULT,Ve] : (VOptTyp0 = vsomeType(Ve) => (RESULT = vgetSomeType(VOptTyp0) => RESULT = Ve)), file('theBenchmark.p',getSomeType0)).
% 106.44/15.23 fof(lookup0, axiom, ! [Vx,VVar0,VCtx0,RESULT] : ((VVar0 = Vx & VCtx0 = vempty) => (RESULT = vlookup(VVar0,VCtx0) => RESULT = vnoType)), file('theBenchmark.p',lookup0)).
% 106.44/15.23 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)).
% 106.44/15.23 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)).
% 106.44/15.23 fof(gensym-is-fresh, axiom, ! [Vv,Ve] : (vgensym(Ve) = Vv => ~ (visFreeVar(Vv,Ve))), file('theBenchmark.p',gensym-is-fresh)).
% 106.44/15.23 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)).
% 106.44/15.23 fof(getSomeExp0, axiom, ! [VOptExp0,RESULT,Ve] : (VOptExp0 = vsomeExp(Ve) => (RESULT = vgetSomeExp(VOptExp0) => RESULT = Ve)), file('theBenchmark.p',getSomeExp0)).
% 106.44/15.23 fof(T-var, axiom, ! [VC,Vx,VT] : (vlookup(Vx,VC) = vsomeType(VT) => vtcheck(VC,vvar(Vx),VT)), file('theBenchmark.p',T-var)).
% 106.44/15.23 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)).
% 106.44/15.23 fof(fresh-free-2, conjecture, ! [Ve,Vx,Vfresh,Ve1] : (Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) => ~ (visFreeVar(Vfresh,Ve1))), file('theBenchmark.p',fresh-free-2)).
% 106.44/15.23 fof(fresh-free-2_neg, negated_conjecture, ~(! [Ve,Vx,Vfresh,Ve1] : (Vfresh = vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) => ~ (visFreeVar(Vfresh,Ve1)))), inference(assume_negation, [status(cth)], [fresh-free-2])).
% 106.44/15.23 cnf(c_706, plain, vsomeExp(A) != B | vgetSomeExp(B) != C | C = A, inference(clausify, [status(thm)], [getSomeExp0])).
% 106.44/15.23 cnf(c_863, plain, vlookup(A,B) != vsomeType(C) | vtcheck(B,vvar(A),C), inference(clausify, [status(thm)], [T-var])).
% 106.44/15.23 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])).
% 106.44/15.23 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),sK17(Ve,VT,VC)) = VT & vtcheck(vbind(sK1(Ve,VT,VC),sK2(Ve,VT,VC),VC),sK3(Ve,VT,VC),sK17(Ve,VT,VC))) | (vapp(sK4(Ve,VT,VC),sK5(Ve,VT,VC)) = Ve & vtcheck(VC,sK4(Ve,VT,VC),varrow(sK18(Ve,VT,VC),VT)) & vtcheck(VC,sK5(Ve,VT,VC),sK18(Ve,VT,VC)))), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3,sK17,sK4,sK5,sK18]), 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,sK17(Ve,VT,VC)), skolemize(Ve1,sK4(Ve,VT,VC)), skolemize(Ve2,sK5(Ve,VT,VC)), skolemize(VS,sK18(Ve,VT,VC))], [nnf_54])).
% 106.44/15.23 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(sK18(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),sK18(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),sK17(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),sK17(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK18(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),sK17(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK18(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),sK17(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),sK17(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK18(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),sK17(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK18(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(sK18(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),sK18(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),sK17(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),sK17(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK18(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),sK17(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK18(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),sK17(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),sK17(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK4(VAR_1,VAR_2,VAR_0),varrow(sK18(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),sK17(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK5(VAR_1,VAR_2,VAR_0),sK18(VAR_1,VAR_2,VAR_0)))), inference(cnf_transformation, [status(thm)], [sk_T-inv_sk])).
% 106.44/15.23 cnf(c_866, 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])).
% 106.44/15.23 fof(nnf_66, plain, ? [Ve,Vx,Vfresh,Ve1] : (vgensym(vapp(vapp(Ve,Ve1),vvar(Vx))) = Vfresh & visFreeVar(Vfresh,Ve1)), inference(fof_nnf, [status(thm)], [fresh-free-2_neg])).
% 106.44/15.23 fof(sk_fresh-free-2_neg, plain, (vgensym(vapp(vapp(sK6,sK7),vvar(sK8))) = sK9 & visFreeVar(sK9,sK7)), inference(skolemize, [status(esa), new_symbols(skolem, [sK6,sK7,sK8,sK9]), skolemize(Ve,sK6), skolemize(Vx,sK8), skolemize(Vfresh,sK9), skolemize(Ve1,sK7)], [nnf_66])).
% 106.44/15.23 cnf(c_895, negated_conjecture, vgensym(vapp(vapp(sK6,sK7),vvar(sK8))) = sK9, inference(split_conjunct, [status(thm)], [sk_fresh-free-2_neg])).
% 106.44/15.23 cnf(c_896, negated_conjecture, visFreeVar(sK9,sK7), inference(split_conjunct, [status(thm)], [sk_fresh-free-2_neg])).
% 106.44/15.23 cnf(c_1101, plain, A != B | C != D | vvar(E) != F | E != A | vsubst(B,D,F) != V6 | V6 = C, inference(clausify, [status(thm)], [subst0])).
% 106.44/15.23 cnf(c_1102, plain, vgensym(A) != B | ~visFreeVar(B,A), inference(clausify, [status(thm)], [gensym-is-fresh])).
% 106.44/15.23 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])).
% 106.44/15.23 fof(sk_lookup-INV_sk, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | (sK10(VVar0,VCtx0,RESULT) = VVar0 & VCtx0 = vempty & RESULT = vnoType) | (sK19(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK11(VVar0,VCtx0,RESULT),sK12(VVar0,VCtx0,RESULT),sK13(VVar0,VCtx0,RESULT)) = VCtx0 & sK11(VVar0,VCtx0,RESULT) = sK19(VVar0,VCtx0,RESULT) & vsomeType(sK12(VVar0,VCtx0,RESULT)) = RESULT) | (sK20(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK14(VVar0,VCtx0,RESULT),sK15(VVar0,VCtx0,RESULT),sK16(VVar0,VCtx0,RESULT)) = VCtx0 & ~ (sK14(VVar0,VCtx0,RESULT) = sK20(VVar0,VCtx0,RESULT)) & vlookup(sK20(VVar0,VCtx0,RESULT),sK16(VVar0,VCtx0,RESULT)) = RESULT)), inference(skolemize, [status(esa), new_symbols(skolem, [sK10,sK19,sK11,sK12,sK13,sK20,sK14,sK15,sK16]), skolemize(X2,sK10(VVar0,VCtx0,RESULT)), skolemize(X1,sK13(VVar0,VCtx0,RESULT)), skolemize(X0,sK19(VVar0,VCtx0,RESULT)), skolemize(X3,sK11(VVar0,VCtx0,RESULT)), skolemize(X4,sK12(VVar0,VCtx0,RESULT)), skolemize(VTy,sK15(VVar0,VCtx0,RESULT)), skolemize(Vy,sK14(VVar0,VCtx0,RESULT)), skolemize(Vx,sK20(VVar0,VCtx0,RESULT)), skolemize(VC,sK16(VVar0,VCtx0,RESULT))], [nnf_25])).
% 106.44/15.23 fof(sk_lookup-INV, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | sK20(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK20(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = sK19(VAR_0,VAR_1,VAR_2) | sK20(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = sK19(VAR_0,VAR_1,VAR_2) | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = sK19(VAR_0,VAR_1,VAR_2) | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | sK11(VAR_0,VAR_1,VAR_2) = sK19(VAR_0,VAR_1,VAR_2) | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK20(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK10(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | sK20(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(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(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK20(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(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(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(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(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) = sK19(VAR_0,VAR_1,VAR_2) | sK20(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) = sK19(VAR_0,VAR_1,VAR_2) | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(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) = sK19(VAR_0,VAR_1,VAR_2) | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(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) = sK19(VAR_0,VAR_1,VAR_2) | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(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(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK20(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(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(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(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | sK20(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK19(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(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(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK20(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(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(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(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK11(VAR_0,VAR_1,VAR_2),sK12(VAR_0,VAR_1,VAR_2),sK13(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(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) = sK19(VAR_0,VAR_1,VAR_2) | sK20(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) = sK19(VAR_0,VAR_1,VAR_2) | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(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) = sK19(VAR_0,VAR_1,VAR_2) | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(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) = sK19(VAR_0,VAR_1,VAR_2) | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(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(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK20(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(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK14(VAR_0,VAR_1,VAR_2),sK15(VAR_0,VAR_1,VAR_2),sK16(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(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK14(VAR_0,VAR_1,VAR_2) = sK20(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK12(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK20(VAR_0,VAR_1,VAR_2),sK16(VAR_0,VAR_1,VAR_2)) = VAR_2)), inference(cnf_transformation, [status(thm)], [sk_lookup-INV_sk])).
% 106.44/15.23 cnf(c_1182, plain, vlookup(A,B) != C | sK10(A,B,C) = A | vbind(sK11(A,B,C),sK12(A,B,C),sK13(A,B,C)) = B | vbind(sK14(A,B,C),sK15(A,B,C),sK16(A,B,C)) = B, inference(split_conjunct, [status(thm)], [sk_lookup-INV])).
% 106.44/15.23 cnf(c_1190, plain, A != B | vbind(C,D,E) != F | C != A | vlookup(B,F) != V6 | vsomeType(D) = V6, inference(clausify, [status(thm)], [lookup1])).
% 106.44/15.23 cnf(c_1191, plain, A != B | C != vempty | vlookup(B,C) != D | D = vnoType, inference(clausify, [status(thm)], [lookup0])).
% 106.44/15.23 cnf(c_8774, plain, A != B | vempty != C | vlookup(B,C) != D | D = vnoType,
% 106.44/15.23 inference(copy, [status(thm)], [c_1191])).
% 106.44/15.23 cnf(c_8775, plain, A != B | vempty != C | vlookup(B,C) != D | vnoType = D,
% 106.44/15.23 inference(copy, [status(thm)], [c_8774])).
% 106.44/15.23 cnf(c_1192, plain, vempty != A | vlookup(B,A) != C | vnoType = C,
% 106.44/15.23 inference(copy, [status(thm)], [c_8775])).
% 106.44/15.23 cnf(c_1193, plain, vsomeType(A) != B | vgetSomeType(B) != C | C = A, inference(clausify, [status(thm)], [getSomeType0])).
% 106.44/15.23 cnf(c_1195, plain, vbind(A,B,C) != vempty, inference(clausify, [status(thm)], [DIFF-empty-bind])).
% 106.44/15.23 cnf(c_1203, plain, A != B | vapp(C,D) != E | ~visFreeVar(A,D) | visFreeVar(B,E), inference(clausify, [status(thm)], [isFreeVar2])).
% 106.44/15.23 cnf(c_1204, plain, A != B | vapp(C,D) != E | ~visFreeVar(A,C) | visFreeVar(B,E), inference(clausify, [status(thm)], [isFreeVar2])).
% 106.44/15.23 cnf(c_1208, plain, A != B | vvar(C) != D | ~visFreeVar(B,D) | A = C, inference(clausify, [status(thm)], [isFreeVar0])).
% 106.44/15.23 cnf(c_1209, plain, A != B | vvar(C) != D | A != C | visFreeVar(B,D), inference(clausify, [status(thm)], [isFreeVar0])).
% 106.44/15.23 cnf(c_1214, plain, vapp(A,B) != vvar(C), inference(clausify, [status(thm)], [DIFF-var-app])).
% 106.44/15.23 cnf(c_1215, plain, vabs(A,B,C) != vvar(D), inference(clausify, [status(thm)], [DIFF-var-abs])).
% 106.44/15.23 cnf(c_4327, plain, vgetSomeExp(vsomeExp(A)) != B | B = A,
% 106.44/15.23 inference(xxres, [status(thm)], [c_706])).
% 106.44/15.23 cnf(c_4616, plain, A != B | vvar(C) != D | C != A | vsubst(B,E,D) != F | F = E,
% 106.44/15.23 inference(xxres, [status(thm)], [c_1101])).
% 106.44/15.23 cnf(c_4617, plain, A != B | C != D | E != A | vsubst(B,D,vvar(E)) != F | F = C,
% 106.44/15.23 inference(xxres, [status(thm)], [c_1101])).
% 106.44/15.23 cnf(c_8776, plain, A != A | vvar(A) != B | vsubst(A,C,B) != D | D = C,
% 106.44/15.23 inference(factor, [status(thm)], [c_4616])).
% 106.44/15.23 cnf(c_4629, plain, vvar(A) != B | vsubst(A,C,B) != D | D = C,
% 106.44/15.23 inference(copy, [status(thm)], [c_8776])).
% 106.44/15.23 cnf(c_4632, plain, A != B | C != A | vsubst(B,B,vvar(C)) != D | D = A,
% 106.44/15.23 inference(factor, [status(thm)], [c_4617])).
% 106.44/15.23 cnf(c_8777, plain, A != A | vsubst(A,A,vvar(A)) != B | B = A,
% 106.44/15.23 inference(factor, [status(thm)], [c_4632])).
% 106.44/15.23 cnf(c_4644, plain, vsubst(A,A,vvar(A)) != B | B = A,
% 106.44/15.23 inference(copy, [status(thm)], [c_8777])).
% 106.44/15.23 cnf(c_4699, plain, A != B | C != A | vlookup(B,vbind(C,D,E)) != F | vsomeType(D) = F,
% 106.44/15.23 inference(xxres, [status(thm)], [c_1190])).
% 106.44/15.23 cnf(c_8778, plain, A != A | vlookup(A,vbind(A,B,C)) != D | vsomeType(B) = D,
% 106.44/15.23 inference(factor, [status(thm)], [c_4699])).
% 106.44/15.23 cnf(c_4702, plain, vlookup(A,vbind(A,B,C)) != D | vsomeType(B) = D,
% 106.44/15.23 inference(copy, [status(thm)], [c_8778])).
% 106.44/15.23 cnf(c_8779, plain, vempty != A | vnoType = vlookup(B,A),
% 106.44/15.23 inference(xxres, [status(thm)], [c_1192])).
% 106.44/15.23 cnf(c_4706, plain, vempty != A | vlookup(B,A) = vnoType,
% 106.44/15.23 inference(copy, [status(thm)], [c_8779])).
% 106.44/15.23 cnf(c_4707, plain, vgetSomeType(vsomeType(A)) != B | B = A,
% 106.44/15.23 inference(xxres, [status(thm)], [c_1193])).
% 106.44/15.23 cnf(c_4723, plain, sK9 != A | vapp(B,sK7) != C | visFreeVar(A,C),
% 106.44/15.23 inference(resolve, [status(thm)], [c_1203, c_896])).
% 106.44/15.23 cnf(c_4733, plain, A != B | A != C | visFreeVar(B,vvar(C)),
% 106.44/15.23 inference(xxres, [status(thm)], [c_1209])).
% 106.44/15.23 cnf(c_8780, plain, A != B | visFreeVar(B,vvar(B)),
% 106.44/15.23 inference(factor, [status(thm)], [c_4733])).
% 106.44/15.23 cnf(c_4737, plain, visFreeVar(A,vvar(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_8780])).
% 106.44/15.23 cnf(c_5573, plain, A != B | vvar(C) != vvar(B) | A = C,
% 106.44/15.23 inference(resolve, [status(thm)], [c_4737, c_1208])).
% 106.44/15.23 cnf(c_5580, plain, vgetSomeExp(vsomeExp(A)) = A,
% 106.44/15.23 inference(xxres, [status(thm)], [c_4327])).
% 106.44/15.23 cnf(c_8781, plain, A = vgetSomeExp(vsomeExp(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_5580])).
% 106.44/15.23 cnf(c_8782, plain, vlookup(A,vgetSomeExp(vsomeExp(vempty))) = vnoType,
% 106.44/15.23 inference(resolve, [status(thm)], [c_4706, c_8781])).
% 106.44/15.23 cnf(c_5620, plain, vlookup(A,vempty) = vnoType,
% 106.44/15.23 inference(paramod, [status(thm)], [c_5580, c_8782])).
% 106.44/15.23 cnf(c_8783, plain, sK10(A,vempty,vnoType) = A | vbind(sK11(A,vempty,vnoType),sK12(A,vempty,vnoType),sK13(A,vempty,vnoType)) = vempty | vbind(sK14(A,vempty,vnoType),sK15(A,vempty,vnoType),sK16(A,vempty,vnoType)) = vempty,
% 106.44/15.23 inference(resolve, [status(thm)], [c_5620, c_1182])).
% 106.44/15.23 cnf(c_8784, plain, sK10(A,vempty,vnoType) = A | vbind(sK14(A,vempty,vnoType),sK15(A,vempty,vnoType),sK16(A,vempty,vnoType)) = vempty,
% 106.44/15.23 inference(resolve, [status(thm)], [c_1195, c_8783])).
% 106.44/15.23 cnf(c_5637, plain, sK10(A,vempty,vnoType) = A,
% 106.44/15.23 inference(resolve, [status(thm)], [c_1195, c_8784])).
% 106.44/15.23 cnf(c_8785, plain, A = sK10(A,vempty,vnoType),
% 106.44/15.23 inference(copy, [status(thm)], [c_5637])).
% 106.44/15.23 cnf(c_8786, plain, sK10(vgetSomeType(vsomeType(A)),vempty,vnoType) = A,
% 106.44/15.23 inference(resolve, [status(thm)], [c_4707, c_8785])).
% 106.44/15.23 cnf(c_5653, plain, vgetSomeType(vsomeType(A)) = A,
% 106.44/15.23 inference(paramod, [status(thm)], [c_5637, c_8786])).
% 106.44/15.23 cnf(c_8787, plain, A = vgetSomeType(vsomeType(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_5653])).
% 106.44/15.23 cnf(c_8788, plain, vgetSomeType(vsomeType(vsubst(A,A,vvar(A)))) = A,
% 106.44/15.23 inference(resolve, [status(thm)], [c_4644, c_8787])).
% 106.44/15.23 cnf(c_5668, plain, vsubst(A,A,vvar(A)) = A,
% 106.44/15.23 inference(paramod, [status(thm)], [c_5653, c_8788])).
% 106.44/15.23 cnf(c_8789, plain, A = vsubst(A,A,vvar(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_5668])).
% 106.44/15.23 cnf(c_8790, plain, vapp(A,sK7) != B | visFreeVar(vsubst(sK9,sK9,vvar(sK9)),B),
% 106.44/15.23 inference(resolve, [status(thm)], [c_4723, c_8789])).
% 106.44/15.23 cnf(c_7031, plain, vapp(A,sK7) != B | visFreeVar(sK9,B),
% 106.44/15.23 inference(paramod, [status(thm)], [c_5668, c_8790])).
% 106.44/15.23 cnf(c_8791, plain, A = vsubst(A,A,vvar(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_5668])).
% 106.44/15.23 cnf(c_8792, plain, visFreeVar(sK9,vsubst(vapp(A,sK7),vapp(A,sK7),vvar(vapp(A,sK7)))),
% 106.44/15.23 inference(resolve, [status(thm)], [c_7031, c_8791])).
% 106.44/15.23 cnf(c_7033, plain, visFreeVar(sK9,vapp(A,sK7)),
% 106.44/15.23 inference(paramod, [status(thm)], [c_5668, c_8792])).
% 106.44/15.23 cnf(c_7040, plain, sK9 != A | vapp(vapp(B,sK7),C) != D | visFreeVar(A,D),
% 106.44/15.23 inference(resolve, [status(thm)], [c_7033, c_1204])).
% 106.44/15.23 cnf(c_8793, plain, vvar(A) != vvar(B) | vsubst(B,B,vvar(B)) = A,
% 106.44/15.23 inference(resolve, [status(thm)], [c_5573, c_5668])).
% 106.44/15.23 cnf(c_7061, plain, vvar(A) != vvar(B) | B = A,
% 106.44/15.23 inference(paramod, [status(thm)], [c_5668, c_8793])).
% 106.44/15.23 cnf(c_8794, plain, A = vsubst(A,A,vvar(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_5668])).
% 106.44/15.23 cnf(c_8795, plain, vsomeType(A) = vsubst(vlookup(B,vbind(B,A,C)),vlookup(B,vbind(B,A,C)),vvar(vlookup(B,vbind(B,A,C)))),
% 106.44/15.23 inference(resolve, [status(thm)], [c_4702, c_8794])).
% 106.44/15.23 cnf(c_8796, plain, vsomeType(A) = vlookup(B,vbind(B,A,C)),
% 106.44/15.23 inference(paramod, [status(thm)], [c_5668, c_8795])).
% 106.44/15.23 cnf(c_7064, plain, vlookup(A,vbind(A,B,C)) = vsomeType(B),
% 106.44/15.23 inference(copy, [status(thm)], [c_8796])).
% 106.44/15.23 cnf(c_7115, plain, vtcheck(vbind(A,B,C),vvar(A),B),
% 106.44/15.23 inference(resolve, [status(thm)], [c_7064, c_863])).
% 106.44/15.23 cnf(c_8797, 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),
% 106.44/15.23 inference(resolve, [status(thm)], [c_7115, c_866])).
% 106.44/15.23 cnf(c_8798, 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),
% 106.44/15.23 inference(resolve, [status(thm)], [c_1215, c_8797])).
% 106.44/15.23 cnf(c_7172, plain, vvar(sK0(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 106.44/15.23 inference(resolve, [status(thm)], [c_1214, c_8798])).
% 106.44/15.23 cnf(c_8799, plain, A = sK0(vvar(A),B,vbind(A,B,C)),
% 106.44/15.23 inference(resolve, [status(thm)], [c_7172, c_7061])).
% 106.44/15.23 cnf(c_7248, plain, sK0(vvar(A),B,vbind(A,B,C)) = A,
% 106.44/15.23 inference(copy, [status(thm)], [c_8799])).
% 106.44/15.23 cnf(c_8800, plain, A = sK0(vvar(A),B,vbind(A,B,C)),
% 106.44/15.23 inference(copy, [status(thm)], [c_7248])).
% 106.44/15.23 cnf(c_8801, plain, vvar(A) != B | sK0(vvar(vsubst(A,C,B)),D,vbind(vsubst(A,C,B),D,E)) = C,
% 106.44/15.23 inference(resolve, [status(thm)], [c_4629, c_8800])).
% 106.44/15.23 cnf(c_8006, plain, vvar(A) != B | vsubst(A,C,B) = C,
% 106.44/15.23 inference(paramod, [status(thm)], [c_7248, c_8801])).
% 106.44/15.23 cnf(c_8802, plain, A = sK0(vvar(A),B,vbind(A,B,C)),
% 106.44/15.23 inference(copy, [status(thm)], [c_7248])).
% 106.44/15.23 cnf(c_8803, plain, vsubst(A,B,sK0(vvar(vvar(A)),C,vbind(vvar(A),C,D))) = B,
% 106.44/15.23 inference(resolve, [status(thm)], [c_8006, c_8802])).
% 106.44/15.23 cnf(c_8007, plain, vsubst(A,B,vvar(A)) = B,
% 106.44/15.23 inference(paramod, [status(thm)], [c_7248, c_8803])).
% 106.44/15.23 cnf(c_8804, plain, B = vsubst(A,B,vvar(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_8007])).
% 106.44/15.23 cnf(c_8805, plain, vapp(vapp(A,sK7),B) != C | visFreeVar(vsubst(D,sK9,vvar(D)),C),
% 106.44/15.23 inference(resolve, [status(thm)], [c_7040, c_8804])).
% 106.44/15.23 cnf(c_8760, plain, vapp(vapp(A,sK7),B) != C | visFreeVar(sK9,C),
% 106.44/15.23 inference(paramod, [status(thm)], [c_8007, c_8805])).
% 106.44/15.23 cnf(c_8806, plain, B = vsubst(A,B,vvar(A)),
% 106.44/15.23 inference(copy, [status(thm)], [c_8007])).
% 106.44/15.23 cnf(c_8807, plain, visFreeVar(sK9,vsubst(A,vapp(vapp(B,sK7),C),vvar(A))),
% 106.44/15.23 inference(resolve, [status(thm)], [c_8760, c_8806])).
% 106.44/15.23 cnf(c_8762, plain, visFreeVar(sK9,vapp(vapp(A,sK7),B)),
% 106.44/15.23 inference(paramod, [status(thm)], [c_8007, c_8807])).
% 106.44/15.23 cnf(c_8772, plain, vgensym(vapp(vapp(A,sK7),B)) != sK9,
% 106.44/15.23 inference(resolve, [status(thm)], [c_8762, c_1102])).
% 106.44/15.23 cnf(c_8773, plain, $false,
% 106.44/15.23 inference(resolve, [status(thm)], [c_8772, c_895])).
% 106.44/15.23 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------