%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM135+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 : n020.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 227.33s 41.79s
% Output : CNFRefutation 227.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM135+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.10/10.39 % Computer : n020.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:34:46 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.39 % Process 2796940 was started by sandbox on n020,
% 0.10/10.39 % Sat Sep 26 23:34:46 2026
% 0.10/10.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/10.69
% 0.15/10.69 % From the command line: assign(max_seconds, 300).
% 227.33/41.79
% 227.33/41.79 % given #500 (I,wt=7): 977 -defn_30(A,B) | -visValue(f60(A,B)) # tptp_name(reduce-INV). [clausify(49)].
% 227.33/41.79
% 227.33/41.79 % given #1000 (I,wt=54): 1758 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) | visFreeVar(f28(A,B,C,D),f26(A,B,C,D)). [copy(1757),flip(b)].
% 227.33/41.79
% 227.33/41.79 % given #1500 (I,wt=68): 2717 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) | f26(A,B,C,D) = B. [resolve(173,f,67,a)].
% 227.33/41.79
% 227.33/41.79 % given #2000 (I,wt=79): 3217 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 | vabs(f22(A,B,C,D),f23(A,B,C,D),f24(A,B,C,D)) = C | 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(245,f,63,a)].
% 227.33/41.79
% 227.33/41.79 % given #2500 (I,wt=65): 3717 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) | vabs(f28(A,B,C,D),f27(A,B,C,D),f30(A,B,C,D)) = C. [resolve(316,f,66,a)].
% 227.33/41.79
% 227.33/41.79 % given #3000 (I,wt=123): 4217 vsubst(A,B,C) != D | f12(A,B,C,D) = B | f15(A,B,C,D) != f14(A,B,C,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 | 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(388,f,62,a)].
% 227.33/41.79
% 227.33/41.79 % given #3500 (T,wt=10): 5250 A != B | vapp(A,C) = vapp(B,C). [xx_res(1268,b)].
% 227.33/41.79
% 227.33/41.79 % given #4000 (T,wt=16): 9231 A != B | vapp(C,vapp(vapp(D,vvar(A)),E)) != F | visFreeVar(B,F). [resolve(9223,a,1255,c)].
% 227.33/41.79
% 227.33/41.79 % SZS status Theorem for theBenchmark
% 227.33/41.79
% 227.33/41.79 % Proof 1 at 28.72 (+ 1.59) seconds.
% 227.33/41.79 % Length of proof is 93.
% 227.33/41.79 % Level of proof is 19.
% 227.33/41.79 % Maximum clause weight is 66.000.
% 227.33/41.79 % Given clauses 4164.
% 227.33/41.79
% 227.33/41.79 % SZS output start CNFRefutation for theBenchmark
% 227.33/41.79 fof(DIFF-var-abs, axiom, ! [VVar0,VVar1,VTyp0,VExp0] : ~ (vvar(VVar0) = vabs(VVar1,VTyp0,VExp0)), file('theBenchmark.p',DIFF-var-abs)).
% 227.33/41.79 fof(DIFF-var-app, axiom, ! [VVar0,VExp0,VExp1] : ~ (vvar(VVar0) = vapp(VExp0,VExp1)), file('theBenchmark.p',DIFF-var-app)).
% 227.33/41.79 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)).
% 227.33/41.79 fof(DIFF-empty-bind, axiom, ! [VVar0,VTyp0,VCtx0] : ~ (vempty = vbind(VVar0,VTyp0,VCtx0)), file('theBenchmark.p',DIFF-empty-bind)).
% 227.33/41.79 fof(getSomeType0, axiom, ! [VOptTyp0,RESULT,Ve] : (VOptTyp0 = vsomeType(Ve) => (RESULT = vgetSomeType(VOptTyp0) => RESULT = Ve)), file('theBenchmark.p',getSomeType0)).
% 227.33/41.79 fof(lookup0, axiom, ! [Vx,VVar0,VCtx0,RESULT] : ((VVar0 = Vx & VCtx0 = vempty) => (RESULT = vlookup(VVar0,VCtx0) => RESULT = vnoType)), file('theBenchmark.p',lookup0)).
% 227.33/41.79 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)).
% 227.33/41.79 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)).
% 227.33/41.79 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)).
% 227.33/41.79 fof(subst1, axiom, ! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy] : ((VVar0 = Vx & VExp0 = Ve & VExp1 = vvar(Vy)) => (~ (Vx = Vy) => (RESULT = vsubst(VVar0,VExp0,VExp1) => RESULT = vvar(Vy)))), file('theBenchmark.p',subst1)).
% 227.33/41.79 fof(DIFF-noExp-someExp, axiom, ! [VExp0] : ~ (vnoExp = vsomeExp(VExp0)), file('theBenchmark.p',DIFF-noExp-someExp)).
% 227.33/41.79 fof(getSomeExp0, axiom, ! [VOptExp0,RESULT,Ve] : (VOptExp0 = vsomeExp(Ve) => (RESULT = vgetSomeExp(VOptExp0) => RESULT = Ve)), file('theBenchmark.p',getSomeExp0)).
% 227.33/41.79 fof(reduce0, axiom, ! [Vx,VExp0,RESULT] : (VExp0 = vvar(Vx) => (RESULT = vreduce(VExp0) => RESULT = vnoExp)), file('theBenchmark.p',reduce0)).
% 227.33/41.79 fof(reduce-INV, axiom, ! [VExp0,RESULT] : (vreduce(VExp0) = RESULT => (? [Vx] : (VExp0 = vvar(Vx) & RESULT = vnoExp) | ? [Vx,VS,Ve] : (VExp0 = vabs(Vx,VS,Ve) & RESULT = vnoExp) | ? [Ve2,Vx,VS,Ve1,Ve2red] : (VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) & Ve2red = vreduce(Ve2) & visSomeExp(Ve2red) & RESULT = vsomeExp(vapp(vabs(Vx,VS,Ve1),vgetSomeExp(Ve2red)))) | ? [VS,Ve2red,Vx,Ve2,Ve1] : (VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) & Ve2red = vreduce(Ve2) & ~ (visSomeExp(Ve2red)) & visValue(Ve2) & RESULT = vsomeExp(vsubst(Vx,Ve2,Ve1))) | ? [Vx,VS,Ve1,Ve2red,Ve2] : (VExp0 = vapp(vabs(Vx,VS,Ve1),Ve2) & Ve2red = vreduce(Ve2) & ~ (visSomeExp(Ve2red)) & ~ (visValue(Ve2)) & RESULT = vnoExp) | ? [Ve1,Ve1red,Ve2] : (VExp0 = vapp(Ve1,Ve2) & ! [VVx0,VVS0,VVe10] : ~ (Ve1 = vabs(VVx0,VVS0,VVe10)) & Ve1red = vreduce(Ve1) & visSomeExp(Ve1red) & RESULT = vsomeExp(vapp(vgetSomeExp(Ve1red),Ve2))) | ? [Ve2,Ve1,Ve1red] : (VExp0 = vapp(Ve1,Ve2) & ! [VVx0,VVS0,VVe10] : ~ (Ve1 = vabs(VVx0,VVS0,VVe10)) & Ve1red = vreduce(Ve1) & ~ (visSomeExp(Ve1red)) & RESULT = vnoExp))), file('theBenchmark.p',reduce-INV)).
% 227.33/41.79 fof(T-var, axiom, ! [VC,Vx,VT] : (vlookup(Vx,VC) = vsomeType(VT) => vtcheck(VC,vvar(Vx),VT)), file('theBenchmark.p',T-var)).
% 227.33/41.79 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)).
% 227.33/41.79 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)).
% 227.33/41.79 fof(T-subst-var, conjecture, ! [VT,VC,Vx,Ve,Vy,VT2] : ((vtcheck(VC,Ve,VT) & vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2)) => vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2)), file('theBenchmark.p',T-subst-var)).
% 227.33/41.79 fof(T-subst-var_neg, negated_conjecture, ~(! [VT,VC,Vx,Ve,Vy,VT2] : ((vtcheck(VC,Ve,VT) & vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2)) => vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2))), inference(assume_negation, [status(cth)], [T-subst-var])).
% 227.33/41.79 cnf(c_828, plain, vsomeExp(A) != vnoExp, inference(clausify, [status(thm)], [DIFF-noExp-someExp])).
% 227.33/41.79 cnf(c_832, plain, vsomeExp(A) != B | vgetSomeExp(B) != C | C = A, inference(clausify, [status(thm)], [getSomeExp0])).
% 227.33/41.79 cnf(c_833, plain, vvar(A) != B | vreduce(B) != C | vnoExp = C, inference(clausify, [status(thm)], [reduce0])).
% 227.33/41.79 fof(nnf_49, plain, ! [VExp0,RESULT] : (~ (vreduce(VExp0) = RESULT) | ? [X0] : (vvar(X0) = VExp0 & vnoExp = RESULT) | ? [X1,X2,Ve] : (vabs(X1,X2,Ve) = VExp0 & vnoExp = RESULT) | ? [X3,X4,X5,X6,X7] : (vapp(vabs(X4,X5,X6),X3) = VExp0 & vreduce(X3) = X7 & visSomeExp(X7) & vsomeExp(vapp(vabs(X4,X5,X6),vgetSomeExp(X7))) = RESULT) | ? [X8,X9,X10,X11,X12] : (vapp(vabs(X10,X8,X12),X11) = VExp0 & vreduce(X11) = X9 & ~ (visSomeExp(X9)) & visValue(X11) & vsomeExp(vsubst(X10,X11,X12)) = RESULT) | ? [Vx,VS,X13,Ve2red,X14] : (vapp(vabs(Vx,VS,X13),X14) = VExp0 & vreduce(X14) = Ve2red & ~ (visSomeExp(Ve2red)) & ~ (visValue(X14)) & vnoExp = RESULT) | ? [X15,X16,X17] : (vapp(X15,X17) = VExp0 & ! [X18,X19,X20] : ~ (vabs(X18,X19,X20) = X15) & vreduce(X15) = X16 & visSomeExp(X16) & vsomeExp(vapp(vgetSomeExp(X16),X17)) = RESULT) | ? [Ve2,Ve1,Ve1red] : (vapp(Ve1,Ve2) = VExp0 & ! [VVx0,VVS0,VVe10] : ~ (vabs(VVx0,VVS0,VVe10) = Ve1) & vreduce(Ve1) = Ve1red & ~ (visSomeExp(Ve1red)) & vnoExp = RESULT)), inference(fof_nnf, [status(thm)], [reduce-INV])).
% 227.33/41.79 fof(sk_reduce-INV_sk, plain, ! [VExp0,RESULT] : (~ (vreduce(VExp0) = RESULT) | (vvar(sK0(VExp0,RESULT)) = VExp0 & vnoExp = RESULT) | (vabs(sK1(VExp0,RESULT),sK2(VExp0,RESULT),sK3(VExp0,RESULT)) = VExp0 & vnoExp = RESULT) | (vapp(vabs(sK4(VExp0,RESULT),sK5(VExp0,RESULT),sK6(VExp0,RESULT)),sK39(VExp0,RESULT)) = VExp0 & vreduce(sK39(VExp0,RESULT)) = sK7(VExp0,RESULT) & visSomeExp(sK7(VExp0,RESULT)) & vsomeExp(vapp(vabs(sK4(VExp0,RESULT),sK5(VExp0,RESULT),sK6(VExp0,RESULT)),vgetSomeExp(sK7(VExp0,RESULT)))) = RESULT) | (vapp(vabs(sK16(VExp0,RESULT),sK17(VExp0,RESULT),sK18(VExp0,RESULT)),sK19(VExp0,RESULT)) = VExp0 & vreduce(sK19(VExp0,RESULT)) = sK40(VExp0,RESULT) & ~ (visSomeExp(sK40(VExp0,RESULT))) & visValue(sK19(VExp0,RESULT)) & vsomeExp(vsubst(sK16(VExp0,RESULT),sK19(VExp0,RESULT),sK18(VExp0,RESULT))) = RESULT) | (vapp(vabs(sK12(VExp0,RESULT),sK13(VExp0,RESULT),sK14(VExp0,RESULT)),sK15(VExp0,RESULT)) = VExp0 & vreduce(sK15(VExp0,RESULT)) = sK41(VExp0,RESULT) & ~ (visSomeExp(sK41(VExp0,RESULT))) & ~ (visValue(sK15(VExp0,RESULT))) & vnoExp = RESULT) | (vapp(sK42(VExp0,RESULT),sK9(VExp0,RESULT)) = VExp0 & ! [X18,X19,X20] : ~ (vabs(X18,X19,X20) = sK42(VExp0,RESULT)) & vreduce(sK42(VExp0,RESULT)) = sK8(VExp0,RESULT) & visSomeExp(sK8(VExp0,RESULT)) & vsomeExp(vapp(vgetSomeExp(sK8(VExp0,RESULT)),sK9(VExp0,RESULT))) = RESULT) | (vapp(sK10(VExp0,RESULT),sK11(VExp0,RESULT)) = VExp0 & ! [VVx0,VVS0,VVe10] : ~ (vabs(VVx0,VVS0,VVe10) = sK10(VExp0,RESULT)) & vreduce(sK10(VExp0,RESULT)) = sK43(VExp0,RESULT) & ~ (visSomeExp(sK43(VExp0,RESULT))) & vnoExp = RESULT)), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK39,sK7,sK16,sK17,sK18,sK19,sK40,sK12,sK13,sK14,sK15,sK41,sK42,sK9,sK8,sK10,sK11,sK43]), skolemize(X0,sK0(VExp0,RESULT)), skolemize(X1,sK1(VExp0,RESULT)), skolemize(X2,sK2(VExp0,RESULT)), skolemize(Ve,sK3(VExp0,RESULT)), skolemize(X3,sK39(VExp0,RESULT)), skolemize(X4,sK4(VExp0,RESULT)), skolemize(X5,sK5(VExp0,RESULT)), skolemize(X6,sK6(VExp0,RESULT)), skolemize(X7,sK7(VExp0,RESULT)), skolemize(X8,sK17(VExp0,RESULT)), skolemize(X9,sK40(VExp0,RESULT)), skolemize(X10,sK16(VExp0,RESULT)), skolemize(X11,sK19(VExp0,RESULT)), skolemize(X12,sK18(VExp0,RESULT)), skolemize(Vx,sK12(VExp0,RESULT)), skolemize(VS,sK13(VExp0,RESULT)), skolemize(X13,sK14(VExp0,RESULT)), skolemize(Ve2red,sK41(VExp0,RESULT)), skolemize(X14,sK15(VExp0,RESULT)), skolemize(X15,sK42(VExp0,RESULT)), skolemize(X16,sK8(VExp0,RESULT)), skolemize(X17,sK9(VExp0,RESULT)), skolemize(Ve2,sK11(VExp0,RESULT)), skolemize(Ve1,sK10(VExp0,RESULT)), skolemize(Ve1red,sK43(VExp0,RESULT))], [nnf_49])).
% 227.33/41.79 fof(def_defn_20, definition, ! [X21,X22] : (defn_20(X21,X22) <=> (vapp(vabs(sK16(X21,X22),sK17(X21,X22),sK18(X21,X22)),sK19(X21,X22)) = X21 & vreduce(sK19(X21,X22)) = sK40(X21,X22) & ~ (visSomeExp(sK40(X21,X22))) & visValue(sK19(X21,X22)) & vsomeExp(vsubst(sK16(X21,X22),sK19(X21,X22),sK18(X21,X22))) = X22)), introduced(definition, [new_symbols(definition, [defn_20])], [])).
% 227.33/41.79 fof(def_defn_30, definition, ! [X23,X24] : (defn_30(X23,X24) <=> (vapp(vabs(sK12(X23,X24),sK13(X23,X24),sK14(X23,X24)),sK15(X23,X24)) = X23 & vreduce(sK15(X23,X24)) = sK41(X23,X24) & ~ (visSomeExp(sK41(X23,X24))) & ~ (visValue(sK15(X23,X24))) & vnoExp = X24)), introduced(definition, [new_symbols(definition, [defn_30])], [])).
% 227.33/41.79 fof(sk_reduce-INV, plain, (! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (vabs(VAR_5,VAR_6,VAR_7) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (vabs(VAR_5,VAR_6,VAR_7) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (vabs(VAR_5,VAR_6,VAR_7) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (vabs(VAR_5,VAR_6,VAR_7) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1)) | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vapp(sK10(VAR_0,VAR_1),sK11(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK10(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | vreduce(sK10(VAR_0,VAR_1)) = sK43(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vvar(sK0(VAR_0,VAR_1)) = VAR_0 | vabs(sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1),sK3(VAR_0,VAR_1)) = VAR_0 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1 | ~ (visSomeExp(sK43(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),sK39(VAR_0,VAR_1)) = VAR_0 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vreduce(sK39(VAR_0,VAR_1)) = sK7(VAR_0,VAR_1) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | visSomeExp(sK7(VAR_0,VAR_1)) | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vapp(sK42(VAR_0,VAR_1),sK9(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | ~ (vabs(VAR_2,VAR_3,VAR_4) = sK42(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vreduce(sK42(VAR_0,VAR_1)) = sK8(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | visSomeExp(sK8(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (vreduce(VAR_0) = VAR_1) | vnoExp = VAR_1 | vsomeExp(vapp(vabs(sK4(VAR_0,VAR_1),sK5(VAR_0,VAR_1),sK6(VAR_0,VAR_1)),vgetSomeExp(sK7(VAR_0,VAR_1)))) = VAR_1 | defn_20(VAR_0,VAR_1) | defn_30(VAR_0,VAR_1) | vsomeExp(vapp(vgetSomeExp(sK8(VAR_0,VAR_1)),sK9(VAR_0,VAR_1))) = VAR_1) & ! [VAR_0,VAR_1] : (~ (defn_30(VAR_0,VAR_1)) | vnoExp = VAR_1) & ! [VAR_0,VAR_1] : (~ (defn_30(VAR_0,VAR_1)) | ~ (visValue(sK15(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (defn_30(VAR_0,VAR_1)) | ~ (visSomeExp(sK41(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (defn_30(VAR_0,VAR_1)) | vreduce(sK15(VAR_0,VAR_1)) = sK41(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (defn_30(VAR_0,VAR_1)) | vapp(vabs(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1),sK14(VAR_0,VAR_1)),sK15(VAR_0,VAR_1)) = VAR_0) & ! [VAR_0,VAR_1] : (~ (defn_20(VAR_0,VAR_1)) | vsomeExp(vsubst(sK16(VAR_0,VAR_1),sK19(VAR_0,VAR_1),sK18(VAR_0,VAR_1))) = VAR_1) & ! [VAR_0,VAR_1] : (~ (defn_20(VAR_0,VAR_1)) | visValue(sK19(VAR_0,VAR_1))) & ! [VAR_0,VAR_1] : (~ (defn_20(VAR_0,VAR_1)) | ~ (visSomeExp(sK40(VAR_0,VAR_1)))) & ! [VAR_0,VAR_1] : (~ (defn_20(VAR_0,VAR_1)) | vreduce(sK19(VAR_0,VAR_1)) = sK40(VAR_0,VAR_1)) & ! [VAR_0,VAR_1] : (~ (defn_20(VAR_0,VAR_1)) | vapp(vabs(sK16(VAR_0,VAR_1),sK17(VAR_0,VAR_1),sK18(VAR_0,VAR_1)),sK19(VAR_0,VAR_1)) = VAR_0)), inference(cnf_transformation, [status(thm)], [sk_reduce-INV_sk, def_defn_20, def_defn_30])).
% 227.33/41.79 cnf(c_947, plain, vreduce(A) != B | vvar(sK0(A,B)) = A | vabs(sK1(A,B),sK2(A,B),sK3(A,B)) = A | vsomeExp(vapp(vabs(sK4(A,B),sK5(A,B),sK6(A,B)),vgetSomeExp(sK7(A,B)))) = B | defn_20(A,B) | defn_30(A,B) | vsomeExp(vapp(vgetSomeExp(sK8(A,B)),sK9(A,B))) = B | vapp(sK10(A,B),sK11(A,B)) = A, inference(split_conjunct, [status(thm)], [sk_reduce-INV])).
% 227.33/41.79 cnf(c_980, plain, ~defn_30(A,B) | vapp(vabs(sK12(A,B),sK13(A,B),sK14(A,B)),sK15(A,B)) = A, inference(split_conjunct, [status(thm)], [sk_reduce-INV])).
% 227.33/41.79 cnf(c_985, plain, ~defn_20(A,B) | vapp(vabs(sK16(A,B),sK17(A,B),sK18(A,B)),sK19(A,B)) = A, inference(split_conjunct, [status(thm)], [sk_reduce-INV])).
% 227.33/41.79 cnf(c_989, plain, vlookup(A,B) != vsomeType(C) | vtcheck(B,vvar(A),C), inference(clausify, [status(thm)], [T-var])).
% 227.33/41.79 fof(nnf_54, plain, ! [Ve,VT,VC] : (~ (vtcheck(VC,Ve,VT)) | ? [X16] : (vvar(X16) = Ve & vlookup(X16,VC) = vsomeType(VT)) | ? [Vx,X15,VT1,VT2] : (vabs(Vx,VT1,X15) = Ve & varrow(VT1,VT2) = VT & vtcheck(vbind(Vx,VT1,VC),X15,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])).
% 227.33/41.79 fof(sk_T-inv_sk, plain, ! [Ve,VT,VC] : (~ (vtcheck(VC,Ve,VT)) | (vvar(sK20(Ve,VT,VC)) = Ve & vlookup(sK20(Ve,VT,VC),VC) = vsomeType(VT)) | (vabs(sK21(Ve,VT,VC),sK22(Ve,VT,VC),sK23(Ve,VT,VC)) = Ve & varrow(sK22(Ve,VT,VC),sK44(Ve,VT,VC)) = VT & vtcheck(vbind(sK21(Ve,VT,VC),sK22(Ve,VT,VC),VC),sK23(Ve,VT,VC),sK44(Ve,VT,VC))) | (vapp(sK24(Ve,VT,VC),sK25(Ve,VT,VC)) = Ve & vtcheck(VC,sK24(Ve,VT,VC),varrow(sK45(Ve,VT,VC),VT)) & vtcheck(VC,sK25(Ve,VT,VC),sK45(Ve,VT,VC)))), inference(skolemize, [status(esa), new_symbols(skolem, [sK20,sK21,sK22,sK23,sK44,sK24,sK25,sK45]), skolemize(X16,sK20(Ve,VT,VC)), skolemize(Vx,sK21(Ve,VT,VC)), skolemize(X15,sK23(Ve,VT,VC)), skolemize(VT1,sK22(Ve,VT,VC)), skolemize(VT2,sK44(Ve,VT,VC)), skolemize(Ve1,sK24(Ve,VT,VC)), skolemize(Ve2,sK25(Ve,VT,VC)), skolemize(VS,sK45(Ve,VT,VC))], [nnf_54])).
% 227.33/41.79 fof(sk_T-inv, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),sK23(VAR_1,VAR_2,VAR_0)) = VAR_1 | vapp(sK24(VAR_1,VAR_2,VAR_0),sK25(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),sK23(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK24(VAR_1,VAR_2,VAR_0),varrow(sK45(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | vabs(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),sK23(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK25(VAR_1,VAR_2,VAR_0),sK45(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK22(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) = VAR_2 | vapp(sK24(VAR_1,VAR_2,VAR_0),sK25(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK22(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK24(VAR_1,VAR_2,VAR_0),varrow(sK45(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | varrow(sK22(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK25(VAR_1,VAR_2,VAR_0),sK45(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),VAR_0),sK23(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) | vapp(sK24(VAR_1,VAR_2,VAR_0),sK25(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),VAR_0),sK23(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK24(VAR_1,VAR_2,VAR_0),varrow(sK45(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vvar(sK20(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(vbind(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),VAR_0),sK23(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK25(VAR_1,VAR_2,VAR_0),sK45(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),sK23(VAR_1,VAR_2,VAR_0)) = VAR_1 | vapp(sK24(VAR_1,VAR_2,VAR_0),sK25(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),sK23(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK24(VAR_1,VAR_2,VAR_0),varrow(sK45(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vabs(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),sK23(VAR_1,VAR_2,VAR_0)) = VAR_1 | vtcheck(VAR_0,sK25(VAR_1,VAR_2,VAR_0),sK45(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK22(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) = VAR_2 | vapp(sK24(VAR_1,VAR_2,VAR_0),sK25(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK22(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK24(VAR_1,VAR_2,VAR_0),varrow(sK45(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | varrow(sK22(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) = VAR_2 | vtcheck(VAR_0,sK25(VAR_1,VAR_2,VAR_0),sK45(VAR_1,VAR_2,VAR_0))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),VAR_0),sK23(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) | vapp(sK24(VAR_1,VAR_2,VAR_0),sK25(VAR_1,VAR_2,VAR_0)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),VAR_0),sK23(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK24(VAR_1,VAR_2,VAR_0),varrow(sK45(VAR_1,VAR_2,VAR_0),VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vtcheck(VAR_0,VAR_1,VAR_2)) | vlookup(sK20(VAR_1,VAR_2,VAR_0),VAR_0) = vsomeType(VAR_2) | vtcheck(vbind(sK21(VAR_1,VAR_2,VAR_0),sK22(VAR_1,VAR_2,VAR_0),VAR_0),sK23(VAR_1,VAR_2,VAR_0),sK44(VAR_1,VAR_2,VAR_0)) | vtcheck(VAR_0,sK25(VAR_1,VAR_2,VAR_0),sK45(VAR_1,VAR_2,VAR_0)))), inference(cnf_transformation, [status(thm)], [sk_T-inv_sk])).
% 227.33/41.79 cnf(c_992, plain, ~vtcheck(A,B,C) | vvar(sK20(B,C,A)) = B | vabs(sK21(B,C,A),sK22(B,C,A),sK23(B,C,A)) = B | vapp(sK24(B,C,A),sK25(B,C,A)) = B, inference(split_conjunct, [status(thm)], [sk_T-inv])).
% 227.33/41.79 cnf(c_1001, plain, ~vtcheck(A,B,C) | vlookup(sK20(B,C,A),A) = vsomeType(C) | vabs(sK21(B,C,A),sK22(B,C,A),sK23(B,C,A)) = B | vapp(sK24(B,C,A),sK25(B,C,A)) = B, inference(split_conjunct, [status(thm)], [sk_T-inv])).
% 227.33/41.79 cnf(c_1011, plain, visFreeVar(A,B) | ~vtcheck(vbind(A,C,D),B,E) | vtcheck(D,B,E), inference(clausify, [status(thm)], [T-Strong])).
% 227.33/41.79 fof(nnf_58, plain, ? [VT,VC,Vx,Ve,Vy,VT2] : (vtcheck(VC,Ve,VT) & vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2) & ~ (vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2))), inference(fof_nnf, [status(thm)], [T-subst-var_neg])).
% 227.33/41.79 fof(sk_T-subst-var_neg, plain, (vtcheck(sK26,sK27,sK28) & vtcheck(vbind(sK29,sK28,sK26),vvar(sK30),sK31) & ~ (vtcheck(sK26,vsubst(sK29,sK27,vvar(sK30)),sK31))), inference(skolemize, [status(esa), new_symbols(skolem, [sK26,sK27,sK28,sK29,sK30,sK31]), skolemize(VT,sK28), skolemize(VC,sK26), skolemize(Vx,sK29), skolemize(Ve,sK27), skolemize(Vy,sK30), skolemize(VT2,sK31)], [nnf_58])).
% 227.33/41.79 cnf(c_1013, negated_conjecture, vtcheck(sK26,sK27,sK28), inference(split_conjunct, [status(thm)], [sk_T-subst-var_neg])).
% 227.33/41.79 cnf(c_1014, negated_conjecture, vtcheck(vbind(sK29,sK28,sK26),vvar(sK30),sK31), inference(split_conjunct, [status(thm)], [sk_T-subst-var_neg])).
% 227.33/41.79 cnf(c_1015, negated_conjecture, ~vtcheck(sK26,vsubst(sK29,sK27,vvar(sK30)),sK31), inference(split_conjunct, [status(thm)], [sk_T-subst-var_neg])).
% 227.33/41.79 cnf(c_1151, plain, A != B | C != D | vvar(E) != F | E = A | vsubst(B,D,F) != V6 | vvar(E) = V6, inference(clausify, [status(thm)], [subst1])).
% 227.33/41.79 cnf(c_1152, plain, A != B | vvar(C) != D | C = A | vsubst(B,E,D) != F | vvar(C) = F,
% 227.33/41.79 inference(copy, [status(thm)], [c_1151])).
% 227.33/41.79 cnf(c_1153, plain, A != B | C != D | vvar(E) != F | E != A | vsubst(B,D,F) != V6 | V6 = C, inference(clausify, [status(thm)], [subst0])).
% 227.33/41.79 fof(nnf_25, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | ? [X19] : (X19 = VVar0 & VCtx0 = vempty & RESULT = vnoType) | ? [X15,X16,X17,X18] : (X16 = VVar0 & vbind(X17,X18,X15) = VCtx0 & X17 = X16 & vsomeType(X18) = 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])).
% 227.33/41.79 fof(sk_lookup-INV_sk, plain, ! [VVar0,VCtx0,RESULT] : (~ (vlookup(VVar0,VCtx0) = RESULT) | (sK32(VVar0,VCtx0,RESULT) = VVar0 & VCtx0 = vempty & RESULT = vnoType) | (sK46(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK33(VVar0,VCtx0,RESULT),sK34(VVar0,VCtx0,RESULT),sK35(VVar0,VCtx0,RESULT)) = VCtx0 & sK33(VVar0,VCtx0,RESULT) = sK46(VVar0,VCtx0,RESULT) & vsomeType(sK34(VVar0,VCtx0,RESULT)) = RESULT) | (sK47(VVar0,VCtx0,RESULT) = VVar0 & vbind(sK36(VVar0,VCtx0,RESULT),sK37(VVar0,VCtx0,RESULT),sK38(VVar0,VCtx0,RESULT)) = VCtx0 & ~ (sK36(VVar0,VCtx0,RESULT) = sK47(VVar0,VCtx0,RESULT)) & vlookup(sK47(VVar0,VCtx0,RESULT),sK38(VVar0,VCtx0,RESULT)) = RESULT)), inference(skolemize, [status(esa), new_symbols(skolem, [sK32,sK46,sK33,sK34,sK35,sK47,sK36,sK37,sK38]), skolemize(X19,sK32(VVar0,VCtx0,RESULT)), skolemize(X15,sK35(VVar0,VCtx0,RESULT)), skolemize(X16,sK46(VVar0,VCtx0,RESULT)), skolemize(X17,sK33(VVar0,VCtx0,RESULT)), skolemize(X18,sK34(VVar0,VCtx0,RESULT)), skolemize(VTy,sK37(VVar0,VCtx0,RESULT)), skolemize(Vy,sK36(VVar0,VCtx0,RESULT)), skolemize(Vx,sK47(VVar0,VCtx0,RESULT)), skolemize(VC,sK38(VVar0,VCtx0,RESULT))], [nnf_25])).
% 227.33/41.79 fof(sk_lookup-INV, plain, (! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | sK32(VAR_0,VAR_1,VAR_2) = VAR_0 | vsomeType(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(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(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK47(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(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(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(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vbind(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(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(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK47(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(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(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(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_1 = vempty | vsomeType(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK46(VAR_0,VAR_1,VAR_2) = VAR_0 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(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(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | sK47(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(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(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(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vbind(sK33(VAR_0,VAR_1,VAR_2),sK34(VAR_0,VAR_1,VAR_2),sK35(VAR_0,VAR_1,VAR_2)) = VAR_1 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | sK47(VAR_0,VAR_1,VAR_2) = VAR_0) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_1) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | sK33(VAR_0,VAR_1,VAR_2) = sK46(VAR_0,VAR_1,VAR_2) | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(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(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | sK47(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(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | vbind(sK36(VAR_0,VAR_1,VAR_2),sK37(VAR_0,VAR_1,VAR_2),sK38(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(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | ~ (sK36(VAR_0,VAR_1,VAR_2) = sK47(VAR_0,VAR_1,VAR_2))) & ! [VAR_0,VAR_1,VAR_2] : (~ (vlookup(VAR_0,VAR_1) = VAR_2) | VAR_2 = vnoType | vsomeType(sK34(VAR_0,VAR_1,VAR_2)) = VAR_2 | vlookup(sK47(VAR_0,VAR_1,VAR_2),sK38(VAR_0,VAR_1,VAR_2)) = VAR_2)), inference(cnf_transformation, [status(thm)], [sk_lookup-INV_sk])).
% 227.33/41.79 cnf(c_1234, plain, vlookup(A,B) != C | sK32(A,B,C) = A | vbind(sK33(A,B,C),sK34(A,B,C),sK35(A,B,C)) = B | vbind(sK36(A,B,C),sK37(A,B,C),sK38(A,B,C)) = B, inference(split_conjunct, [status(thm)], [sk_lookup-INV])).
% 227.33/41.79 cnf(c_1242, plain, A != B | vbind(C,D,E) != F | C != A | vlookup(B,F) != V6 | vsomeType(D) = V6, inference(clausify, [status(thm)], [lookup1])).
% 227.33/41.79 cnf(c_1243, plain, A != B | C != vempty | vlookup(B,C) != D | D = vnoType, inference(clausify, [status(thm)], [lookup0])).
% 227.33/41.79 cnf(c_23359, plain, A != B | vempty != C | vlookup(B,C) != D | D = vnoType,
% 227.33/41.79 inference(copy, [status(thm)], [c_1243])).
% 227.33/41.79 cnf(c_23360, plain, A != B | vempty != C | vlookup(B,C) != D | vnoType = D,
% 227.33/41.79 inference(copy, [status(thm)], [c_23359])).
% 227.33/41.79 cnf(c_1244, plain, vempty != A | vlookup(B,A) != C | vnoType = C,
% 227.33/41.79 inference(copy, [status(thm)], [c_23360])).
% 227.33/41.79 cnf(c_1245, plain, vsomeType(A) != B | vgetSomeType(B) != C | C = A, inference(clausify, [status(thm)], [getSomeType0])).
% 227.33/41.79 cnf(c_1247, plain, vbind(A,B,C) != vempty, inference(clausify, [status(thm)], [DIFF-empty-bind])).
% 227.33/41.79 cnf(c_1260, plain, A != B | vvar(C) != D | ~visFreeVar(B,D) | A = C, inference(clausify, [status(thm)], [isFreeVar0])).
% 227.33/41.79 cnf(c_1261, plain, A != B | vvar(C) != D | A != C | visFreeVar(B,D), inference(clausify, [status(thm)], [isFreeVar0])).
% 227.33/41.79 cnf(c_1266, plain, vapp(A,B) != vvar(C), inference(clausify, [status(thm)], [DIFF-var-app])).
% 227.33/41.79 cnf(c_1267, plain, vabs(A,B,C) != vvar(D), inference(clausify, [status(thm)], [DIFF-var-abs])).
% 227.33/41.79 cnf(c_4885, plain, vgetSomeExp(vsomeExp(A)) != B | B = A,
% 227.33/41.79 inference(xxres, [status(thm)], [c_832])).
% 227.33/41.79 cnf(c_4887, plain, vreduce(vvar(A)) != B | vnoExp = B,
% 227.33/41.79 inference(xxres, [status(thm)], [c_833])).
% 227.33/41.79 cnf(c_5001, plain, visFreeVar(sK29,vvar(sK30)) | vtcheck(sK26,vvar(sK30),sK31),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1014, c_1011])).
% 227.33/41.79 cnf(c_23361, negated_conjecture, vlookup(sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),vbind(sK29,sK28,sK26)) = vsomeType(sK31) | vabs(sK21(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK22(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK23(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30) | vapp(sK24(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK25(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1014, c_1001])).
% 227.33/41.79 cnf(c_23362, negated_conjecture, vlookup(sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),vbind(sK29,sK28,sK26)) = vsomeType(sK31) | vapp(sK24(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK25(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1267, c_23361])).
% 227.33/41.79 cnf(c_5011, negated_conjecture, vlookup(sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),vbind(sK29,sK28,sK26)) = vsomeType(sK31),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1266, c_23362])).
% 227.33/41.79 cnf(c_23363, negated_conjecture, vvar(sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30) | vabs(sK21(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK22(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK23(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30) | vapp(sK24(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK25(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1014, c_992])).
% 227.33/41.79 cnf(c_23364, negated_conjecture, vvar(sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30) | vapp(sK24(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),sK25(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1267, c_23363])).
% 227.33/41.79 cnf(c_5020, negated_conjecture, vvar(sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26))) = vvar(sK30),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1266, c_23364])).
% 227.33/41.79 cnf(c_5146, plain, vvar(A) != B | A = C | vsubst(C,D,B) != E | vvar(A) = E,
% 227.33/41.79 inference(xxres, [status(thm)], [c_1152])).
% 227.33/41.79 cnf(c_5154, plain, A != B | vvar(C) != D | C != A | vsubst(B,E,D) != F | F = E,
% 227.33/41.79 inference(xxres, [status(thm)], [c_1153])).
% 227.33/41.79 cnf(c_5155, plain, A != B | C != D | E != A | vsubst(B,D,vvar(E)) != F | F = C,
% 227.33/41.79 inference(xxres, [status(thm)], [c_1153])).
% 227.33/41.79 cnf(c_23365, plain, A != A | vvar(A) != B | vsubst(A,C,B) != D | D = C,
% 227.33/41.79 inference(factor, [status(thm)], [c_5154])).
% 227.33/41.79 cnf(c_5161, plain, vvar(A) != B | vsubst(A,C,B) != D | D = C,
% 227.33/41.79 inference(copy, [status(thm)], [c_23365])).
% 227.33/41.79 cnf(c_5164, plain, A != B | C != A | vsubst(B,B,vvar(C)) != D | D = A,
% 227.33/41.79 inference(factor, [status(thm)], [c_5155])).
% 227.33/41.79 cnf(c_23366, plain, A != A | vsubst(A,A,vvar(A)) != B | B = A,
% 227.33/41.79 inference(factor, [status(thm)], [c_5164])).
% 227.33/41.79 cnf(c_5175, plain, vsubst(A,A,vvar(A)) != B | B = A,
% 227.33/41.79 inference(copy, [status(thm)], [c_23366])).
% 227.33/41.79 cnf(c_5227, plain, A != B | C != A | vlookup(B,vbind(C,D,E)) != F | vsomeType(D) = F,
% 227.33/41.79 inference(xxres, [status(thm)], [c_1242])).
% 227.33/41.79 cnf(c_23367, plain, A != A | vlookup(A,vbind(A,B,C)) != D | vsomeType(B) = D,
% 227.33/41.79 inference(factor, [status(thm)], [c_5227])).
% 227.33/41.79 cnf(c_5230, plain, vlookup(A,vbind(A,B,C)) != D | vsomeType(B) = D,
% 227.33/41.79 inference(copy, [status(thm)], [c_23367])).
% 227.33/41.79 cnf(c_23368, plain, vempty != A | vnoType = vlookup(B,A),
% 227.33/41.79 inference(xxres, [status(thm)], [c_1244])).
% 227.33/41.79 cnf(c_5234, plain, vempty != A | vlookup(B,A) = vnoType,
% 227.33/41.79 inference(copy, [status(thm)], [c_23368])).
% 227.33/41.79 cnf(c_5235, plain, vgetSomeType(vsomeType(A)) != B | B = A,
% 227.33/41.79 inference(xxres, [status(thm)], [c_1245])).
% 227.33/41.79 cnf(c_5244, plain, A != B | A != C | visFreeVar(B,vvar(C)),
% 227.33/41.79 inference(xxres, [status(thm)], [c_1261])).
% 227.33/41.79 cnf(c_23369, plain, A != B | visFreeVar(B,vvar(B)),
% 227.33/41.79 inference(factor, [status(thm)], [c_5244])).
% 227.33/41.79 cnf(c_5247, plain, visFreeVar(A,vvar(A)),
% 227.33/41.79 inference(copy, [status(thm)], [c_23369])).
% 227.33/41.79 cnf(c_6225, plain, A != B | vvar(C) != vvar(B) | A = C,
% 227.33/41.79 inference(resolve, [status(thm)], [c_5247, c_1260])).
% 227.33/41.79 cnf(c_6232, plain, vgetSomeExp(vsomeExp(A)) = A,
% 227.33/41.79 inference(xxres, [status(thm)], [c_4885])).
% 227.33/41.79 cnf(c_23370, plain, A = vgetSomeExp(vsomeExp(A)),
% 227.33/41.79 inference(copy, [status(thm)], [c_6232])).
% 227.33/41.79 cnf(c_23371, plain, vnoExp = vgetSomeExp(vsomeExp(vreduce(vvar(A)))),
% 227.33/41.79 inference(resolve, [status(thm)], [c_4887, c_23370])).
% 227.33/41.79 cnf(c_23372, plain, vnoExp = vreduce(vvar(A)),
% 227.33/41.79 inference(paramod, [status(thm)], [c_6232, c_23371])).
% 227.33/41.79 cnf(c_6242, plain, vreduce(vvar(A)) = vnoExp,
% 227.33/41.79 inference(copy, [status(thm)], [c_23372])).
% 227.33/41.79 cnf(c_23373, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | vabs(sK1(vvar(A),vnoExp),sK2(vvar(A),vnoExp),sK3(vvar(A),vnoExp)) = vvar(A) | vsomeExp(vapp(vabs(sK4(vvar(A),vnoExp),sK5(vvar(A),vnoExp),sK6(vvar(A),vnoExp)),vgetSomeExp(sK7(vvar(A),vnoExp)))) = vnoExp | defn_20(vvar(A),vnoExp) | defn_30(vvar(A),vnoExp) | vsomeExp(vapp(vgetSomeExp(sK8(vvar(A),vnoExp)),sK9(vvar(A),vnoExp))) = vnoExp | vapp(sK10(vvar(A),vnoExp),sK11(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_6242, c_947])).
% 227.33/41.79 cnf(c_23374, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | vsomeExp(vapp(vabs(sK4(vvar(A),vnoExp),sK5(vvar(A),vnoExp),sK6(vvar(A),vnoExp)),vgetSomeExp(sK7(vvar(A),vnoExp)))) = vnoExp | defn_20(vvar(A),vnoExp) | defn_30(vvar(A),vnoExp) | vsomeExp(vapp(vgetSomeExp(sK8(vvar(A),vnoExp)),sK9(vvar(A),vnoExp))) = vnoExp | vapp(sK10(vvar(A),vnoExp),sK11(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1267, c_23373])).
% 227.33/41.79 cnf(c_23375, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | defn_20(vvar(A),vnoExp) | defn_30(vvar(A),vnoExp) | vsomeExp(vapp(vgetSomeExp(sK8(vvar(A),vnoExp)),sK9(vvar(A),vnoExp))) = vnoExp | vapp(sK10(vvar(A),vnoExp),sK11(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_828, c_23374])).
% 227.33/41.79 cnf(c_23376, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | defn_20(vvar(A),vnoExp) | defn_30(vvar(A),vnoExp) | vapp(sK10(vvar(A),vnoExp),sK11(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_828, c_23375])).
% 227.33/41.79 cnf(c_6264, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | defn_20(vvar(A),vnoExp) | defn_30(vvar(A),vnoExp),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1266, c_23376])).
% 227.33/41.79 cnf(c_23377, plain, A = vgetSomeExp(vsomeExp(A)),
% 227.33/41.79 inference(copy, [status(thm)], [c_6232])).
% 227.33/41.79 cnf(c_23378, plain, vlookup(A,vgetSomeExp(vsomeExp(vempty))) = vnoType,
% 227.33/41.79 inference(resolve, [status(thm)], [c_5234, c_23377])).
% 227.33/41.79 cnf(c_6271, plain, vlookup(A,vempty) = vnoType,
% 227.33/41.79 inference(paramod, [status(thm)], [c_6232, c_23378])).
% 227.33/41.79 cnf(c_23379, plain, sK32(A,vempty,vnoType) = A | vbind(sK33(A,vempty,vnoType),sK34(A,vempty,vnoType),sK35(A,vempty,vnoType)) = vempty | vbind(sK36(A,vempty,vnoType),sK37(A,vempty,vnoType),sK38(A,vempty,vnoType)) = vempty,
% 227.33/41.79 inference(resolve, [status(thm)], [c_6271, c_1234])).
% 227.33/41.79 cnf(c_23380, plain, sK32(A,vempty,vnoType) = A | vbind(sK36(A,vempty,vnoType),sK37(A,vempty,vnoType),sK38(A,vempty,vnoType)) = vempty,
% 227.33/41.79 inference(resolve, [status(thm)], [c_1247, c_23379])).
% 227.33/41.79 cnf(c_6288, plain, sK32(A,vempty,vnoType) = A,
% 227.33/41.79 inference(resolve, [status(thm)], [c_1247, c_23380])).
% 227.33/41.79 cnf(c_23381, plain, A = sK32(A,vempty,vnoType),
% 227.33/41.79 inference(copy, [status(thm)], [c_6288])).
% 227.33/41.79 cnf(c_23382, plain, sK32(vgetSomeType(vsomeType(A)),vempty,vnoType) = A,
% 227.33/41.79 inference(resolve, [status(thm)], [c_5235, c_23381])).
% 227.33/41.79 cnf(c_6304, plain, vgetSomeType(vsomeType(A)) = A,
% 227.33/41.79 inference(paramod, [status(thm)], [c_6288, c_23382])).
% 227.33/41.79 cnf(c_6305, plain, vsomeType(A) != vsomeType(B) | B = A,
% 227.33/41.79 inference(resolve, [status(thm)], [c_6304, c_1245])).
% 227.33/41.79 cnf(c_23383, plain, A = vgetSomeType(vsomeType(A)),
% 227.33/41.79 inference(copy, [status(thm)], [c_6304])).
% 227.33/41.79 cnf(c_23384, plain, vgetSomeType(vsomeType(vsubst(A,A,vvar(A)))) = A,
% 227.33/41.79 inference(resolve, [status(thm)], [c_5175, c_23383])).
% 227.33/41.79 cnf(c_6387, plain, vsubst(A,A,vvar(A)) = A,
% 227.33/41.79 inference(paramod, [status(thm)], [c_6304, c_23384])).
% 227.33/41.79 cnf(c_23385, plain, vvar(A) != vvar(B) | vsubst(B,B,vvar(B)) = A,
% 227.33/41.79 inference(resolve, [status(thm)], [c_6225, c_6387])).
% 227.33/41.79 cnf(c_7825, plain, vvar(A) != vvar(B) | B = A,
% 227.33/41.79 inference(paramod, [status(thm)], [c_6387, c_23385])).
% 227.33/41.79 cnf(c_23386, plain, sK30 = sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26)),
% 227.33/41.79 inference(resolve, [status(thm)], [c_5020, c_7825])).
% 227.33/41.79 cnf(c_7851, plain, sK20(vvar(sK30),sK31,vbind(sK29,sK28,sK26)) = sK30,
% 227.33/41.79 inference(copy, [status(thm)], [c_23386])).
% 227.33/41.79 cnf(c_7860, negated_conjecture, vlookup(sK30,vbind(sK29,sK28,sK26)) = vsomeType(sK31),
% 227.33/41.79 inference(paramod, [status(thm)], [c_7851, c_5011])).
% 227.33/41.79 cnf(c_23387, plain, A = vsubst(A,A,vvar(A)),
% 227.33/41.79 inference(copy, [status(thm)], [c_6387])).
% 227.33/41.79 cnf(c_23388, plain, vsomeType(A) = vsubst(vlookup(B,vbind(B,A,C)),vlookup(B,vbind(B,A,C)),vvar(vlookup(B,vbind(B,A,C)))),
% 227.33/41.79 inference(resolve, [status(thm)], [c_5230, c_23387])).
% 227.33/41.79 cnf(c_23389, plain, vsomeType(A) = vlookup(B,vbind(B,A,C)),
% 227.33/41.79 inference(paramod, [status(thm)], [c_6387, c_23388])).
% 227.33/41.79 cnf(c_7966, plain, vlookup(A,vbind(A,B,C)) = vsomeType(B),
% 227.33/41.79 inference(copy, [status(thm)], [c_23389])).
% 227.33/41.79 cnf(c_8017, plain, vtcheck(vbind(A,B,C),vvar(A),B),
% 227.33/41.79 inference(resolve, [status(thm)], [c_7966, c_989])).
% 227.33/41.79 cnf(c_23390, plain, vvar(sK20(vvar(A),B,vbind(A,B,C))) = vvar(A) | vabs(sK21(vvar(A),B,vbind(A,B,C)),sK22(vvar(A),B,vbind(A,B,C)),sK23(vvar(A),B,vbind(A,B,C))) = vvar(A) | vapp(sK24(vvar(A),B,vbind(A,B,C)),sK25(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_8017, c_992])).
% 227.33/41.79 cnf(c_23391, plain, vvar(sK20(vvar(A),B,vbind(A,B,C))) = vvar(A) | vapp(sK24(vvar(A),B,vbind(A,B,C)),sK25(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1267, c_23390])).
% 227.33/41.79 cnf(c_8072, plain, vvar(sK20(vvar(A),B,vbind(A,B,C))) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1266, c_23391])).
% 227.33/41.79 cnf(c_23392, plain, A = sK20(vvar(A),B,vbind(A,B,C)),
% 227.33/41.79 inference(resolve, [status(thm)], [c_8072, c_7825])).
% 227.33/41.79 cnf(c_8236, plain, sK20(vvar(A),B,vbind(A,B,C)) = A,
% 227.33/41.79 inference(copy, [status(thm)], [c_23392])).
% 227.33/41.79 cnf(c_23393, plain, A = sK20(vvar(A),B,vbind(A,B,C)),
% 227.33/41.79 inference(copy, [status(thm)], [c_8236])).
% 227.33/41.79 cnf(c_23394, plain, vvar(A) != B | sK20(vvar(vsubst(A,C,B)),D,vbind(vsubst(A,C,B),D,E)) = C,
% 227.33/41.79 inference(resolve, [status(thm)], [c_5161, c_23393])).
% 227.33/41.79 cnf(c_8259, plain, vvar(A) != B | vsubst(A,C,B) = C,
% 227.33/41.79 inference(paramod, [status(thm)], [c_8236, c_23394])).
% 227.33/41.79 cnf(c_23395, plain, A = sK20(vvar(A),B,vbind(A,B,C)),
% 227.33/41.79 inference(copy, [status(thm)], [c_8236])).
% 227.33/41.79 cnf(c_23396, plain, vsubst(A,B,sK20(vvar(vvar(A)),C,vbind(vvar(A),C,D))) = B,
% 227.33/41.79 inference(resolve, [status(thm)], [c_8259, c_23395])).
% 227.33/41.79 cnf(c_8260, plain, vsubst(A,B,vvar(A)) = B,
% 227.33/41.79 inference(paramod, [status(thm)], [c_8236, c_23396])).
% 227.33/41.79 cnf(c_23397, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | defn_20(vvar(A),vnoExp) | vapp(vabs(sK12(vvar(A),vnoExp),sK13(vvar(A),vnoExp),sK14(vvar(A),vnoExp)),sK15(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_6264, c_980])).
% 227.33/41.79 cnf(c_15550, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | defn_20(vvar(A),vnoExp),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1266, c_23397])).
% 227.33/41.79 cnf(c_23398, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A) | vapp(vabs(sK16(vvar(A),vnoExp),sK17(vvar(A),vnoExp),sK18(vvar(A),vnoExp)),sK19(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_15550, c_985])).
% 227.33/41.79 cnf(c_15551, plain, vvar(sK0(vvar(A),vnoExp)) = vvar(A),
% 227.33/41.79 inference(resolve, [status(thm)], [c_1266, c_23398])).
% 227.33/41.79 cnf(c_23399, plain, A = sK0(vvar(A),vnoExp),
% 227.33/41.79 inference(resolve, [status(thm)], [c_15551, c_7825])).
% 227.33/41.79 cnf(c_15564, plain, sK0(vvar(A),vnoExp) = A,
% 227.33/41.79 inference(copy, [status(thm)], [c_23399])).
% 227.33/41.79 cnf(c_23400, plain, A = sK0(vvar(A),vnoExp),
% 227.33/41.79 inference(copy, [status(thm)], [c_15564])).
% 227.33/41.79 cnf(c_23401, plain, A = B | vsubst(B,C,sK0(vvar(vvar(A)),vnoExp)) != D | vvar(A) = D,
% 227.33/41.79 inference(resolve, [status(thm)], [c_5146, c_23400])).
% 227.33/41.79 cnf(c_17133, plain, A = B | vsubst(B,C,vvar(A)) != D | vvar(A) = D,
% 227.33/41.79 inference(paramod, [status(thm)], [c_15564, c_23401])).
% 227.33/41.79 cnf(c_23402, plain, A = sK0(vvar(A),vnoExp),
% 227.33/41.79 inference(copy, [status(thm)], [c_15564])).
% 227.33/41.79 cnf(c_23403, plain, A = B | vvar(A) = sK0(vvar(vsubst(B,C,vvar(A))),vnoExp),
% 227.33/41.79 inference(resolve, [status(thm)], [c_17133, c_23402])).
% 227.33/41.79 cnf(c_23404, plain, A = B | vvar(A) = vsubst(B,C,vvar(A)),
% 227.33/41.79 inference(paramod, [status(thm)], [c_15564, c_23403])).
% 227.33/41.79 cnf(c_17151, plain, A = B | vsubst(B,C,vvar(A)) = vvar(A),
% 227.33/41.79 inference(copy, [status(thm)], [c_23404])).
% 227.33/41.79 cnf(c_17972, plain, sK30 = sK29 | ~vtcheck(sK26,vvar(sK30),sK31),
% 227.33/41.79 inference(paramod, [status(thm)], [c_17151, c_1015])).
% 227.33/41.79 cnf(c_18344, plain, sK30 = sK29 | visFreeVar(sK29,vvar(sK30)),
% 227.33/41.79 inference(resolve, [status(thm)], [c_17972, c_5001])).
% 227.33/41.79 cnf(c_23405, plain, sK30 = sK29 | A != sK29 | vvar(B) != vvar(sK30) | A = B,
% 227.33/41.79 inference(resolve, [status(thm)], [c_18344, c_1260])).
% 227.33/41.79 cnf(c_23406, plain, sK30 = sK29 | sK29 != A | vvar(B) != vvar(sK30) | A = B,
% 227.33/41.79 inference(copy, [status(thm)], [c_23405])).
% 227.33/41.79 cnf(c_18348, plain, sK30 = sK29 | sK29 != A | vvar(sK30) != vvar(B) | A = B,
% 227.33/41.79 inference(copy, [status(thm)], [c_23406])).
% 227.33/41.79 cnf(c_23407, plain, sK30 = sK29 | sK29 != A | A = sK30,
% 227.33/41.79 inference(xxres, [status(thm)], [c_18348])).
% 227.33/41.79 cnf(c_23004, plain, sK30 = sK29 | sK29 != A | sK30 = A,
% 227.33/41.79 inference(copy, [status(thm)], [c_23407])).
% 227.33/41.79 cnf(c_23408, plain, sK30 = sK29 | sK29 != sK29,
% 227.33/41.79 inference(factor, [status(thm)], [c_23004])).
% 227.33/41.79 cnf(c_23010, plain, sK30 = sK29,
% 227.33/41.79 inference(copy, [status(thm)], [c_23408])).
% 227.33/41.79 cnf(c_23409, negated_conjecture, vlookup(sK29,vbind(sK29,sK28,sK26)) = vsomeType(sK31),
% 227.33/41.79 inference(paramod, [status(thm)], [c_23010, c_7860])).
% 227.33/41.79 cnf(c_23410, negated_conjecture, vsomeType(sK28) = vsomeType(sK31),
% 227.33/41.79 inference(paramod, [status(thm)], [c_7966, c_23409])).
% 227.33/41.79 cnf(c_23304, negated_conjecture, vsomeType(sK31) = vsomeType(sK28),
% 227.33/41.79 inference(copy, [status(thm)], [c_23410])).
% 227.33/41.79 cnf(c_23411, negated_conjecture, ~vtcheck(sK26,vsubst(sK29,sK27,vvar(sK29)),sK31),
% 227.33/41.79 inference(paramod, [status(thm)], [c_23010, c_1015])).
% 227.33/41.79 cnf(c_23332, negated_conjecture, ~vtcheck(sK26,sK27,sK31),
% 227.33/41.79 inference(paramod, [status(thm)], [c_8260, c_23411])).
% 227.33/41.79 cnf(c_23412, plain, sK28 = sK31,
% 227.33/41.79 inference(resolve, [status(thm)], [c_23304, c_6305])).
% 227.33/41.79 cnf(c_23352, plain, sK31 = sK28,
% 227.33/41.79 inference(copy, [status(thm)], [c_23412])).
% 227.33/41.79 cnf(c_23413, negated_conjecture, ~vtcheck(sK26,sK27,sK28),
% 227.33/41.79 inference(paramod, [status(thm)], [c_23352, c_23332])).
% 227.33/41.79 cnf(c_23358, negated_conjecture, $false,
% 227.33/41.79 inference(resolve, [status(thm)], [c_1013, c_23413])).
% 227.33/41.79 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------