%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM125+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 : n015.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:50 PM UTC 2026
% Result : Theorem 0.12s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM125+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 14:20:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.39 fof(f11,axiom,(
% 0.12/0.39 (! [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.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f58,axiom,(
% 0.12/0.39 (! [Vx,VS,VC,Vy,VS1,VT] :( ( Vx != Vy& ~ visFreeVar(Vx,vabs(Vy,VS1,veabs))& vtcheck(VC,vabs(Vy,VS1,veabs),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f59,axiom,(
% 0.12/0.39 (! [Vx,VS,VC,Vy,VS1,VT] :( ( Vx = Vy& ~ visFreeVar(Vx,vabs(Vy,VS1,veabs))& vtcheck(VC,vabs(Vy,VS1,veabs),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f60,conjecture,(
% 0.12/0.39 (! [Vx,VS,VC,Vy,VS1,VT] :( ( ~ visFreeVar(Vx,vabs(Vy,VS1,veabs))& vtcheck(VC,vabs(Vy,VS1,veabs),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ) )),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f61,negated_conjecture,(
% 0.12/0.39 ~((! [Vx,VS,VC,Vy,VS1,VT] :( ( ~ visFreeVar(Vx,vabs(Vy,VS1,veabs))& vtcheck(VC,vabs(Vy,VS1,veabs),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT) ) ))),
% 0.12/0.39 inference(negated_conjecture,[status(cth)],[f60])).
% 0.12/0.39 fof(f92,plain,(
% 0.12/0.39 ![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.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.12/0.39 fof(f93,plain,(
% 0.12/0.39 ![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.12/0.39 inference(miniscoping,[status(thm)],[f92])).
% 0.12/0.39 fof(f95,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|~X2=vabs(X3,X4,X5)|~visFreeVar(X0,X2)|~X3=X1)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.39 fof(f258,plain,(
% 0.12/0.39 ![Vx,VS,VC,Vy,VS1,VT]: (((Vx=Vy|visFreeVar(Vx,vabs(Vy,VS1,veabs)))|~vtcheck(VC,vabs(Vy,VS1,veabs),VT))|vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.12/0.39 fof(f259,plain,(
% 0.12/0.39 ![Vx,VC,Vy,VS1,VT]: (((Vx=Vy|visFreeVar(Vx,vabs(Vy,VS1,veabs)))|~vtcheck(VC,vabs(Vy,VS1,veabs),VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f258])).
% 0.12/0.39 fof(f260,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5]: (X0=X1|visFreeVar(X0,vabs(X1,X2,veabs))|~vtcheck(X3,vabs(X1,X2,veabs),X4)|vtcheck(vbind(X0,X5,X3),vabs(X1,X2,veabs),X4))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f259])).
% 0.12/0.39 fof(f261,plain,(
% 0.12/0.39 ![Vx,VS,VC,Vy,VS1,VT]: (((~Vx=Vy|visFreeVar(Vx,vabs(Vy,VS1,veabs)))|~vtcheck(VC,vabs(Vy,VS1,veabs),VT))|vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.12/0.39 fof(f262,plain,(
% 0.12/0.39 ![Vx,VC,Vy,VS1,VT]: (((~Vx=Vy|visFreeVar(Vx,vabs(Vy,VS1,veabs)))|~vtcheck(VC,vabs(Vy,VS1,veabs),VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f261])).
% 0.12/0.39 fof(f263,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|visFreeVar(X0,vabs(X1,X2,veabs))|~vtcheck(X3,vabs(X1,X2,veabs),X4)|vtcheck(vbind(X0,X5,X3),vabs(X1,X2,veabs),X4))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f262])).
% 0.12/0.39 fof(f264,plain,(
% 0.12/0.39 (?[Vx,VS,VC,Vy,VS1,VT]: ((~visFreeVar(Vx,vabs(Vy,VS1,veabs))&vtcheck(VC,vabs(Vy,VS1,veabs),VT))&~vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.12/0.39 fof(f265,plain,(
% 0.12/0.39 ?[Vx,VC,Vy,VS1,VT]: ((~visFreeVar(Vx,vabs(Vy,VS1,veabs))&vtcheck(VC,vabs(Vy,VS1,veabs),VT))&(?[VS]: ~vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,veabs),VT)))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f264])).
% 0.12/0.39 fof(f266,plain,(
% 0.12/0.39 ((~visFreeVar(sK21_skl,vabs(sK23_skl,sK24_skl,veabs))&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))),
% 0.12/0.39 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)],[f265])).
% 0.12/0.39 fof(f267,plain,(
% 0.12/0.39 ~visFreeVar(sK21_skl,vabs(sK23_skl,sK24_skl,veabs))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f266])).
% 0.12/0.39 fof(f268,plain,(
% 0.12/0.39 vtcheck(sK22_skl,vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f266])).
% 0.12/0.39 fof(f269,plain,(
% 0.12/0.39 ~vtcheck(vbind(sK21_skl,sK26_skl,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f266])).
% 0.12/0.39 fof(f421,plain,(
% 0.12/0.39 ![X0,X1,X2]: (~visFreeVar(X0,vabs(X0,X1,X2)))),
% 0.12/0.39 inference(destructive_equality_resolution,[status(thm)],[f95])).
% 0.12/0.39 fof(f465,plain,(
% 0.12/0.39 ![X1,X2,X3,X4,X5]: (visFreeVar(X1,vabs(X1,X2,veabs))|~vtcheck(X3,vabs(X1,X2,veabs),X4)|vtcheck(vbind(X1,X5,X3),vabs(X1,X2,veabs),X4))),
% 0.12/0.39 inference(destructive_equality_resolution,[status(thm)],[f263])).
% 0.12/0.39 fof(f466,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,vabs(X1,X2,veabs),X3)|vtcheck(vbind(X1,X4,X0),vabs(X1,X2,veabs),X3))),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f465,f421])).
% 0.12/0.39 fof(f554,plain,(
% 0.12/0.39 ![X0,X1]: (X0=sK23_skl|visFreeVar(X0,vabs(sK23_skl,sK24_skl,veabs))|vtcheck(vbind(X0,X1,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl))),
% 0.12/0.39 inference(resolution,[status(thm)],[f260,f268])).
% 0.12/0.39 fof(f555,plain,(
% 0.12/0.39 ![X0]: (vtcheck(vbind(sK23_skl,X0,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl))),
% 0.12/0.39 inference(resolution,[status(thm)],[f466,f268])).
% 0.12/0.39 fof(f588,plain,(
% 0.12/0.39 sK21_skl=sK23_skl|visFreeVar(sK21_skl,vabs(sK23_skl,sK24_skl,veabs))),
% 0.12/0.39 inference(resolution,[status(thm)],[f554,f269])).
% 0.12/0.39 fof(f594,plain,(
% 0.12/0.39 ![X0]: (vtcheck(vbind(sK23_skl,X0,sK22_skl),vabs(sK21_skl,sK24_skl,veabs),sK25_skl))),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f604,f555])).
% 0.12/0.39 fof(f598,plain,(
% 0.12/0.39 ~vtcheck(vbind(sK21_skl,sK26_skl,sK22_skl),vabs(sK21_skl,sK24_skl,veabs),sK25_skl)),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f604,f269])).
% 0.12/0.39 fof(f604,plain,(
% 0.12/0.39 sK21_skl=sK23_skl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f588,f267])).
% 0.12/0.39 fof(f623,plain,(
% 0.12/0.39 ![X0]: (vtcheck(vbind(sK21_skl,X0,sK22_skl),vabs(sK21_skl,sK24_skl,veabs),sK25_skl))),
% 0.12/0.39 inference(forward_demodulation,[status(thm)],[f604,f594])).
% 0.12/0.39 fof(f625,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f598,f623])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.41 % Elapsed time: 0.051353 seconds
% 0.12/0.41 % CPU time: 0.154023 seconds
% 0.12/0.41 % Total memory used: 46.384 MB
% 0.12/0.41 % Net memory used: 46.197 MB
%------------------------------------------------------------------------------