%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM137+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 : n018.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 10.25s 1.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM137+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.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 14:20:14 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 10.25/1.77 % Refutation found
% 10.25/1.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.25/1.77 % SZS output start CNFRefutation for theBenchmark
% 10.25/1.77 fof(f3,axiom,(
% 10.25/1.77 (! [VExp0,VExp1,VExp2,VExp3] :( ( vapp(VExp0,VExp1) = vapp(VExp2,VExp3)=> ( VExp0 = VExp2& VExp1 = VExp3 ) )& ( ( VExp0 = VExp2& VExp1 = VExp3 )=> vapp(VExp0,VExp1) = vapp(VExp2,VExp3) ) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f4,axiom,(
% 10.25/1.77 (! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f5,axiom,(
% 10.25/1.77 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f6,axiom,(
% 10.25/1.77 (! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f12,axiom,(
% 10.25/1.77 (! [VVar0,VExp0,Ve1,Vv,Ve2] :( ( VVar0 = Vv& VExp0 = vapp(Ve1,Ve2) )=> ( ( ( visFreeVar(Vv,Ve1)| visFreeVar(Vv,Ve2) )=> visFreeVar(VVar0,VExp0) )& ( visFreeVar(VVar0,VExp0)=> ( visFreeVar(Vv,Ve1)| visFreeVar(Vv,Ve2) ) ) ) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f21,axiom,(
% 10.25/1.77 (! [VOptTyp0,RESULT,Ve] :( VOptTyp0 = vsomeType(Ve)=> ( RESULT = vgetSomeType(VOptTyp0)=> RESULT = Ve ) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f29,axiom,(
% 10.25/1.77 (! [Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vvar(Vy) )=> ( Vx = Vy=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = Ve ) ) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f38,axiom,(
% 10.25/1.77 (! [VExp0] : vnoExp != vsomeExp(VExp0) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f39,axiom,(
% 10.25/1.77 (! [VOptExp0] :( VOptExp0 = vnoExp=> ~ visSomeExp(VOptExp0) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f41,axiom,(
% 10.25/1.77 (! [VOptExp0,RESULT,Ve] :( VOptExp0 = vsomeExp(Ve)=> ( RESULT = vgetSomeExp(VOptExp0)=> RESULT = Ve ) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f43,axiom,(
% 10.25/1.77 (! [Vx,VS,Ve,VExp0,RESULT] :( VExp0 = vabs(Vx,VS,Ve)=> ( RESULT = vreduce(VExp0)=> RESULT = vnoExp ) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f53,axiom,(
% 10.25/1.77 (! [VS,VC,Ve1,Ve2,VT] :( ( vtcheck(VC,Ve1,varrow(VS,VT))& vtcheck(VC,Ve2,VS) )=> vtcheck(VC,vapp(Ve1,Ve2),VT) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f54,axiom,(
% 10.25/1.77 (! [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) ) )) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f56,axiom,(
% 10.25/1.77 (! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,ve1app)& vtcheck(vbind(Vx,VS,VC),ve1app,VT) )=> vtcheck(VC,ve1app,VT) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f57,axiom,(
% 10.25/1.77 (! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,ve2app)& vtcheck(vbind(Vx,VS,VC),ve2app,VT) )=> vtcheck(VC,ve2app,VT) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f58,conjecture,(
% 10.25/1.77 (! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,vapp(ve1app,ve2app))& vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT) )=> vtcheck(VC,vapp(ve1app,ve2app),VT) ) )),
% 10.25/1.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.77 fof(f59,negated_conjecture,(
% 10.25/1.77 ~((! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,vapp(ve1app,ve2app))& vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT) )=> vtcheck(VC,vapp(ve1app,ve2app),VT) ) ))),
% 10.25/1.77 inference(negated_conjecture,[status(cth)],[f58])).
% 10.25/1.77 fof(f70,plain,(
% 10.25/1.77 ![VExp0,VExp1,VExp2,VExp3]: ((~vapp(VExp0,VExp1)=vapp(VExp2,VExp3)|(VExp0=VExp2&VExp1=VExp3))&((~VExp0=VExp2|~VExp1=VExp3)|vapp(VExp0,VExp1)=vapp(VExp2,VExp3)))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 10.25/1.77 fof(f71,plain,(
% 10.25/1.77 (![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)))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f70])).
% 10.25/1.77 fof(f72,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X0=X2)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f71])).
% 10.25/1.77 fof(f73,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X1=X3)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f71])).
% 10.25/1.77 fof(f75,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~vvar(X0)=vabs(X1,X2,X3))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f4])).
% 10.25/1.77 fof(f76,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f5])).
% 10.25/1.77 fof(f77,plain,(
% 10.25/1.77 ![X0,X1,X2,X3,X4]: (~vabs(X0,X1,X2)=vapp(X3,X4))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f6])).
% 10.25/1.77 fof(f95,plain,(
% 10.25/1.77 ![VVar0,VExp0,Ve1,Vv,Ve2]: ((~VVar0=Vv|~VExp0=vapp(Ve1,Ve2))|(((~visFreeVar(Vv,Ve1)&~visFreeVar(Vv,Ve2))|visFreeVar(VVar0,VExp0))&(~visFreeVar(VVar0,VExp0)|(visFreeVar(Vv,Ve1)|visFreeVar(Vv,Ve2)))))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 10.25/1.77 fof(f96,plain,(
% 10.25/1.77 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X3)|visFreeVar(X0,X2))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f95])).
% 10.25/1.77 fof(f97,plain,(
% 10.25/1.77 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X4)|visFreeVar(X0,X2))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f95])).
% 10.25/1.77 fof(f122,plain,(
% 10.25/1.77 ![VOptTyp0,RESULT,Ve]: (~VOptTyp0=vsomeType(Ve)|(~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 10.25/1.77 fof(f123,plain,(
% 10.25/1.77 ![VOptTyp0,Ve]: (~VOptTyp0=vsomeType(Ve)|(![RESULT]: (~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve)))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f122])).
% 10.25/1.77 fof(f124,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~X0=vsomeType(X1)|~X2=vgetSomeType(X0)|X2=X1)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f123])).
% 10.25/1.77 fof(f150,plain,(
% 10.25/1.77 ![Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve)))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 10.25/1.77 fof(f151,plain,(
% 10.25/1.77 ![Vx,Vy,VVar0,VExp0,VExp1,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve))))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f150])).
% 10.25/1.77 fof(f152,plain,(
% 10.25/1.77 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=X3|~X4=vvar(X5)|~X1=X5|~X6=vsubst(X0,X2,X4)|X6=X3)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f151])).
% 10.25/1.77 fof(f185,plain,(
% 10.25/1.77 ![X0]: (~vnoExp=vsomeExp(X0))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f38])).
% 10.25/1.77 fof(f186,plain,(
% 10.25/1.77 ![VOptExp0]: (~VOptExp0=vnoExp|~visSomeExp(VOptExp0))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 10.25/1.77 fof(f187,plain,(
% 10.25/1.77 ![X0]: (~X0=vnoExp|~visSomeExp(X0))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f186])).
% 10.25/1.77 fof(f191,plain,(
% 10.25/1.77 ![VOptExp0,RESULT,Ve]: (~VOptExp0=vsomeExp(Ve)|(~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 10.25/1.77 fof(f192,plain,(
% 10.25/1.77 ![VOptExp0,Ve]: (~VOptExp0=vsomeExp(Ve)|(![RESULT]: (~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve)))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f191])).
% 10.25/1.77 fof(f193,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~X0=vsomeExp(X1)|~X2=vgetSomeExp(X0)|X2=X1)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f192])).
% 10.25/1.77 fof(f197,plain,(
% 10.25/1.77 ![Vx,VS,Ve,VExp0,RESULT]: (~VExp0=vabs(Vx,VS,Ve)|(~RESULT=vreduce(VExp0)|RESULT=vnoExp))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 10.25/1.77 fof(f198,plain,(
% 10.25/1.77 ![VExp0]: ((![Vx,VS,Ve]: ~VExp0=vabs(Vx,VS,Ve))|(![RESULT]: (~RESULT=vreduce(VExp0)|RESULT=vnoExp)))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f197])).
% 10.25/1.77 fof(f199,plain,(
% 10.25/1.77 ![X0,X1,X2,X3,X4]: (~X0=vabs(X1,X2,X3)|~X4=vreduce(X0)|X4=vnoExp)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f198])).
% 10.25/1.77 fof(f236,plain,(
% 10.25/1.77 ![VS,VC,Ve1,Ve2,VT]: ((~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 10.25/1.77 fof(f237,plain,(
% 10.25/1.77 ![VC,Ve1,Ve2,VT]: ((![VS]: (~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS)))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f236])).
% 10.25/1.77 fof(f238,plain,(
% 10.25/1.77 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,X1,varrow(X2,X3))|~vtcheck(X0,X4,X2)|vtcheck(X0,vapp(X1,X4),X3))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f237])).
% 10.25/1.77 fof(f239,plain,(
% 10.25/1.77 ![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)))))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 10.25/1.77 fof(f240,definition,(
% 10.25/1.77 ![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)))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 10.25/1.77 fof(f241,plain,(
% 10.25/1.77 ![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)))))),
% 10.25/1.77 inference(formula_renaming,[status(thm)],[f239,f240])).
% 10.25/1.77 fof(f242,plain,(
% 10.25/1.77 ![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)))))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f241])).
% 10.25/1.77 fof(f243,plain,(
% 10.25/1.77 ![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)))))),
% 10.25/1.77 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))],[f242])).
% 10.25/1.77 fof(f244,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f243])).
% 10.25/1.77 fof(f245,plain,(
% 10.25/1.77 ![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)))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f243])).
% 10.25/1.77 fof(f246,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|vtcheck(X0,sK18_skl(X0,X2,X1),sK19_skl(X0,X2,X1)))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f243])).
% 10.25/1.77 fof(f250,plain,(
% 10.25/1.77 ![Vx,VS,VC,VT]: ((visFreeVar(Vx,ve1app)|~vtcheck(vbind(Vx,VS,VC),ve1app,VT))|vtcheck(VC,ve1app,VT))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 10.25/1.77 fof(f251,plain,(
% 10.25/1.77 ![VC,VT]: ((![Vx]: (visFreeVar(Vx,ve1app)|(![VS]: ~vtcheck(vbind(Vx,VS,VC),ve1app,VT))))|vtcheck(VC,ve1app,VT))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f250])).
% 10.25/1.77 fof(f252,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (visFreeVar(X0,ve1app)|~vtcheck(vbind(X0,X1,X2),ve1app,X3)|vtcheck(X2,ve1app,X3))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f251])).
% 10.25/1.77 fof(f253,plain,(
% 10.25/1.77 ![Vx,VS,VC,VT]: ((visFreeVar(Vx,ve2app)|~vtcheck(vbind(Vx,VS,VC),ve2app,VT))|vtcheck(VC,ve2app,VT))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 10.25/1.77 fof(f254,plain,(
% 10.25/1.77 ![VC,VT]: ((![Vx]: (visFreeVar(Vx,ve2app)|(![VS]: ~vtcheck(vbind(Vx,VS,VC),ve2app,VT))))|vtcheck(VC,ve2app,VT))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f253])).
% 10.25/1.77 fof(f255,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (visFreeVar(X0,ve2app)|~vtcheck(vbind(X0,X1,X2),ve2app,X3)|vtcheck(X2,ve2app,X3))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f254])).
% 10.25/1.77 fof(f256,plain,(
% 10.25/1.77 (?[Vx,VS,VC,VT]: ((~visFreeVar(Vx,vapp(ve1app,ve2app))&vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT))&~vtcheck(VC,vapp(ve1app,ve2app),VT)))),
% 10.25/1.77 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 10.25/1.77 fof(f257,plain,(
% 10.25/1.77 ?[VC,VT]: ((?[Vx]: (~visFreeVar(Vx,vapp(ve1app,ve2app))&(?[VS]: vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT))))&~vtcheck(VC,vapp(ve1app,ve2app),VT))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f256])).
% 10.25/1.77 fof(f258,plain,(
% 10.25/1.77 ((~visFreeVar(sK23_skl,vapp(ve1app,ve2app))&vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),vapp(ve1app,ve2app),sK22_skl))&~vtcheck(sK21_skl,vapp(ve1app,ve2app),sK22_skl))),
% 10.25/1.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(VC,sK21_skl),skolemize(VT,sK22_skl),skolemize(Vx,sK23_skl),skolemize(VS,sK24_skl)],[f257])).
% 10.25/1.77 fof(f259,plain,(
% 10.25/1.77 ~visFreeVar(sK23_skl,vapp(ve1app,ve2app))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f258])).
% 10.25/1.77 fof(f260,plain,(
% 10.25/1.77 vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),vapp(ve1app,ve2app),sK22_skl)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f258])).
% 10.25/1.77 fof(f261,plain,(
% 10.25/1.77 ~vtcheck(sK21_skl,vapp(ve1app,ve2app),sK22_skl)),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f258])).
% 10.25/1.77 fof(f299,definition,(
% 10.25/1.77 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 10.25/1.77 fof(f300,plain,(
% 10.25/1.77 ![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)))))),
% 10.25/1.77 inference(formula_renaming,[status(thm)],[f240,f299])).
% 10.25/1.77 fof(f301,plain,(
% 10.25/1.77 ![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))))))),
% 10.25/1.77 inference(NNF_transformation,[status(thm)],[f300])).
% 10.25/1.77 fof(f302,plain,(
% 10.25/1.77 (![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))))))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f301])).
% 10.25/1.77 fof(f303,plain,(
% 10.25/1.77 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|(sP7_prd(sK42_skl(VC,VT,Ve),VC,VT,Ve)|((Ve=vabs(sK43_skl(VC,VT,Ve),sK45_skl(VC,VT,Ve),sK44_skl(VC,VT,Ve))&VT=varrow(sK45_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve)))&vtcheck(vbind(sK43_skl(VC,VT,Ve),sK45_skl(VC,VT,Ve),VC),sK44_skl(VC,VT,Ve),sK46_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))))))),
% 10.25/1.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK42_skl,sK43_skl,sK44_skl,sK45_skl,sK46_skl]),skolemize(Vx,sK42_skl(VC,VT,Ve)),skolemize(Vx,sK43_skl(VC,VT,Ve)),skolemize(Ve2,sK44_skl(VC,VT,Ve)),skolemize(VT1,sK45_skl(VC,VT,Ve)),skolemize(VT2,sK46_skl(VC,VT,Ve))],[f302])).
% 10.25/1.77 fof(f304,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|sP7_prd(sK42_skl(X0,X1,X2),X0,X1,X2)|X2=vabs(sK43_skl(X0,X1,X2),sK45_skl(X0,X1,X2),sK44_skl(X0,X1,X2)))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f303])).
% 10.25/1.77 fof(f339,plain,(
% 10.25/1.77 ![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))))),
% 10.25/1.77 inference(NNF_transformation,[status(thm)],[f299])).
% 10.25/1.77 fof(f340,plain,(
% 10.25/1.77 (![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))))),
% 10.25/1.77 inference(miniscoping,[status(thm)],[f339])).
% 10.25/1.77 fof(f341,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|X3=vvar(X0))),
% 10.25/1.77 inference(cnf_transformation,[status(thm)],[f340])).
% 10.25/1.77 fof(f412,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~X0=vapp(X1,X2)|~visFreeVar(X3,X1)|visFreeVar(X3,X0))),
% 10.25/1.77 inference(destructive_equality_resolution,[status(thm)],[f96])).
% 10.25/1.77 fof(f413,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~X0=vapp(X1,X2)|~visFreeVar(X3,X2)|visFreeVar(X3,X0))),
% 10.25/1.77 inference(destructive_equality_resolution,[status(thm)],[f97])).
% 10.25/1.77 fof(f419,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~X0=vvar(X1)|~X2=vsubst(X1,X3,X0)|X2=X3)),
% 10.25/1.77 inference(destructive_equality_resolution,[status(thm)],[f152])).
% 10.25/1.77 fof(f472,plain,(
% 10.25/1.77 ![X0,X1]: (~X0=vgetSomeType(vsomeType(X1))|X0=X1)),
% 10.25/1.77 inference(equality_resolution,[status(thm)],[f124])).
% 10.25/1.77 fof(f542,plain,(
% 10.25/1.77 ![X0,X1,X2]: (~X0=vvar(X1)|vsubst(X1,X2,X0)=X2)),
% 10.25/1.77 inference(equality_resolution,[status(thm)],[f419])).
% 10.25/1.77 fof(f560,plain,(
% 10.25/1.77 ![X0]: (vgetSomeType(vsomeType(X0))=X0)),
% 10.25/1.77 inference(equality_resolution,[status(thm)],[f472])).
% 10.25/1.77 fof(f784,plain,(
% 10.25/1.77 ![X0,X1]: (~X0=vgetSomeExp(vgetSomeType(vsomeType(vsomeExp(X1))))|X0=X1)),
% 10.25/1.77 inference(resolution,[status(thm)],[f193,f560])).
% 10.25/1.77 fof(f786,plain,(
% 10.25/1.77 ![X0,X1]: (~X0=vgetSomeExp(vsomeExp(X1))|X0=X1)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f560,f784])).
% 10.25/1.77 fof(f816,plain,(
% 10.25/1.77 ![X0]: (vgetSomeType(vsomeType(vgetSomeExp(vsomeExp(X0))))=X0)),
% 10.25/1.77 inference(resolution,[status(thm)],[f786,f560])).
% 10.25/1.77 fof(f818,plain,(
% 10.25/1.77 ![X0]: (vgetSomeExp(vsomeExp(X0))=X0)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f560,f816])).
% 10.25/1.77 fof(f939,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~X0=vreduce(vgetSomeExp(vsomeExp(vabs(X1,X2,X3))))|X0=vnoExp)),
% 10.25/1.77 inference(resolution,[status(thm)],[f199,f818])).
% 10.25/1.77 fof(f944,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (~X0=vreduce(vabs(X1,X2,X3))|X0=vnoExp)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f818,f939])).
% 10.25/1.77 fof(f1241,plain,(
% 10.25/1.77 ![X0,X1]: (vsubst(X0,X1,vgetSomeExp(vsomeExp(vvar(X0))))=X1)),
% 10.25/1.77 inference(resolution,[status(thm)],[f542,f818])).
% 10.25/1.77 fof(f1244,plain,(
% 10.25/1.77 ![X0,X1]: (vsubst(X0,X1,vvar(X0))=X1)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f818,f1241])).
% 10.25/1.77 fof(f1437,plain,(
% 10.25/1.77 sP3_prd(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vapp(sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))),
% 10.25/1.77 inference(resolution,[status(thm)],[f244,f260])).
% 10.25/1.77 fof(f1445,definition,(
% 10.25/1.77 sQ23_spl <=> (sP3_prd(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f1446,plain,(
% 10.25/1.77 sP3_prd(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|~sQ23_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f1445])).
% 10.25/1.77 fof(f1448,definition,(
% 10.25/1.77 sQ24_spl <=> (vapp(ve1app,ve2app)=vapp(sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f1449,plain,(
% 10.25/1.77 vapp(ve1app,ve2app)=vapp(sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ24_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f1448])).
% 10.25/1.77 fof(f1451,plain,(
% 10.25/1.77 sQ23_spl|sQ24_spl),
% 10.25/1.77 inference(split_clause,[status(thm)],[f1437,f1445,f1448])).
% 10.25/1.77 fof(f1453,plain,(
% 10.25/1.77 sP3_prd(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl))),
% 10.25/1.77 inference(resolution,[status(thm)],[f245,f260])).
% 10.25/1.77 fof(f1458,definition,(
% 10.25/1.77 sQ26_spl <=> (vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl)))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f1459,plain,(
% 10.25/1.77 vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl))|~sQ26_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f1458])).
% 10.25/1.77 fof(f1461,plain,(
% 10.25/1.77 sQ23_spl|sQ26_spl),
% 10.25/1.77 inference(split_clause,[status(thm)],[f1453,f1445,f1458])).
% 10.25/1.77 fof(f1463,plain,(
% 10.25/1.77 sP3_prd(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))),
% 10.25/1.77 inference(resolution,[status(thm)],[f246,f260])).
% 10.25/1.77 fof(f1468,definition,(
% 10.25/1.77 sQ28_spl <=> (vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f1469,plain,(
% 10.25/1.77 vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ28_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f1468])).
% 10.25/1.77 fof(f1471,plain,(
% 10.25/1.77 sQ23_spl|sQ28_spl),
% 10.25/1.77 inference(split_clause,[status(thm)],[f1463,f1445,f1468])).
% 10.25/1.77 fof(f1998,plain,(
% 10.25/1.77 sP7_prd(sK42_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vabs(sK43_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK45_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK44_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ23_spl),
% 10.25/1.77 inference(resolution,[status(thm)],[f304,f1446])).
% 10.25/1.77 fof(f1999,definition,(
% 10.25/1.77 sQ37_spl <=> (sP7_prd(sK42_skl(sK21_skl,varrow(sK24_skl,sK22_skl),vabs(sK23_skl,sK24_skl,vapp(ve1app,ve2app))),sK21_skl,varrow(sK24_skl,sK22_skl),vabs(sK23_skl,sK24_skl,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2000,plain,(
% 10.25/1.77 sP7_prd(sK42_skl(sK21_skl,varrow(sK24_skl,sK22_skl),vabs(sK23_skl,sK24_skl,vapp(ve1app,ve2app))),sK21_skl,varrow(sK24_skl,sK22_skl),vabs(sK23_skl,sK24_skl,vapp(ve1app,ve2app)))|~sQ37_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f1999])).
% 10.25/1.77 fof(f2006,definition,(
% 10.25/1.77 sQ39_spl <=> (sP7_prd(sK42_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2007,plain,(
% 10.25/1.77 sP7_prd(sK42_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|~sQ39_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2006])).
% 10.25/1.77 fof(f2009,definition,(
% 10.25/1.77 sQ40_spl <=> (vapp(ve1app,ve2app)=vabs(sK43_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK45_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK44_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2010,plain,(
% 10.25/1.77 vapp(ve1app,ve2app)=vabs(sK43_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK45_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK44_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ40_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2009])).
% 10.25/1.77 fof(f2012,plain,(
% 10.25/1.77 sQ39_spl|sQ40_spl|~sQ23_spl),
% 10.25/1.77 inference(split_clause,[status(thm)],[f1998,f2006,f2009,f1445])).
% 10.25/1.77 fof(f2031,plain,(
% 10.25/1.77 vapp(ve1app,ve2app)=vvar(sK42_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ39_spl),
% 10.25/1.77 inference(resolution,[status(thm)],[f2007,f341])).
% 10.25/1.77 fof(f2032,plain,(
% 10.25/1.77 $false|~sQ39_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2031,f76])).
% 10.25/1.77 fof(f2033,plain,(
% 10.25/1.77 ~sQ39_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2032])).
% 10.25/1.77 fof(f2034,plain,(
% 10.25/1.77 $false|~sQ40_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2010,f77])).
% 10.25/1.77 fof(f2035,plain,(
% 10.25/1.77 ~sQ40_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2034])).
% 10.25/1.77 fof(f2036,plain,(
% 10.25/1.77 ve2app=sK18_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|~sQ24_spl),
% 10.25/1.77 inference(resolution,[status(thm)],[f1449,f73])).
% 10.25/1.77 fof(f2037,plain,(
% 10.25/1.77 ve1app=sK20_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))|~sQ24_spl),
% 10.25/1.77 inference(resolution,[status(thm)],[f1449,f72])).
% 10.25/1.77 fof(f2116,plain,(
% 10.25/1.77 ![X0,X1,X2,X3]: (vsubst(X0,vreduce(vabs(X1,X2,X3)),vvar(X0))=vnoExp)),
% 10.25/1.77 inference(resolution,[status(thm)],[f944,f1244])).
% 10.25/1.77 fof(f2122,plain,(
% 10.25/1.77 ![X0,X1,X2]: (vreduce(vabs(X0,X1,X2))=vnoExp)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f1244,f2116])).
% 10.25/1.77 fof(f2245,plain,(
% 10.25/1.77 vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),ve2app,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ24_spl|~sQ28_spl),
% 10.25/1.77 inference(backward_demodulation,[status(thm)],[f2036,f1469])).
% 10.25/1.77 fof(f2247,plain,(
% 10.25/1.77 visFreeVar(sK23_skl,ve2app)|vtcheck(sK21_skl,ve2app,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ24_spl|~sQ28_spl),
% 10.25/1.77 inference(resolution,[status(thm)],[f2245,f255])).
% 10.25/1.77 fof(f2254,definition,(
% 10.25/1.77 sQ64_spl <=> (visFreeVar(sK23_skl,ve2app))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2255,plain,(
% 10.25/1.77 visFreeVar(sK23_skl,ve2app)|~sQ64_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2254])).
% 10.25/1.77 fof(f2257,definition,(
% 10.25/1.77 sQ65_spl <=> (vtcheck(sK21_skl,ve2app,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2258,plain,(
% 10.25/1.77 vtcheck(sK21_skl,ve2app,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|~sQ65_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2257])).
% 10.25/1.77 fof(f2260,plain,(
% 10.25/1.77 sQ64_spl|sQ65_spl|~sQ24_spl|~sQ28_spl),
% 10.25/1.77 inference(split_clause,[status(thm)],[f2247,f2254,f2257,f1448,f1468])).
% 10.25/1.77 fof(f2325,plain,(
% 10.25/1.77 ![X0,X1]: (~X0=vapp(X1,ve2app)|visFreeVar(sK23_skl,X0)|~sQ64_spl)),
% 10.25/1.77 inference(resolution,[status(thm)],[f2255,f413])).
% 10.25/1.77 fof(f2332,plain,(
% 10.25/1.77 vtcheck(vbind(sK23_skl,sK24_skl,sK21_skl),ve1app,varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl))|~sQ24_spl|~sQ26_spl),
% 10.25/1.77 inference(backward_demodulation,[status(thm)],[f2037,f1459])).
% 10.25/1.77 fof(f2333,plain,(
% 10.25/1.77 visFreeVar(sK23_skl,ve1app)|vtcheck(sK21_skl,ve1app,varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl))|~sQ24_spl|~sQ26_spl),
% 10.25/1.77 inference(resolution,[status(thm)],[f2332,f252])).
% 10.25/1.77 fof(f2341,definition,(
% 10.25/1.77 sQ72_spl <=> (visFreeVar(sK23_skl,ve1app))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2342,plain,(
% 10.25/1.77 visFreeVar(sK23_skl,ve1app)|~sQ72_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2341])).
% 10.25/1.77 fof(f2344,definition,(
% 10.25/1.77 sQ73_spl <=> (vtcheck(sK21_skl,ve1app,varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl)))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2345,plain,(
% 10.25/1.77 vtcheck(sK21_skl,ve1app,varrow(sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)),sK22_skl))|~sQ73_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2344])).
% 10.25/1.77 fof(f2347,plain,(
% 10.25/1.77 sQ72_spl|sQ73_spl|~sQ24_spl|~sQ26_spl),
% 10.25/1.77 inference(split_clause,[status(thm)],[f2333,f2341,f2344,f1448,f1458])).
% 10.25/1.77 fof(f2368,plain,(
% 10.25/1.77 ![X0,X1]: (~X0=vapp(ve1app,X1)|visFreeVar(sK23_skl,X0)|~sQ72_spl)),
% 10.25/1.77 inference(resolution,[status(thm)],[f2342,f412])).
% 10.25/1.77 fof(f2502,plain,(
% 10.25/1.77 ![X0,X1]: (visFreeVar(sK23_skl,vsubst(X0,vapp(X1,ve2app),vvar(X0)))|~sQ64_spl)),
% 10.25/1.77 inference(resolution,[status(thm)],[f2325,f1244])).
% 10.25/1.77 fof(f2506,plain,(
% 10.25/1.77 ![X0]: (visFreeVar(sK23_skl,vapp(X0,ve2app))|~sQ64_spl)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f1244,f2502])).
% 10.25/1.77 fof(f2515,plain,(
% 10.25/1.77 $false|~sQ64_spl),
% 10.25/1.77 inference(backward_subsumption_resolution,[status(thm)],[f259,f2506])).
% 10.25/1.77 fof(f2526,plain,(
% 10.25/1.77 ~sQ64_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2515])).
% 10.25/1.77 fof(f2657,plain,(
% 10.25/1.77 ![X0,X1]: (visFreeVar(sK23_skl,vsubst(X0,vapp(ve1app,X1),vvar(X0)))|~sQ72_spl)),
% 10.25/1.77 inference(resolution,[status(thm)],[f2368,f1244])).
% 10.25/1.77 fof(f2661,plain,(
% 10.25/1.77 ![X0]: (visFreeVar(sK23_skl,vapp(ve1app,X0))|~sQ72_spl)),
% 10.25/1.77 inference(forward_demodulation,[status(thm)],[f1244,f2657])).
% 10.25/1.77 fof(f2680,plain,(
% 10.25/1.77 $false|~sQ72_spl),
% 10.25/1.77 inference(backward_subsumption_resolution,[status(thm)],[f259,f2661])).
% 10.25/1.77 fof(f2691,plain,(
% 10.25/1.77 ~sQ72_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2680])).
% 10.25/1.77 fof(f2700,definition,(
% 10.25/1.77 sQ99_spl <=> (vnoExp=vsomeExp(vsubst(sK61_skl(vnoExp,vapp(ve1app,ve2app)),sK62_skl(vnoExp,vapp(ve1app,ve2app)),sK63_skl(vnoExp,vapp(ve1app,ve2app)))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2701,plain,(
% 10.25/1.77 vnoExp=vsomeExp(vsubst(sK61_skl(vnoExp,vapp(ve1app,ve2app)),sK62_skl(vnoExp,vapp(ve1app,ve2app)),sK63_skl(vnoExp,vapp(ve1app,ve2app))))|~sQ99_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2700])).
% 10.25/1.77 fof(f2732,definition,(
% 10.25/1.77 sQ103_spl <=> (vabs(sK23_skl,sK24_skl,ve2app)=vapp(sK20_skl(sK21_skl,varrow(sK24_skl,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))),vabs(sK23_skl,sK24_skl,ve2app)),sK18_skl(sK21_skl,varrow(sK24_skl,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))),vabs(sK23_skl,sK24_skl,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2733,plain,(
% 10.25/1.77 vabs(sK23_skl,sK24_skl,ve2app)=vapp(sK20_skl(sK21_skl,varrow(sK24_skl,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))),vabs(sK23_skl,sK24_skl,ve2app)),sK18_skl(sK21_skl,varrow(sK24_skl,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app))),vabs(sK23_skl,sK24_skl,ve2app)))|~sQ103_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2732])).
% 10.25/1.77 fof(f2736,plain,(
% 10.25/1.77 $false|~sQ103_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2733,f77])).
% 10.25/1.77 fof(f2737,plain,(
% 10.25/1.77 ~sQ103_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2736])).
% 10.25/1.77 fof(f2882,plain,(
% 10.25/1.77 $false|~sQ99_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2701,f185])).
% 10.25/1.77 fof(f2883,plain,(
% 10.25/1.77 ~sQ99_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2882])).
% 10.25/1.77 fof(f2903,definition,(
% 10.25/1.77 sQ112_spl <=> (vnoExp=vsomeExp(vapp(vabs(sK72_skl(vnoExp,vapp(ve1app,ve2app)),sK73_skl(vnoExp,vapp(ve1app,ve2app)),sK74_skl(vnoExp,vapp(ve1app,ve2app))),vgetSomeExp(sK75_skl(vnoExp,vapp(ve1app,ve2app))))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2904,plain,(
% 10.25/1.77 vnoExp=vsomeExp(vapp(vabs(sK72_skl(vnoExp,vapp(ve1app,ve2app)),sK73_skl(vnoExp,vapp(ve1app,ve2app)),sK74_skl(vnoExp,vapp(ve1app,ve2app))),vgetSomeExp(sK75_skl(vnoExp,vapp(ve1app,ve2app)))))|~sQ112_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2903])).
% 10.25/1.77 fof(f2907,plain,(
% 10.25/1.77 $false|~sQ112_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2904,f185])).
% 10.25/1.77 fof(f2908,plain,(
% 10.25/1.77 ~sQ112_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2907])).
% 10.25/1.77 fof(f2948,definition,(
% 10.25/1.77 sQ116_spl <=> (vapp(ve1app,ve2app)=vvar(sK77_skl(vnoExp,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2949,plain,(
% 10.25/1.77 vapp(ve1app,ve2app)=vvar(sK77_skl(vnoExp,vapp(ve1app,ve2app)))|~sQ116_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2948])).
% 10.25/1.77 fof(f2951,definition,(
% 10.25/1.77 sQ117_spl <=> (vapp(ve1app,ve2app)=vabs(sK78_skl(vnoExp,vapp(ve1app,ve2app)),sK79_skl(vnoExp,vapp(ve1app,ve2app)),sK80_skl(vnoExp,vapp(ve1app,ve2app))))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f2952,plain,(
% 10.25/1.77 vapp(ve1app,ve2app)=vabs(sK78_skl(vnoExp,vapp(ve1app,ve2app)),sK79_skl(vnoExp,vapp(ve1app,ve2app)),sK80_skl(vnoExp,vapp(ve1app,ve2app)))|~sQ117_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f2951])).
% 10.25/1.77 fof(f2957,plain,(
% 10.25/1.77 $false|~sQ116_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2949,f76])).
% 10.25/1.77 fof(f2958,plain,(
% 10.25/1.77 ~sQ116_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2957])).
% 10.25/1.77 fof(f2959,plain,(
% 10.25/1.77 $false|~sQ117_spl),
% 10.25/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2952,f77])).
% 10.25/1.77 fof(f2960,plain,(
% 10.25/1.77 ~sQ117_spl),
% 10.25/1.77 inference(contradiction_clause,[status(thm)],[f2959])).
% 10.25/1.77 fof(f3371,plain,(
% 10.25/1.77 ![X0]: (~vtcheck(sK21_skl,X0,sK19_skl(vbind(sK23_skl,sK24_skl,sK21_skl),sK22_skl,vapp(ve1app,ve2app)))|vtcheck(sK21_skl,vapp(ve1app,X0),sK22_skl)|~sQ73_spl)),
% 10.25/1.77 inference(resolution,[status(thm)],[f2345,f238])).
% 10.25/1.77 fof(f3755,definition,(
% 10.25/1.77 sQ156_spl <=> (visSomeExp(vnoExp))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f3756,plain,(
% 10.25/1.77 visSomeExp(vnoExp)|~sQ156_spl),
% 10.25/1.77 inference(component_clause,[status(thm)],[f3755])).
% 10.25/1.77 fof(f3767,definition,(
% 10.25/1.77 ![X0]: (sQ159_spl <=> (~X0=vnoExp|visSomeExp(X0)))),
% 10.25/1.77 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 10.25/1.77 fof(f3768,plain,(
% 10.25/1.77 ![X0]: (~X0=vnoExp|visSomeExp(X0)|~sQ159_spl)),
% 10.25/1.77 inference(component_clause,[status(thm)],[f3767])).
% 10.25/1.78 fof(f3772,plain,(
% 10.25/1.78 ![X0]: (~X0=vnoExp|~sQ159_spl)),
% 10.25/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3768,f187])).
% 10.25/1.78 fof(f3828,plain,(
% 10.25/1.78 $false|~sQ159_spl),
% 10.25/1.78 inference(backward_subsumption_resolution,[status(thm)],[f2122,f3772])).
% 10.25/1.78 fof(f3835,plain,(
% 10.25/1.78 ~sQ159_spl),
% 10.25/1.78 inference(contradiction_clause,[status(thm)],[f3828])).
% 10.25/1.78 fof(f3890,plain,(
% 10.25/1.78 vabs(sK23_skl,sK24_skl,vapp(ve1app,ve2app))=vvar(sK42_skl(sK21_skl,varrow(sK24_skl,sK22_skl),vabs(sK23_skl,sK24_skl,vapp(ve1app,ve2app))))|~sQ37_spl),
% 10.25/1.78 inference(resolution,[status(thm)],[f2000,f341])).
% 10.25/1.78 fof(f3891,plain,(
% 10.25/1.78 $false|~sQ37_spl),
% 10.25/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3890,f75])).
% 10.25/1.78 fof(f3892,plain,(
% 10.25/1.78 ~sQ37_spl),
% 10.25/1.78 inference(contradiction_clause,[status(thm)],[f3891])).
% 10.25/1.78 fof(f3893,plain,(
% 10.25/1.78 ~vnoExp=vnoExp|~sQ156_spl),
% 10.25/1.78 inference(resolution,[status(thm)],[f187,f3756])).
% 10.25/1.78 fof(f3896,plain,(
% 10.25/1.78 $false|~sQ156_spl),
% 10.25/1.78 inference(trivial_equality_resolution,[status(thm)],[f3893])).
% 10.25/1.78 fof(f3897,plain,(
% 10.25/1.78 ~sQ156_spl),
% 10.25/1.78 inference(contradiction_clause,[status(thm)],[f3896])).
% 10.25/1.78 fof(f4773,plain,(
% 10.25/1.78 vtcheck(sK21_skl,vapp(ve1app,ve2app),sK22_skl)|~sQ73_spl|~sQ65_spl),
% 10.25/1.78 inference(resolution,[status(thm)],[f3371,f2258])).
% 10.25/1.78 fof(f4774,plain,(
% 10.25/1.78 $false|~sQ73_spl|~sQ65_spl),
% 10.25/1.78 inference(forward_subsumption_resolution,[status(thm)],[f4773,f261])).
% 10.25/1.78 fof(f4775,plain,(
% 10.25/1.78 ~sQ73_spl|~sQ65_spl),
% 10.25/1.78 inference(contradiction_clause,[status(thm)],[f4774])).
% 10.25/1.78 fof(f4776,plain,(
% 10.25/1.78 $false),
% 10.25/1.78 inference(sat_refutation,[status(thm)],[f1451,f1461,f1471,f2012,f2033,f2035,f2260,f2347,f2526,f2691,f2737,f2883,f2908,f2958,f2960,f3835,f3892,f3897,f4775])).
% 10.25/1.78 % SZS output end CNFRefutation for theBenchmark.p
% 5.51/1.80 % Elapsed time: 1.429516 seconds
% 5.51/1.80 % CPU time: 10.956248 seconds
% 5.51/1.80 % Total memory used: 208.394 MB
% 5.51/1.80 % Net memory used: 192.964 MB
%------------------------------------------------------------------------------