%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM126+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:10:50 PM UTC 2026
% Result : Theorem 49.28s 6.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM126+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:17:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 49.28/6.84 % Refutation found
% 49.28/6.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 49.28/6.84 % SZS output start CNFRefutation for theBenchmark
% 49.28/6.84 fof(f3,axiom,(
% 49.28/6.84 (! [VExp0,VExp1,VExp2,VExp3] :( ( vapp(VExp0,VExp1) = vapp(VExp2,VExp3)=> ( VExp0 = VExp2& VExp1 = VExp3 ) )& ( ( VExp0 = VExp2& VExp1 = VExp3 )=> vapp(VExp0,VExp1) = vapp(VExp2,VExp3) ) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f5,axiom,(
% 49.28/6.84 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f6,axiom,(
% 49.28/6.84 (! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f12,axiom,(
% 49.28/6.84 (! [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) ) ) ) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f21,axiom,(
% 49.28/6.84 (! [VOptTyp0,RESULT,Ve] :( VOptTyp0 = vsomeType(Ve)=> ( RESULT = vgetSomeType(VOptTyp0)=> RESULT = Ve ) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f29,axiom,(
% 49.28/6.84 (! [Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vvar(Vy) )=> ( Vx = Vy=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = Ve ) ) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f41,axiom,(
% 49.28/6.84 (! [VOptExp0,RESULT,Ve] :( VOptExp0 = vsomeExp(Ve)=> ( RESULT = vgetSomeExp(VOptExp0)=> RESULT = Ve ) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f53,axiom,(
% 49.28/6.84 (! [VS,VC,Ve1,Ve2,VT] :( ( vtcheck(VC,Ve1,varrow(VS,VT))& vtcheck(VC,Ve2,VS) )=> vtcheck(VC,vapp(Ve1,Ve2),VT) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f54,axiom,(
% 49.28/6.84 (! [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) ) )) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f57,axiom,(
% 49.28/6.84 (! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,ve1app)& vtcheck(VC,ve1app,VT) )=> vtcheck(vbind(Vx,VS,VC),ve1app,VT) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f58,axiom,(
% 49.28/6.84 (! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,ve2app)& vtcheck(VC,ve2app,VT) )=> vtcheck(vbind(Vx,VS,VC),ve2app,VT) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f59,conjecture,(
% 49.28/6.84 (! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,vapp(ve1app,ve2app))& vtcheck(VC,vapp(ve1app,ve2app),VT) )=> vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT) ) )),
% 49.28/6.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 49.28/6.84 fof(f60,negated_conjecture,(
% 49.28/6.84 ~((! [Vx,VS,VC,VT] :( ( ~ visFreeVar(Vx,vapp(ve1app,ve2app))& vtcheck(VC,vapp(ve1app,ve2app),VT) )=> vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT) ) ))),
% 49.28/6.84 inference(negated_conjecture,[status(cth)],[f59])).
% 49.28/6.84 fof(f71,plain,(
% 49.28/6.84 ![VExp0,VExp1,VExp2,VExp3]: ((~vapp(VExp0,VExp1)=vapp(VExp2,VExp3)|(VExp0=VExp2&VExp1=VExp3))&((~VExp0=VExp2|~VExp1=VExp3)|vapp(VExp0,VExp1)=vapp(VExp2,VExp3)))),
% 49.28/6.84 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 49.28/6.84 fof(f72,plain,(
% 49.28/6.84 (![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)))),
% 49.28/6.84 inference(miniscoping,[status(thm)],[f71])).
% 49.28/6.84 fof(f73,plain,(
% 49.28/6.84 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X0=X2)),
% 49.28/6.84 inference(cnf_transformation,[status(thm)],[f72])).
% 49.28/6.84 fof(f74,plain,(
% 49.28/6.84 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X1=X3)),
% 49.28/6.84 inference(cnf_transformation,[status(thm)],[f72])).
% 49.28/6.84 fof(f77,plain,(
% 49.28/6.84 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 49.28/6.84 inference(cnf_transformation,[status(thm)],[f5])).
% 49.28/6.84 fof(f78,plain,(
% 49.28/6.84 ![X0,X1,X2,X3,X4]: (~vabs(X0,X1,X2)=vapp(X3,X4))),
% 49.28/6.84 inference(cnf_transformation,[status(thm)],[f6])).
% 49.28/6.84 fof(f96,plain,(
% 49.28/6.84 ![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)))))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 50.94/6.84 fof(f97,plain,(
% 50.94/6.84 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X3)|visFreeVar(X0,X2))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f96])).
% 50.94/6.84 fof(f98,plain,(
% 50.94/6.84 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X4)|visFreeVar(X0,X2))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f96])).
% 50.94/6.84 fof(f123,plain,(
% 50.94/6.84 ![VOptTyp0,RESULT,Ve]: (~VOptTyp0=vsomeType(Ve)|(~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 50.94/6.84 fof(f124,plain,(
% 50.94/6.84 ![VOptTyp0,Ve]: (~VOptTyp0=vsomeType(Ve)|(![RESULT]: (~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve)))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f123])).
% 50.94/6.84 fof(f125,plain,(
% 50.94/6.84 ![X0,X1,X2]: (~X0=vsomeType(X1)|~X2=vgetSomeType(X0)|X2=X1)),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f124])).
% 50.94/6.84 fof(f151,plain,(
% 50.94/6.84 ![Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve)))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 50.94/6.84 fof(f152,plain,(
% 50.94/6.84 ![Vx,Vy,VVar0,VExp0,VExp1,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve))))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f151])).
% 50.94/6.84 fof(f153,plain,(
% 50.94/6.84 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=X3|~X4=vvar(X5)|~X1=X5|~X6=vsubst(X0,X2,X4)|X6=X3)),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f152])).
% 50.94/6.84 fof(f192,plain,(
% 50.94/6.84 ![VOptExp0,RESULT,Ve]: (~VOptExp0=vsomeExp(Ve)|(~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 50.94/6.84 fof(f193,plain,(
% 50.94/6.84 ![VOptExp0,Ve]: (~VOptExp0=vsomeExp(Ve)|(![RESULT]: (~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve)))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f192])).
% 50.94/6.84 fof(f194,plain,(
% 50.94/6.84 ![X0,X1,X2]: (~X0=vsomeExp(X1)|~X2=vgetSomeExp(X0)|X2=X1)),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f193])).
% 50.94/6.84 fof(f237,plain,(
% 50.94/6.84 ![VS,VC,Ve1,Ve2,VT]: ((~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 50.94/6.84 fof(f238,plain,(
% 50.94/6.84 ![VC,Ve1,Ve2,VT]: ((![VS]: (~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS)))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f237])).
% 50.94/6.84 fof(f239,plain,(
% 50.94/6.84 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,X1,varrow(X2,X3))|~vtcheck(X0,X4,X2)|vtcheck(X0,vapp(X1,X4),X3))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f238])).
% 50.94/6.84 fof(f240,plain,(
% 50.94/6.84 ![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)))))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 50.94/6.84 fof(f241,definition,(
% 50.94/6.84 ![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)))))),
% 50.94/6.84 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 50.94/6.84 fof(f242,plain,(
% 50.94/6.84 ![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)))))),
% 50.94/6.84 inference(formula_renaming,[status(thm)],[f240,f241])).
% 50.94/6.84 fof(f243,plain,(
% 50.94/6.84 ![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)))))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f242])).
% 50.94/6.84 fof(f244,plain,(
% 50.94/6.84 ![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)))))),
% 50.94/6.84 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))],[f243])).
% 50.94/6.84 fof(f245,plain,(
% 50.94/6.84 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f244])).
% 50.94/6.84 fof(f246,plain,(
% 50.94/6.84 ![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)))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f244])).
% 50.94/6.84 fof(f247,plain,(
% 50.94/6.84 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|vtcheck(X0,sK18_skl(X0,X2,X1),sK19_skl(X0,X2,X1)))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f244])).
% 50.94/6.84 fof(f254,plain,(
% 50.94/6.84 ![Vx,VS,VC,VT]: ((visFreeVar(Vx,ve1app)|~vtcheck(VC,ve1app,VT))|vtcheck(vbind(Vx,VS,VC),ve1app,VT))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 50.94/6.84 fof(f255,plain,(
% 50.94/6.84 ![Vx,VC,VT]: ((visFreeVar(Vx,ve1app)|~vtcheck(VC,ve1app,VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),ve1app,VT)))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f254])).
% 50.94/6.84 fof(f256,plain,(
% 50.94/6.84 ![X0,X1,X2,X3]: (visFreeVar(X0,ve1app)|~vtcheck(X1,ve1app,X2)|vtcheck(vbind(X0,X3,X1),ve1app,X2))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f255])).
% 50.94/6.84 fof(f257,plain,(
% 50.94/6.84 ![Vx,VS,VC,VT]: ((visFreeVar(Vx,ve2app)|~vtcheck(VC,ve2app,VT))|vtcheck(vbind(Vx,VS,VC),ve2app,VT))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 50.94/6.84 fof(f258,plain,(
% 50.94/6.84 ![Vx,VC,VT]: ((visFreeVar(Vx,ve2app)|~vtcheck(VC,ve2app,VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),ve2app,VT)))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f257])).
% 50.94/6.84 fof(f259,plain,(
% 50.94/6.84 ![X0,X1,X2,X3]: (visFreeVar(X0,ve2app)|~vtcheck(X1,ve2app,X2)|vtcheck(vbind(X0,X3,X1),ve2app,X2))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f258])).
% 50.94/6.84 fof(f260,plain,(
% 50.94/6.84 (?[Vx,VS,VC,VT]: ((~visFreeVar(Vx,vapp(ve1app,ve2app))&vtcheck(VC,vapp(ve1app,ve2app),VT))&~vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT)))),
% 50.94/6.84 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 50.94/6.84 fof(f261,plain,(
% 50.94/6.84 ?[Vx,VC,VT]: ((~visFreeVar(Vx,vapp(ve1app,ve2app))&vtcheck(VC,vapp(ve1app,ve2app),VT))&(?[VS]: ~vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT)))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f260])).
% 50.94/6.84 fof(f262,plain,(
% 50.94/6.84 ((~visFreeVar(sK21_skl,vapp(ve1app,ve2app))&vtcheck(sK22_skl,vapp(ve1app,ve2app),sK23_skl))&~vtcheck(vbind(sK21_skl,sK24_skl,sK22_skl),vapp(ve1app,ve2app),sK23_skl))),
% 50.94/6.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(Vx,sK21_skl),skolemize(VC,sK22_skl),skolemize(VT,sK23_skl),skolemize(VS,sK24_skl)],[f261])).
% 50.94/6.84 fof(f263,plain,(
% 50.94/6.84 ~visFreeVar(sK21_skl,vapp(ve1app,ve2app))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f262])).
% 50.94/6.84 fof(f264,plain,(
% 50.94/6.84 vtcheck(sK22_skl,vapp(ve1app,ve2app),sK23_skl)),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f262])).
% 50.94/6.84 fof(f265,plain,(
% 50.94/6.84 ~vtcheck(vbind(sK21_skl,sK24_skl,sK22_skl),vapp(ve1app,ve2app),sK23_skl)),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f262])).
% 50.94/6.84 fof(f303,definition,(
% 50.94/6.84 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 50.94/6.84 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 50.94/6.84 fof(f304,plain,(
% 50.94/6.84 ![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)))))),
% 50.94/6.84 inference(formula_renaming,[status(thm)],[f241,f303])).
% 50.94/6.84 fof(f305,plain,(
% 50.94/6.84 ![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))))))),
% 50.94/6.84 inference(NNF_transformation,[status(thm)],[f304])).
% 50.94/6.84 fof(f306,plain,(
% 50.94/6.84 (![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))))))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f305])).
% 50.94/6.84 fof(f307,plain,(
% 50.94/6.84 (![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))))))),
% 50.94/6.84 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))],[f306])).
% 50.94/6.84 fof(f308,plain,(
% 50.94/6.84 ![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)))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f307])).
% 50.94/6.84 fof(f343,plain,(
% 50.94/6.84 ![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))))),
% 50.94/6.84 inference(NNF_transformation,[status(thm)],[f303])).
% 50.94/6.84 fof(f344,plain,(
% 50.94/6.84 (![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))))),
% 50.94/6.84 inference(miniscoping,[status(thm)],[f343])).
% 50.94/6.84 fof(f345,plain,(
% 50.94/6.84 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|X3=vvar(X0))),
% 50.94/6.84 inference(cnf_transformation,[status(thm)],[f344])).
% 50.94/6.84 fof(f416,plain,(
% 50.94/6.84 ![X0,X1,X2,X3]: (~X0=vapp(X1,X2)|~visFreeVar(X3,X1)|visFreeVar(X3,X0))),
% 50.94/6.84 inference(destructive_equality_resolution,[status(thm)],[f97])).
% 50.94/6.84 fof(f417,plain,(
% 50.94/6.84 ![X0,X1,X2,X3]: (~X0=vapp(X1,X2)|~visFreeVar(X3,X2)|visFreeVar(X3,X0))),
% 50.94/6.84 inference(destructive_equality_resolution,[status(thm)],[f98])).
% 50.94/6.84 fof(f423,plain,(
% 50.94/6.84 ![X0,X1,X2,X3]: (~X0=vvar(X1)|~X2=vsubst(X1,X3,X0)|X2=X3)),
% 50.94/6.84 inference(destructive_equality_resolution,[status(thm)],[f153])).
% 50.94/6.84 fof(f476,plain,(
% 50.94/6.84 ![X0,X1]: (~X0=vgetSomeType(vsomeType(X1))|X0=X1)),
% 50.94/6.84 inference(equality_resolution,[status(thm)],[f125])).
% 50.94/6.84 fof(f542,plain,(
% 50.94/6.84 ![X0,X1,X2]: (~X0=vvar(X1)|vsubst(X1,X2,X0)=X2)),
% 50.94/6.84 inference(equality_resolution,[status(thm)],[f423])).
% 50.94/6.84 fof(f569,plain,(
% 50.94/6.84 ![X0]: (vgetSomeType(vsomeType(X0))=X0)),
% 50.94/6.84 inference(equality_resolution,[status(thm)],[f476])).
% 50.94/6.84 fof(f744,plain,(
% 50.94/6.84 ![X0,X1]: (~X0=vgetSomeExp(vgetSomeType(vsomeType(vsomeExp(X1))))|X0=X1)),
% 50.94/6.84 inference(resolution,[status(thm)],[f194,f569])).
% 50.94/6.84 fof(f746,plain,(
% 50.94/6.84 ![X0,X1]: (~X0=vgetSomeExp(vsomeExp(X1))|X0=X1)),
% 50.94/6.84 inference(forward_demodulation,[status(thm)],[f569,f744])).
% 50.94/6.84 fof(f813,plain,(
% 50.94/6.84 ![X0]: (vgetSomeType(vsomeType(vgetSomeExp(vsomeExp(X0))))=X0)),
% 50.94/6.84 inference(resolution,[status(thm)],[f746,f569])).
% 50.94/6.84 fof(f815,plain,(
% 50.94/6.84 ![X0]: (vgetSomeExp(vsomeExp(X0))=X0)),
% 50.94/6.84 inference(forward_demodulation,[status(thm)],[f569,f813])).
% 50.94/6.84 fof(f1242,plain,(
% 50.94/6.84 ![X0,X1]: (vsubst(X0,X1,vgetSomeExp(vsomeExp(vvar(X0))))=X1)),
% 50.94/6.84 inference(resolution,[status(thm)],[f542,f815])).
% 50.94/6.84 fof(f1245,plain,(
% 50.94/6.84 ![X0,X1]: (vsubst(X0,X1,vvar(X0))=X1)),
% 50.94/6.85 inference(forward_demodulation,[status(thm)],[f815,f1242])).
% 50.94/6.85 fof(f1439,plain,(
% 50.94/6.85 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 50.94/6.85 inference(resolution,[status(thm)],[f245,f264])).
% 50.94/6.85 fof(f1440,definition,(
% 50.94/6.85 sQ20_spl <=> (sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 50.94/6.85 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 50.94/6.85 fof(f1441,plain,(
% 50.94/6.85 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~sQ20_spl),
% 50.94/6.85 inference(component_clause,[status(thm)],[f1440])).
% 50.94/6.85 fof(f1443,definition,(
% 50.94/6.85 sQ21_spl <=> (vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))))),
% 50.94/6.85 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 50.94/6.85 fof(f1444,plain,(
% 50.94/6.85 vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ21_spl),
% 50.94/6.85 inference(component_clause,[status(thm)],[f1443])).
% 50.94/6.85 fof(f1446,plain,(
% 50.94/6.85 sQ20_spl|sQ21_spl),
% 50.94/6.85 inference(split_clause,[status(thm)],[f1439,f1440,f1443])).
% 50.94/6.85 fof(f1447,plain,(
% 50.94/6.85 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vtcheck(sK22_skl,sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl))),
% 50.94/6.85 inference(resolution,[status(thm)],[f246,f264])).
% 50.94/6.85 fof(f1448,definition,(
% 50.94/6.85 sQ22_spl <=> (vtcheck(sK22_skl,sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl)))),
% 50.94/6.85 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 50.94/6.85 fof(f1449,plain,(
% 50.94/6.85 vtcheck(sK22_skl,sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl))|~sQ22_spl),
% 50.94/6.85 inference(component_clause,[status(thm)],[f1448])).
% 50.94/6.85 fof(f1451,plain,(
% 50.94/6.85 sQ20_spl|sQ22_spl),
% 50.94/6.85 inference(split_clause,[status(thm)],[f1447,f1440,f1448])).
% 50.94/6.85 fof(f1452,plain,(
% 50.94/6.85 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vtcheck(sK22_skl,sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 50.94/6.85 inference(resolution,[status(thm)],[f247,f264])).
% 50.94/6.85 fof(f1453,definition,(
% 50.94/6.85 sQ23_spl <=> (vtcheck(sK22_skl,sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))))),
% 50.94/6.85 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 50.94/6.85 fof(f1454,plain,(
% 50.94/6.85 vtcheck(sK22_skl,sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ23_spl),
% 50.94/6.85 inference(component_clause,[status(thm)],[f1453])).
% 50.94/6.85 fof(f1456,plain,(
% 50.94/6.85 sQ20_spl|sQ23_spl),
% 50.94/6.85 inference(split_clause,[status(thm)],[f1452,f1440,f1453])).
% 50.94/6.85 fof(f2019,plain,(
% 50.94/6.85 sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vabs(sK43_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK45_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK44_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ20_spl),
% 50.94/6.85 inference(resolution,[status(thm)],[f308,f1441])).
% 50.94/6.85 fof(f2020,definition,(
% 50.94/6.85 sQ32_spl <=> (sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 50.94/6.85 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 50.94/6.85 fof(f2021,plain,(
% 50.94/6.85 sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~sQ32_spl),
% 50.94/6.85 inference(component_clause,[status(thm)],[f2020])).
% 50.94/6.85 fof(f2023,definition,(
% 50.94/6.85 sQ33_spl <=> (vapp(ve1app,ve2app)=vabs(sK43_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK45_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK44_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))))),
% 50.94/6.85 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 50.94/6.85 fof(f2024,plain,(
% 50.94/6.85 vapp(ve1app,ve2app)=vabs(sK43_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK45_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK44_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ33_spl),
% 50.94/6.85 inference(component_clause,[status(thm)],[f2023])).
% 50.94/6.85 fof(f2026,plain,(
% 50.94/6.85 sQ32_spl|sQ33_spl|~sQ20_spl),
% 50.94/6.85 inference(split_clause,[status(thm)],[f2019,f2020,f2023,f1440])).
% 50.94/6.85 fof(f2040,plain,(
% 50.94/6.85 vapp(ve1app,ve2app)=vvar(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ32_spl),
% 50.94/6.85 inference(resolution,[status(thm)],[f2021,f345])).
% 50.94/6.85 fof(f2041,plain,(
% 50.94/6.85 $false|~sQ32_spl),
% 50.94/6.85 inference(forward_subsumption_resolution,[status(thm)],[f2040,f77])).
% 50.94/6.85 fof(f2042,plain,(
% 50.94/6.85 ~sQ32_spl),
% 50.94/6.85 inference(contradiction_clause,[status(thm)],[f2041])).
% 50.94/6.85 fof(f2043,plain,(
% 50.94/6.85 $false|~sQ33_spl),
% 50.94/6.85 inference(forward_subsumption_resolution,[status(thm)],[f2024,f78])).
% 50.94/6.85 fof(f2044,plain,(
% 50.94/6.85 ~sQ33_spl),
% 50.94/6.85 inference(contradiction_clause,[status(thm)],[f2043])).
% 50.94/6.85 fof(f2045,plain,(
% 50.94/6.85 ve2app=sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~sQ21_spl),
% 50.94/6.85 inference(resolution,[status(thm)],[f1444,f74])).
% 50.94/6.85 fof(f2046,plain,(
% 50.94/6.85 ve1app=sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~sQ21_spl),
% 50.94/6.85 inference(resolution,[status(thm)],[f1444,f73])).
% 50.94/6.85 fof(f2197,plain,(
% 50.94/6.85 vtcheck(sK22_skl,ve2app,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ21_spl|~sQ23_spl),
% 50.94/6.88 inference(backward_demodulation,[status(thm)],[f2045,f1454])).
% 50.94/6.88 fof(f2226,plain,(
% 50.94/6.88 ![X0,X1]: (visFreeVar(X0,ve2app)|vtcheck(vbind(X0,X1,sK22_skl),ve2app,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|~sQ21_spl|~sQ23_spl)),
% 50.94/6.88 inference(resolution,[status(thm)],[f2197,f259])).
% 50.94/6.88 fof(f2301,plain,(
% 50.94/6.88 vtcheck(sK22_skl,ve1app,varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl))|~sQ21_spl|~sQ22_spl),
% 50.94/6.88 inference(backward_demodulation,[status(thm)],[f2046,f1449])).
% 50.94/6.88 fof(f2304,plain,(
% 50.94/6.88 ![X0,X1]: (visFreeVar(X0,ve1app)|vtcheck(vbind(X0,X1,sK22_skl),ve1app,varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl))|~sQ21_spl|~sQ22_spl)),
% 50.94/6.88 inference(resolution,[status(thm)],[f2301,f256])).
% 50.94/6.88 fof(f2682,plain,(
% 50.94/6.88 ![X0,X1,X2]: (visFreeVar(X0,ve1app)|~vtcheck(vbind(X0,X1,sK22_skl),X2,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|vtcheck(vbind(X0,X1,sK22_skl),vapp(ve1app,X2),sK23_skl)|~sQ21_spl|~sQ22_spl)),
% 50.94/6.88 inference(resolution,[status(thm)],[f2304,f239])).
% 50.94/6.89 fof(f3834,plain,(
% 50.94/6.89 ![X0,X1]: (visFreeVar(X0,ve1app)|vtcheck(vbind(X0,X1,sK22_skl),vapp(ve1app,ve2app),sK23_skl)|visFreeVar(X0,ve2app)|~sQ22_spl|~sQ21_spl|~sQ23_spl)),
% 50.94/6.89 inference(resolution,[status(thm)],[f2682,f2226])).
% 50.94/6.89 fof(f18622,plain,(
% 50.94/6.89 visFreeVar(sK21_skl,ve1app)|visFreeVar(sK21_skl,ve2app)|~sQ22_spl|~sQ21_spl|~sQ23_spl),
% 50.94/6.89 inference(resolution,[status(thm)],[f3834,f265])).
% 50.94/6.89 fof(f18630,definition,(
% 50.94/6.89 sQ850_spl <=> (visFreeVar(sK21_skl,ve1app))),
% 50.94/6.89 introduced(definition,[new_symbols(definition,[sQ850_spl])],[split_symbol_definition])).
% 50.94/6.89 fof(f18631,plain,(
% 50.94/6.89 visFreeVar(sK21_skl,ve1app)|~sQ850_spl),
% 50.94/6.89 inference(component_clause,[status(thm)],[f18630])).
% 50.94/6.89 fof(f18633,definition,(
% 50.94/6.89 sQ851_spl <=> (visFreeVar(sK21_skl,ve2app))),
% 50.94/6.89 introduced(definition,[new_symbols(definition,[sQ851_spl])],[split_symbol_definition])).
% 50.94/6.89 fof(f18634,plain,(
% 50.94/6.89 visFreeVar(sK21_skl,ve2app)|~sQ851_spl),
% 50.94/6.89 inference(component_clause,[status(thm)],[f18633])).
% 50.94/6.89 fof(f18636,plain,(
% 50.94/6.89 sQ850_spl|sQ851_spl|~sQ22_spl|~sQ21_spl|~sQ23_spl),
% 50.94/6.89 inference(split_clause,[status(thm)],[f18622,f18630,f18633,f1448,f1443,f1453])).
% 50.94/6.89 fof(f18649,plain,(
% 50.94/6.89 ![X0,X1]: (~X0=vapp(ve1app,X1)|visFreeVar(sK21_skl,X0)|~sQ850_spl)),
% 50.94/6.89 inference(resolution,[status(thm)],[f18631,f416])).
% 50.94/6.89 fof(f18660,plain,(
% 50.94/6.89 ![X0,X1]: (~X0=vapp(X1,ve2app)|visFreeVar(sK21_skl,X0)|~sQ851_spl)),
% 50.94/6.89 inference(resolution,[status(thm)],[f18634,f417])).
% 50.94/6.89 fof(f18690,plain,(
% 50.94/6.89 ![X0,X1]: (visFreeVar(sK21_skl,vsubst(X0,vapp(ve1app,X1),vvar(X0)))|~sQ850_spl)),
% 50.94/6.89 inference(resolution,[status(thm)],[f18649,f1245])).
% 50.94/6.89 fof(f18696,plain,(
% 50.94/6.89 ![X0]: (visFreeVar(sK21_skl,vapp(ve1app,X0))|~sQ850_spl)),
% 50.94/6.89 inference(forward_demodulation,[status(thm)],[f1245,f18690])).
% 50.94/6.89 fof(f18701,plain,(
% 50.94/6.89 $false|~sQ850_spl),
% 50.94/6.89 inference(backward_subsumption_resolution,[status(thm)],[f263,f18696])).
% 50.94/6.89 fof(f18712,plain,(
% 50.94/6.89 ~sQ850_spl),
% 50.94/6.89 inference(contradiction_clause,[status(thm)],[f18701])).
% 50.94/6.89 fof(f18773,plain,(
% 50.94/6.89 ![X0,X1]: (visFreeVar(sK21_skl,vsubst(X0,vapp(X1,ve2app),vvar(X0)))|~sQ851_spl)),
% 50.94/6.89 inference(resolution,[status(thm)],[f18660,f1245])).
% 50.94/6.89 fof(f18779,plain,(
% 50.94/6.89 ![X0]: (visFreeVar(sK21_skl,vapp(X0,ve2app))|~sQ851_spl)),
% 50.94/6.89 inference(forward_demodulation,[status(thm)],[f1245,f18773])).
% 50.94/6.89 fof(f18784,plain,(
% 50.94/6.89 $false|~sQ851_spl),
% 50.94/6.89 inference(backward_subsumption_resolution,[status(thm)],[f263,f18779])).
% 50.94/6.89 fof(f18795,plain,(
% 50.94/6.89 ~sQ851_spl),
% 50.94/6.89 inference(contradiction_clause,[status(thm)],[f18784])).
% 50.94/6.89 fof(f18796,plain,(
% 50.94/6.89 $false),
% 50.94/6.89 inference(sat_refutation,[status(thm)],[f1446,f1451,f1456,f2026,f2042,f2044,f18636,f18712,f18795])).
% 50.94/6.89 % SZS output end CNFRefutation for theBenchmark.p
% 50.94/6.90 % Elapsed time: 6.530185 seconds
% 50.94/6.90 % CPU time: 51.466920 seconds
% 50.94/6.90 % Total memory used: 430.265 MB
% 50.94/6.90 % Net memory used: 379.214 MB
%------------------------------------------------------------------------------