%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM134+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Thu Sep 24 12:10:51 PM UTC 2026
% Result : Theorem 57.78s 7.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM134+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n011.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 14:18:10 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 57.78/7.74 % Refutation found
% 57.78/7.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.78/7.74 % SZS output start CNFRefutation for theBenchmark
% 57.78/7.74 fof(f1,axiom,(
% 57.78/7.74 (! [VVar0,VVar1] :( ( vvar(VVar0) = vvar(VVar1)=> VVar0 = VVar1 )& ( VVar0 = VVar1=> vvar(VVar0) = vvar(VVar1) ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f3,axiom,(
% 57.78/7.74 (! [VExp0,VExp1,VExp2,VExp3] :( ( vapp(VExp0,VExp1) = vapp(VExp2,VExp3)=> ( VExp0 = VExp2& VExp1 = VExp3 ) )& ( ( VExp0 = VExp2& VExp1 = VExp3 )=> vapp(VExp0,VExp1) = vapp(VExp2,VExp3) ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f4,axiom,(
% 57.78/7.74 (! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f5,axiom,(
% 57.78/7.74 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f6,axiom,(
% 57.78/7.74 (! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f9,axiom,(
% 57.78/7.74 (! [Ve1,Ve2,VExp0] :( VExp0 = vapp(Ve1,Ve2)=> ~ visValue(VExp0) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f17,axiom,(
% 57.78/7.74 (! [VVar0,VTyp0,VCtx0] : vempty != vbind(VVar0,VTyp0,VCtx0) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f21,axiom,(
% 57.78/7.74 (! [VOptTyp0,RESULT,Ve] :( VOptTyp0 = vsomeType(Ve)=> ( RESULT = vgetSomeType(VOptTyp0)=> RESULT = Ve ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f22,axiom,(
% 57.78/7.74 (! [Vx,VVar0,VCtx0,RESULT] :( ( VVar0 = Vx& VCtx0 = vempty )=> ( RESULT = vlookup(VVar0,VCtx0)=> RESULT = vnoType ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f25,axiom,(
% 57.78/7.74 (! [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) ) )) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f28,axiom,(
% 57.78/7.74 (! [Vv,Ve] :( vgensym(Ve) = Vv=> ~ visFreeVar(Vv,Ve) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f31,axiom,(
% 57.78/7.74 (! [VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vapp(Ve1,Ve2) )=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2)) ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f38,axiom,(
% 57.78/7.74 (! [VExp0] : vnoExp != vsomeExp(VExp0) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f39,axiom,(
% 57.78/7.74 (! [VOptExp0] :( VOptExp0 = vnoExp=> ~ visSomeExp(VOptExp0) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f41,axiom,(
% 57.78/7.74 (! [VOptExp0,RESULT,Ve] :( VOptExp0 = vsomeExp(Ve)=> ( RESULT = vgetSomeExp(VOptExp0)=> RESULT = Ve ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f42,axiom,(
% 57.78/7.74 (! [Vx,VExp0,RESULT] :( VExp0 = vvar(Vx)=> ( RESULT = vreduce(VExp0)=> RESULT = vnoExp ) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f49,axiom,(
% 57.78/7.74 (! [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 ) )) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f53,axiom,(
% 57.78/7.74 (! [VS,VC,Ve1,Ve2,VT] :( ( vtcheck(VC,Ve1,varrow(VS,VT))& vtcheck(VC,Ve2,VS) )=> vtcheck(VC,vapp(Ve1,Ve2),VT) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f54,axiom,(
% 57.78/7.74 (! [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) ) )) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f58,axiom,(
% 57.78/7.74 (! [VT,VC,Vx,Ve,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),ve1,VT2) )=> vtcheck(VC,vsubst(Vx,Ve,ve1),VT2) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f59,axiom,(
% 57.78/7.74 (! [VT,VC,Vx,Ve,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),ve2,VT2) )=> vtcheck(VC,vsubst(Vx,Ve,ve2),VT2) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f60,conjecture,(
% 57.78/7.74 (! [VT,VC,Vx,Ve,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vapp(ve1,ve2),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vapp(ve1,ve2)),VT2) ) )),
% 57.78/7.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.78/7.74 fof(f61,negated_conjecture,(
% 57.78/7.74 ~((! [VT,VC,Vx,Ve,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vapp(ve1,ve2),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vapp(ve1,ve2)),VT2) ) ))),
% 57.78/7.74 inference(negated_conjecture,[status(cth)],[f60])).
% 57.78/7.74 fof(f62,plain,(
% 57.78/7.74 ![VVar0,VVar1]: ((~vvar(VVar0)=vvar(VVar1)|VVar0=VVar1)&(~VVar0=VVar1|vvar(VVar0)=vvar(VVar1)))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 57.78/7.74 fof(f63,plain,(
% 57.78/7.74 (![VVar0,VVar1]: (~vvar(VVar0)=vvar(VVar1)|VVar0=VVar1))&(![VVar0,VVar1]: (~VVar0=VVar1|vvar(VVar0)=vvar(VVar1)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f62])).
% 57.78/7.74 fof(f64,plain,(
% 57.78/7.74 ![X0,X1]: (~vvar(X0)=vvar(X1)|X0=X1)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f63])).
% 57.78/7.74 fof(f72,plain,(
% 57.78/7.74 ![VExp0,VExp1,VExp2,VExp3]: ((~vapp(VExp0,VExp1)=vapp(VExp2,VExp3)|(VExp0=VExp2&VExp1=VExp3))&((~VExp0=VExp2|~VExp1=VExp3)|vapp(VExp0,VExp1)=vapp(VExp2,VExp3)))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 57.78/7.74 fof(f73,plain,(
% 57.78/7.74 (![VExp0,VExp1,VExp2,VExp3]: (~vapp(VExp0,VExp1)=vapp(VExp2,VExp3)|(VExp0=VExp2&VExp1=VExp3)))&(![VExp0,VExp1,VExp2,VExp3]: ((~VExp0=VExp2|~VExp1=VExp3)|vapp(VExp0,VExp1)=vapp(VExp2,VExp3)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f72])).
% 57.78/7.74 fof(f74,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X0=X2)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f73])).
% 57.78/7.74 fof(f75,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X1=X3)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f73])).
% 57.78/7.74 fof(f77,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (~vvar(X0)=vabs(X1,X2,X3))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f4])).
% 57.78/7.74 fof(f78,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f5])).
% 57.78/7.74 fof(f79,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4]: (~vabs(X0,X1,X2)=vapp(X3,X4))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f6])).
% 57.78/7.74 fof(f86,plain,(
% 57.78/7.74 ![Ve1,Ve2,VExp0]: (~VExp0=vapp(Ve1,Ve2)|~visValue(VExp0))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 57.78/7.74 fof(f87,plain,(
% 57.78/7.74 ![VExp0]: ((![Ve1,Ve2]: ~VExp0=vapp(Ve1,Ve2))|~visValue(VExp0))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f86])).
% 57.78/7.74 fof(f88,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~X0=vapp(X1,X2)|~visValue(X0))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f87])).
% 57.78/7.74 fof(f117,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~vempty=vbind(X0,X1,X2))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f17])).
% 57.78/7.74 fof(f124,plain,(
% 57.78/7.74 ![VOptTyp0,RESULT,Ve]: (~VOptTyp0=vsomeType(Ve)|(~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 57.78/7.74 fof(f125,plain,(
% 57.78/7.74 ![VOptTyp0,Ve]: (~VOptTyp0=vsomeType(Ve)|(![RESULT]: (~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f124])).
% 57.78/7.74 fof(f126,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~X0=vsomeType(X1)|~X2=vgetSomeType(X0)|X2=X1)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f125])).
% 57.78/7.74 fof(f127,plain,(
% 57.78/7.74 ![Vx,VVar0,VCtx0,RESULT]: ((~VVar0=Vx|~VCtx0=vempty)|(~RESULT=vlookup(VVar0,VCtx0)|RESULT=vnoType))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 57.78/7.74 fof(f128,plain,(
% 57.78/7.74 ![VVar0,VCtx0]: (((![Vx]: ~VVar0=Vx)|~VCtx0=vempty)|(![RESULT]: (~RESULT=vlookup(VVar0,VCtx0)|RESULT=vnoType)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f127])).
% 57.78/7.74 fof(f129,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (~X0=X1|~X2=vempty|~X3=vlookup(X0,X2)|X3=vnoType)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f128])).
% 57.78/7.74 fof(f136,plain,(
% 57.78/7.74 ![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)))))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 57.78/7.74 fof(f137,definition,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT]: (sP0_prd(RESULT,VCtx0,VVar0)<=>((?[Vx]: ((VVar0=Vx&VCtx0=vempty)&RESULT=vnoType))|(?[VC,Vx,Vy,VTy]: (((VVar0=Vx&VCtx0=vbind(Vy,VTy,VC))&Vx=Vy)&RESULT=vsomeType(VTy)))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 57.78/7.74 fof(f138,plain,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT]: (~vlookup(VVar0,VCtx0)=RESULT|(sP0_prd(RESULT,VCtx0,VVar0)|(?[VTy,Vy,Vx,VC]: (((VVar0=Vx&VCtx0=vbind(Vy,VTy,VC))&~Vx=Vy)&RESULT=vlookup(Vx,VC)))))),
% 57.78/7.74 inference(formula_renaming,[status(thm)],[f136,f137])).
% 57.78/7.74 fof(f139,plain,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT]: (~vlookup(VVar0,VCtx0)=RESULT|(sP0_prd(RESULT,VCtx0,VVar0)|(?[Vx,VC]: ((?[Vy]: ((VVar0=Vx&(?[VTy]: VCtx0=vbind(Vy,VTy,VC)))&~Vx=Vy))&RESULT=vlookup(Vx,VC)))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f138])).
% 57.78/7.74 fof(f140,plain,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT]: (~vlookup(VVar0,VCtx0)=RESULT|(sP0_prd(RESULT,VCtx0,VVar0)|(((VVar0=sK0_skl(RESULT,VCtx0,VVar0)&VCtx0=vbind(sK2_skl(RESULT,VCtx0,VVar0),sK3_skl(RESULT,VCtx0,VVar0),sK1_skl(RESULT,VCtx0,VVar0)))&~sK0_skl(RESULT,VCtx0,VVar0)=sK2_skl(RESULT,VCtx0,VVar0))&RESULT=vlookup(sK0_skl(RESULT,VCtx0,VVar0),sK1_skl(RESULT,VCtx0,VVar0)))))),
% 57.78/7.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(Vx,sK0_skl(RESULT,VCtx0,VVar0)),skolemize(VC,sK1_skl(RESULT,VCtx0,VVar0)),skolemize(Vy,sK2_skl(RESULT,VCtx0,VVar0)),skolemize(VTy,sK3_skl(RESULT,VCtx0,VVar0))],[f139])).
% 57.78/7.74 fof(f142,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~vlookup(X0,X1)=X2|sP0_prd(X2,X1,X0)|X1=vbind(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0),sK1_skl(X2,X1,X0)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f140])).
% 57.78/7.74 fof(f150,plain,(
% 57.78/7.74 ![Vv,Ve]: (~vgensym(Ve)=Vv|~visFreeVar(Vv,Ve))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 57.78/7.74 fof(f151,plain,(
% 57.78/7.74 ![X0,X1]: (~vgensym(X0)=X1|~visFreeVar(X1,X0))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f150])).
% 57.78/7.74 fof(f158,plain,(
% 57.78/7.74 ![VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vapp(Ve1,Ve2))|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2))))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 57.78/7.74 fof(f159,plain,(
% 57.78/7.74 ![VVar0,VExp0,VExp1,Ve1,Vx,Ve,Ve2]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vapp(Ve1,Ve2))|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2)))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f158])).
% 57.78/7.74 fof(f160,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~X0=X1|~X2=X3|~X4=vapp(X5,X6)|~X7=vsubst(X0,X2,X4)|X7=vapp(vsubst(X1,X3,X5),vsubst(X1,X3,X6)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f159])).
% 57.78/7.74 fof(f187,plain,(
% 57.78/7.74 ![X0]: (~vnoExp=vsomeExp(X0))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f38])).
% 57.78/7.74 fof(f188,plain,(
% 57.78/7.74 ![VOptExp0]: (~VOptExp0=vnoExp|~visSomeExp(VOptExp0))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 57.78/7.74 fof(f189,plain,(
% 57.78/7.74 ![X0]: (~X0=vnoExp|~visSomeExp(X0))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f188])).
% 57.78/7.74 fof(f193,plain,(
% 57.78/7.74 ![VOptExp0,RESULT,Ve]: (~VOptExp0=vsomeExp(Ve)|(~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 57.78/7.74 fof(f194,plain,(
% 57.78/7.74 ![VOptExp0,Ve]: (~VOptExp0=vsomeExp(Ve)|(![RESULT]: (~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f193])).
% 57.78/7.74 fof(f195,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~X0=vsomeExp(X1)|~X2=vgetSomeExp(X0)|X2=X1)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f194])).
% 57.78/7.74 fof(f196,plain,(
% 57.78/7.74 ![Vx,VExp0,RESULT]: (~VExp0=vvar(Vx)|(~RESULT=vreduce(VExp0)|RESULT=vnoExp))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 57.78/7.74 fof(f197,plain,(
% 57.78/7.74 ![VExp0]: ((![Vx]: ~VExp0=vvar(Vx))|(![RESULT]: (~RESULT=vreduce(VExp0)|RESULT=vnoExp)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f196])).
% 57.78/7.74 fof(f198,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~X0=vvar(X1)|~X2=vreduce(X0)|X2=vnoExp)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f197])).
% 57.78/7.74 fof(f219,plain,(
% 57.78/7.74 ![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))))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 57.78/7.74 fof(f220,definition,(
% 57.78/7.74 ![VExp0,RESULT]: (sP2_prd(RESULT,VExp0)<=>((((((?[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))))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 57.78/7.74 fof(f238,plain,(
% 57.78/7.74 ![VS,VC,Ve1,Ve2,VT]: ((~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 57.78/7.74 fof(f239,plain,(
% 57.78/7.74 ![VC,Ve1,Ve2,VT]: ((![VS]: (~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS)))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f238])).
% 57.78/7.74 fof(f240,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,X1,varrow(X2,X3))|~vtcheck(X0,X4,X2)|vtcheck(X0,vapp(X1,X4),X3))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f239])).
% 57.78/7.74 fof(f241,plain,(
% 57.78/7.74 ![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)))))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 57.78/7.74 fof(f242,definition,(
% 57.78/7.74 ![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)<=>((?[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)))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 57.78/7.74 fof(f243,plain,(
% 57.78/7.74 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(sP3_prd(VC,VT,Ve)|(?[Ve1,Ve2,VS]: ((Ve=vapp(Ve1,Ve2)&vtcheck(VC,Ve1,varrow(VS,VT)))&vtcheck(VC,Ve2,VS)))))),
% 57.78/7.74 inference(formula_renaming,[status(thm)],[f241,f242])).
% 57.78/7.74 fof(f244,plain,(
% 57.78/7.74 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(sP3_prd(VC,VT,Ve)|(?[Ve2,VS]: ((?[Ve1]: (Ve=vapp(Ve1,Ve2)&vtcheck(VC,Ve1,varrow(VS,VT))))&vtcheck(VC,Ve2,VS)))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f243])).
% 57.78/7.74 fof(f245,plain,(
% 57.78/7.74 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(sP3_prd(VC,VT,Ve)|((Ve=vapp(sK20_skl(VC,VT,Ve),sK18_skl(VC,VT,Ve))&vtcheck(VC,sK20_skl(VC,VT,Ve),varrow(sK19_skl(VC,VT,Ve),VT)))&vtcheck(VC,sK18_skl(VC,VT,Ve),sK19_skl(VC,VT,Ve)))))),
% 57.78/7.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(Ve2,sK18_skl(VC,VT,Ve)),skolemize(VS,sK19_skl(VC,VT,Ve)),skolemize(Ve1,sK20_skl(VC,VT,Ve))],[f244])).
% 57.78/7.74 fof(f246,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f245])).
% 57.78/7.74 fof(f247,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|vtcheck(X0,sK20_skl(X0,X2,X1),varrow(sK19_skl(X0,X2,X1),X2)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f245])).
% 57.78/7.74 fof(f248,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|vtcheck(X0,sK18_skl(X0,X2,X1),sK19_skl(X0,X2,X1)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f245])).
% 57.78/7.74 fof(f258,plain,(
% 57.78/7.74 ![VT,VC,Vx,Ve,VT2]: ((~vtcheck(VC,Ve,VT)|~vtcheck(vbind(Vx,VT,VC),ve1,VT2))|vtcheck(VC,vsubst(Vx,Ve,ve1),VT2))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 57.78/7.74 fof(f259,plain,(
% 57.78/7.74 ![VC,Vx,Ve,VT2]: ((![VT]: (~vtcheck(VC,Ve,VT)|~vtcheck(vbind(Vx,VT,VC),ve1,VT2)))|vtcheck(VC,vsubst(Vx,Ve,ve1),VT2))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f258])).
% 57.78/7.74 fof(f260,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,X1,X2)|~vtcheck(vbind(X3,X2,X0),ve1,X4)|vtcheck(X0,vsubst(X3,X1,ve1),X4))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f259])).
% 57.78/7.74 fof(f261,plain,(
% 57.78/7.74 ![VT,VC,Vx,Ve,VT2]: ((~vtcheck(VC,Ve,VT)|~vtcheck(vbind(Vx,VT,VC),ve2,VT2))|vtcheck(VC,vsubst(Vx,Ve,ve2),VT2))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 57.78/7.74 fof(f262,plain,(
% 57.78/7.74 ![VC,Vx,Ve,VT2]: ((![VT]: (~vtcheck(VC,Ve,VT)|~vtcheck(vbind(Vx,VT,VC),ve2,VT2)))|vtcheck(VC,vsubst(Vx,Ve,ve2),VT2))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f261])).
% 57.78/7.74 fof(f263,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,X1,X2)|~vtcheck(vbind(X3,X2,X0),ve2,X4)|vtcheck(X0,vsubst(X3,X1,ve2),X4))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f262])).
% 57.78/7.74 fof(f264,plain,(
% 57.78/7.74 (?[VT,VC,Vx,Ve,VT2]: ((vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vapp(ve1,ve2),VT2))&~vtcheck(VC,vsubst(Vx,Ve,vapp(ve1,ve2)),VT2)))),
% 57.78/7.74 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 57.78/7.74 fof(f265,plain,(
% 57.78/7.74 ?[VC,Vx,Ve,VT2]: ((?[VT]: (vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vapp(ve1,ve2),VT2)))&~vtcheck(VC,vsubst(Vx,Ve,vapp(ve1,ve2)),VT2))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f264])).
% 57.78/7.74 fof(f266,plain,(
% 57.78/7.74 ((vtcheck(sK21_skl,sK23_skl,sK25_skl)&vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),vapp(ve1,ve2),sK24_skl))&~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vapp(ve1,ve2)),sK24_skl))),
% 57.78/7.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl]),skolemize(VC,sK21_skl),skolemize(Vx,sK22_skl),skolemize(Ve,sK23_skl),skolemize(VT2,sK24_skl),skolemize(VT,sK25_skl)],[f265])).
% 57.78/7.74 fof(f267,plain,(
% 57.78/7.74 vtcheck(sK21_skl,sK23_skl,sK25_skl)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f266])).
% 57.78/7.74 fof(f268,plain,(
% 57.78/7.74 vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),vapp(ve1,ve2),sK24_skl)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f266])).
% 57.78/7.74 fof(f269,plain,(
% 57.78/7.74 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vapp(ve1,ve2)),sK24_skl)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f266])).
% 57.78/7.74 fof(f270,definition,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT,Vx]: (sP4_prd(Vx,RESULT,VCtx0,VVar0)<=>((VVar0=Vx&VCtx0=vempty)&RESULT=vnoType))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 57.78/7.74 fof(f271,plain,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT]: (sP0_prd(RESULT,VCtx0,VVar0)<=>((?[Vx]: sP4_prd(Vx,RESULT,VCtx0,VVar0))|(?[VC,Vx,Vy,VTy]: (((VVar0=Vx&VCtx0=vbind(Vy,VTy,VC))&Vx=Vy)&RESULT=vsomeType(VTy)))))),
% 57.78/7.74 inference(formula_renaming,[status(thm)],[f137,f270])).
% 57.78/7.74 fof(f272,plain,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT]: ((~sP0_prd(RESULT,VCtx0,VVar0)|((?[Vx]: sP4_prd(Vx,RESULT,VCtx0,VVar0))|(?[VC,Vx,Vy,VTy]: (((VVar0=Vx&VCtx0=vbind(Vy,VTy,VC))&Vx=Vy)&RESULT=vsomeType(VTy)))))&(sP0_prd(RESULT,VCtx0,VVar0)|((![Vx]: ~sP4_prd(Vx,RESULT,VCtx0,VVar0))&(![VC,Vx,Vy,VTy]: (((~VVar0=Vx|~VCtx0=vbind(Vy,VTy,VC))|~Vx=Vy)|~RESULT=vsomeType(VTy))))))),
% 57.78/7.74 inference(NNF_transformation,[status(thm)],[f271])).
% 57.78/7.74 fof(f273,plain,(
% 57.78/7.74 (![VVar0,VCtx0,RESULT]: (~sP0_prd(RESULT,VCtx0,VVar0)|((?[Vx]: sP4_prd(Vx,RESULT,VCtx0,VVar0))|(?[VTy]: ((?[Vx,Vy]: ((VVar0=Vx&(?[VC]: VCtx0=vbind(Vy,VTy,VC)))&Vx=Vy))&RESULT=vsomeType(VTy))))))&(![VVar0,VCtx0,RESULT]: (sP0_prd(RESULT,VCtx0,VVar0)|((![Vx]: ~sP4_prd(Vx,RESULT,VCtx0,VVar0))&(![VTy]: ((![Vx,Vy]: ((~VVar0=Vx|(![VC]: ~VCtx0=vbind(Vy,VTy,VC)))|~Vx=Vy))|~RESULT=vsomeType(VTy))))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f272])).
% 57.78/7.74 fof(f274,plain,(
% 57.78/7.74 (![VVar0,VCtx0,RESULT]: (~sP0_prd(RESULT,VCtx0,VVar0)|(sP4_prd(sK26_skl(RESULT,VCtx0,VVar0),RESULT,VCtx0,VVar0)|(((VVar0=sK28_skl(RESULT,VCtx0,VVar0)&VCtx0=vbind(sK29_skl(RESULT,VCtx0,VVar0),sK27_skl(RESULT,VCtx0,VVar0),sK30_skl(RESULT,VCtx0,VVar0)))&sK28_skl(RESULT,VCtx0,VVar0)=sK29_skl(RESULT,VCtx0,VVar0))&RESULT=vsomeType(sK27_skl(RESULT,VCtx0,VVar0))))))&(![VVar0,VCtx0,RESULT]: (sP0_prd(RESULT,VCtx0,VVar0)|((![Vx]: ~sP4_prd(Vx,RESULT,VCtx0,VVar0))&(![VTy]: ((![Vx,Vy]: ((~VVar0=Vx|(![VC]: ~VCtx0=vbind(Vy,VTy,VC)))|~Vx=Vy))|~RESULT=vsomeType(VTy))))))),
% 57.78/7.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl]),skolemize(Vx,sK26_skl(RESULT,VCtx0,VVar0)),skolemize(VTy,sK27_skl(RESULT,VCtx0,VVar0)),skolemize(Vx,sK28_skl(RESULT,VCtx0,VVar0)),skolemize(Vy,sK29_skl(RESULT,VCtx0,VVar0)),skolemize(VC,sK30_skl(RESULT,VCtx0,VVar0))],[f273])).
% 57.78/7.74 fof(f276,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|sP4_prd(sK26_skl(X0,X1,X2),X0,X1,X2)|X1=vbind(sK29_skl(X0,X1,X2),sK27_skl(X0,X1,X2),sK30_skl(X0,X1,X2)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f274])).
% 57.78/7.74 fof(f295,definition,(
% 57.78/7.74 ![VExp0,RESULT]: (sP6_prd(RESULT,VExp0)<=>(((((?[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))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 57.78/7.74 fof(f307,definition,(
% 57.78/7.74 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 57.78/7.74 fof(f308,plain,(
% 57.78/7.74 ![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)<=>((?[Vx]: sP7_prd(Vx,VC,VT,Ve))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)))))),
% 57.78/7.74 inference(formula_renaming,[status(thm)],[f242,f307])).
% 57.78/7.74 fof(f309,plain,(
% 57.78/7.74 ![Ve,VT,VC]: ((~sP3_prd(VC,VT,Ve)|((?[Vx]: sP7_prd(Vx,VC,VT,Ve))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)))))&(sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 57.78/7.74 inference(NNF_transformation,[status(thm)],[f308])).
% 57.78/7.74 fof(f310,plain,(
% 57.78/7.74 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|((?[Vx]: sP7_prd(Vx,VC,VT,Ve))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))&(![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f309])).
% 57.78/7.74 fof(f311,plain,(
% 57.78/7.74 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|(sP7_prd(sK43_skl(VC,VT,Ve),VC,VT,Ve)|((Ve=vabs(sK44_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve),sK45_skl(VC,VT,Ve))&VT=varrow(sK46_skl(VC,VT,Ve),sK47_skl(VC,VT,Ve)))&vtcheck(vbind(sK44_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve),VC),sK45_skl(VC,VT,Ve),sK47_skl(VC,VT,Ve))))))&(![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 57.78/7.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl,sK44_skl,sK45_skl,sK46_skl,sK47_skl]),skolemize(Vx,sK43_skl(VC,VT,Ve)),skolemize(Vx,sK44_skl(VC,VT,Ve)),skolemize(Ve2,sK45_skl(VC,VT,Ve)),skolemize(VT1,sK46_skl(VC,VT,Ve)),skolemize(VT2,sK47_skl(VC,VT,Ve))],[f310])).
% 57.78/7.74 fof(f312,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|sP7_prd(sK43_skl(X0,X1,X2),X0,X1,X2)|X2=vabs(sK44_skl(X0,X1,X2),sK46_skl(X0,X1,X2),sK45_skl(X0,X1,X2)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f311])).
% 57.78/7.74 fof(f317,plain,(
% 57.78/7.74 ![VVar0,VCtx0,RESULT,Vx]: ((~sP4_prd(Vx,RESULT,VCtx0,VVar0)|((VVar0=Vx&VCtx0=vempty)&RESULT=vnoType))&(sP4_prd(Vx,RESULT,VCtx0,VVar0)|((~VVar0=Vx|~VCtx0=vempty)|~RESULT=vnoType)))),
% 57.78/7.74 inference(NNF_transformation,[status(thm)],[f270])).
% 57.78/7.74 fof(f318,plain,(
% 57.78/7.74 (![VVar0,VCtx0,RESULT,Vx]: (~sP4_prd(Vx,RESULT,VCtx0,VVar0)|((VVar0=Vx&VCtx0=vempty)&RESULT=vnoType)))&(![VVar0,VCtx0,RESULT,Vx]: (sP4_prd(Vx,RESULT,VCtx0,VVar0)|((~VVar0=Vx|~VCtx0=vempty)|~RESULT=vnoType)))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f317])).
% 57.78/7.74 fof(f319,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (~sP4_prd(X0,X1,X2,X3)|X3=X0)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f318])).
% 57.78/7.74 fof(f335,definition,(
% 57.78/7.74 ![VExp0,RESULT]: (sP9_prd(RESULT,VExp0)<=>((((?[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))))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 57.78/7.74 fof(f347,plain,(
% 57.78/7.74 ![Ve,VT,VC,Vx]: ((~sP7_prd(Vx,VC,VT,Ve)|(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))&(sP7_prd(Vx,VC,VT,Ve)|(~Ve=vvar(Vx)|~vlookup(Vx,VC)=vsomeType(VT))))),
% 57.78/7.74 inference(NNF_transformation,[status(thm)],[f307])).
% 57.78/7.74 fof(f348,plain,(
% 57.78/7.74 (![Ve,VT,VC,Vx]: (~sP7_prd(Vx,VC,VT,Ve)|(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT))))&(![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)|(~Ve=vvar(Vx)|~vlookup(Vx,VC)=vsomeType(VT))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f347])).
% 57.78/7.74 fof(f349,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|X3=vvar(X0))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f348])).
% 57.78/7.74 fof(f363,definition,(
% 57.78/7.74 ![VExp0,RESULT]: (sP11_prd(RESULT,VExp0)<=>(((?[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)))))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 57.78/7.74 fof(f387,definition,(
% 57.78/7.74 ![VExp0,RESULT]: (sP13_prd(RESULT,VExp0)<=>((?[Vx]: (VExp0=vvar(Vx)&RESULT=vnoExp))|(?[Vx,VS,Ve]: (VExp0=vabs(Vx,VS,Ve)&RESULT=vnoExp))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 57.78/7.74 fof(f406,plain,(
% 57.78/7.74 ![VExp0,RESULT]: ((~sP13_prd(RESULT,VExp0)|((?[Vx]: (VExp0=vvar(Vx)&RESULT=vnoExp))|(?[Vx,VS,Ve]: (VExp0=vabs(Vx,VS,Ve)&RESULT=vnoExp))))&(sP13_prd(RESULT,VExp0)|((![Vx]: (~VExp0=vvar(Vx)|~RESULT=vnoExp))&(![Vx,VS,Ve]: (~VExp0=vabs(Vx,VS,Ve)|~RESULT=vnoExp)))))),
% 57.78/7.74 inference(NNF_transformation,[status(thm)],[f387])).
% 57.78/7.74 fof(f407,plain,(
% 57.78/7.74 (![VExp0,RESULT]: (~sP13_prd(RESULT,VExp0)|(((?[Vx]: VExp0=vvar(Vx))&RESULT=vnoExp)|((?[Vx,VS,Ve]: VExp0=vabs(Vx,VS,Ve))&RESULT=vnoExp))))&(![VExp0,RESULT]: (sP13_prd(RESULT,VExp0)|(((![Vx]: ~VExp0=vvar(Vx))|~RESULT=vnoExp)&((![Vx,VS,Ve]: ~VExp0=vabs(Vx,VS,Ve))|~RESULT=vnoExp))))),
% 57.78/7.74 inference(miniscoping,[status(thm)],[f406])).
% 57.78/7.74 fof(f408,plain,(
% 57.78/7.74 (![VExp0,RESULT]: (~sP13_prd(RESULT,VExp0)|((VExp0=vvar(sK78_skl(RESULT,VExp0))&RESULT=vnoExp)|(VExp0=vabs(sK79_skl(RESULT,VExp0),sK80_skl(RESULT,VExp0),sK81_skl(RESULT,VExp0))&RESULT=vnoExp))))&(![VExp0,RESULT]: (sP13_prd(RESULT,VExp0)|(((![Vx]: ~VExp0=vvar(Vx))|~RESULT=vnoExp)&((![Vx,VS,Ve]: ~VExp0=vabs(Vx,VS,Ve))|~RESULT=vnoExp))))),
% 57.78/7.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK78_skl,sK79_skl,sK80_skl,sK81_skl]),skolemize(Vx,sK78_skl(RESULT,VExp0)),skolemize(Vx,sK79_skl(RESULT,VExp0)),skolemize(VS,sK80_skl(RESULT,VExp0)),skolemize(Ve,sK81_skl(RESULT,VExp0))],[f407])).
% 57.78/7.74 fof(f409,plain,(
% 57.78/7.74 ![X0,X1]: (~sP13_prd(X0,X1)|X1=vvar(sK78_skl(X0,X1))|X1=vabs(sK79_skl(X0,X1),sK80_skl(X0,X1),sK81_skl(X0,X1)))),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f408])).
% 57.78/7.74 fof(f413,plain,(
% 57.78/7.74 ![X0,X1,X2]: (sP13_prd(X0,X1)|~X1=vvar(X2)|~X0=vnoExp)),
% 57.78/7.74 inference(cnf_transformation,[status(thm)],[f408])).
% 57.78/7.74 fof(f423,plain,(
% 57.78/7.74 ![X0,X1,X2]: (~X0=vempty|~X1=vlookup(X2,X0)|X1=vnoType)),
% 57.78/7.74 inference(destructive_equality_resolution,[status(thm)],[f129])).
% 57.78/7.74 fof(f429,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4,X5]: (~X0=vapp(X1,X2)|~X3=vsubst(X4,X5,X0)|X3=vapp(vsubst(X4,X5,X1),vsubst(X4,X5,X2)))),
% 57.78/7.74 inference(destructive_equality_resolution,[status(thm)],[f160])).
% 57.78/7.74 fof(f453,plain,(
% 57.78/7.74 ![X0,X1,X2,X3,X4]: (~X0=vsubst(X1,X2,vapp(X3,X4))|X0=vapp(vsubst(X1,X2,X3),vsubst(X1,X2,X4)))),
% 57.78/7.74 inference(equality_resolution,[status(thm)],[f429])).
% 57.78/7.74 fof(f461,plain,(
% 57.78/7.74 ![X0,X1]: (~vtcheck(vbind(X0,sK25_skl,sK21_skl),ve1,X1)|vtcheck(sK21_skl,vsubst(X0,sK23_skl,ve1),X1))),
% 57.78/7.74 inference(resolution,[status(thm)],[f260,f267])).
% 57.78/7.74 fof(f463,plain,(
% 57.78/7.74 ![X0,X1]: (~vtcheck(vbind(X0,sK25_skl,sK21_skl),ve2,X1)|vtcheck(sK21_skl,vsubst(X0,sK23_skl,ve2),X1))),
% 57.78/7.74 inference(resolution,[status(thm)],[f263,f267])).
% 57.78/7.74 fof(f468,plain,(
% 57.78/7.74 ![X0,X1,X2,X3]: (vsubst(X0,X1,vapp(X2,X3))=vapp(vsubst(X0,X1,X2),vsubst(X0,X1,X3)))),
% 57.78/7.74 inference(equality_resolution,[status(thm)],[f453])).
% 57.78/7.74 fof(f543,plain,(
% 57.78/7.74 ![X0,X1]: (~X0=vgetSomeType(vsomeType(X1))|X0=X1)),
% 57.78/7.74 inference(equality_resolution,[status(thm)],[f126])).
% 57.78/7.74 fof(f544,plain,(
% 57.78/7.74 ![X0,X1]: (~X0=vempty|vlookup(X1,X0)=vnoType)),
% 57.78/7.74 inference(equality_resolution,[status(thm)],[f423])).
% 57.78/7.74 fof(f753,plain,(
% 57.78/7.74 ![X0]: (vgetSomeType(vsomeType(X0))=X0)),
% 57.78/7.74 inference(equality_resolution,[status(thm)],[f543])).
% 57.78/7.74 fof(f1056,plain,(
% 57.78/7.74 ![X0]: (vlookup(X0,vgetSomeType(vsomeType(vempty)))=vnoType)),
% 57.78/7.74 inference(resolution,[status(thm)],[f544,f753])).
% 57.78/7.74 fof(f1058,plain,(
% 57.78/7.74 ![X0]: (vlookup(X0,vempty)=vnoType)),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f753,f1056])).
% 57.78/7.74 fof(f1060,plain,(
% 57.78/7.74 ![X0]: (sP0_prd(vnoType,vempty,X0)|vempty=vbind(sK2_skl(vnoType,vempty,X0),sK3_skl(vnoType,vempty,X0),sK1_skl(vnoType,vempty,X0)))),
% 57.78/7.74 inference(resolution,[status(thm)],[f1058,f142])).
% 57.78/7.74 fof(f1067,plain,(
% 57.78/7.74 ![X0]: (sP0_prd(vnoType,vempty,X0))),
% 57.78/7.74 inference(forward_subsumption_resolution,[status(thm)],[f1060,f117])).
% 57.78/7.74 fof(f1421,plain,(
% 57.78/7.74 ![X0,X1]: (~X0=vgetSomeExp(vgetSomeType(vsomeType(vsomeExp(X1))))|X0=X1)),
% 57.78/7.74 inference(resolution,[status(thm)],[f195,f753])).
% 57.78/7.74 fof(f1423,plain,(
% 57.78/7.74 ![X0,X1]: (~X0=vgetSomeExp(vsomeExp(X1))|X0=X1)),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f753,f1421])).
% 57.78/7.74 fof(f1424,plain,(
% 57.78/7.74 ![X0]: (vgetSomeType(vsomeType(vgetSomeExp(vsomeExp(X0))))=X0)),
% 57.78/7.74 inference(resolution,[status(thm)],[f1423,f753])).
% 57.78/7.74 fof(f1426,plain,(
% 57.78/7.74 ![X0]: (vgetSomeExp(vsomeExp(X0))=X0)),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f753,f1424])).
% 57.78/7.74 fof(f1505,plain,(
% 57.78/7.74 ![X0,X1]: (~X0=vreduce(vgetSomeExp(vsomeExp(vvar(X1))))|X0=vnoExp)),
% 57.78/7.74 inference(resolution,[status(thm)],[f198,f1426])).
% 57.78/7.74 fof(f1508,plain,(
% 57.78/7.74 ![X0,X1]: (~X0=vreduce(vvar(X1))|X0=vnoExp)),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f1426,f1505])).
% 57.78/7.74 fof(f1541,plain,(
% 57.78/7.74 ![X0]: (vgetSomeExp(vsomeExp(vreduce(vvar(X0))))=vnoExp)),
% 57.78/7.74 inference(resolution,[status(thm)],[f1508,f1426])).
% 57.78/7.74 fof(f1544,plain,(
% 57.78/7.74 ![X0]: (vreduce(vvar(X0))=vnoExp)),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f1426,f1541])).
% 57.78/7.74 fof(f2169,plain,(
% 57.78/7.74 sP3_prd(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|vapp(ve1,ve2)=vapp(sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),
% 57.78/7.74 inference(resolution,[status(thm)],[f246,f268])).
% 57.78/7.74 fof(f2172,definition,(
% 57.78/7.74 sQ9_spl <=> (sP3_prd(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f2173,plain,(
% 57.78/7.74 sP3_prd(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|~sQ9_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f2172])).
% 57.78/7.74 fof(f2175,definition,(
% 57.78/7.74 sQ10_spl <=> (vapp(ve1,ve2)=vapp(sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f2176,plain,(
% 57.78/7.74 vapp(ve1,ve2)=vapp(sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ10_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f2175])).
% 57.78/7.74 fof(f2178,plain,(
% 57.78/7.74 sQ9_spl|sQ10_spl),
% 57.78/7.74 inference(split_clause,[status(thm)],[f2169,f2172,f2175])).
% 57.78/7.74 fof(f2193,plain,(
% 57.78/7.74 sP3_prd(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))),
% 57.78/7.74 inference(resolution,[status(thm)],[f247,f268])).
% 57.78/7.74 fof(f2196,definition,(
% 57.78/7.74 sQ15_spl <=> (vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl)))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f2197,plain,(
% 57.78/7.74 vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))|~sQ15_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f2196])).
% 57.78/7.74 fof(f2199,plain,(
% 57.78/7.74 sQ9_spl|sQ15_spl),
% 57.78/7.74 inference(split_clause,[status(thm)],[f2193,f2172,f2196])).
% 57.78/7.74 fof(f2208,plain,(
% 57.78/7.74 sP3_prd(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),
% 57.78/7.74 inference(resolution,[status(thm)],[f248,f268])).
% 57.78/7.74 fof(f2211,definition,(
% 57.78/7.74 sQ18_spl <=> (vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f2212,plain,(
% 57.78/7.74 vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ18_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f2211])).
% 57.78/7.74 fof(f2214,plain,(
% 57.78/7.74 sQ9_spl|sQ18_spl),
% 57.78/7.74 inference(split_clause,[status(thm)],[f2208,f2172,f2211])).
% 57.78/7.74 fof(f2611,plain,(
% 57.78/7.74 ![X0]: (sP4_prd(sK26_skl(vnoType,vempty,X0),vnoType,vempty,X0)|vempty=vbind(sK29_skl(vnoType,vempty,X0),sK27_skl(vnoType,vempty,X0),sK30_skl(vnoType,vempty,X0)))),
% 57.78/7.74 inference(resolution,[status(thm)],[f276,f1067])).
% 57.78/7.74 fof(f2612,plain,(
% 57.78/7.74 ![X0]: (sP4_prd(sK26_skl(vnoType,vempty,X0),vnoType,vempty,X0))),
% 57.78/7.74 inference(forward_subsumption_resolution,[status(thm)],[f2611,f117])).
% 57.78/7.74 fof(f2990,plain,(
% 57.78/7.74 sP7_prd(sK43_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|vapp(ve1,ve2)=vabs(sK44_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK46_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK45_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ9_spl),
% 57.78/7.74 inference(resolution,[status(thm)],[f312,f2173])).
% 57.78/7.74 fof(f2994,definition,(
% 57.78/7.74 sQ46_spl <=> (sP7_prd(sK43_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f2995,plain,(
% 57.78/7.74 sP7_prd(sK43_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|~sQ46_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f2994])).
% 57.78/7.74 fof(f2997,definition,(
% 57.78/7.74 sQ47_spl <=> (vapp(ve1,ve2)=vabs(sK44_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK46_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK45_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f2998,plain,(
% 57.78/7.74 vapp(ve1,ve2)=vabs(sK44_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK46_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK45_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ47_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f2997])).
% 57.78/7.74 fof(f3000,plain,(
% 57.78/7.74 sQ46_spl|sQ47_spl|~sQ9_spl),
% 57.78/7.74 inference(split_clause,[status(thm)],[f2990,f2994,f2997,f2172])).
% 57.78/7.74 fof(f3002,definition,(
% 57.78/7.74 sQ48_spl <=> (sP7_prd(sK43_skl(sK21_skl,varrow(sK25_skl,sK24_skl),vabs(sK22_skl,sK25_skl,vapp(ve1,ve2))),sK21_skl,varrow(sK25_skl,sK24_skl),vabs(sK22_skl,sK25_skl,vapp(ve1,ve2))))),
% 57.78/7.74 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 57.78/7.74 fof(f3003,plain,(
% 57.78/7.74 sP7_prd(sK43_skl(sK21_skl,varrow(sK25_skl,sK24_skl),vabs(sK22_skl,sK25_skl,vapp(ve1,ve2))),sK21_skl,varrow(sK25_skl,sK24_skl),vabs(sK22_skl,sK25_skl,vapp(ve1,ve2)))|~sQ48_spl),
% 57.78/7.74 inference(component_clause,[status(thm)],[f3002])).
% 57.78/7.74 fof(f3051,plain,(
% 57.78/7.74 ![X0,X1]: (sP13_prd(X0,vgetSomeExp(vsomeExp(vvar(X1))))|~X0=vnoExp)),
% 57.78/7.74 inference(resolution,[status(thm)],[f413,f1426])).
% 57.78/7.74 fof(f3055,plain,(
% 57.78/7.74 ![X0,X1]: (sP13_prd(X0,vvar(X1))|~X0=vnoExp)),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f1426,f3051])).
% 57.78/7.74 fof(f3217,plain,(
% 57.78/7.74 ![X0,X1]: (sP13_prd(vreduce(vvar(X0)),vvar(X1)))),
% 57.78/7.74 inference(resolution,[status(thm)],[f3055,f1544])).
% 57.78/7.74 fof(f3223,plain,(
% 57.78/7.74 ![X0]: (sP13_prd(vnoExp,vvar(X0)))),
% 57.78/7.74 inference(forward_demodulation,[status(thm)],[f1544,f3217])).
% 57.78/7.74 fof(f3240,plain,(
% 57.78/7.74 ve2=sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|~sQ10_spl),
% 57.78/7.74 inference(resolution,[status(thm)],[f2176,f75])).
% 57.78/7.74 fof(f3241,plain,(
% 57.78/7.74 ve1=sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))|~sQ10_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f2176,f74])).
% 57.78/7.75 fof(f3918,plain,(
% 57.78/7.75 $false|~sQ47_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f2998,f79])).
% 57.78/7.75 fof(f3919,plain,(
% 57.78/7.75 ~sQ47_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f3918])).
% 57.78/7.75 fof(f4433,plain,(
% 57.78/7.75 vapp(ve1,ve2)=vvar(sK43_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ46_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f2995,f349])).
% 57.78/7.75 fof(f4434,plain,(
% 57.78/7.75 $false|~sQ46_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f4433,f78])).
% 57.78/7.75 fof(f4435,plain,(
% 57.78/7.75 ~sQ46_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f4434])).
% 57.78/7.75 fof(f4444,definition,(
% 57.78/7.75 sQ136_spl <=> (vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK23_skl),sK63_skl(vnoExp,sK23_skl),sK64_skl(vnoExp,sK23_skl))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f4445,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK23_skl),sK63_skl(vnoExp,sK23_skl),sK64_skl(vnoExp,sK23_skl)))|~sQ136_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f4444])).
% 57.78/7.75 fof(f4460,plain,(
% 57.78/7.75 $false|~sQ136_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f4445,f187])).
% 57.78/7.75 fof(f4461,plain,(
% 57.78/7.75 ~sQ136_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f4460])).
% 57.78/7.75 fof(f4480,definition,(
% 57.78/7.75 sQ141_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK23_skl),sK74_skl(vnoExp,sK23_skl),sK75_skl(vnoExp,sK23_skl)),vgetSomeExp(sK76_skl(vnoExp,sK23_skl)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f4481,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK23_skl),sK74_skl(vnoExp,sK23_skl),sK75_skl(vnoExp,sK23_skl)),vgetSomeExp(sK76_skl(vnoExp,sK23_skl))))|~sQ141_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f4480])).
% 57.78/7.75 fof(f4496,plain,(
% 57.78/7.75 $false|~sQ141_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f4481,f187])).
% 57.78/7.75 fof(f4497,plain,(
% 57.78/7.75 ~sQ141_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f4496])).
% 57.78/7.75 fof(f4505,plain,(
% 57.78/7.75 ![X0]: (vvar(X0)=vvar(sK78_skl(vnoExp,vvar(X0)))|vvar(X0)=vabs(sK79_skl(vnoExp,vvar(X0)),sK80_skl(vnoExp,vvar(X0)),sK81_skl(vnoExp,vvar(X0))))),
% 57.78/7.75 inference(resolution,[status(thm)],[f409,f3223])).
% 57.78/7.75 fof(f4506,plain,(
% 57.78/7.75 ![X0]: (vvar(X0)=vvar(sK78_skl(vnoExp,vvar(X0))))),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f4505,f77])).
% 57.78/7.75 fof(f4681,definition,(
% 57.78/7.75 sQ150_spl <=> (vapp(ve1,ve2)=vvar(sK78_skl(vnoExp,vapp(ve1,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f4682,plain,(
% 57.78/7.75 vapp(ve1,ve2)=vvar(sK78_skl(vnoExp,vapp(ve1,ve2)))|~sQ150_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f4681])).
% 57.78/7.75 fof(f4684,definition,(
% 57.78/7.75 sQ151_spl <=> (vapp(ve1,ve2)=vabs(sK79_skl(vnoExp,vapp(ve1,ve2)),sK80_skl(vnoExp,vapp(ve1,ve2)),sK81_skl(vnoExp,vapp(ve1,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f4685,plain,(
% 57.78/7.75 vapp(ve1,ve2)=vabs(sK79_skl(vnoExp,vapp(ve1,ve2)),sK80_skl(vnoExp,vapp(ve1,ve2)),sK81_skl(vnoExp,vapp(ve1,ve2)))|~sQ151_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f4684])).
% 57.78/7.75 fof(f4689,plain,(
% 57.78/7.75 $false|~sQ150_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f4682,f78])).
% 57.78/7.75 fof(f4690,plain,(
% 57.78/7.75 ~sQ150_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f4689])).
% 57.78/7.75 fof(f4691,plain,(
% 57.78/7.75 $false|~sQ151_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f4685,f79])).
% 57.78/7.75 fof(f4692,plain,(
% 57.78/7.75 ~sQ151_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f4691])).
% 57.78/7.75 fof(f4815,plain,(
% 57.78/7.75 vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),ve2,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ10_spl|~sQ18_spl),
% 57.78/7.75 inference(backward_demodulation,[status(thm)],[f3240,f2212])).
% 57.78/7.75 fof(f4828,plain,(
% 57.78/7.75 vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,ve2),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|~sQ10_spl|~sQ18_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f4815,f463])).
% 57.78/7.75 fof(f5023,plain,(
% 57.78/7.75 vtcheck(vbind(sK22_skl,sK25_skl,sK21_skl),ve1,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))|~sQ10_spl|~sQ15_spl),
% 57.78/7.75 inference(backward_demodulation,[status(thm)],[f3241,f2197])).
% 57.78/7.75 fof(f5024,plain,(
% 57.78/7.75 vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,ve1),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))|~sQ10_spl|~sQ15_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f5023,f461])).
% 57.78/7.75 fof(f5066,definition,(
% 57.78/7.75 sQ172_spl <=> (visSomeExp(vnoExp))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f5067,plain,(
% 57.78/7.75 visSomeExp(vnoExp)|~sQ172_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f5066])).
% 57.78/7.75 fof(f5077,definition,(
% 57.78/7.75 ![X0]: (sQ175_spl <=> (~X0=vnoExp|visSomeExp(X0)))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f5078,plain,(
% 57.78/7.75 ![X0]: (~X0=vnoExp|visSomeExp(X0)|~sQ175_spl)),
% 57.78/7.75 inference(component_clause,[status(thm)],[f5077])).
% 57.78/7.75 fof(f5082,plain,(
% 57.78/7.75 ![X0]: (~X0=vnoExp|~sQ175_spl)),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f5078,f189])).
% 57.78/7.75 fof(f5148,plain,(
% 57.78/7.75 $false|~sQ175_spl),
% 57.78/7.75 inference(backward_subsumption_resolution,[status(thm)],[f1544,f5082])).
% 57.78/7.75 fof(f5154,plain,(
% 57.78/7.75 ~sQ175_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f5148])).
% 57.78/7.75 fof(f5188,plain,(
% 57.78/7.75 ~vnoExp=vnoExp|~sQ172_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f189,f5067])).
% 57.78/7.75 fof(f5194,plain,(
% 57.78/7.75 $false|~sQ172_spl),
% 57.78/7.75 inference(trivial_equality_resolution,[status(thm)],[f5188])).
% 57.78/7.75 fof(f5195,plain,(
% 57.78/7.75 ~sQ172_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f5194])).
% 57.78/7.75 fof(f5389,definition,(
% 57.78/7.75 sQ186_spl <=> (vabs(sK22_skl,sK25_skl,ve1)=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl)),vabs(sK22_skl,sK25_skl,ve1)),sK18_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl)),vabs(sK22_skl,sK25_skl,ve1))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f5390,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,ve1)=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl)),vabs(sK22_skl,sK25_skl,ve1)),sK18_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl)),vabs(sK22_skl,sK25_skl,ve1)))|~sQ186_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f5389])).
% 57.78/7.75 fof(f5393,plain,(
% 57.78/7.75 $false|~sQ186_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f5390,f79])).
% 57.78/7.75 fof(f5394,plain,(
% 57.78/7.75 ~sQ186_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f5393])).
% 57.78/7.75 fof(f5446,definition,(
% 57.78/7.75 ![X0]: (sQ190_spl <=> (visFreeVar(X0,ve1)|visFreeVar(X0,ve1)))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f5447,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,ve1)|visFreeVar(X0,ve1)|~sQ190_spl)),
% 57.78/7.75 inference(component_clause,[status(thm)],[f5446])).
% 57.78/7.75 fof(f5453,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,ve1)|~sQ190_spl)),
% 57.78/7.75 inference(duplicate_literals_removal,[status(thm)],[f5447])).
% 57.78/7.75 fof(f5456,plain,(
% 57.78/7.75 ![X0]: (~vgensym(ve1)=X0|~sQ190_spl)),
% 57.78/7.75 inference(resolution,[status(thm)],[f5453,f151])).
% 57.78/7.75 fof(f5464,plain,(
% 57.78/7.75 $false|~sQ190_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f5456,f1426])).
% 57.78/7.75 fof(f5468,plain,(
% 57.78/7.75 ~sQ190_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f5464])).
% 57.78/7.75 fof(f5857,definition,(
% 57.78/7.75 sQ221_spl <=> (vabs(sK22_skl,sK25_skl,ve2)=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))),vabs(sK22_skl,sK25_skl,ve2)),sK18_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))),vabs(sK22_skl,sK25_skl,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f5858,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,ve2)=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))),vabs(sK22_skl,sK25_skl,ve2)),sK18_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2))),vabs(sK22_skl,sK25_skl,ve2)))|~sQ221_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f5857])).
% 57.78/7.75 fof(f5861,plain,(
% 57.78/7.75 $false|~sQ221_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f5858,f79])).
% 57.78/7.75 fof(f5862,plain,(
% 57.78/7.75 ~sQ221_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f5861])).
% 57.78/7.75 fof(f5888,definition,(
% 57.78/7.75 ![X0]: (sQ224_spl <=> (visFreeVar(X0,ve2)|visFreeVar(X0,ve2)))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f5889,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,ve2)|visFreeVar(X0,ve2)|~sQ224_spl)),
% 57.78/7.75 inference(component_clause,[status(thm)],[f5888])).
% 57.78/7.75 fof(f5895,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,ve2)|~sQ224_spl)),
% 57.78/7.75 inference(duplicate_literals_removal,[status(thm)],[f5889])).
% 57.78/7.75 fof(f5899,plain,(
% 57.78/7.75 ![X0]: (~vgensym(ve2)=X0|~sQ224_spl)),
% 57.78/7.75 inference(resolution,[status(thm)],[f5895,f151])).
% 57.78/7.75 fof(f5907,plain,(
% 57.78/7.75 $false|~sQ224_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f5899,f1426])).
% 57.78/7.75 fof(f5911,plain,(
% 57.78/7.75 ~sQ224_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f5907])).
% 57.78/7.75 fof(f6213,definition,(
% 57.78/7.75 sQ260_spl <=> (vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,ve2)),sK38_skl(vnoExp,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f6214,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,ve2)),sK38_skl(vnoExp,ve2)))|~sQ260_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f6213])).
% 57.78/7.75 fof(f6233,plain,(
% 57.78/7.75 $false|~sQ260_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f6214,f187])).
% 57.78/7.75 fof(f6234,plain,(
% 57.78/7.75 ~sQ260_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f6233])).
% 57.78/7.75 fof(f6323,definition,(
% 57.78/7.75 sQ273_spl <=> (vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,ve2),sK63_skl(vnoExp,ve2),sK64_skl(vnoExp,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f6324,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,ve2),sK63_skl(vnoExp,ve2),sK64_skl(vnoExp,ve2)))|~sQ273_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f6323])).
% 57.78/7.75 fof(f6340,plain,(
% 57.78/7.75 $false|~sQ273_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f6324,f187])).
% 57.78/7.75 fof(f6341,plain,(
% 57.78/7.75 ~sQ273_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f6340])).
% 57.78/7.75 fof(f6503,definition,(
% 57.78/7.75 sQ284_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,ve2),sK74_skl(vnoExp,ve2),sK75_skl(vnoExp,ve2)),vgetSomeExp(sK76_skl(vnoExp,ve2)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f6504,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,ve2),sK74_skl(vnoExp,ve2),sK75_skl(vnoExp,ve2)),vgetSomeExp(sK76_skl(vnoExp,ve2))))|~sQ284_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f6503])).
% 57.78/7.75 fof(f6520,plain,(
% 57.78/7.75 $false|~sQ284_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f6504,f187])).
% 57.78/7.75 fof(f6521,plain,(
% 57.78/7.75 ~sQ284_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f6520])).
% 57.78/7.75 fof(f7037,definition,(
% 57.78/7.75 sQ327_spl <=> (sP7_prd(sK43_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)),sK21_skl,sK24_skl,vapp(ve1,ve2)))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f7038,plain,(
% 57.78/7.75 sP7_prd(sK43_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)),sK21_skl,sK24_skl,vapp(ve1,ve2))|~sQ327_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f7037])).
% 57.78/7.75 fof(f7048,definition,(
% 57.78/7.75 sQ330_spl <=> (vapp(ve1,ve2)=vabs(sK44_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)),sK46_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)),sK45_skl(sK21_skl,sK24_skl,vapp(ve1,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f7049,plain,(
% 57.78/7.75 vapp(ve1,ve2)=vabs(sK44_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)),sK46_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)),sK45_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)))|~sQ330_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f7048])).
% 57.78/7.75 fof(f7052,plain,(
% 57.78/7.75 $false|~sQ330_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f7049,f79])).
% 57.78/7.75 fof(f7053,plain,(
% 57.78/7.75 ~sQ330_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f7052])).
% 57.78/7.75 fof(f7979,definition,(
% 57.78/7.75 sQ361_spl <=> (visValue(vapp(ve1,ve2)))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f7980,plain,(
% 57.78/7.75 visValue(vapp(ve1,ve2))|~sQ361_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f7979])).
% 57.78/7.75 fof(f8012,plain,(
% 57.78/7.75 ![X0,X1]: (~vapp(ve1,ve2)=vapp(X0,X1)|~sQ361_spl)),
% 57.78/7.75 inference(resolution,[status(thm)],[f7980,f88])).
% 57.78/7.75 fof(f8211,plain,(
% 57.78/7.75 ![X0]: (~vtcheck(sK21_skl,X0,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))|vtcheck(sK21_skl,vapp(vsubst(sK22_skl,sK23_skl,ve1),X0),sK24_skl)|~sQ10_spl|~sQ15_spl)),
% 57.78/7.75 inference(resolution,[status(thm)],[f5024,f240])).
% 57.78/7.75 fof(f8358,plain,(
% 57.78/7.75 $false|~sQ361_spl),
% 57.78/7.75 inference(equality_resolution,[status(thm)],[f8012])).
% 57.78/7.75 fof(f8359,plain,(
% 57.78/7.75 ~sQ361_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f8358])).
% 57.78/7.75 fof(f9084,definition,(
% 57.78/7.75 sQ383_spl <=> (sK23_skl=sK23_skl)),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f9086,plain,(
% 57.78/7.75 ~sK23_skl=sK23_skl|sQ383_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f9084])).
% 57.78/7.75 fof(f9105,plain,(
% 57.78/7.75 $false|sQ383_spl),
% 57.78/7.75 inference(trivial_equality_resolution,[status(thm)],[f9086])).
% 57.78/7.75 fof(f9106,plain,(
% 57.78/7.75 sQ383_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f9105])).
% 57.78/7.75 fof(f10380,plain,(
% 57.78/7.75 ![X0]: (X0=sK78_skl(vnoExp,vvar(X0)))),
% 57.78/7.75 inference(resolution,[status(thm)],[f4506,f64])).
% 57.78/7.75 fof(f13135,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,vapp(ve1,ve2))=vvar(sK43_skl(sK21_skl,varrow(sK25_skl,sK24_skl),vabs(sK22_skl,sK25_skl,vapp(ve1,ve2))))|~sQ48_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f3003,f349])).
% 57.78/7.75 fof(f13136,plain,(
% 57.78/7.75 $false|~sQ48_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f13135,f77])).
% 57.78/7.75 fof(f13137,plain,(
% 57.78/7.75 ~sQ48_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f13136])).
% 57.78/7.75 fof(f14528,definition,(
% 57.78/7.75 ![X0]: (sQ477_spl <=> (visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve1))|visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve1))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ477_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f14529,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve1))|visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve1))|~sQ477_spl)),
% 57.78/7.75 inference(component_clause,[status(thm)],[f14528])).
% 57.78/7.75 fof(f14536,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve1))|~sQ477_spl)),
% 57.78/7.75 inference(duplicate_literals_removal,[status(thm)],[f14529])).
% 57.78/7.75 fof(f14539,plain,(
% 57.78/7.75 ![X0]: (~vgensym(vabs(sK22_skl,sK25_skl,ve1))=X0|~sQ477_spl)),
% 57.78/7.75 inference(resolution,[status(thm)],[f14536,f151])).
% 57.78/7.75 fof(f14547,plain,(
% 57.78/7.75 $false|~sQ477_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f14539,f10380])).
% 57.78/7.75 fof(f14552,plain,(
% 57.78/7.75 ~sQ477_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f14547])).
% 57.78/7.75 fof(f14821,plain,(
% 57.78/7.75 ![X0]: (X0=sK26_skl(vnoType,vempty,X0))),
% 57.78/7.75 inference(resolution,[status(thm)],[f2612,f319])).
% 57.78/7.75 fof(f14897,definition,(
% 57.78/7.75 sQ498_spl <=> (ve1=ve1)),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ498_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f14899,plain,(
% 57.78/7.75 ~ve1=ve1|sQ498_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f14897])).
% 57.78/7.75 fof(f14904,plain,(
% 57.78/7.75 $false|sQ498_spl),
% 57.78/7.75 inference(trivial_equality_resolution,[status(thm)],[f14899])).
% 57.78/7.75 fof(f14905,plain,(
% 57.78/7.75 sQ498_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f14904])).
% 57.78/7.75 fof(f15290,definition,(
% 57.78/7.75 sQ505_spl <=> (vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))),sK18_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f15291,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))),sK18_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))))|~sQ505_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f15290])).
% 57.78/7.75 fof(f15294,plain,(
% 57.78/7.75 $false|~sQ505_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f15291,f79])).
% 57.78/7.75 fof(f15295,plain,(
% 57.78/7.75 ~sQ505_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f15294])).
% 57.78/7.75 fof(f15426,definition,(
% 57.78/7.75 sQ516_spl <=> (vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))),sK18_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ516_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f15427,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))),sK18_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),sK24_skl),ve1))))|~sQ516_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f15426])).
% 57.78/7.75 fof(f15430,plain,(
% 57.78/7.75 $false|~sQ516_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f15427,f79])).
% 57.78/7.75 fof(f15431,plain,(
% 57.78/7.75 ~sQ516_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f15430])).
% 57.78/7.75 fof(f15750,definition,(
% 57.78/7.75 ![X0]: (sQ549_spl <=> (visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve2))|visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve2))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f15751,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve2))|visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve2))|~sQ549_spl)),
% 57.78/7.75 inference(component_clause,[status(thm)],[f15750])).
% 57.78/7.75 fof(f15758,plain,(
% 57.78/7.75 ![X0]: (visFreeVar(X0,vabs(sK22_skl,sK25_skl,ve2))|~sQ549_spl)),
% 57.78/7.75 inference(duplicate_literals_removal,[status(thm)],[f15751])).
% 57.78/7.75 fof(f15761,plain,(
% 57.78/7.75 ![X0]: (~vgensym(vabs(sK22_skl,sK25_skl,ve2))=X0|~sQ549_spl)),
% 57.78/7.75 inference(resolution,[status(thm)],[f15758,f151])).
% 57.78/7.75 fof(f15769,plain,(
% 57.78/7.75 $false|~sQ549_spl),
% 57.78/7.75 inference(resolution,[status(thm)],[f15761,f14821])).
% 57.78/7.75 fof(f15775,plain,(
% 57.78/7.75 ~sQ549_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f15769])).
% 57.78/7.75 fof(f16151,definition,(
% 57.78/7.75 sQ569_spl <=> (ve2=ve2)),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ569_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f16153,plain,(
% 57.78/7.75 ~ve2=ve2|sQ569_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f16151])).
% 57.78/7.75 fof(f16159,plain,(
% 57.78/7.75 $false|sQ569_spl),
% 57.78/7.75 inference(trivial_equality_resolution,[status(thm)],[f16153])).
% 57.78/7.75 fof(f16160,plain,(
% 57.78/7.75 sQ569_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f16159])).
% 57.78/7.75 fof(f16388,definition,(
% 57.78/7.75 sQ600_spl <=> (vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))),sK18_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f16389,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))),sK18_skl(sK21_skl,varrow(sK25_skl,varrow(sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)))),vabs(sK22_skl,sK25_skl,sK20_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))))|~sQ600_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f16388])).
% 57.78/7.75 fof(f16392,plain,(
% 57.78/7.75 $false|~sQ600_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f16389,f79])).
% 57.78/7.75 fof(f16393,plain,(
% 57.78/7.75 ~sQ600_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f16392])).
% 57.78/7.75 fof(f16648,definition,(
% 57.78/7.75 sQ620_spl <=> (vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))),sK18_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f16649,plain,(
% 57.78/7.75 vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))=vapp(sK20_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))),sK18_skl(sK21_skl,varrow(sK25_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2)),vabs(sK22_skl,sK25_skl,sK18_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),ve2))))|~sQ620_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f16648])).
% 57.78/7.75 fof(f16652,plain,(
% 57.78/7.75 $false|~sQ620_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f16649,f79])).
% 57.78/7.75 fof(f16653,plain,(
% 57.78/7.75 ~sQ620_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f16652])).
% 57.78/7.75 fof(f16680,definition,(
% 57.78/7.75 sQ623_spl <=> (vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK16_skl(vnoExp,ve2))),sK38_skl(vnoExp,sK16_skl(vnoExp,ve2)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f16681,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK16_skl(vnoExp,ve2))),sK38_skl(vnoExp,sK16_skl(vnoExp,ve2))))|~sQ623_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f16680])).
% 57.78/7.75 fof(f16694,plain,(
% 57.78/7.75 $false|~sQ623_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f16681,f187])).
% 57.78/7.75 fof(f16695,plain,(
% 57.78/7.75 ~sQ623_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f16694])).
% 57.78/7.75 fof(f16778,definition,(
% 57.78/7.75 sQ632_spl <=> (vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK63_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK64_skl(vnoExp,sK16_skl(vnoExp,ve2)))))),
% 57.78/7.75 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 57.78/7.75 fof(f16779,plain,(
% 57.78/7.75 vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK63_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK64_skl(vnoExp,sK16_skl(vnoExp,ve2))))|~sQ632_spl),
% 57.78/7.75 inference(component_clause,[status(thm)],[f16778])).
% 57.78/7.75 fof(f16796,plain,(
% 57.78/7.75 $false|~sQ632_spl),
% 57.78/7.75 inference(forward_subsumption_resolution,[status(thm)],[f16779,f187])).
% 57.78/7.75 fof(f16797,plain,(
% 57.78/7.75 ~sQ632_spl),
% 57.78/7.75 inference(contradiction_clause,[status(thm)],[f16796])).
% 57.78/7.76 fof(f16810,definition,(
% 57.78/7.76 sQ637_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK74_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK75_skl(vnoExp,sK16_skl(vnoExp,ve2))),vgetSomeExp(sK76_skl(vnoExp,sK16_skl(vnoExp,ve2))))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f16811,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK74_skl(vnoExp,sK16_skl(vnoExp,ve2)),sK75_skl(vnoExp,sK16_skl(vnoExp,ve2))),vgetSomeExp(sK76_skl(vnoExp,sK16_skl(vnoExp,ve2)))))|~sQ637_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f16810])).
% 57.78/7.76 fof(f16826,plain,(
% 57.78/7.76 $false|~sQ637_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f16811,f187])).
% 57.78/7.76 fof(f16827,plain,(
% 57.78/7.76 ~sQ637_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f16826])).
% 57.78/7.76 fof(f18397,definition,(
% 57.78/7.76 sQ703_spl <=> (vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))),sK38_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ703_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f18398,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))),sK38_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))))|~sQ703_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f18397])).
% 57.78/7.76 fof(f18411,plain,(
% 57.78/7.76 $false|~sQ703_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f18398,f187])).
% 57.78/7.76 fof(f18412,plain,(
% 57.78/7.76 ~sQ703_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f18411])).
% 57.78/7.76 fof(f19175,definition,(
% 57.78/7.76 sQ711_spl <=> (vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK63_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK64_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ711_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f19176,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK63_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK64_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))))|~sQ711_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f19175])).
% 57.78/7.76 fof(f19191,plain,(
% 57.78/7.76 $false|~sQ711_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f19176,f187])).
% 57.78/7.76 fof(f19192,plain,(
% 57.78/7.76 ~sQ711_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f19191])).
% 57.78/7.76 fof(f19846,definition,(
% 57.78/7.76 sQ751_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK74_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK75_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))),vgetSomeExp(sK76_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ751_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f19847,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK74_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)),sK75_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl))),vgetSomeExp(sK76_skl(vnoExp,sK18_skl(sK21_skl,sK25_skl,sK23_skl)))))|~sQ751_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f19846])).
% 57.78/7.76 fof(f19864,plain,(
% 57.78/7.76 $false|~sQ751_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f19847,f187])).
% 57.78/7.76 fof(f19865,plain,(
% 57.78/7.76 ~sQ751_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f19864])).
% 57.78/7.76 fof(f20790,definition,(
% 57.78/7.76 sQ836_spl <=> (vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))),sK38_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ836_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f20791,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))),sK38_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))))|~sQ836_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f20790])).
% 57.78/7.76 fof(f20804,plain,(
% 57.78/7.76 $false|~sQ836_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f20791,f187])).
% 57.78/7.76 fof(f20805,plain,(
% 57.78/7.76 ~sQ836_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f20804])).
% 57.78/7.76 fof(f21451,definition,(
% 57.78/7.76 sQ858_spl <=> (vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK63_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK64_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ858_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f21452,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK63_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK64_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))))|~sQ858_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f21451])).
% 57.78/7.76 fof(f21467,plain,(
% 57.78/7.76 $false|~sQ858_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f21452,f187])).
% 57.78/7.76 fof(f21468,plain,(
% 57.78/7.76 ~sQ858_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f21467])).
% 57.78/7.76 fof(f21701,definition,(
% 57.78/7.76 sQ884_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK74_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK75_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))),vgetSomeExp(sK76_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ884_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f21702,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK74_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)),sK75_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl))),vgetSomeExp(sK76_skl(vnoExp,sK20_skl(sK21_skl,sK25_skl,sK23_skl)))))|~sQ884_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f21701])).
% 57.78/7.76 fof(f21717,plain,(
% 57.78/7.76 $false|~sQ884_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f21702,f187])).
% 57.78/7.76 fof(f21718,plain,(
% 57.78/7.76 ~sQ884_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f21717])).
% 57.78/7.76 fof(f22196,plain,(
% 57.78/7.76 vapp(ve1,ve2)=vvar(sK43_skl(sK21_skl,sK24_skl,vapp(ve1,ve2)))|~sQ327_spl),
% 57.78/7.76 inference(resolution,[status(thm)],[f7038,f349])).
% 57.78/7.76 fof(f22197,plain,(
% 57.78/7.76 $false|~sQ327_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f22196,f78])).
% 57.78/7.76 fof(f22198,plain,(
% 57.78/7.76 ~sQ327_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f22197])).
% 57.78/7.76 fof(f24754,definition,(
% 57.78/7.76 sQ1050_spl <=> (vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)))=vabs(sK4_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),sK5_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),vsubst(sK6_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),sK7_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),sK8_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ1050_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f24755,plain,(
% 57.78/7.76 vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)))=vabs(sK4_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),sK5_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),vsubst(sK6_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),sK7_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl),sK8_skl(vapp(sK20_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2)),sK18_skl(sK21_skl,sK19_skl(vbind(sK22_skl,sK25_skl,sK21_skl),sK24_skl,vapp(ve1,ve2)),vsubst(sK22_skl,sK23_skl,ve2))),ve2,sK23_skl,sK22_skl)))|~sQ1050_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f24754])).
% 57.78/7.76 fof(f24879,plain,(
% 57.78/7.76 $false|~sQ1050_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f24755,f79])).
% 57.78/7.76 fof(f24880,plain,(
% 57.78/7.76 ~sQ1050_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f24879])).
% 57.78/7.76 fof(f25529,definition,(
% 57.78/7.76 sQ1081_spl <=> (vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK77_skl(vnoExp,ve2))),sK38_skl(vnoExp,sK77_skl(vnoExp,ve2)))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ1081_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f25530,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vgetSomeExp(sK37_skl(vnoExp,sK77_skl(vnoExp,ve2))),sK38_skl(vnoExp,sK77_skl(vnoExp,ve2))))|~sQ1081_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f25529])).
% 57.78/7.76 fof(f25543,plain,(
% 57.78/7.76 $false|~sQ1081_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f25530,f187])).
% 57.78/7.76 fof(f25544,plain,(
% 57.78/7.76 ~sQ1081_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f25543])).
% 57.78/7.76 fof(f26217,definition,(
% 57.78/7.76 sQ1085_spl <=> (vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK63_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK64_skl(vnoExp,sK77_skl(vnoExp,ve2)))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ1085_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f26218,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vsubst(sK62_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK63_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK64_skl(vnoExp,sK77_skl(vnoExp,ve2))))|~sQ1085_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f26217])).
% 57.78/7.76 fof(f26233,plain,(
% 57.78/7.76 $false|~sQ1085_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f26218,f187])).
% 57.78/7.76 fof(f26234,plain,(
% 57.78/7.76 ~sQ1085_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f26233])).
% 57.78/7.76 fof(f26243,definition,(
% 57.78/7.76 sQ1090_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK74_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK75_skl(vnoExp,sK77_skl(vnoExp,ve2))),vgetSomeExp(sK76_skl(vnoExp,sK77_skl(vnoExp,ve2))))))),
% 57.78/7.76 introduced(definition,[new_symbols(definition,[sQ1090_spl])],[split_symbol_definition])).
% 57.78/7.76 fof(f26244,plain,(
% 57.78/7.76 vnoExp=vsomeExp(vapp(vabs(sK73_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK74_skl(vnoExp,sK77_skl(vnoExp,ve2)),sK75_skl(vnoExp,sK77_skl(vnoExp,ve2))),vgetSomeExp(sK76_skl(vnoExp,sK77_skl(vnoExp,ve2)))))|~sQ1090_spl),
% 57.78/7.76 inference(component_clause,[status(thm)],[f26243])).
% 57.78/7.76 fof(f26259,plain,(
% 57.78/7.76 $false|~sQ1090_spl),
% 57.78/7.76 inference(forward_subsumption_resolution,[status(thm)],[f26244,f187])).
% 57.78/7.76 fof(f26260,plain,(
% 57.78/7.76 ~sQ1090_spl),
% 57.78/7.76 inference(contradiction_clause,[status(thm)],[f26259])).
% 57.78/7.76 fof(f26409,plain,(
% 57.78/7.76 vtcheck(sK21_skl,vapp(vsubst(sK22_skl,sK23_skl,ve1),vsubst(sK22_skl,sK23_skl,ve2)),sK24_skl)|~sQ15_spl|~sQ10_spl|~sQ18_spl),
% 57.78/7.76 inference(resolution,[status(thm)],[f8211,f4828])).
% 57.78/7.76 fof(f26410,plain,(
% 57.78/7.76 vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vapp(ve1,ve2)),sK24_skl)|~sQ15_spl|~sQ10_spl|~sQ18_spl),
% 57.78/7.79 inference(forward_demodulation,[status(thm)],[f468,f26409])).
% 57.78/7.79 fof(f26411,plain,(
% 57.78/7.79 $false|~sQ15_spl|~sQ10_spl|~sQ18_spl),
% 57.78/7.79 inference(forward_subsumption_resolution,[status(thm)],[f26410,f269])).
% 57.78/7.79 fof(f26412,plain,(
% 57.78/7.79 ~sQ15_spl|~sQ10_spl|~sQ18_spl),
% 57.78/7.79 inference(contradiction_clause,[status(thm)],[f26411])).
% 57.78/7.79 fof(f26413,plain,(
% 57.78/7.79 $false),
% 57.78/7.79 inference(sat_refutation,[status(thm)],[f2178,f2199,f2214,f3000,f3919,f4435,f4461,f4497,f4690,f4692,f5154,f5195,f5394,f5468,f5862,f5911,f6234,f6341,f6521,f7053,f8359,f9106,f13137,f14552,f14905,f15295,f15431,f15775,f16160,f16393,f16653,f16695,f16797,f16827,f18412,f19192,f19865,f20805,f21468,f21718,f22198,f24880,f25544,f26234,f26260,f26412])).
% 57.78/7.79 % SZS output end CNFRefutation for theBenchmark.p
% 3.85/7.97 % Elapsed time: 7.596065 seconds
% 3.85/7.97 % CPU time: 58.886650 seconds
% 3.85/7.97 % Total memory used: 489.702 MB
% 3.85/7.97 % Net memory used: 448.254 MB
%------------------------------------------------------------------------------