%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM124+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 : n012.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 159.11s 20.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM124+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n012.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.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 14:17:21 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 159.11/20.43 % Refutation found
% 159.11/20.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 159.11/20.43 % SZS output start CNFRefutation for theBenchmark
% 159.11/20.43 fof(f10,axiom,(
% 159.11/20.43 (! [VVar0,VExp0,Vx,Vv] :( ( VVar0 = Vv& VExp0 = vvar(Vx) )=> ( ( Vx = Vv=> visFreeVar(VVar0,VExp0) )& ( visFreeVar(VVar0,VExp0)=> Vx = Vv ) ) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f11,axiom,(
% 159.11/20.43 (! [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) ) ) ) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f12,axiom,(
% 159.11/20.43 (! [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) ) ) ) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f28,axiom,(
% 159.11/20.43 (! [Vv,Ve] :( vgensym(Ve) = Vv=> ~ visFreeVar(Vv,Ve) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f56,axiom,(
% 159.11/20.43 (! [Ve2,Ve1] :( valphaEquivalent(Ve1,Ve2)=> valphaEquivalent(Ve2,Ve1) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f58,axiom,(
% 159.11/20.43 (! [VS,Vx,Vy,Ve] :( ~ visFreeVar(Vy,Ve)=> valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve))) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f59,axiom,(
% 159.11/20.43 (! [Ve,VC,Ve1,VT] :( ( vtcheck(VC,Ve,VT)& valphaEquivalent(Ve,Ve1) )=> vtcheck(VC,Ve1,VT) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f60,axiom,(
% 159.11/20.43 (! [Ve,Vx,Ve1] :( ( ~ visFreeVar(Vx,Ve)& valphaEquivalent(Ve,Ve1) )=> ~ visFreeVar(Vx,Ve1) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f63,axiom,(
% 159.11/20.43 (! [Vx,VS,VC,Vy,VS1,Ve1,VT] :( ( Vx != Vy& ~ visFreeVar(Vx,vabs(Vy,VS1,Ve1))& vtcheck(VC,vabs(Vy,VS1,Ve1),VT) )=> vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,Ve1),VT) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f64,conjecture,(
% 159.11/20.43 (! [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) ) )),
% 159.11/20.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.11/20.43 fof(f65,negated_conjecture,(
% 159.11/20.43 ~((! [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) ) ))),
% 159.11/20.43 inference(negated_conjecture,[status(cth)],[f64])).
% 159.11/20.43 fof(f93,plain,(
% 159.11/20.43 ![VVar0,VExp0,Vx,Vv]: ((~VVar0=Vv|~VExp0=vvar(Vx))|((~Vx=Vv|visFreeVar(VVar0,VExp0))&(~visFreeVar(VVar0,VExp0)|Vx=Vv)))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 159.11/20.43 fof(f94,plain,(
% 159.11/20.43 ![X0,X1,X2,X3]: (~X0=X1|~X2=vvar(X3)|~X3=X1|visFreeVar(X0,X2))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f93])).
% 159.11/20.43 fof(f96,plain,(
% 159.11/20.43 ![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)))))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 159.11/20.43 fof(f97,plain,(
% 159.11/20.43 ![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)))))),
% 159.11/20.43 inference(miniscoping,[status(thm)],[f96])).
% 159.11/20.43 fof(f99,plain,(
% 159.11/20.43 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|~X2=vabs(X3,X4,X5)|~visFreeVar(X0,X2)|~X3=X1)),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f97])).
% 159.11/20.43 fof(f101,plain,(
% 159.11/20.43 ![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)))))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 159.11/20.43 fof(f102,plain,(
% 159.11/20.43 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X3)|visFreeVar(X0,X2))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f101])).
% 159.11/20.43 fof(f103,plain,(
% 159.11/20.43 ![X0,X1,X2,X3,X4]: (~X0=X1|~X2=vapp(X3,X4)|~visFreeVar(X1,X4)|visFreeVar(X0,X2))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f101])).
% 159.11/20.43 fof(f154,plain,(
% 159.11/20.43 ![Vv,Ve]: (~vgensym(Ve)=Vv|~visFreeVar(Vv,Ve))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 159.11/20.43 fof(f155,plain,(
% 159.11/20.43 ![X0,X1]: (~vgensym(X0)=X1|~visFreeVar(X1,X0))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f154])).
% 159.11/20.43 fof(f254,plain,(
% 159.11/20.43 ![Ve2,Ve1]: (~valphaEquivalent(Ve1,Ve2)|valphaEquivalent(Ve2,Ve1))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 159.11/20.43 fof(f255,plain,(
% 159.11/20.43 ![X0,X1]: (~valphaEquivalent(X0,X1)|valphaEquivalent(X1,X0))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f254])).
% 159.11/20.43 fof(f259,plain,(
% 159.11/20.43 ![VS,Vx,Vy,Ve]: (visFreeVar(Vy,Ve)|valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve))))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 159.11/20.43 fof(f260,plain,(
% 159.11/20.43 ![Vy,Ve]: (visFreeVar(Vy,Ve)|(![VS,Vx]: valphaEquivalent(vabs(Vx,VS,Ve),vabs(Vy,VS,vsubst(Vx,vvar(Vy),Ve)))))),
% 159.11/20.43 inference(miniscoping,[status(thm)],[f259])).
% 159.11/20.43 fof(f261,plain,(
% 159.11/20.43 ![X0,X1,X2,X3]: (visFreeVar(X0,X1)|valphaEquivalent(vabs(X2,X3,X1),vabs(X0,X3,vsubst(X2,vvar(X0),X1))))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f260])).
% 159.11/20.43 fof(f262,plain,(
% 159.11/20.43 ![Ve,VC,Ve1,VT]: ((~vtcheck(VC,Ve,VT)|~valphaEquivalent(Ve,Ve1))|vtcheck(VC,Ve1,VT))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 159.11/20.43 fof(f263,plain,(
% 159.11/20.43 ![VC,Ve1,VT]: ((![Ve]: (~vtcheck(VC,Ve,VT)|~valphaEquivalent(Ve,Ve1)))|vtcheck(VC,Ve1,VT))),
% 159.11/20.43 inference(miniscoping,[status(thm)],[f262])).
% 159.11/20.43 fof(f264,plain,(
% 159.11/20.43 ![X0,X1,X2,X3]: (~vtcheck(X0,X1,X2)|~valphaEquivalent(X1,X3)|vtcheck(X0,X3,X2))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f263])).
% 159.11/20.43 fof(f265,plain,(
% 159.11/20.43 ![Ve,Vx,Ve1]: ((visFreeVar(Vx,Ve)|~valphaEquivalent(Ve,Ve1))|~visFreeVar(Vx,Ve1))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 159.11/20.43 fof(f266,plain,(
% 159.11/20.43 ![Vx,Ve1]: ((![Ve]: (visFreeVar(Vx,Ve)|~valphaEquivalent(Ve,Ve1)))|~visFreeVar(Vx,Ve1))),
% 159.11/20.43 inference(miniscoping,[status(thm)],[f265])).
% 159.11/20.43 fof(f267,plain,(
% 159.11/20.43 ![X0,X1,X2]: (visFreeVar(X0,X1)|~valphaEquivalent(X1,X2)|~visFreeVar(X0,X2))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f266])).
% 159.11/20.43 fof(f274,plain,(
% 159.11/20.43 ![Vx,VS,VC,Vy,VS1,Ve1,VT]: (((Vx=Vy|visFreeVar(Vx,vabs(Vy,VS1,Ve1)))|~vtcheck(VC,vabs(Vy,VS1,Ve1),VT))|vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,Ve1),VT))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 159.11/20.43 fof(f275,plain,(
% 159.11/20.43 ![Vx,VC,Vy,VS1,Ve1,VT]: (((Vx=Vy|visFreeVar(Vx,vabs(Vy,VS1,Ve1)))|~vtcheck(VC,vabs(Vy,VS1,Ve1),VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),vabs(Vy,VS1,Ve1),VT)))),
% 159.11/20.43 inference(miniscoping,[status(thm)],[f274])).
% 159.11/20.43 fof(f276,plain,(
% 159.11/20.43 ![X0,X1,X2,X3,X4,X5,X6]: (X0=X1|visFreeVar(X0,vabs(X1,X2,X3))|~vtcheck(X4,vabs(X1,X2,X3),X5)|vtcheck(vbind(X0,X6,X4),vabs(X1,X2,X3),X5))),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f275])).
% 159.11/20.43 fof(f277,plain,(
% 159.11/20.43 (?[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)))),
% 159.11/20.43 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 159.11/20.43 fof(f278,plain,(
% 159.11/20.43 ?[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)))),
% 159.11/20.43 inference(miniscoping,[status(thm)],[f277])).
% 159.11/20.43 fof(f279,plain,(
% 159.11/20.43 (((sK21_skl=sK23_skl&~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))),
% 159.11/20.43 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)],[f278])).
% 159.11/20.43 fof(f280,plain,(
% 159.11/20.43 sK21_skl=sK23_skl),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f279])).
% 159.11/20.43 fof(f282,plain,(
% 159.11/20.43 vtcheck(sK22_skl,vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f279])).
% 159.11/20.43 fof(f283,plain,(
% 159.11/20.43 ~vtcheck(vbind(sK21_skl,sK26_skl,sK22_skl),vabs(sK23_skl,sK24_skl,veabs),sK25_skl)),
% 159.11/20.43 inference(cnf_transformation,[status(thm)],[f279])).
% 159.11/20.43 fof(f432,plain,(
% 159.11/20.43 ![X0]: (visFreeVar(X0,vvar(X0)))),
% 159.11/20.46 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 159.11/20.46 fof(f435,plain,(
% 159.11/20.46 ![X0,X1,X2]: (~visFreeVar(X0,vabs(X0,X1,X2)))),
% 159.11/20.46 inference(destructive_equality_resolution,[status(thm)],[f99])).
% 159.11/20.46 fof(f437,plain,(
% 159.11/20.46 ![X0,X1,X2]: (~visFreeVar(X0,X1)|visFreeVar(X0,vapp(X1,X2)))),
% 159.11/20.46 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 159.11/20.46 fof(f438,plain,(
% 159.11/20.46 ![X0,X1,X2]: (~visFreeVar(X0,X1)|visFreeVar(X0,vapp(X2,X1)))),
% 159.11/20.46 inference(destructive_equality_resolution,[status(thm)],[f103])).
% 159.11/20.46 fof(f451,plain,(
% 159.11/20.46 ![X0]: (~visFreeVar(vgensym(X0),X0))),
% 159.11/20.46 inference(destructive_equality_resolution,[status(thm)],[f155])).
% 159.11/20.46 fof(f496,plain,(
% 159.11/20.46 vtcheck(sK22_skl,vabs(sK21_skl,sK24_skl,veabs),sK25_skl)),
% 159.11/20.46 inference(forward_demodulation,[status(thm)],[f280,f282])).
% 159.11/20.46 fof(f889,plain,(
% 159.11/20.46 ~vtcheck(vbind(sK21_skl,sK26_skl,sK22_skl),vabs(sK21_skl,sK24_skl,veabs),sK25_skl)),
% 159.11/20.46 inference(forward_demodulation,[status(thm)],[f280,f283])).
% 159.11/20.46 fof(f932,plain,(
% 159.11/20.46 ![X0,X1,X2,X3]: (visFreeVar(X0,vapp(vapp(X1,X2),X3))|~visFreeVar(X0,X1))),
% 159.11/20.46 inference(resolution,[status(thm)],[f437,f437])).
% 159.11/20.46 fof(f945,plain,(
% 159.11/20.46 ![X0,X1]: (visFreeVar(X0,vapp(vvar(X0),X1)))),
% 159.11/20.46 inference(resolution,[status(thm)],[f437,f432])).
% 159.11/20.46 fof(f2163,plain,(
% 159.11/20.46 ![X0,X1,X2,X3]: (visFreeVar(X0,vapp(vapp(vapp(vvar(X0),X1),X2),X3)))),
% 159.11/20.46 inference(resolution,[status(thm)],[f932,f945])).
% 159.11/20.46 fof(f2388,plain,(
% 159.11/20.46 ![X0,X1]: (~visFreeVar(vgensym(vapp(X0,X1)),X1))),
% 159.11/20.46 inference(resolution,[status(thm)],[f451,f438])).
% 159.11/20.46 fof(f2389,plain,(
% 159.11/20.46 ![X0,X1]: (~visFreeVar(vgensym(vapp(X0,X1)),X0))),
% 159.11/20.46 inference(resolution,[status(thm)],[f451,f437])).
% 159.11/20.46 fof(f10555,plain,(
% 159.11/20.46 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~valphaEquivalent(vabs(X0,X1,X2),X3)|vtcheck(vbind(X4,X5,X6),X3,X7)|X4=X0|visFreeVar(X4,vabs(X0,X1,X2))|~vtcheck(X6,vabs(X0,X1,X2),X7))),
% 159.11/20.46 inference(resolution,[status(thm)],[f264,f276])).
% 159.11/20.46 fof(f10561,plain,(
% 159.11/20.46 ![X0]: (~valphaEquivalent(vabs(sK21_skl,sK24_skl,veabs),X0)|vtcheck(sK22_skl,X0,sK25_skl))),
% 159.11/20.46 inference(resolution,[status(thm)],[f264,f496])).
% 159.11/20.46 fof(f10657,plain,(
% 159.11/20.46 ![X0,X1,X2,X3]: (~valphaEquivalent(vabs(X0,X1,X2),X3)|~visFreeVar(X0,X3))),
% 159.11/20.46 inference(resolution,[status(thm)],[f267,f435])).
% 159.11/20.46 fof(f11860,plain,(
% 159.11/20.46 ![X0,X1,X2]: (~valphaEquivalent(vabs(X0,X1,X2),vabs(sK21_skl,sK24_skl,veabs))|sK21_skl=X0|visFreeVar(sK21_skl,vabs(X0,X1,X2))|~vtcheck(sK22_skl,vabs(X0,X1,X2),sK25_skl))),
% 159.11/20.46 inference(resolution,[status(thm)],[f10555,f889])).
% 159.11/20.46 fof(f15890,plain,(
% 159.11/20.46 ![X0]: (vtcheck(sK22_skl,X0,sK25_skl)|~valphaEquivalent(X0,vabs(sK21_skl,sK24_skl,veabs)))),
% 159.11/20.46 inference(resolution,[status(thm)],[f10561,f255])).
% 159.11/20.46 fof(f18642,plain,(
% 159.11/20.46 ![X0,X1,X2]: (~valphaEquivalent(vabs(X0,X1,X2),vabs(sK21_skl,sK24_skl,veabs))|sK21_skl=X0|visFreeVar(sK21_skl,vabs(X0,X1,X2)))),
% 159.11/20.46 inference(backward_subsumption_resolution,[status(thm)],[f11860,f15890])).
% 159.11/20.46 fof(f19675,plain,(
% 159.11/20.46 ![X0,X1,X2]: (sK21_skl=X0|visFreeVar(sK21_skl,vabs(X0,X1,X2))|~valphaEquivalent(vabs(sK21_skl,sK24_skl,veabs),vabs(X0,X1,X2)))),
% 159.11/20.46 inference(resolution,[status(thm)],[f18642,f255])).
% 159.11/20.46 fof(f19678,plain,(
% 159.11/20.46 ![X0,X1,X2]: (sK21_skl=X0|~valphaEquivalent(vabs(sK21_skl,sK24_skl,veabs),vabs(X0,X1,X2)))),
% 159.11/20.46 inference(forward_subsumption_resolution,[status(thm)],[f19675,f10657])).
% 159.11/20.46 fof(f25865,plain,(
% 159.11/20.46 ![X0]: (sK21_skl=X0|visFreeVar(X0,veabs))),
% 159.11/20.46 inference(resolution,[status(thm)],[f19678,f261])).
% 159.11/20.46 fof(f26154,plain,(
% 159.11/20.46 ![X0]: (sK21_skl=vgensym(vapp(veabs,X0)))),
% 159.11/20.46 inference(resolution,[status(thm)],[f25865,f2389])).
% 159.11/20.46 fof(f28805,plain,(
% 159.11/20.46 ![X0]: (~visFreeVar(sK21_skl,X0))),
% 159.11/20.46 inference(paramodulation,[status(thm)],[f26154,f2388])).
% 159.11/20.46 fof(f29088,plain,(
% 159.11/20.46 $false),
% 159.11/20.46 inference(resolution,[status(thm)],[f28805,f2163])).
% 159.11/20.46 % SZS output end CNFRefutation for theBenchmark.p
% 159.11/20.49 % Elapsed time: 20.130203 seconds
% 159.11/20.49 % CPU time: 159.751956 seconds
% 159.11/20.49 % Total memory used: 737.455 MB
% 159.11/20.49 % Net memory used: 655.221 MB
%------------------------------------------------------------------------------