%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM140+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 : 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 125.99s 16.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM140+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.07/0.34 % Computer : n019.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 14:18:04 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.37 % Drodi V4.1.1
% 125.99/16.37 % Refutation found
% 125.99/16.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 125.99/16.37 % SZS output start CNFRefutation for theBenchmark
% 125.99/16.37 fof(f10,axiom,(
% 125.99/16.37 (! [VVar0,VExp0,Vx,Vv] :( ( VVar0 = Vv& VExp0 = vvar(Vx) )=> ( ( Vx = Vv=> visFreeVar(VVar0,VExp0) )& ( visFreeVar(VVar0,VExp0)=> Vx = Vv ) ) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f12,axiom,(
% 125.99/16.37 (! [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) ) ) ) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f28,axiom,(
% 125.99/16.37 (! [Vv,Ve] :( vgensym(Ve) = Vv=> ~ visFreeVar(Vv,Ve) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f29,axiom,(
% 125.99/16.37 (! [Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vvar(Vy) )=> ( Vx = Vy=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = Ve ) ) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f31,axiom,(
% 125.99/16.37 (! [VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vapp(Ve1,Ve2) )=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2)) ) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f56,axiom,(
% 125.99/16.37 (! [Ve2,Ve1] :( valphaEquivalent(Ve1,Ve2)=> valphaEquivalent(Ve2,Ve1) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f58,axiom,(
% 125.99/16.37 (! [VS,Vx,Vy,Ve] :( ~ visFreeVar(Vy,Ve)=> valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve))) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f59,axiom,(
% 125.99/16.37 (! [Ve,VC,Ve1,VT] :( ( vtcheck(VC,Ve,VT)& valphaEquivalent(Ve,Ve1) )=> vtcheck(VC,Ve1,VT) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f61,axiom,(
% 125.99/16.37 (! [Vx,VS,VC,Vy,VS1,Ve1,VT] :( ( Vx != Vy& vlookup(Vx,VC) = vnoType& vtcheck(VC,vabs(Vy,VS1,Ve1),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,Ve1),VT) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f62,conjecture,(
% 125.99/16.37 (! [Vx,VS,VC,Vy,VS1,VT] :( ( Vx = Vy& vlookup(Vx,VC) = vnoType& vtcheck(VC,vabs(Vy,VS1,veabs),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ) )),
% 125.99/16.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 125.99/16.37 fof(f63,negated_conjecture,(
% 125.99/16.37 ~((! [Vx,VS,VC,Vy,VS1,VT] :( ( Vx = Vy& vlookup(Vx,VC) = vnoType& vtcheck(VC,vabs(Vy,VS1,veabs),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ) ))),
% 125.99/16.37 inference(negated_conjecture,[status(cth)],[f62])).
% 125.99/16.37 fof(f91,plain,(
% 125.99/16.37 ![VVar0,VExp0,Vx,Vv]: ((~VVar0=Vv|~VExp0=vvar(Vx))|((~Vx=Vv|visFreeVar(VVar0,VExp0))&(~visFreeVar(VVar0,VExp0)|Vx=Vv)))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 125.99/16.37 fof(f92,plain,(
% 125.99/16.37 ![X0,X1,X2,X3]: (~X0=X1|~X2=vvar(X3)|~X3=X1|visFreeVar(X0,X2))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f91])).
% 125.99/16.37 fof(f99,plain,(
% 125.99/16.37 ![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)))))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 125.99/16.37 fof(f100,plain,(
% 125.99/16.37 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X3)|visFreeVar(X0,X2))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f99])).
% 125.99/16.37 fof(f101,plain,(
% 125.99/16.37 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X4)|visFreeVar(X0,X2))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f99])).
% 125.99/16.37 fof(f152,plain,(
% 125.99/16.37 ![Vv,Ve]: (~vgensym(Ve)=Vv|~visFreeVar(Vv,Ve))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 125.99/16.37 fof(f153,plain,(
% 125.99/16.37 ![X0,X1]: (~vgensym(X0)=X1|~visFreeVar(X1,X0))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f152])).
% 125.99/16.37 fof(f154,plain,(
% 125.99/16.37 ![Vx,Vy,VVar0,VExp0,VExp1,RESULT,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve)))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 125.99/16.37 fof(f155,plain,(
% 125.99/16.37 ![Vx,Vy,VVar0,VExp0,VExp1,Ve]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vvar(Vy))|(~Vx=Vy|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=Ve))))),
% 125.99/16.37 inference(miniscoping,[status(thm)],[f154])).
% 125.99/16.37 fof(f156,plain,(
% 125.99/16.37 ![X0,X1,X2,X3,X4,X5,X6]: (~X0=X1|~X2=X3|~X4=vvar(X5)|~X1=X5|~X6=vsubst(X0,X2,X4)|X6=X3)),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f155])).
% 125.99/16.37 fof(f160,plain,(
% 125.99/16.37 ![VVar0,VExp0,VExp1,RESULT,Ve1,Vx,Ve,Ve2]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vapp(Ve1,Ve2))|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2))))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 125.99/16.37 fof(f161,plain,(
% 125.99/16.37 ![VVar0,VExp0,VExp1,Ve1,Vx,Ve,Ve2]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vapp(Ve1,Ve2))|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vapp(vsubst(Vx,Ve,Ve1),vsubst(Vx,Ve,Ve2)))))),
% 125.99/16.37 inference(miniscoping,[status(thm)],[f160])).
% 125.99/16.37 fof(f162,plain,(
% 125.99/16.37 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~X0=X1|~X2=X3|~X4=vapp(X5,X6)|~X7=vsubst(X0,X2,X4)|X7=vapp(vsubst(X1,X3,X5),vsubst(X1,X3,X6)))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f161])).
% 125.99/16.37 fof(f252,plain,(
% 125.99/16.37 ![Ve2,Ve1]: (~valphaEquivalent(Ve1,Ve2)|valphaEquivalent(Ve2,Ve1))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 125.99/16.37 fof(f253,plain,(
% 125.99/16.37 ![X0,X1]: (~valphaEquivalent(X0,X1)|valphaEquivalent(X1,X0))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f252])).
% 125.99/16.37 fof(f257,plain,(
% 125.99/16.37 ![VS,Vx,Vy,Ve]: (visFreeVar(Vy,Ve)|valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve))))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 125.99/16.37 fof(f258,plain,(
% 125.99/16.37 ![Vy,Ve]: (visFreeVar(Vy,Ve)|(![VS,Vx]: valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve)))))),
% 125.99/16.37 inference(miniscoping,[status(thm)],[f257])).
% 125.99/16.37 fof(f259,plain,(
% 125.99/16.37 ![X0,X1,X2,X3]: (visFreeVar(X0,X1)|valphaEquivalent(vabs(X2,X3,X1),vabs(X0,X3,vsubst(X2,vvar(X0),X1))))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f258])).
% 125.99/16.37 fof(f260,plain,(
% 125.99/16.37 ![Ve,VC,Ve1,VT]: ((~vtcheck(VC,Ve,VT)|~valphaEquivalent(Ve,Ve1))|vtcheck(VC,Ve1,VT))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 125.99/16.37 fof(f261,plain,(
% 125.99/16.37 ![VC,Ve1,VT]: ((![Ve]: (~vtcheck(VC,Ve,VT)|~valphaEquivalent(Ve,Ve1)))|vtcheck(VC,Ve1,VT))),
% 125.99/16.37 inference(miniscoping,[status(thm)],[f260])).
% 125.99/16.37 fof(f262,plain,(
% 125.99/16.37 ![X0,X1,X2,X3]: (~vtcheck(X0,X1,X2)|~valphaEquivalent(X1,X3)|vtcheck(X0,X3,X2))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f261])).
% 125.99/16.37 fof(f266,plain,(
% 125.99/16.37 ![Vx,VS,VC,Vy,VS1,Ve1,VT]: (((Vx=Vy|~vlookup(Vx,VC)=vnoType)|~vtcheck(VC,vabs(Vy,VS1,Ve1),VT))|vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,Ve1),VT))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 125.99/16.37 fof(f267,plain,(
% 125.99/16.37 ![Vx,VC,Vy,VS1,Ve1,VT]: (((Vx=Vy|~vlookup(Vx,VC)=vnoType)|~vtcheck(VC,vabs(Vy,VS1,Ve1),VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,Ve1),VT)))),
% 125.99/16.37 inference(miniscoping,[status(thm)],[f266])).
% 125.99/16.37 fof(f268,plain,(
% 125.99/16.37 ![X0,X1,X2,X3,X4,X5,X6]: (X0=X1|~vlookup(X0,X2)=vnoType|~vtcheck(X2,vabs(X1,X3,X4),X5)|vtcheck(vbind(X0,X6,X2),vabs(X1,X3,X4),X5))),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f267])).
% 125.99/16.37 fof(f269,plain,(
% 125.99/16.37 (?[Vx,VS,VC,Vy,VS1,VT]: (((Vx=Vy&vlookup(Vx,VC)=vnoType)&vtcheck(VC,vabs(Vy,VS1,veabs),VT))&~vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)))),
% 125.99/16.37 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 125.99/16.37 fof(f270,plain,(
% 125.99/16.37 ?[Vx,VC,Vy,VS1,VT]: (((Vx=Vy&vlookup(Vx,VC)=vnoType)&vtcheck(VC,vabs(Vy,VS1,veabs),VT))&(?[VS]: ~vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)))),
% 125.99/16.37 inference(miniscoping,[status(thm)],[f269])).
% 125.99/16.37 fof(f271,plain,(
% 125.99/16.37 (((sK21_skl=sK23_skl&vlookup(sK21_skl,sK22_skl)=vnoType)&vtcheck(sK22_skl,vabs(sK23_skl,sK24_skl,veabs),sK25_skl))&~vtcheck(vbind(sK21_skl,sK26_skl,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl))),
% 125.99/16.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(Vx,sK21_skl),skolemize(VC,sK22_skl),skolemize(Vy,sK23_skl),skolemize(VS1,sK24_skl),skolemize(VT,sK25_skl),skolemize(VS,sK26_skl)],[f270])).
% 125.99/16.37 fof(f272,plain,(
% 125.99/16.37 sK21_skl=sK23_skl),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f271])).
% 125.99/16.37 fof(f273,plain,(
% 125.99/16.37 vlookup(sK21_skl,sK22_skl)=vnoType),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f271])).
% 125.99/16.37 fof(f274,plain,(
% 125.99/16.37 vtcheck(sK22_skl,vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f271])).
% 125.99/16.37 fof(f275,plain,(
% 125.99/16.37 ~vtcheck(vbind(sK21_skl,sK26_skl,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 125.99/16.37 inference(cnf_transformation,[status(thm)],[f271])).
% 125.99/16.37 fof(f424,plain,(
% 125.99/16.37 ![X0]: (visFreeVar(X0,vvar(X0)))),
% 125.99/16.37 inference(destructive_equality_resolution,[status(thm)],[f92])).
% 125.99/16.37 fof(f429,plain,(
% 125.99/16.37 ![X0,X1,X2]: (~visFreeVar(X0,X1)|visFreeVar(X0,vapp(X1,X2)))),
% 125.99/16.37 inference(destructive_equality_resolution,[status(thm)],[f100])).
% 125.99/16.37 fof(f430,plain,(
% 125.99/16.37 ![X0,X1,X2]: (~visFreeVar(X0,X1)|visFreeVar(X0,vapp(X2,X1)))),
% 125.99/16.37 inference(destructive_equality_resolution,[status(thm)],[f101])).
% 125.99/16.37 fof(f443,plain,(
% 125.99/16.37 ![X0]: (~visFreeVar(vgensym(X0),X0))),
% 125.99/16.37 inference(destructive_equality_resolution,[status(thm)],[f153])).
% 125.99/16.37 fof(f444,plain,(
% 125.99/16.37 ![X0,X1]: (vsubst(X0,X1,vvar(X0))=X1)),
% 125.99/16.37 inference(destructive_equality_resolution,[status(thm)],[f156])).
% 125.99/16.37 fof(f446,plain,(
% 125.99/16.37 ![X0,X1,X2,X3]: (vsubst(X0,X1,vapp(X2,X3))=vapp(vsubst(X0,X1,X2),vsubst(X0,X1,X3)))),
% 125.99/16.37 inference(destructive_equality_resolution,[status(thm)],[f162])).
% 125.99/16.37 fof(f487,plain,(
% 125.99/16.37 vlookup(sK23_skl,sK22_skl)=vnoType),
% 125.99/16.37 inference(forward_demodulation,[status(thm)],[f272,f273])).
% 125.99/16.37 fof(f488,plain,(
% 125.99/16.37 ~vtcheck(vbind(sK23_skl,sK26_skl,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 125.99/16.37 inference(forward_demodulation,[status(thm)],[f272,f275])).
% 125.99/16.37 fof(f513,plain,(
% 125.99/16.37 ![X0,X1]: (visFreeVar(X0,vapp(vvar(X0),X1)))),
% 125.99/16.37 inference(resolution,[status(thm)],[f429,f424])).
% 125.99/16.37 fof(f520,plain,(
% 125.99/16.37 ![X0,X1,X2]: (visFreeVar(X0,vapp(vapp(vvar(X0),X1),X2)))),
% 125.99/16.37 inference(resolution,[status(thm)],[f513,f429])).
% 125.99/16.37 fof(f645,plain,(
% 125.99/16.37 ![X0,X1,X2]: (vsubst(X0,X1,vapp(vvar(X0),X2))=vapp(X1,vsubst(X0,X1,X2)))),
% 125.99/16.37 inference(paramodulation,[status(thm)],[f444,f446])).
% 125.99/16.37 fof(f758,plain,(
% 125.99/16.37 ![X0]: (~valphaEquivalent(vabs(sK23_skl,sK24_skl,veabs),X0)|vtcheck(sK22_skl,X0,sK25_skl))),
% 125.99/16.37 inference(resolution,[status(thm)],[f262,f274])).
% 125.99/16.37 fof(f1494,plain,(
% 125.99/16.37 ![X0]: (visFreeVar(X0,veabs)|vtcheck(sK22_skl,vabs(X0,sK24_skl,vsubst(sK23_skl,vvar(X0),veabs)),sK25_skl))),
% 125.99/16.37 inference(resolution,[status(thm)],[f259,f758])).
% 125.99/16.37 fof(f1509,plain,(
% 125.99/16.37 ![X0,X1,X2,X3]: (visFreeVar(X0,X1)|valphaEquivalent(vabs(X0,X2,vsubst(X3,vvar(X0),X1)),vabs(X3,X2,X1)))),
% 125.99/16.37 inference(resolution,[status(thm)],[f259,f253])).
% 125.99/16.37 fof(f1513,plain,(
% 125.99/16.37 ![X0,X1,X2]: (visFreeVar(X0,veabs)|X1=X0|~vlookup(X1,sK22_skl)=vnoType|vtcheck(vbind(X1,X2,sK22_skl),vabs(X0,sK24_skl,vsubst(sK23_skl,vvar(X0),veabs)),sK25_skl))),
% 125.99/16.37 inference(resolution,[status(thm)],[f1494,f268])).
% 125.99/16.37 fof(f1530,plain,(
% 125.99/16.37 ![X0,X1]: (visFreeVar(X0,veabs)|sK23_skl=X0|vtcheck(vbind(sK23_skl,X1,sK22_skl),vabs(X0,sK24_skl,vsubst(sK23_skl,vvar(X0),veabs)),sK25_skl))),
% 125.99/16.37 inference(resolution,[status(thm)],[f1513,f487])).
% 125.99/16.37 fof(f1684,plain,(
% 125.99/16.37 ![X0,X1,X2,X3]: (visFreeVar(X0,vapp(vsubst(X1,vvar(X0),vapp(vvar(X1),X2)),X3)))),
% 125.99/16.37 inference(paramodulation,[status(thm)],[f645,f520])).
% 125.99/16.37 fof(f3147,plain,(
% 125.99/16.37 ![X0,X1,X2]: (visFreeVar(X0,veabs)|sK23_skl=X0|~valphaEquivalent(vabs(X0,sK24_skl,vsubst(sK23_skl,vvar(X0),veabs)),X1)|vtcheck(vbind(sK23_skl,X2,sK22_skl),X1,sK25_skl))),
% 125.99/16.37 inference(resolution,[status(thm)],[f1530,f262])).
% 125.99/16.37 fof(f15161,plain,(
% 125.99/16.37 ![X0,X1]: (visFreeVar(X0,veabs)|sK23_skl=X0|vtcheck(vbind(sK23_skl,X1,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl)|visFreeVar(X0,veabs))),
% 125.99/16.37 inference(resolution,[status(thm)],[f3147,f1509])).
% 125.99/16.37 fof(f15170,plain,(
% 125.99/16.37 ![X0,X1]: (visFreeVar(X0,veabs)|sK23_skl=X0|vtcheck(vbind(sK23_skl,X1,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl))),
% 125.99/16.37 inference(duplicate_literals_removal,[status(thm)],[f15161])).
% 125.99/16.37 fof(f15179,plain,(
% 125.99/16.37 ![X0]: (visFreeVar(X0,veabs)|sK23_skl=X0)),
% 125.99/16.37 inference(resolution,[status(thm)],[f15170,f488])).
% 125.99/16.37 fof(f15198,plain,(
% 125.99/16.37 ![X0,X1]: (sK23_skl=X0|visFreeVar(X0,vapp(X1,veabs)))),
% 125.99/16.37 inference(resolution,[status(thm)],[f15179,f430])).
% 125.99/16.37 fof(f15250,plain,(
% 125.99/16.37 ![X0]: (sK23_skl=vgensym(vapp(X0,veabs)))),
% 125.99/16.37 inference(resolution,[status(thm)],[f15198,f443])).
% 125.99/16.37 fof(f15278,plain,(
% 125.99/16.37 ![X0]: (~visFreeVar(sK23_skl,vapp(X0,veabs)))),
% 125.99/16.37 inference(paramodulation,[status(thm)],[f15250,f443])).
% 125.99/16.37 fof(f15304,plain,(
% 125.99/16.37 $false),
% 125.99/16.37 inference(resolution,[status(thm)],[f15278,f1684])).
% 125.99/16.41 % SZS output end CNFRefutation for theBenchmark.p
% 19.88/16.51 % Elapsed time: 16.144716 seconds
% 19.88/16.51 % CPU time: 126.985698 seconds
% 19.88/16.51 % Total memory used: 479.150 MB
% 19.88/16.51 % Net memory used: 435.860 MB
%------------------------------------------------------------------------------