%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM130+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.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM130+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.10/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 14:17:40 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.42 % Refutation found
% 0.14/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.42 fof(f11,axiom,(
% 0.14/0.42 (! [VT,VVar0,VExp0,Vx,Vv,Ve] :( ( VVar0 = Vv& VExp0 = vabs(Vx,VT,Ve) )=> ( ( ( Vx != Vv& visFreeVar(Vv,Ve) )=> visFreeVar(VVar0,VExp0) )& ( visFreeVar(VVar0,VExp0)=> ( Vx != Vv& visFreeVar(Vv,Ve) ) ) ) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f32,axiom,(
% 0.14/0.42 (! [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.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f56,axiom,(
% 0.14/0.42 (! [Vx,VS,VC,Ve,VT] :( ( ~ visFreeVar(Vx,Ve)& vtcheck(vbind(Vx,VS,VC),Ve,VT) )=> vtcheck(VC,Ve,VT) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f59,conjecture,(
% 0.14/0.42 (! [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.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f60,negated_conjecture,(
% 0.14/0.42 ~((! [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.42 inference(negated_conjecture,[status(cth)],[f59])).
% 0.14/0.42 fof(f91,plain,(
% 0.14/0.42 ![VT,VVar0,VExp0,Vx,Vv,Ve]: ((~VVar0=Vv|~VExp0=vabs(Vx,VT,Ve))|(((Vx=Vv|~visFreeVar(Vv,Ve))|visFreeVar(VVar0,VExp0))&(~visFreeVar(VVar0,VExp0)|(~Vx=Vv&visFreeVar(Vv,Ve)))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.14/0.42 fof(f92,plain,(
% 0.14/0.42 ![VVar0,VExp0,Vx,Vv,Ve]: ((~VVar0=Vv|(![VT]: ~VExp0=vabs(Vx,VT,Ve)))|(((Vx=Vv|~visFreeVar(Vv,Ve))|visFreeVar(VVar0,VExp0))&(~visFreeVar(VVar0,VExp0)|(~Vx=Vv&visFreeVar(Vv,Ve)))))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f91])).
% 0.14/0.42 fof(f94,plain,(
% 0.14/0.42 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|~X2=vabs(X3,X4,X5)|~visFreeVar(X0,X2)|~X3=X1)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.14/0.42 fof(f160,plain,(
% 0.14/0.42 ![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.42 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.14/0.42 fof(f161,plain,(
% 0.14/0.42 ![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.42 inference(miniscoping,[status(thm)],[f160])).
% 0.14/0.42 fof(f162,plain,(
% 0.14/0.42 ![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.42 inference(cnf_transformation,[status(thm)],[f161])).
% 0.14/0.42 fof(f251,plain,(
% 0.14/0.42 ![Vx,VS,VC,Ve,VT]: ((visFreeVar(Vx,Ve)|~vtcheck(vbind(Vx,VS,VC),Ve,VT))|vtcheck(VC,Ve,VT))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.14/0.42 fof(f252,plain,(
% 0.14/0.42 ![VC,Ve,VT]: ((![Vx]: (visFreeVar(Vx,Ve)|(![VS]: ~vtcheck(vbind(Vx,VS,VC),Ve,VT))))|vtcheck(VC,Ve,VT))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f251])).
% 0.14/0.42 fof(f253,plain,(
% 0.14/0.42 ![X0,X1,X2,X3,X4]: (visFreeVar(X0,X1)|~vtcheck(vbind(X0,X2,X3),X1,X4)|vtcheck(X3,X1,X4))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f252])).
% 0.14/0.42 fof(f260,plain,(
% 0.14/0.42 (?[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.42 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.14/0.42 fof(f261,plain,(
% 0.14/0.42 ?[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.42 inference(miniscoping,[status(thm)],[f260])).
% 0.14/0.42 fof(f262,plain,(
% 0.14/0.42 (((sK22_skl=sK24_skl&vtcheck(sK21_skl,sK23_skl,sK28_skl))&vtcheck(vbind(sK22_skl,sK28_skl,sK21_skl),vabs(sK24_skl,sK25_skl,sK26_skl),sK27_skl))&~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK24_skl,sK25_skl,sK26_skl)),sK27_skl))),
% 0.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(VC,sK21_skl),skolemize(Vx,sK22_skl),skolemize(Ve,sK23_skl),skolemize(Vy,sK24_skl),skolemize(VS,sK25_skl),skolemize(Ve1,sK26_skl),skolemize(VT2,sK27_skl),skolemize(VT,sK28_skl)],[f261])).
% 0.14/0.43 fof(f263,plain,(
% 0.14/0.43 sK22_skl=sK24_skl),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f262])).
% 0.14/0.43 fof(f265,plain,(
% 0.14/0.43 vtcheck(vbind(sK22_skl,sK28_skl,sK21_skl),vabs(sK24_skl,sK25_skl,sK26_skl),sK27_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f262])).
% 0.14/0.43 fof(f266,plain,(
% 0.14/0.43 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK24_skl,sK25_skl,sK26_skl)),sK27_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f262])).
% 0.14/0.43 fof(f418,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~visFreeVar(X0,vabs(X0,X1,X2)))),
% 0.14/0.43 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 0.14/0.43 fof(f438,plain,(
% 0.14/0.43 ![X0,X1,X2,X3]: (vsubst(X0,X1,vabs(X0,X2,X3))=vabs(X0,X2,X3))),
% 0.14/0.43 inference(destructive_equality_resolution,[status(thm)],[f162])).
% 0.14/0.43 fof(f462,plain,(
% 0.14/0.43 vtcheck(vbind(sK22_skl,sK28_skl,sK21_skl),vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl)),
% 0.14/0.43 inference(forward_demodulation,[status(thm)],[f263,f265])).
% 0.14/0.43 fof(f463,plain,(
% 0.14/0.43 ~vtcheck(sK21_skl,vsubst(sK22_skl,sK23_skl,vabs(sK22_skl,sK25_skl,sK26_skl)),sK27_skl)),
% 0.14/0.43 inference(forward_demodulation,[status(thm)],[f263,f266])).
% 0.14/0.43 fof(f464,plain,(
% 0.14/0.43 ~vtcheck(sK21_skl,vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl)),
% 0.14/0.43 inference(forward_demodulation,[status(thm)],[f438,f463])).
% 0.14/0.43 fof(f495,plain,(
% 0.14/0.43 visFreeVar(sK22_skl,vabs(sK22_skl,sK25_skl,sK26_skl))|vtcheck(sK21_skl,vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl)),
% 0.14/0.43 inference(resolution,[status(thm)],[f253,f462])).
% 0.14/0.43 fof(f498,plain,(
% 0.14/0.43 vtcheck(sK21_skl,vabs(sK22_skl,sK25_skl,sK26_skl),sK27_skl)),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f495,f418])).
% 0.14/0.43 fof(f499,plain,(
% 0.14/0.43 $false),
% 0.14/0.43 inference(backward_subsumption_resolution,[status(thm)],[f464,f498])).
% 0.14/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.078894 seconds
% 0.14/0.44 % CPU time: 0.340641 seconds
% 0.14/0.44 % Total memory used: 97.978 MB
% 0.14/0.44 % Net memory used: 97.425 MB
%------------------------------------------------------------------------------