%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM149+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 : n017.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 0.18s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COM149+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n017.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 14:13:58 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.51 % Drodi V4.1.1
% 0.18/0.57 % Refutation found
% 0.18/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.57 fof(f4,axiom,(
% 0.18/0.57 (! [VVar0,VVar1,VTyp0,VExp0] : vvar(VVar0) != vabs(VVar1,VTyp0,VExp0) )),
% 0.18/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.57 fof(f5,axiom,(
% 0.18/0.57 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 0.18/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.57 fof(f18,axiom,(
% 0.18/0.57 (! [VTyp0] : vnoType != vsomeType(VTyp0) )),
% 0.18/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.57 fof(f22,axiom,(
% 0.18/0.57 (! [Vx,VVar0,VCtx0,RESULT] :( ( VVar0 = Vx& VCtx0 = vempty )=> ( RESULT = vlookup(VVar0,VCtx0)=> RESULT = vnoType ) ) )),
% 0.18/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.57 fof(f54,axiom,(
% 0.18/0.57 (! [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) ) )) ) )),
% 0.18/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.57 fof(f57,conjecture,(
% 0.18/0.57 (! [VT,Vx] :( ( vtcheck(vempty,vvar(Vx),VT)& ~ visValue(vvar(Vx)) )=> (? [Veout] : vreduce(vvar(Vx)) = vsomeExp(Veout) )) )),
% 0.18/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.57 fof(f58,negated_conjecture,(
% 0.18/0.57 ~((! [VT,Vx] :( ( vtcheck(vempty,vvar(Vx),VT)& ~ visValue(vvar(Vx)) )=> (? [Veout] : vreduce(vvar(Vx)) = vsomeExp(Veout) )) ))),
% 0.18/0.57 inference(negated_conjecture,[status(cth)],[f57])).
% 0.18/0.57 fof(f74,plain,(
% 0.18/0.57 ![X0,X1,X2,X3]: (~vvar(X0)=vabs(X1,X2,X3))),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.18/0.57 fof(f75,plain,(
% 0.18/0.57 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.18/0.57 fof(f115,plain,(
% 0.18/0.57 ![X0]: (~vnoType=vsomeType(X0))),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f18])).
% 0.18/0.57 fof(f124,plain,(
% 0.18/0.57 ![Vx,VVar0,VCtx0,RESULT]: ((~VVar0=Vx|~VCtx0=vempty)|(~RESULT=vlookup(VVar0,VCtx0)|RESULT=vnoType))),
% 0.18/0.57 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.18/0.57 fof(f125,plain,(
% 0.18/0.57 ![VVar0,VCtx0]: (((![Vx]: ~VVar0=Vx)|~VCtx0=vempty)|(![RESULT]: (~RESULT=vlookup(VVar0,VCtx0)|RESULT=vnoType)))),
% 0.18/0.57 inference(miniscoping,[status(thm)],[f124])).
% 0.18/0.57 fof(f126,plain,(
% 0.18/0.57 ![X0,X1,X2,X3]: (~X0=X1|~X2=vempty|~X3=vlookup(X0,X2)|X3=vnoType)),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f125])).
% 0.18/0.57 fof(f238,plain,(
% 0.18/0.57 ![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)))))),
% 0.18/0.57 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.18/0.57 fof(f239,definition,(
% 0.18/0.57 ![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)))))),
% 0.18/0.57 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.18/0.57 fof(f240,plain,(
% 0.18/0.57 ![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)))))),
% 0.18/0.57 inference(formula_renaming,[status(thm)],[f238,f239])).
% 0.18/0.57 fof(f241,plain,(
% 0.18/0.57 ![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)))))),
% 0.18/0.57 inference(miniscoping,[status(thm)],[f240])).
% 0.18/0.57 fof(f242,plain,(
% 0.18/0.57 ![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)))))),
% 0.18/0.57 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))],[f241])).
% 0.18/0.57 fof(f243,plain,(
% 0.18/0.57 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f242])).
% 0.18/0.57 fof(f252,plain,(
% 0.18/0.57 (?[VT,Vx]: ((vtcheck(vempty,vvar(Vx),VT)&~visValue(vvar(Vx)))&(![Veout]: ~vreduce(vvar(Vx))=vsomeExp(Veout))))),
% 0.18/0.57 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.18/0.57 fof(f253,plain,(
% 0.18/0.57 ?[Vx]: (((?[VT]: vtcheck(vempty,vvar(Vx),VT))&~visValue(vvar(Vx)))&(![Veout]: ~vreduce(vvar(Vx))=vsomeExp(Veout)))),
% 0.18/0.57 inference(miniscoping,[status(thm)],[f252])).
% 0.18/0.57 fof(f254,plain,(
% 0.18/0.57 ((vtcheck(vempty,vvar(sK21_skl),sK22_skl)&~visValue(vvar(sK21_skl)))&(![Veout]: ~vreduce(vvar(sK21_skl))=vsomeExp(Veout)))),
% 0.18/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(Vx,sK21_skl),skolemize(VT,sK22_skl)],[f253])).
% 0.18/0.57 fof(f255,plain,(
% 0.18/0.57 vtcheck(vempty,vvar(sK21_skl),sK22_skl)),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f254])).
% 0.18/0.57 fof(f295,definition,(
% 0.18/0.57 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 0.18/0.57 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.18/0.57 fof(f296,plain,(
% 0.18/0.57 ![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)))))),
% 0.18/0.57 inference(formula_renaming,[status(thm)],[f239,f295])).
% 0.18/0.57 fof(f297,plain,(
% 0.18/0.57 ![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))))))),
% 0.18/0.57 inference(NNF_transformation,[status(thm)],[f296])).
% 0.18/0.57 fof(f298,plain,(
% 0.18/0.57 (![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))))))),
% 0.18/0.57 inference(miniscoping,[status(thm)],[f297])).
% 0.18/0.57 fof(f299,plain,(
% 0.18/0.57 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|(sP7_prd(sK40_skl(VC,VT,Ve),VC,VT,Ve)|((Ve=vabs(sK41_skl(VC,VT,Ve),sK43_skl(VC,VT,Ve),sK42_skl(VC,VT,Ve))&VT=varrow(sK43_skl(VC,VT,Ve),sK44_skl(VC,VT,Ve)))&vtcheck(vbind(sK41_skl(VC,VT,Ve),sK43_skl(VC,VT,Ve),VC),sK42_skl(VC,VT,Ve),sK44_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))))))),
% 0.18/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl,sK41_skl,sK42_skl,sK43_skl,sK44_skl]),skolemize(Vx,sK40_skl(VC,VT,Ve)),skolemize(Vx,sK41_skl(VC,VT,Ve)),skolemize(Ve2,sK42_skl(VC,VT,Ve)),skolemize(VT1,sK43_skl(VC,VT,Ve)),skolemize(VT2,sK44_skl(VC,VT,Ve))],[f298])).
% 0.18/0.57 fof(f300,plain,(
% 0.18/0.57 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|sP7_prd(sK40_skl(X0,X1,X2),X0,X1,X2)|X2=vabs(sK41_skl(X0,X1,X2),sK43_skl(X0,X1,X2),sK42_skl(X0,X1,X2)))),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f299])).
% 0.18/0.57 fof(f335,plain,(
% 0.18/0.57 ![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))))),
% 0.18/0.57 inference(NNF_transformation,[status(thm)],[f295])).
% 0.18/0.57 fof(f336,plain,(
% 0.18/0.57 (![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))))),
% 0.18/0.57 inference(miniscoping,[status(thm)],[f335])).
% 0.18/0.57 fof(f338,plain,(
% 0.18/0.57 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|vlookup(X0,X1)=vsomeType(X2))),
% 0.18/0.57 inference(cnf_transformation,[status(thm)],[f336])).
% 0.18/0.57 fof(f417,plain,(
% 0.18/0.57 ![X0]: (vlookup(X0,vempty)=vnoType)),
% 0.18/0.57 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 0.18/0.57 fof(f480,plain,(
% 0.18/0.57 ![X0,X1,X2]: (vlookup(sK40_skl(X0,X1,X2),X0)=vsomeType(X1)|~sP3_prd(X0,X1,X2)|X2=vabs(sK41_skl(X0,X1,X2),sK43_skl(X0,X1,X2),sK42_skl(X0,X1,X2)))),
% 0.18/0.57 inference(resolution,[status(thm)],[f338,f300])).
% 0.18/0.57 fof(f487,plain,(
% 0.18/0.57 ![X0,X1,X2]: (vlookup(sK40_skl(X0,X1,X2),X0)=vsomeType(X1)|X2=vabs(sK41_skl(X0,X1,X2),sK43_skl(X0,X1,X2),sK42_skl(X0,X1,X2))|~vtcheck(X0,X2,X1)|X2=vapp(sK20_skl(X0,X1,X2),sK18_skl(X0,X1,X2)))),
% 0.18/0.57 inference(resolution,[status(thm)],[f480,f243])).
% 0.18/0.57 fof(f488,plain,(
% 0.18/0.57 vlookup(sK40_skl(vempty,sK22_skl,vvar(sK21_skl)),vempty)=vsomeType(sK22_skl)|vvar(sK21_skl)=vabs(sK41_skl(vempty,sK22_skl,vvar(sK21_skl)),sK43_skl(vempty,sK22_skl,vvar(sK21_skl)),sK42_skl(vempty,sK22_skl,vvar(sK21_skl)))|vvar(sK21_skl)=vapp(sK20_skl(vempty,sK22_skl,vvar(sK21_skl)),sK18_skl(vempty,sK22_skl,vvar(sK21_skl)))),
% 0.18/0.57 inference(resolution,[status(thm)],[f487,f255])).
% 0.18/0.57 fof(f489,definition,(
% 0.18/0.57 sQ0_spl <=> (vlookup(sK40_skl(vempty,sK22_skl,vvar(sK21_skl)),vempty)=vsomeType(sK22_skl))),
% 0.18/0.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.18/0.57 fof(f490,plain,(
% 0.18/0.57 vlookup(sK40_skl(vempty,sK22_skl,vvar(sK21_skl)),vempty)=vsomeType(sK22_skl)|~sQ0_spl),
% 0.18/0.57 inference(component_clause,[status(thm)],[f489])).
% 0.18/0.57 fof(f492,definition,(
% 0.18/0.57 sQ1_spl <=> (vvar(sK21_skl)=vabs(sK41_skl(vempty,sK22_skl,vvar(sK21_skl)),sK43_skl(vempty,sK22_skl,vvar(sK21_skl)),sK42_skl(vempty,sK22_skl,vvar(sK21_skl))))),
% 0.18/0.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.18/0.57 fof(f493,plain,(
% 0.18/0.57 vvar(sK21_skl)=vabs(sK41_skl(vempty,sK22_skl,vvar(sK21_skl)),sK43_skl(vempty,sK22_skl,vvar(sK21_skl)),sK42_skl(vempty,sK22_skl,vvar(sK21_skl)))|~sQ1_spl),
% 0.18/0.57 inference(component_clause,[status(thm)],[f492])).
% 0.18/0.57 fof(f495,definition,(
% 0.18/0.57 sQ2_spl <=> (vvar(sK21_skl)=vapp(sK20_skl(vempty,sK22_skl,vvar(sK21_skl)),sK18_skl(vempty,sK22_skl,vvar(sK21_skl))))),
% 0.18/0.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.18/0.57 fof(f496,plain,(
% 0.18/0.57 vvar(sK21_skl)=vapp(sK20_skl(vempty,sK22_skl,vvar(sK21_skl)),sK18_skl(vempty,sK22_skl,vvar(sK21_skl)))|~sQ2_spl),
% 0.18/0.57 inference(component_clause,[status(thm)],[f495])).
% 0.18/0.57 fof(f498,plain,(
% 0.18/0.57 sQ0_spl|sQ1_spl|sQ2_spl),
% 0.18/0.57 inference(split_clause,[status(thm)],[f488,f489,f492,f495])).
% 0.18/0.57 fof(f499,plain,(
% 0.18/0.57 $false|~sQ2_spl),
% 0.18/0.57 inference(forward_subsumption_resolution,[status(thm)],[f496,f75])).
% 0.18/0.57 fof(f500,plain,(
% 0.18/0.57 ~sQ2_spl),
% 0.18/0.57 inference(contradiction_clause,[status(thm)],[f499])).
% 0.18/0.57 fof(f501,plain,(
% 0.18/0.57 vnoType=vsomeType(sK22_skl)|~sQ0_spl),
% 0.18/0.57 inference(forward_demodulation,[status(thm)],[f417,f490])).
% 0.18/0.57 fof(f502,plain,(
% 0.18/0.57 $false|~sQ0_spl),
% 0.18/0.57 inference(forward_subsumption_resolution,[status(thm)],[f501,f115])).
% 0.18/0.57 fof(f503,plain,(
% 0.18/0.57 ~sQ0_spl),
% 0.18/0.57 inference(contradiction_clause,[status(thm)],[f502])).
% 0.18/0.57 fof(f504,plain,(
% 0.18/0.57 $false|~sQ1_spl),
% 0.18/0.57 inference(forward_subsumption_resolution,[status(thm)],[f493,f74])).
% 0.18/0.57 fof(f505,plain,(
% 0.18/0.57 ~sQ1_spl),
% 0.18/0.57 inference(contradiction_clause,[status(thm)],[f504])).
% 0.18/0.57 fof(f506,plain,(
% 0.18/0.57 $false),
% 0.18/0.57 inference(sat_refutation,[status(thm)],[f498,f500,f503,f505])).
% 0.18/0.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.60 % Elapsed time: 0.119199 seconds
% 0.22/0.60 % CPU time: 0.339307 seconds
% 0.22/0.60 % Total memory used: 68.915 MB
% 0.22/0.60 % Net memory used: 68.728 MB
%------------------------------------------------------------------------------