%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM133+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 : n010.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 0.14s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM133+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 14:18:25 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f32,axiom,(
% 0.14/0.41 (! [Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1] :( ( VVar0 = Vx& VExp0 = Ve& VExp1 = vabs(Vy,VT,Ve1) )=> ( Vx = Vy=> ( RESULT = vsubst(VVar0,VExp0,VExp1)=> RESULT = vabs(Vy,VT,Ve1) ) ) ) )),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f59,axiom,(
% 0.14/0.41 (! [VT,VC,Vx,Ve,Vy,VS,Ve1,VT2] :( ( Vx = Vy& vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2) ) )),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f60,axiom,(
% 0.14/0.41 (! [VT,VC,Vx,Ve,Vy,VS,VT2] :( ( Vx != Vy& ~ visFreeVar(Vy,Ve)& vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2) ) )),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f61,axiom,(
% 0.14/0.41 (! [VT,VC,Vx,Ve,Vy,VS,VT2] :( ( Vx != Vy& visFreeVar(Vy,Ve)& vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2) ) )),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f62,conjecture,(
% 0.14/0.41 (! [VT,VC,Vx,Ve,Vy,VS,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2) ) )),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f63,negated_conjecture,(
% 0.14/0.41 ~((! [VT,VC,Vx,Ve,Vy,VS,VT2] :( ( vtcheck(VC,Ve,VT)& vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2) )=> vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2) ) ))),
% 0.14/0.41 inference(negated_conjecture,[status(cth)],[f62])).
% 0.14/0.41 fof(f163,plain,(
% 0.14/0.41 ![Ve,Vx,VVar0,VExp0,VExp1,RESULT,Vy,VT,Ve1]: (((~VVar0=Vx|~VExp0=Ve)|~VExp1=vabs(Vy,VT,Ve1))|(~Vx=Vy|(~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vabs(Vy,VT,Ve1))))),
% 0.14/0.41 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.14/0.41 fof(f164,plain,(
% 0.14/0.41 ![Vx,VVar0,VExp0,VExp1,Vy,VT,Ve1]: (((~VVar0=Vx|(![Ve]: ~VExp0=Ve))|~VExp1=vabs(Vy,VT,Ve1))|(~Vx=Vy|(![RESULT]: (~RESULT=vsubst(VVar0,VExp0,VExp1)|RESULT=vabs(Vy,VT,Ve1)))))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f163])).
% 0.14/0.41 fof(f165,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~X0=X1|~X2=X3|~X4=vabs(X5,X6,X7)|~X1=X5|~X8=vsubst(X0,X2,X4)|X8=vabs(X5,X6,X7))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f164])).
% 0.14/0.41 fof(f263,plain,(
% 0.14/0.41 ![VT,VC,Vx,Ve,Vy,VS,Ve1,VT2]: (((~Vx=Vy|~vtcheck(VC,Ve,VT))|~vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2))|vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2))),
% 0.14/0.41 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.14/0.41 fof(f264,plain,(
% 0.14/0.41 ![VC,Vx,Ve,Vy,VS,Ve1,VT2]: ((![VT]: ((~Vx=Vy|~vtcheck(VC,Ve,VT))|~vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,Ve1),VT2)))|vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,Ve1)),VT2))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f263])).
% 0.14/0.41 fof(f265,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~X0=X1|~vtcheck(X2,X3,X4)|~vtcheck(vbind(X0,X4,X2),vabs(X1,X5,X6),X7)|vtcheck(X2,vsubst(X0,X3,vabs(X1,X5,X6)),X7))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f264])).
% 0.14/0.41 fof(f266,plain,(
% 0.14/0.41 ![VT,VC,Vx,Ve,Vy,VS,VT2]: ((((Vx=Vy|visFreeVar(Vy,Ve))|~vtcheck(VC,Ve,VT))|~vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))|vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2))),
% 0.14/0.41 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.14/0.41 fof(f267,plain,(
% 0.14/0.41 ![VC,Vx,Ve,Vy,VS,VT2]: ((![VT]: (((Vx=Vy|visFreeVar(Vy,Ve))|~vtcheck(VC,Ve,VT))|~vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2)))|vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f266])).
% 0.14/0.41 fof(f268,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (X0=X1|visFreeVar(X1,X2)|~vtcheck(X3,X2,X4)|~vtcheck(vbind(X0,X4,X3),vabs(X1,X5,veabs),X6)|vtcheck(X3,vsubst(X0,X2,vabs(X1,X5,veabs)),X6))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f267])).
% 0.14/0.41 fof(f269,plain,(
% 0.14/0.41 ![VT,VC,Vx,Ve,Vy,VS,VT2]: ((((Vx=Vy|~visFreeVar(Vy,Ve))|~vtcheck(VC,Ve,VT))|~vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))|vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2))),
% 0.14/0.41 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.14/0.41 fof(f270,plain,(
% 0.14/0.41 ![VC,Vx,Ve,Vy,VS,VT2]: ((![VT]: (((Vx=Vy|~visFreeVar(Vy,Ve))|~vtcheck(VC,Ve,VT))|~vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2)))|vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f269])).
% 0.14/0.41 fof(f271,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (X0=X1|~visFreeVar(X1,X2)|~vtcheck(X3,X2,X4)|~vtcheck(vbind(X0,X4,X3),vabs(X1,X5,veabs),X6)|vtcheck(X3,vsubst(X0,X2,vabs(X1,X5,veabs)),X6))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f270])).
% 0.14/0.41 fof(f272,plain,(
% 0.14/0.41 (?[VT,VC,Vx,Ve,Vy,VS,VT2]: ((vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2))&~vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2)))),
% 0.14/0.41 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.14/0.41 fof(f273,plain,(
% 0.14/0.41 ?[VC,Vx,Ve,Vy,VS,VT2]: ((?[VT]: (vtcheck(VC,Ve,VT)&vtcheck(vbind(Vx,VT,VC),vabs(Vy,VS,veabs),VT2)))&~vtcheck(VC,vsubst(Vx,Ve,vabs(Vy,VS,veabs)),VT2))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f272])).
% 0.14/0.41 fof(f274,plain,(
% 0.14/0.41 ((vtcheck(sK21_skl,sK23_skl,sK27_skl)&vtcheck(vbind(sK22_skl,sK27_skl,sK21_skl),vabs(sK24_skl,sK25_skl,veabs),sK26_skl))&~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK24_skl,sK25_skl,veabs)),sK26_skl))),
% 0.14/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl]),skolemize(VC,sK21_skl),skolemize(Vx,sK22_skl),skolemize(Ve,sK23_skl),skolemize(Vy,sK24_skl),skolemize(VS,sK25_skl),skolemize(VT2,sK26_skl),skolemize(VT,sK27_skl)],[f273])).
% 0.14/0.41 fof(f275,plain,(
% 0.14/0.41 vtcheck(sK21_skl,sK23_skl,sK27_skl)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/0.41 fof(f276,plain,(
% 0.14/0.41 vtcheck(vbind(sK22_skl,sK27_skl,sK21_skl),vabs(sK24_skl,sK25_skl,veabs),sK26_skl)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/0.41 fof(f277,plain,(
% 0.14/0.41 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK24_skl,sK25_skl,veabs)),sK26_skl)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/0.41 fof(f449,plain,(
% 0.14/0.41 ![X0,X1,X2,X3]: (vsubst(X0,X1,vabs(X0,X2,X3))=vabs(X0,X2,X3))),
% 0.14/0.41 inference(destructive_equality_resolution,[status(thm)],[f165])).
% 0.14/0.41 fof(f473,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (~vtcheck(X0,X1,X2)|~vtcheck(vbind(X3,X2,X0),vabs(X3,X4,X5),X6)|vtcheck(X0,vsubst(X3,X1,vabs(X3,X4,X5)),X6))),
% 0.14/0.41 inference(destructive_equality_resolution,[status(thm)],[f265])).
% 0.14/0.41 fof(f508,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (~vtcheck(X0,X1,X2)|~vtcheck(vbind(X3,X2,X0),vabs(X3,X4,X5),X6)|vtcheck(X0,vabs(X3,X4,X5),X6))),
% 0.14/0.41 inference(forward_demodulation,[status(thm)],[f449,f473])).
% 0.14/0.41 fof(f510,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (X0=X1|~vtcheck(X2,X3,X4)|~vtcheck(vbind(X0,X4,X2),vabs(X1,X5,veabs),X6)|vtcheck(X2,vsubst(X0,X3,vabs(X1,X5,veabs)),X6))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f271,f268])).
% 0.14/0.41 fof(f511,plain,(
% 0.14/0.41 ![X0]: (sK22_skl=sK24_skl|~vtcheck(sK21_skl,X0,sK27_skl)|vtcheck(sK21_skl,vsubst(sK22_skl,X0,vabs(sK24_skl,sK25_skl,veabs)),sK26_skl))),
% 0.14/0.41 inference(resolution,[status(thm)],[f510,f276])).
% 0.14/0.41 fof(f515,plain,(
% 0.14/0.41 sK22_skl=sK24_skl|~vtcheck(sK21_skl,sK23_skl,sK27_skl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f511,f277])).
% 0.14/0.41 fof(f516,plain,(
% 0.14/0.41 sK22_skl=sK24_skl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f515,f275])).
% 0.14/0.41 fof(f518,plain,(
% 0.14/0.41 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK22_skl,sK25_skl,veabs)),sK26_skl)),
% 0.14/0.41 inference(backward_demodulation,[status(thm)],[f516,f277])).
% 0.14/0.41 fof(f519,plain,(
% 0.14/0.41 vtcheck(vbind(sK22_skl,sK27_skl,sK21_skl),vabs(sK22_skl,sK25_skl,veabs),sK26_skl)),
% 0.14/0.41 inference(backward_demodulation,[status(thm)],[f516,f276])).
% 0.14/0.41 fof(f520,plain,(
% 0.14/0.41 ~vtcheck(sK21_skl,vabs(sK22_skl,sK25_skl,veabs),sK26_skl)),
% 0.14/0.41 inference(forward_demodulation,[status(thm)],[f449,f518])).
% 0.14/0.41 fof(f524,plain,(
% 0.14/0.41 ![X0]: (~vtcheck(sK21_skl,X0,sK27_skl)|vtcheck(sK21_skl,vabs(sK22_skl,sK25_skl,veabs),sK26_skl))),
% 0.14/0.41 inference(resolution,[status(thm)],[f519,f508])).
% 0.14/0.41 fof(f525,plain,(
% 0.14/0.41 ![X0]: (~vtcheck(sK21_skl,X0,sK27_skl))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f524,f520])).
% 0.14/0.41 fof(f559,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f275,f525])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.065822 seconds
% 0.14/0.44 % CPU time: 0.164875 seconds
% 0.14/0.44 % Total memory used: 79.982 MB
% 0.14/0.44 % Net memory used: 79.784 MB
%------------------------------------------------------------------------------