%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM135+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 : 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 17.07s 2.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM135+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.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 14:18:10 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 17.07/2.67 % Refutation found
% 17.07/2.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.07/2.67 % SZS output start CNFRefutation for theBenchmark
% 17.07/2.67 fof(f1,axiom,(
% 17.07/2.67 (! [VVar0,VVar1] :( ( vvar(VVar0) = vvar(VVar1)=> VVar0 = VVar1 )& ( VVar0 = VVar1=> vvar(VVar0) = vvar(VVar1) ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f4,axiom,(
% 17.07/2.67 (! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f5,axiom,(
% 17.07/2.67 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f10,axiom,(
% 17.07/2.67 (! [VVar0,VExp0,Vx,Vv] :( ( VVar0 = Vv& VExp0 = vvar(Vx) )=> ( ( Vx = Vv=> visFreeVar(VVar0,VExp0) )& ( visFreeVar(VVar0,VExp0)=> Vx = Vv ) ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f16,axiom,(
% 17.07/2.67 (! [VTyp0,VTyp1] :( ( vsomeType(VTyp0) = vsomeType(VTyp1)=> VTyp0 = VTyp1 )& ( VTyp0 = VTyp1=> vsomeType(VTyp0) = vsomeType(VTyp1) ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f21,axiom,(
% 17.07/2.67 (! [VOptTyp0,RESULT,Ve] :( VOptTyp0 = vsomeType(Ve)=> ( RESULT = vgetSomeType(VOptTyp0)=> RESULT = Ve ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f23,axiom,(
% 17.07/2.67 (! [VC,Vx,Vy,VVar0,VCtx0,RESULT,VTy] :( ( VVar0 = Vx& VCtx0 = vbind(Vy,VTy,VC) )=> ( Vx = Vy=> ( RESULT = vlookup(VVar0,VCtx0)=> RESULT = vsomeType(VTy) ) ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f29,axiom,(
% 17.07/2.67 (! [Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vvar(Vy) )=> ( Vx = Vy=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = Ve ) ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f30,axiom,(
% 17.07/2.67 (! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vvar(Vy) )=> ( Vx != Vy=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = vvar(Vy) ) ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f41,axiom,(
% 17.07/2.67 (! [VOptExp0,RESULT,Ve] :( VOptExp0 = vsomeExp(Ve)=> ( RESULT = vgetSomeExp(VOptExp0)=> RESULT = Ve ) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f54,axiom,(
% 17.07/2.67 (! [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) ) )) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f56,axiom,(
% 17.07/2.67 (! [Vx,VS,VC,Ve,VT] :( ( ~ visFreeVar(Vx,Ve)& vtcheck(vbind(Vx,VS,VC),Ve,VT) )=> vtcheck(VC,Ve,VT) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f58,conjecture,(
% 17.07/2.67 (! [VT,VC,Vx,Ve,Vy,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2) ) )),
% 17.07/2.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.07/2.67 fof(f59,negated_conjecture,(
% 17.07/2.67 ~((! [VT,VC,Vx,Ve,Vy,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2) ) ))),
% 17.07/2.67 inference(negated_conjecture,[status(cth)],[f58])).
% 17.07/2.67 fof(f60,plain,(
% 17.07/2.67 ![VVar0,VVar1]: ((~vvar(VVar0)=vvar(VVar1)|VVar0=VVar1)&(~VVar0=VVar1|vvar(VVar0)=vvar(VVar1)))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 17.07/2.67 fof(f61,plain,(
% 17.07/2.67 (![VVar0,VVar1]: (~vvar(VVar0)=vvar(VVar1)|VVar0=VVar1))&(![VVar0,VVar1]: (~VVar0=VVar1|vvar(VVar0)=vvar(VVar1)))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f60])).
% 17.07/2.67 fof(f62,plain,(
% 17.07/2.67 ![X0,X1]: (~vvar(X0)=vvar(X1)|X0=X1)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f61])).
% 17.07/2.67 fof(f75,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (~vvar(X0)=vabs(X1,X2,X3))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f4])).
% 17.07/2.67 fof(f76,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f5])).
% 17.07/2.67 fof(f87,plain,(
% 17.07/2.67 ![VVar0,VExp0,Vx,Vv]: ((~VVar0=Vv|~VExp0=vvar(Vx))|((~Vx=Vv|visFreeVar(VVar0,VExp0))&(~visFreeVar(VVar0,VExp0)|Vx=Vv)))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 17.07/2.67 fof(f89,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (~X0=X1|~X2=vvar(X3)|~visFreeVar(X0,X2)|X3=X1)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f87])).
% 17.07/2.67 fof(f111,plain,(
% 17.07/2.67 ![VTyp0,VTyp1]: ((~vsomeType(VTyp0)=vsomeType(VTyp1)|VTyp0=VTyp1)&(~VTyp0=VTyp1|vsomeType(VTyp0)=vsomeType(VTyp1)))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 17.07/2.67 fof(f112,plain,(
% 17.07/2.67 (![VTyp0,VTyp1]: (~vsomeType(VTyp0)=vsomeType(VTyp1)|VTyp0=VTyp1))&(![VTyp0,VTyp1]: (~VTyp0=VTyp1|vsomeType(VTyp0)=vsomeType(VTyp1)))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f111])).
% 17.07/2.67 fof(f113,plain,(
% 17.07/2.67 ![X0,X1]: (~vsomeType(X0)=vsomeType(X1)|X0=X1)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f112])).
% 17.07/2.67 fof(f122,plain,(
% 17.07/2.67 ![VOptTyp0,RESULT,Ve]: (~VOptTyp0=vsomeType(Ve)|(~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 17.07/2.67 fof(f123,plain,(
% 17.07/2.67 ![VOptTyp0,Ve]: (~VOptTyp0=vsomeType(Ve)|(![RESULT]: (~RESULT=vgetSomeType(VOptTyp0)|RESULT=Ve)))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f122])).
% 17.07/2.67 fof(f124,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~X0=vsomeType(X1)|~X2=vgetSomeType(X0)|X2=X1)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f123])).
% 17.07/2.67 fof(f128,plain,(
% 17.07/2.67 ![VC,Vx,Vy,VVar0,VCtx0,RESULT,VTy]: ((~VVar0=Vx|~VCtx0=vbind(Vy,VTy,VC))|(~Vx=Vy|(~RESULT=vlookup(VVar0,VCtx0)|RESULT=vsomeType(VTy))))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 17.07/2.67 fof(f129,plain,(
% 17.07/2.67 ![Vx,Vy,VVar0,VCtx0,VTy]: ((~VVar0=Vx|(![VC]: ~VCtx0=vbind(Vy,VTy,VC)))|(~Vx=Vy|(![RESULT]: (~RESULT=vlookup(VVar0,VCtx0)|RESULT=vsomeType(VTy)))))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f128])).
% 17.07/2.67 fof(f130,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=vbind(X3,X4,X5)|~X1=X3|~X6=vlookup(X0,X2)|X6=vsomeType(X4))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f129])).
% 17.07/2.67 fof(f150,plain,(
% 17.07/2.67 ![Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve)))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 17.07/2.67 fof(f151,plain,(
% 17.07/2.67 ![Vx,Vy,VVar0,VExp0,VExp1,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve))))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f150])).
% 17.07/2.67 fof(f152,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=X3|~X4=vvar(X5)|~X1=X5|~X6=vsubst(X0,X2,X4)|X6=X3)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f151])).
% 17.07/2.67 fof(f153,plain,(
% 17.07/2.67 ![Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(Vx=Vy|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vvar(Vy))))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 17.07/2.67 fof(f154,plain,(
% 17.07/2.67 ![Vx,VVar0,VExp0,VExp1,Vy]: (((~VVar0=Vx|(![Ve]: ~VExp0=Ve))|~VExp1=vvar(Vy))|(Vx=Vy|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vvar(Vy)))))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f153])).
% 17.07/2.67 fof(f155,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=X3|~X4=vvar(X5)|X1=X5|~X6=vsubst(X0,X2,X4)|X6=vvar(X5))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f154])).
% 17.07/2.67 fof(f191,plain,(
% 17.07/2.67 ![VOptExp0,RESULT,Ve]: (~VOptExp0=vsomeExp(Ve)|(~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 17.07/2.67 fof(f192,plain,(
% 17.07/2.67 ![VOptExp0,Ve]: (~VOptExp0=vsomeExp(Ve)|(![RESULT]: (~RESULT=vgetSomeExp(VOptExp0)|RESULT=Ve)))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f191])).
% 17.07/2.67 fof(f193,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~X0=vsomeExp(X1)|~X2=vgetSomeExp(X0)|X2=X1)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f192])).
% 17.07/2.67 fof(f239,plain,(
% 17.07/2.67 ![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)))))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 17.07/2.67 fof(f240,definition,(
% 17.07/2.67 ![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)))))),
% 17.07/2.67 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 17.07/2.67 fof(f241,plain,(
% 17.07/2.67 ![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)))))),
% 17.07/2.67 inference(formula_renaming,[status(thm)],[f239,f240])).
% 17.07/2.67 fof(f242,plain,(
% 17.07/2.67 ![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)))))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f241])).
% 17.07/2.67 fof(f243,plain,(
% 17.07/2.67 ![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)))))),
% 17.07/2.67 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])).
% 17.07/2.67 fof(f244,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f243])).
% 17.07/2.67 fof(f250,plain,(
% 17.07/2.67 ![Vx,VS,VC,Ve,VT]: ((visFreeVar(Vx,Ve)|~vtcheck(vbind(Vx,VS,VC),Ve,VT))|vtcheck(VC,Ve,VT))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 17.07/2.67 fof(f251,plain,(
% 17.07/2.67 ![VC,Ve,VT]: ((![Vx]: (visFreeVar(Vx,Ve)|(![VS]: ~vtcheck(vbind(Vx,VS,VC),Ve,VT))))|vtcheck(VC,Ve,VT))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f250])).
% 17.07/2.67 fof(f252,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4]: (visFreeVar(X0,X1)|~vtcheck(vbind(X0,X2,X3),X1,X4)|vtcheck(X3,X1,X4))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f251])).
% 17.07/2.67 fof(f256,plain,(
% 17.07/2.67 (?[VT,VC,Vx,Ve,Vy,VT2]: ((vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2))&~vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2)))),
% 17.07/2.67 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 17.07/2.67 fof(f257,plain,(
% 17.07/2.67 ?[VC,Vx,Ve,Vy,VT2]: ((?[VT]: (vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vvar(Vy),VT2)))&~vtcheck(VC,vsubst(Vx,Ve,vvar(Vy)),VT2))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f256])).
% 17.07/2.67 fof(f258,plain,(
% 17.07/2.67 ((vtcheck(sK21_skl,sK23_skl,sK26_skl)&vtcheck(vbind(sK22_skl,sK26_skl,sK21_skl),vvar(sK24_skl),sK25_skl))&~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vvar(sK24_skl)),sK25_skl))),
% 17.07/2.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(VC,sK21_skl),skolemize(Vx,sK22_skl),skolemize(Ve,sK23_skl),skolemize(Vy,sK24_skl),skolemize(VT2,sK25_skl),skolemize(VT,sK26_skl)],[f257])).
% 17.07/2.67 fof(f259,plain,(
% 17.07/2.67 vtcheck(sK21_skl,sK23_skl,sK26_skl)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f258])).
% 17.07/2.67 fof(f260,plain,(
% 17.07/2.67 vtcheck(vbind(sK22_skl,sK26_skl,sK21_skl),vvar(sK24_skl),sK25_skl)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f258])).
% 17.07/2.67 fof(f261,plain,(
% 17.07/2.67 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vvar(sK24_skl)),sK25_skl)),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f258])).
% 17.07/2.67 fof(f299,definition,(
% 17.07/2.67 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 17.07/2.67 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 17.07/2.67 fof(f300,plain,(
% 17.07/2.67 ![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)))))),
% 17.07/2.67 inference(formula_renaming,[status(thm)],[f240,f299])).
% 17.07/2.67 fof(f301,plain,(
% 17.07/2.67 ![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))))))),
% 17.07/2.67 inference(NNF_transformation,[status(thm)],[f300])).
% 17.07/2.67 fof(f302,plain,(
% 17.07/2.67 (![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))))))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f301])).
% 17.07/2.67 fof(f303,plain,(
% 17.07/2.67 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|(sP7_prd(sK44_skl(VC,VT,Ve),VC,VT,Ve)|((Ve=vabs(sK45_skl(VC,VT,Ve),sK47_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve))&VT=varrow(sK47_skl(VC,VT,Ve),sK48_skl(VC,VT,Ve)))&vtcheck(vbind(sK45_skl(VC,VT,Ve),sK47_skl(VC,VT,Ve),VC),sK46_skl(VC,VT,Ve),sK48_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))))))),
% 17.07/2.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl,sK45_skl,sK46_skl,sK47_skl,sK48_skl]),skolemize(Vx,sK44_skl(VC,VT,Ve)),skolemize(Vx,sK45_skl(VC,VT,Ve)),skolemize(Ve2,sK46_skl(VC,VT,Ve)),skolemize(VT1,sK47_skl(VC,VT,Ve)),skolemize(VT2,sK48_skl(VC,VT,Ve))],[f302])).
% 17.07/2.67 fof(f304,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|sP7_prd(sK44_skl(X0,X1,X2),X0,X1,X2)|X2=vabs(sK45_skl(X0,X1,X2),sK47_skl(X0,X1,X2),sK46_skl(X0,X1,X2)))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f303])).
% 17.07/2.67 fof(f339,plain,(
% 17.07/2.67 ![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))))),
% 17.07/2.67 inference(NNF_transformation,[status(thm)],[f299])).
% 17.07/2.67 fof(f340,plain,(
% 17.07/2.67 (![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))))),
% 17.07/2.67 inference(miniscoping,[status(thm)],[f339])).
% 17.07/2.67 fof(f341,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|X3=vvar(X0))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f340])).
% 17.07/2.67 fof(f342,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|vlookup(X0,X1)=vsomeType(X2))),
% 17.07/2.67 inference(cnf_transformation,[status(thm)],[f340])).
% 17.07/2.67 fof(f408,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~X0=vvar(X1)|~visFreeVar(X2,X0)|X1=X2)),
% 17.07/2.67 inference(destructive_equality_resolution,[status(thm)],[f89])).
% 17.07/2.67 fof(f416,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4]: (~X0=vbind(X1,X2,X3)|~X4=vlookup(X1,X0)|X4=vsomeType(X2))),
% 17.07/2.67 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 17.07/2.67 fof(f419,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (~X0=vvar(X1)|~X2=vsubst(X1,X3,X0)|X2=X3)),
% 17.07/2.67 inference(destructive_equality_resolution,[status(thm)],[f152])).
% 17.07/2.67 fof(f420,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4]: (~X0=vvar(X1)|X2=X1|~X3=vsubst(X2,X4,X0)|X3=vvar(X1))),
% 17.07/2.67 inference(destructive_equality_resolution,[status(thm)],[f155])).
% 17.07/2.67 fof(f442,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~X0=vvar(X1)|vsubst(X1,X2,X0)=X2)),
% 17.07/2.67 inference(equality_resolution,[status(thm)],[f419])).
% 17.07/2.67 fof(f443,plain,(
% 17.07/2.67 ![X0,X1]: (vsubst(X0,X1,vvar(X0))=X1)),
% 17.07/2.67 inference(equality_resolution,[status(thm)],[f442])).
% 17.07/2.67 fof(f453,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (X0=X1|~X2=vsubst(X0,X3,vvar(X1))|X2=vvar(X1))),
% 17.07/2.67 inference(equality_resolution,[status(thm)],[f420])).
% 17.07/2.67 fof(f471,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (X0=X1|vsubst(X2,vsubst(X0,X3,vvar(X1)),vvar(X2))=vvar(X1))),
% 17.07/2.67 inference(resolution,[status(thm)],[f453,f443])).
% 17.07/2.67 fof(f475,plain,(
% 17.07/2.67 ![X0,X1,X2]: (X0=X1|vsubst(X0,X2,vvar(X1))=vvar(X1))),
% 17.07/2.67 inference(forward_demodulation,[status(thm)],[f443,f471])).
% 17.07/2.67 fof(f503,plain,(
% 17.07/2.67 ~vtcheck(sK21_skl,vvar(sK24_skl),sK25_skl)|sK22_skl=sK24_skl),
% 17.07/2.67 inference(paramodulation,[status(thm)],[f475,f261])).
% 17.07/2.67 fof(f525,plain,(
% 17.07/2.67 ![X0,X1,X2]: (~X0=vgetSomeType(vsubst(X1,vsomeType(X2),vvar(X1)))|X0=X2)),
% 17.07/2.67 inference(resolution,[status(thm)],[f124,f443])).
% 17.07/2.67 fof(f529,plain,(
% 17.07/2.67 ![X0,X1]: (~X0=vgetSomeType(vsomeType(X1))|X0=X1)),
% 17.07/2.67 inference(forward_demodulation,[status(thm)],[f443,f525])).
% 17.07/2.67 fof(f550,plain,(
% 17.07/2.67 ![X0,X1]: (vsubst(X0,vgetSomeType(vsomeType(X1)),vvar(X0))=X1)),
% 17.07/2.67 inference(resolution,[status(thm)],[f529,f443])).
% 17.07/2.67 fof(f552,plain,(
% 17.07/2.67 ![X0]: (vgetSomeType(vsomeType(X0))=X0)),
% 17.07/2.67 inference(forward_demodulation,[status(thm)],[f443,f550])).
% 17.07/2.67 fof(f617,plain,(
% 17.07/2.67 ![X0,X1,X2,X3,X4]: (~X0=vlookup(X1,vsubst(X2,vbind(X1,X3,X4),vvar(X2)))|X0=vsomeType(X3))),
% 17.07/2.67 inference(resolution,[status(thm)],[f416,f443])).
% 17.07/2.67 fof(f623,plain,(
% 17.07/2.67 ![X0,X1,X2,X3]: (~X0=vlookup(X1,vbind(X1,X2,X3))|X0=vsomeType(X2))),
% 17.07/2.67 inference(forward_demodulation,[status(thm)],[f443,f617])).
% 17.07/2.67 fof(f818,plain,(
% 17.07/2.67 ![X0,X1]: (~X0=vgetSomeExp(vgetSomeType(vsomeType(vsomeExp(X1))))|X0=X1)),
% 17.07/2.67 inference(resolution,[status(thm)],[f193,f552])).
% 17.07/2.67 fof(f824,plain,(
% 17.07/2.67 ![X0,X1]: (~X0=vgetSomeExp(vsomeExp(X1))|X0=X1)),
% 17.07/2.67 inference(forward_demodulation,[status(thm)],[f552,f818])).
% 17.07/2.69 fof(f976,plain,(
% 17.07/2.69 ![X0]: (vgetSomeType(vsomeType(vgetSomeExp(vsomeExp(X0))))=X0)),
% 17.07/2.69 inference(resolution,[status(thm)],[f824,f552])).
% 17.07/2.69 fof(f979,plain,(
% 17.07/2.69 ![X0]: (vgetSomeExp(vsomeExp(X0))=X0)),
% 17.07/2.69 inference(forward_demodulation,[status(thm)],[f552,f976])).
% 17.07/2.69 fof(f1241,plain,(
% 17.07/2.69 ![X0,X1,X2]: (vgetSomeExp(vsomeExp(vlookup(X0,vbind(X0,X1,X2))))=vsomeType(X1))),
% 17.07/2.69 inference(resolution,[status(thm)],[f623,f979])).
% 17.07/2.69 fof(f1245,plain,(
% 17.07/2.69 ![X0,X1,X2]: (vlookup(X0,vbind(X0,X1,X2))=vsomeType(X1))),
% 17.07/2.69 inference(forward_demodulation,[status(thm)],[f979,f1241])).
% 17.07/2.69 fof(f1275,plain,(
% 17.07/2.69 sP3_prd(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK24_skl))|vvar(sK24_skl)=vapp(sK20_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK24_skl)),sK18_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK24_skl)))),
% 17.07/2.69 inference(resolution,[status(thm)],[f244,f260])).
% 17.07/2.69 fof(f1277,plain,(
% 17.07/2.69 sP3_prd(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK24_skl))),
% 17.07/2.69 inference(forward_subsumption_resolution,[status(thm)],[f1275,f76])).
% 17.07/2.69 fof(f1302,plain,(
% 17.07/2.69 visFreeVar(sK22_skl,vvar(sK24_skl))|vtcheck(sK21_skl,vvar(sK24_skl),sK25_skl)),
% 17.07/2.69 inference(resolution,[status(thm)],[f252,f260])).
% 17.07/2.69 fof(f1356,plain,(
% 17.07/2.69 visFreeVar(sK22_skl,vvar(sK24_skl))|sK22_skl=sK24_skl),
% 17.07/2.69 inference(resolution,[status(thm)],[f1302,f503])).
% 17.07/2.69 fof(f1404,plain,(
% 17.07/2.69 ![X0]: (sK22_skl=sK24_skl|~vvar(sK24_skl)=vvar(X0)|X0=sK22_skl)),
% 17.07/2.69 inference(resolution,[status(thm)],[f1356,f408])).
% 17.07/2.69 fof(f1487,plain,(
% 17.07/2.69 sK22_skl=sK24_skl|sK24_skl=sK22_skl),
% 17.07/2.69 inference(equality_resolution,[status(thm)],[f1404])).
% 17.07/2.69 fof(f1488,plain,(
% 17.07/2.69 sK22_skl=sK24_skl),
% 17.07/2.69 inference(duplicate_literals_removal,[status(thm)],[f1487])).
% 17.07/2.69 fof(f1513,plain,(
% 17.07/2.69 sP3_prd(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl))),
% 17.07/2.69 inference(backward_demodulation,[status(thm)],[f1488,f1277])).
% 17.07/2.69 fof(f1515,plain,(
% 17.07/2.69 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vvar(sK22_skl)),sK25_skl)),
% 17.07/2.69 inference(backward_demodulation,[status(thm)],[f1488,f261])).
% 17.07/2.69 fof(f1520,plain,(
% 17.07/2.69 ~vtcheck(sK21_skl,sK23_skl,sK25_skl)),
% 17.07/2.69 inference(forward_demodulation,[status(thm)],[f443,f1515])).
% 17.07/2.69 fof(f1570,plain,(
% 17.07/2.69 sP7_prd(sK44_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl)),vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl))|vvar(sK22_skl)=vabs(sK45_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl)),sK47_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl)),sK46_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl)))),
% 17.07/2.69 inference(resolution,[status(thm)],[f1513,f304])).
% 17.07/2.69 fof(f1571,plain,(
% 17.07/2.69 sP7_prd(sK44_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl)),vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl))),
% 17.07/2.69 inference(forward_subsumption_resolution,[status(thm)],[f1570,f75])).
% 17.07/2.69 fof(f2243,plain,(
% 17.07/2.69 vvar(sK22_skl)=vvar(sK44_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl)))),
% 17.07/2.69 inference(resolution,[status(thm)],[f1571,f341])).
% 17.07/2.69 fof(f6082,plain,(
% 17.07/2.69 sK22_skl=sK44_skl(vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl))),
% 17.07/2.69 inference(resolution,[status(thm)],[f2243,f62])).
% 17.07/2.69 fof(f6338,plain,(
% 17.07/2.69 sP7_prd(sK22_skl,vbind(sK22_skl,sK26_skl,sK21_skl),sK25_skl,vvar(sK22_skl))),
% 17.07/2.69 inference(backward_demodulation,[status(thm)],[f6082,f1571])).
% 17.07/2.69 fof(f6339,plain,(
% 17.07/2.69 vlookup(sK22_skl,vbind(sK22_skl,sK26_skl,sK21_skl))=vsomeType(sK25_skl)),
% 17.07/2.69 inference(resolution,[status(thm)],[f6338,f342])).
% 17.07/2.69 fof(f6342,plain,(
% 17.07/2.69 vsomeType(sK26_skl)=vsomeType(sK25_skl)),
% 17.07/2.69 inference(forward_demodulation,[status(thm)],[f1245,f6339])).
% 17.07/2.69 fof(f6353,plain,(
% 17.07/2.69 sK26_skl=sK25_skl),
% 17.07/2.69 inference(resolution,[status(thm)],[f6342,f113])).
% 17.07/2.69 fof(f6501,plain,(
% 17.07/2.69 vtcheck(sK21_skl,sK23_skl,sK25_skl)),
% 17.07/2.69 inference(backward_demodulation,[status(thm)],[f6353,f259])).
% 17.07/2.69 fof(f6830,plain,(
% 17.07/2.69 $false),
% 17.07/2.69 inference(forward_subsumption_resolution,[status(thm)],[f6501,f1520])).
% 17.07/2.69 % SZS output end CNFRefutation for theBenchmark.p
% 17.68/2.73 % Elapsed time: 2.336623 seconds
% 17.68/2.73 % CPU time: 17.670828 seconds
% 17.68/2.73 % Total memory used: 232.557 MB
% 17.68/2.73 % Net memory used: 222.164 MB
%------------------------------------------------------------------------------