%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM143+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 : n019.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:52 PM UTC 2026
% Result : Theorem 3.69s 1.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : COM143+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n019.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 14:18:19 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 3.69/1.05 % Refutation found
% 3.69/1.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.69/1.05 % SZS output start CNFRefutation for theBenchmark
% 3.69/1.05 fof(f1,axiom,(
% 3.69/1.05 (! [VVar0,VVar1] :( ( vvar(VVar0) = vvar(VVar1)=> VVar0 = VVar1 )& ( VVar0 = VVar1=> vvar(VVar0) = vvar(VVar1) ) ) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f4,axiom,(
% 3.69/1.05 (! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f5,axiom,(
% 3.69/1.05 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f18,axiom,(
% 3.69/1.05 (! [VTyp0] : vnoType != vsomeType(VTyp0) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f24,axiom,(
% 3.69/1.05 (! [VTy,Vy,VVar0,VCtx0,RESULT,Vx,VC] :( ( VVar0 = Vx& VCtx0 = vbind(Vy,VTy,VC) )=> ( Vx != Vy=> ( RESULT = vlookup(VVar0,VCtx0)=> RESULT = vlookup(Vx,VC) ) ) ) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f39,axiom,(
% 3.69/1.05 (! [VOptExp0] :( VOptExp0 = vnoExp=> ~ visSomeExp(VOptExp0) ) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f51,axiom,(
% 3.69/1.05 (! [VC,Vx,VT] :( vlookup(Vx,VC) = vsomeType(VT)=> vtcheck(VC,vvar(Vx),VT) ) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f54,axiom,(
% 3.69/1.05 (! [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) ) )) ) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f55,conjecture,(
% 3.69/1.05 (! [Vx,VS,VC,Vy,VT] :( ( vlookup(Vx,VC) = vnoType& vtcheck(VC,vvar(Vy),VT) )=> vtcheck(vbind(Vx,VS,VC),vvar(Vy),VT) ) )),
% 3.69/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.69/1.05 fof(f56,negated_conjecture,(
% 3.69/1.05 ~((! [Vx,VS,VC,Vy,VT] :( ( vlookup(Vx,VC) = vnoType& vtcheck(VC,vvar(Vy),VT) )=> vtcheck(vbind(Vx,VS,VC),vvar(Vy),VT) ) ))),
% 3.69/1.05 inference(negated_conjecture,[status(cth)],[f55])).
% 3.69/1.05 fof(f57,plain,(
% 3.69/1.05 ![VVar0,VVar1]: ((~vvar(VVar0)=vvar(VVar1)|VVar0=VVar1)&(~VVar0=VVar1|vvar(VVar0)=vvar(VVar1)))),
% 3.69/1.05 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 3.69/1.05 fof(f58,plain,(
% 3.69/1.05 (![VVar0,VVar1]: (~vvar(VVar0)=vvar(VVar1)|VVar0=VVar1))&(![VVar0,VVar1]: (~VVar0=VVar1|vvar(VVar0)=vvar(VVar1)))),
% 3.69/1.05 inference(miniscoping,[status(thm)],[f57])).
% 3.69/1.05 fof(f59,plain,(
% 3.69/1.05 ![X0,X1]: (~vvar(X0)=vvar(X1)|X0=X1)),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f58])).
% 3.69/1.05 fof(f72,plain,(
% 3.69/1.05 ![X0,X1,X2,X3]: (~vvar(X0)=vabs(X1,X2,X3))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f4])).
% 3.69/1.05 fof(f73,plain,(
% 3.69/1.05 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f5])).
% 3.69/1.05 fof(f113,plain,(
% 3.69/1.05 ![X0]: (~vnoType=vsomeType(X0))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f18])).
% 3.69/1.05 fof(f128,plain,(
% 3.69/1.05 ![VTy,Vy,VVar0,VCtx0,RESULT,Vx,VC]: ((~VVar0=Vx|~VCtx0=vbind(Vy,VTy,VC))|(Vx=Vy|(~RESULT=vlookup(VVar0,VCtx0)|RESULT=vlookup(Vx,VC))))),
% 3.69/1.05 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 3.69/1.05 fof(f129,plain,(
% 3.69/1.05 ![Vy,VVar0,VCtx0,Vx,VC]: ((~VVar0=Vx|(![VTy]: ~VCtx0=vbind(Vy,VTy,VC)))|(Vx=Vy|(![RESULT]: (~RESULT=vlookup(VVar0,VCtx0)|RESULT=vlookup(Vx,VC)))))),
% 3.69/1.05 inference(miniscoping,[status(thm)],[f128])).
% 3.69/1.05 fof(f130,plain,(
% 3.69/1.05 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=vbind(X3,X4,X5)|X1=X3|~X6=vlookup(X0,X2)|X6=vlookup(X1,X5))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f129])).
% 3.69/1.05 fof(f183,plain,(
% 3.69/1.05 ![VOptExp0]: (~VOptExp0=vnoExp|~visSomeExp(VOptExp0))),
% 3.69/1.05 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 3.69/1.05 fof(f184,plain,(
% 3.69/1.05 ![X0]: (~X0=vnoExp|~visSomeExp(X0))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f183])).
% 3.69/1.05 fof(f229,plain,(
% 3.69/1.05 ![VC,Vx,VT]: (~vlookup(Vx,VC)=vsomeType(VT)|vtcheck(VC,vvar(Vx),VT))),
% 3.69/1.05 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 3.69/1.05 fof(f230,plain,(
% 3.69/1.05 ![X0,X1,X2]: (~vlookup(X0,X1)=vsomeType(X2)|vtcheck(X1,vvar(X0),X2))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f229])).
% 3.69/1.05 fof(f236,plain,(
% 3.69/1.05 ![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)))))),
% 3.69/1.05 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 3.69/1.05 fof(f237,definition,(
% 3.69/1.05 ![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)))))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 3.69/1.05 fof(f238,plain,(
% 3.69/1.05 ![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)))))),
% 3.69/1.05 inference(formula_renaming,[status(thm)],[f236,f237])).
% 3.69/1.05 fof(f239,plain,(
% 3.69/1.05 ![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)))))),
% 3.69/1.05 inference(miniscoping,[status(thm)],[f238])).
% 3.69/1.05 fof(f240,plain,(
% 3.69/1.05 ![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)))))),
% 3.69/1.05 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))],[f239])).
% 3.69/1.05 fof(f241,plain,(
% 3.69/1.05 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f240])).
% 3.69/1.05 fof(f244,plain,(
% 3.69/1.05 (?[Vx,VS,VC,Vy,VT]: ((vlookup(Vx,VC)=vnoType&vtcheck(VC,vvar(Vy),VT))&~vtcheck(vbind(Vx,VS,VC),vvar(Vy),VT)))),
% 3.69/1.05 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 3.69/1.05 fof(f245,plain,(
% 3.69/1.05 ?[Vx,VC,Vy,VT]: ((vlookup(Vx,VC)=vnoType&vtcheck(VC,vvar(Vy),VT))&(?[VS]: ~vtcheck(vbind(Vx,VS,VC),vvar(Vy),VT)))),
% 3.69/1.05 inference(miniscoping,[status(thm)],[f244])).
% 3.69/1.05 fof(f246,plain,(
% 3.69/1.05 ((vlookup(sK21_skl,sK22_skl)=vnoType&vtcheck(sK22_skl,vvar(sK23_skl),sK24_skl))&~vtcheck(vbind(sK21_skl,sK25_skl,sK22_skl),vvar(sK23_skl),sK24_skl))),
% 3.69/1.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl]),skolemize(Vx,sK21_skl),skolemize(VC,sK22_skl),skolemize(Vy,sK23_skl),skolemize(VT,sK24_skl),skolemize(VS,sK25_skl)],[f245])).
% 3.69/1.05 fof(f247,plain,(
% 3.69/1.05 vlookup(sK21_skl,sK22_skl)=vnoType),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f246])).
% 3.69/1.05 fof(f248,plain,(
% 3.69/1.05 vtcheck(sK22_skl,vvar(sK23_skl),sK24_skl)),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f246])).
% 3.69/1.05 fof(f249,plain,(
% 3.69/1.05 ~vtcheck(vbind(sK21_skl,sK25_skl,sK22_skl),vvar(sK23_skl),sK24_skl)),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f246])).
% 3.69/1.05 fof(f287,definition,(
% 3.69/1.05 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 3.69/1.05 fof(f288,plain,(
% 3.69/1.05 ![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)))))),
% 3.69/1.05 inference(formula_renaming,[status(thm)],[f237,f287])).
% 3.69/1.05 fof(f289,plain,(
% 3.69/1.05 ![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))))))),
% 3.69/1.05 inference(NNF_transformation,[status(thm)],[f288])).
% 3.69/1.05 fof(f290,plain,(
% 3.69/1.05 (![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))))))),
% 3.69/1.05 inference(miniscoping,[status(thm)],[f289])).
% 3.69/1.05 fof(f291,plain,(
% 3.69/1.05 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|(sP7_prd(sK43_skl(VC,VT,Ve),VC,VT,Ve)|((Ve=vabs(sK44_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve),sK45_skl(VC,VT,Ve))&VT=varrow(sK46_skl(VC,VT,Ve),sK47_skl(VC,VT,Ve)))&vtcheck(vbind(sK44_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve),VC),sK45_skl(VC,VT,Ve),sK47_skl(VC,VT,Ve))))))&(![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 3.69/1.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl,sK44_skl,sK45_skl,sK46_skl,sK47_skl]),skolemize(Vx,sK43_skl(VC,VT,Ve)),skolemize(Vx,sK44_skl(VC,VT,Ve)),skolemize(Ve2,sK45_skl(VC,VT,Ve)),skolemize(VT1,sK46_skl(VC,VT,Ve)),skolemize(VT2,sK47_skl(VC,VT,Ve))],[f290])).
% 3.69/1.05 fof(f292,plain,(
% 3.69/1.05 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|sP7_prd(sK43_skl(X0,X1,X2),X0,X1,X2)|X2=vabs(sK44_skl(X0,X1,X2),sK46_skl(X0,X1,X2),sK45_skl(X0,X1,X2)))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f291])).
% 3.69/1.05 fof(f327,plain,(
% 3.69/1.05 ![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))))),
% 3.69/1.05 inference(NNF_transformation,[status(thm)],[f287])).
% 3.69/1.05 fof(f328,plain,(
% 3.69/1.05 (![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))))),
% 3.69/1.05 inference(miniscoping,[status(thm)],[f327])).
% 3.69/1.05 fof(f329,plain,(
% 3.69/1.05 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|X3=vvar(X0))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f328])).
% 3.69/1.05 fof(f330,plain,(
% 3.69/1.05 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|vlookup(X0,X1)=vsomeType(X2))),
% 3.69/1.05 inference(cnf_transformation,[status(thm)],[f328])).
% 3.69/1.05 fof(f411,plain,(
% 3.69/1.05 ![X0,X1,X2,X3]: (X0=X1|vlookup(X0,vbind(X1,X2,X3))=vlookup(X0,X3))),
% 3.69/1.05 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 3.69/1.05 fof(f430,plain,(
% 3.69/1.05 ~visSomeExp(vnoExp)),
% 3.69/1.05 inference(destructive_equality_resolution,[status(thm)],[f184])).
% 3.69/1.05 fof(f471,plain,(
% 3.69/1.05 ~vlookup(sK23_skl,vbind(sK21_skl,sK25_skl,sK22_skl))=vsomeType(sK24_skl)),
% 3.69/1.05 inference(resolution,[status(thm)],[f230,f249])).
% 3.69/1.05 fof(f472,plain,(
% 3.69/1.05 ~vlookup(sK23_skl,sK22_skl)=vsomeType(sK24_skl)|sK23_skl=sK21_skl),
% 3.69/1.05 inference(paramodulation,[status(thm)],[f411,f471])).
% 3.69/1.05 fof(f473,definition,(
% 3.69/1.05 sQ0_spl <=> (vlookup(sK23_skl,sK22_skl)=vsomeType(sK24_skl))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f475,plain,(
% 3.69/1.05 ~vlookup(sK23_skl,sK22_skl)=vsomeType(sK24_skl)|sQ0_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f473])).
% 3.69/1.05 fof(f476,definition,(
% 3.69/1.05 sQ1_spl <=> (sK23_skl=sK21_skl)),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f477,plain,(
% 3.69/1.05 sK23_skl=sK21_skl|~sQ1_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f476])).
% 3.69/1.05 fof(f479,plain,(
% 3.69/1.05 ~sQ0_spl|sQ1_spl),
% 3.69/1.05 inference(split_clause,[status(thm)],[f472,f473,f476])).
% 3.69/1.05 fof(f834,plain,(
% 3.69/1.05 ![X0,X1,X2]: (X0=vvar(sK43_skl(X1,X2,X0))|~sP3_prd(X1,X2,X0)|X0=vabs(sK44_skl(X1,X2,X0),sK46_skl(X1,X2,X0),sK45_skl(X1,X2,X0)))),
% 3.69/1.05 inference(resolution,[status(thm)],[f329,f292])).
% 3.69/1.05 fof(f835,plain,(
% 3.69/1.05 ![X0,X1,X2]: (X0=vvar(sK43_skl(X1,X2,X0))|X0=vabs(sK44_skl(X1,X2,X0),sK46_skl(X1,X2,X0),sK45_skl(X1,X2,X0))|~vtcheck(X1,X0,X2)|X0=vapp(sK20_skl(X1,X2,X0),sK18_skl(X1,X2,X0)))),
% 3.69/1.05 inference(resolution,[status(thm)],[f834,f241])).
% 3.69/1.05 fof(f1039,plain,(
% 3.69/1.05 vvar(sK23_skl)=vvar(sK43_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|vvar(sK23_skl)=vabs(sK44_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK46_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK45_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|vvar(sK23_skl)=vapp(sK20_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK18_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))),
% 3.69/1.05 inference(resolution,[status(thm)],[f248,f835])).
% 3.69/1.05 fof(f1040,definition,(
% 3.69/1.05 sQ15_spl <=> (vvar(sK23_skl)=vvar(sK43_skl(sK22_skl,sK24_skl,vvar(sK23_skl))))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1041,plain,(
% 3.69/1.05 vvar(sK23_skl)=vvar(sK43_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|~sQ15_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1040])).
% 3.69/1.05 fof(f1043,definition,(
% 3.69/1.05 sQ16_spl <=> (vvar(sK23_skl)=vabs(sK44_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK46_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK45_skl(sK22_skl,sK24_skl,vvar(sK23_skl))))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1044,plain,(
% 3.69/1.05 vvar(sK23_skl)=vabs(sK44_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK46_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK45_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|~sQ16_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1043])).
% 3.69/1.05 fof(f1046,definition,(
% 3.69/1.05 sQ17_spl <=> (vvar(sK23_skl)=vapp(sK20_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK18_skl(sK22_skl,sK24_skl,vvar(sK23_skl))))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1047,plain,(
% 3.69/1.05 vvar(sK23_skl)=vapp(sK20_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK18_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|~sQ17_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1046])).
% 3.69/1.05 fof(f1049,plain,(
% 3.69/1.05 sQ15_spl|sQ16_spl|sQ17_spl),
% 3.69/1.05 inference(split_clause,[status(thm)],[f1039,f1040,f1043,f1046])).
% 3.69/1.05 fof(f1050,plain,(
% 3.69/1.05 $false|~sQ17_spl),
% 3.69/1.05 inference(forward_subsumption_resolution,[status(thm)],[f1047,f73])).
% 3.69/1.05 fof(f1051,plain,(
% 3.69/1.05 ~sQ17_spl),
% 3.69/1.05 inference(contradiction_clause,[status(thm)],[f1050])).
% 3.69/1.05 fof(f1064,definition,(
% 3.69/1.05 sQ18_spl <=> (visSomeExp(vnoExp))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1065,plain,(
% 3.69/1.05 visSomeExp(vnoExp)|~sQ18_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1064])).
% 3.69/1.05 fof(f1092,plain,(
% 3.69/1.05 sK23_skl=sK43_skl(sK22_skl,sK24_skl,vvar(sK23_skl))|~sQ15_spl),
% 3.69/1.05 inference(resolution,[status(thm)],[f1041,f59])).
% 3.69/1.05 fof(f1148,plain,(
% 3.69/1.05 ~sP3_prd(sK22_skl,sK24_skl,vvar(sK23_skl))|sP7_prd(sK23_skl,sK22_skl,sK24_skl,vvar(sK23_skl))|vvar(sK23_skl)=vabs(sK44_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK46_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK45_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|~sQ15_spl),
% 3.69/1.05 inference(paramodulation,[status(thm)],[f1092,f292])).
% 3.69/1.05 fof(f1149,definition,(
% 3.69/1.05 sQ23_spl <=> (sP3_prd(sK22_skl,sK24_skl,vvar(sK23_skl)))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1151,plain,(
% 3.69/1.05 ~sP3_prd(sK22_skl,sK24_skl,vvar(sK23_skl))|sQ23_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1149])).
% 3.69/1.05 fof(f1152,definition,(
% 3.69/1.05 sQ24_spl <=> (sP7_prd(sK23_skl,sK22_skl,sK24_skl,vvar(sK23_skl)))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1153,plain,(
% 3.69/1.05 sP7_prd(sK23_skl,sK22_skl,sK24_skl,vvar(sK23_skl))|~sQ24_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1152])).
% 3.69/1.05 fof(f1155,plain,(
% 3.69/1.05 ~sQ23_spl|sQ24_spl|sQ16_spl|~sQ15_spl),
% 3.69/1.05 inference(split_clause,[status(thm)],[f1148,f1149,f1152,f1043,f1040])).
% 3.69/1.05 fof(f1156,plain,(
% 3.69/1.05 $false|~sQ16_spl),
% 3.69/1.05 inference(forward_subsumption_resolution,[status(thm)],[f1044,f72])).
% 3.69/1.05 fof(f1157,plain,(
% 3.69/1.05 ~sQ16_spl),
% 3.69/1.05 inference(contradiction_clause,[status(thm)],[f1156])).
% 3.69/1.05 fof(f1163,plain,(
% 3.69/1.05 ~vtcheck(sK22_skl,vvar(sK23_skl),sK24_skl)|vvar(sK23_skl)=vapp(sK20_skl(sK22_skl,sK24_skl,vvar(sK23_skl)),sK18_skl(sK22_skl,sK24_skl,vvar(sK23_skl)))|sQ23_spl),
% 3.69/1.05 inference(resolution,[status(thm)],[f1151,f241])).
% 3.69/1.05 fof(f1164,definition,(
% 3.69/1.05 sQ25_spl <=> (vtcheck(sK22_skl,vvar(sK23_skl),sK24_skl))),
% 3.69/1.05 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 3.69/1.05 fof(f1166,plain,(
% 3.69/1.05 ~vtcheck(sK22_skl,vvar(sK23_skl),sK24_skl)|sQ25_spl),
% 3.69/1.05 inference(component_clause,[status(thm)],[f1164])).
% 3.69/1.05 fof(f1167,plain,(
% 3.69/1.05 ~sQ25_spl|sQ17_spl|sQ23_spl),
% 3.69/1.05 inference(split_clause,[status(thm)],[f1163,f1164,f1046,f1149])).
% 3.69/1.05 fof(f1168,plain,(
% 3.69/1.05 $false|sQ25_spl),
% 3.69/1.05 inference(forward_subsumption_resolution,[status(thm)],[f1166,f248])).
% 3.69/1.05 fof(f1169,plain,(
% 3.69/1.05 sQ25_spl),
% 3.69/1.05 inference(contradiction_clause,[status(thm)],[f1168])).
% 3.69/1.05 fof(f1276,plain,(
% 3.69/1.05 $false|~sQ18_spl),
% 3.69/1.05 inference(forward_subsumption_resolution,[status(thm)],[f1065,f430])).
% 3.69/1.05 fof(f1277,plain,(
% 3.69/1.05 ~sQ18_spl),
% 3.69/1.05 inference(contradiction_clause,[status(thm)],[f1276])).
% 3.69/1.05 fof(f1526,plain,(
% 3.69/1.05 vlookup(sK23_skl,sK22_skl)=vsomeType(sK24_skl)|~sQ24_spl),
% 3.69/1.05 inference(resolution,[status(thm)],[f330,f1153])).
% 3.69/1.05 fof(f1528,plain,(
% 3.69/1.05 $false|sQ0_spl|~sQ24_spl),
% 3.69/1.05 inference(forward_subsumption_resolution,[status(thm)],[f1526,f475])).
% 3.55/1.07 fof(f1529,plain,(
% 3.55/1.07 sQ0_spl|~sQ24_spl),
% 3.55/1.07 inference(contradiction_clause,[status(thm)],[f1528])).
% 3.55/1.07 fof(f1531,plain,(
% 3.55/1.07 sP7_prd(sK23_skl,sK22_skl,sK24_skl,vvar(sK21_skl))|~sQ1_spl|~sQ24_spl),
% 3.55/1.07 inference(backward_demodulation,[status(thm)],[f477,f1153])).
% 3.55/1.07 fof(f1537,plain,(
% 3.55/1.07 sP7_prd(sK21_skl,sK22_skl,sK24_skl,vvar(sK21_skl))|~sQ1_spl|~sQ24_spl),
% 3.55/1.07 inference(forward_demodulation,[status(thm)],[f477,f1531])).
% 3.55/1.07 fof(f1551,plain,(
% 3.55/1.07 vlookup(sK21_skl,sK22_skl)=vsomeType(sK24_skl)|~sQ1_spl|~sQ24_spl),
% 3.55/1.07 inference(resolution,[status(thm)],[f1537,f330])).
% 3.55/1.07 fof(f1554,plain,(
% 3.55/1.07 vnoType=vsomeType(sK24_skl)|~sQ1_spl|~sQ24_spl),
% 3.55/1.07 inference(forward_demodulation,[status(thm)],[f247,f1551])).
% 3.55/1.07 fof(f1555,plain,(
% 3.55/1.07 $false|~sQ1_spl|~sQ24_spl),
% 3.55/1.07 inference(forward_subsumption_resolution,[status(thm)],[f1554,f113])).
% 3.55/1.07 fof(f1556,plain,(
% 3.55/1.07 ~sQ1_spl|~sQ24_spl),
% 3.55/1.07 inference(contradiction_clause,[status(thm)],[f1555])).
% 3.55/1.07 fof(f1557,plain,(
% 3.55/1.07 $false),
% 3.55/1.07 inference(sat_refutation,[status(thm)],[f479,f1049,f1051,f1155,f1157,f1167,f1169,f1277,f1529,f1556])).
% 3.55/1.07 % SZS output end CNFRefutation for theBenchmark.p
% 3.55/1.07 % Elapsed time: 0.619354 seconds
% 3.55/1.07 % CPU time: 4.434032 seconds
% 3.55/1.07 % Total memory used: 149.365 MB
% 3.55/1.07 % Net memory used: 145.703 MB
%------------------------------------------------------------------------------