%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM142+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:52 PM UTC 2026
% Result : Theorem 125.17s 16.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : COM142+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 14:17:51 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 125.17/16.16 % Refutation found
% 125.17/16.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 125.17/16.16 % SZS output start CNFRefutation for theBenchmark
% 125.17/16.16 fof(f3,axiom,(
% 125.17/16.16 (! [VExp0,VExp1,VExp2,VExp3] :( ( vapp(VExp0,VExp1) = vapp(VExp2,VExp3)=> ( VExp0 = VExp2& VExp1 = VExp3 ) )& ( ( VExp0 = VExp2& VExp1 = VExp3 )=> vapp(VExp0,VExp1) = vapp(VExp2,VExp3) ) ) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f5,axiom,(
% 125.17/16.16 (! [VVar0,VExp0,VExp1] : vvar(VVar0) != vapp(VExp0,VExp1) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f6,axiom,(
% 125.17/16.16 (! [VVar0,VTyp0,VExp0,VExp1,VExp2] : vabs(VVar0,VTyp0,VExp0) != vapp(VExp1,VExp2) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f53,axiom,(
% 125.17/16.16 (! [VS,VC,Ve1,Ve2,VT] :( ( vtcheck(VC,Ve1,varrow(VS,VT))& vtcheck(VC,Ve2,VS) )=> vtcheck(VC,vapp(Ve1,Ve2),VT) ) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f54,axiom,(
% 125.17/16.16 (! [Ve,VT,VC] :( vtcheck(VC,Ve,VT)=> ( (? [Vx] :( Ve = vvar(Vx)& vlookup(Vx,VC) = vsomeType(VT) ))| (? [Vx,Ve2,VT1,VT2] :( Ve = vabs(Vx,VT1,Ve2)& VT = varrow(VT1,VT2)& vtcheck(vbind(Vx,VT1,VC),Ve2,VT2) ))| (? [Ve1,Ve2,VS] :( Ve = vapp(Ve1,Ve2)& vtcheck(VC,Ve1,varrow(VS,VT))& vtcheck(VC,Ve2,VS) ) )) ) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f55,axiom,(
% 125.17/16.16 (! [Vx,VS,VC,VT] :( ( vlookup(Vx,VC) = vnoType& vtcheck(VC,ve1app,VT) )=> vtcheck(vbind(Vx,VS,VC),ve1app,VT) ) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f56,axiom,(
% 125.17/16.16 (! [Vx,VS,VC,VT] :( ( vlookup(Vx,VC) = vnoType& vtcheck(VC,ve2app,VT) )=> vtcheck(vbind(Vx,VS,VC),ve2app,VT) ) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f57,conjecture,(
% 125.17/16.16 (! [Vx,VS,VC,VT] :( ( vlookup(Vx,VC) = vnoType& vtcheck(VC,vapp(ve1app,ve2app),VT) )=> vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT) ) )),
% 125.17/16.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 125.17/16.16 fof(f58,negated_conjecture,(
% 125.17/16.16 ~((! [Vx,VS,VC,VT] :( ( vlookup(Vx,VC) = vnoType& vtcheck(VC,vapp(ve1app,ve2app),VT) )=> vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT) ) ))),
% 125.17/16.16 inference(negated_conjecture,[status(cth)],[f57])).
% 125.17/16.16 fof(f69,plain,(
% 125.17/16.16 ![VExp0,VExp1,VExp2,VExp3]: ((~vapp(VExp0,VExp1)=vapp(VExp2,VExp3)|(VExp0=VExp2&VExp1=VExp3))&((~VExp0=VExp2|~VExp1=VExp3)|vapp(VExp0,VExp1)=vapp(VExp2,VExp3)))),
% 125.17/16.16 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 125.17/16.16 fof(f70,plain,(
% 125.17/16.16 (![VExp0,VExp1,VExp2,VExp3]: (~vapp(VExp0,VExp1)=vapp(VExp2,VExp3)|(VExp0=VExp2&VExp1=VExp3)))&(![VExp0,VExp1,VExp2,VExp3]: ((~VExp0=VExp2|~VExp1=VExp3)|vapp(VExp0,VExp1)=vapp(VExp2,VExp3)))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f69])).
% 125.17/16.16 fof(f71,plain,(
% 125.17/16.16 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X0=X2)),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f70])).
% 125.17/16.16 fof(f72,plain,(
% 125.17/16.16 ![X0,X1,X2,X3]: (~vapp(X0,X1)=vapp(X2,X3)|X1=X3)),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f70])).
% 125.17/16.16 fof(f75,plain,(
% 125.17/16.16 ![X0,X1,X2]: (~vvar(X0)=vapp(X1,X2))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f5])).
% 125.17/16.16 fof(f76,plain,(
% 125.17/16.16 ![X0,X1,X2,X3,X4]: (~vabs(X0,X1,X2)=vapp(X3,X4))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f6])).
% 125.17/16.16 fof(f235,plain,(
% 125.17/16.16 ![VS,VC,Ve1,Ve2,VT]: ((~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 125.17/16.16 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 125.17/16.16 fof(f236,plain,(
% 125.17/16.16 ![VC,Ve1,Ve2,VT]: ((![VS]: (~vtcheck(VC,Ve1,varrow(VS,VT))|~vtcheck(VC,Ve2,VS)))|vtcheck(VC,vapp(Ve1,Ve2),VT))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f235])).
% 125.17/16.16 fof(f237,plain,(
% 125.17/16.16 ![X0,X1,X2,X3,X4]: (~vtcheck(X0,X1,varrow(X2,X3))|~vtcheck(X0,X4,X2)|vtcheck(X0,vapp(X1,X4),X3))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f236])).
% 125.17/16.16 fof(f238,plain,(
% 125.17/16.16 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(((?[Vx]: (Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))|(?[Ve1,Ve2,VS]: ((Ve=vapp(Ve1,Ve2)&vtcheck(VC,Ve1,varrow(VS,VT)))&vtcheck(VC,Ve2,VS)))))),
% 125.17/16.16 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 125.17/16.16 fof(f239,definition,(
% 125.17/16.16 ![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)<=>((?[Vx]: (Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)))))),
% 125.17/16.16 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 125.17/16.16 fof(f240,plain,(
% 125.17/16.16 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(sP3_prd(VC,VT,Ve)|(?[Ve1,Ve2,VS]: ((Ve=vapp(Ve1,Ve2)&vtcheck(VC,Ve1,varrow(VS,VT)))&vtcheck(VC,Ve2,VS)))))),
% 125.17/16.16 inference(formula_renaming,[status(thm)],[f238,f239])).
% 125.17/16.16 fof(f241,plain,(
% 125.17/16.16 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(sP3_prd(VC,VT,Ve)|(?[Ve2,VS]: ((?[Ve1]: (Ve=vapp(Ve1,Ve2)&vtcheck(VC,Ve1,varrow(VS,VT))))&vtcheck(VC,Ve2,VS)))))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f240])).
% 125.17/16.16 fof(f242,plain,(
% 125.17/16.16 ![Ve,VT,VC]: (~vtcheck(VC,Ve,VT)|(sP3_prd(VC,VT,Ve)|((Ve=vapp(sK20_skl(VC,VT,Ve),sK18_skl(VC,VT,Ve))&vtcheck(VC,sK20_skl(VC,VT,Ve),varrow(sK19_skl(VC,VT,Ve),VT)))&vtcheck(VC,sK18_skl(VC,VT,Ve),sK19_skl(VC,VT,Ve)))))),
% 125.17/16.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(Ve2,sK18_skl(VC,VT,Ve)),skolemize(VS,sK19_skl(VC,VT,Ve)),skolemize(Ve1,sK20_skl(VC,VT,Ve))],[f241])).
% 125.17/16.16 fof(f243,plain,(
% 125.17/16.16 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|X1=vapp(sK20_skl(X0,X2,X1),sK18_skl(X0,X2,X1)))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f242])).
% 125.17/16.16 fof(f244,plain,(
% 125.17/16.16 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|vtcheck(X0,sK20_skl(X0,X2,X1),varrow(sK19_skl(X0,X2,X1),X2)))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f242])).
% 125.17/16.16 fof(f245,plain,(
% 125.17/16.16 ![X0,X1,X2]: (~vtcheck(X0,X1,X2)|sP3_prd(X0,X2,X1)|vtcheck(X0,sK18_skl(X0,X2,X1),sK19_skl(X0,X2,X1)))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f242])).
% 125.17/16.16 fof(f246,plain,(
% 125.17/16.16 ![Vx,VS,VC,VT]: ((~vlookup(Vx,VC)=vnoType|~vtcheck(VC,ve1app,VT))|vtcheck(vbind(Vx,VS,VC),ve1app,VT))),
% 125.17/16.16 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 125.17/16.16 fof(f247,plain,(
% 125.17/16.16 ![Vx,VC,VT]: ((~vlookup(Vx,VC)=vnoType|~vtcheck(VC,ve1app,VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),ve1app,VT)))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f246])).
% 125.17/16.16 fof(f248,plain,(
% 125.17/16.16 ![X0,X1,X2,X3]: (~vlookup(X0,X1)=vnoType|~vtcheck(X1,ve1app,X2)|vtcheck(vbind(X0,X3,X1),ve1app,X2))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f247])).
% 125.17/16.16 fof(f249,plain,(
% 125.17/16.16 ![Vx,VS,VC,VT]: ((~vlookup(Vx,VC)=vnoType|~vtcheck(VC,ve2app,VT))|vtcheck(vbind(Vx,VS,VC),ve2app,VT))),
% 125.17/16.16 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 125.17/16.16 fof(f250,plain,(
% 125.17/16.16 ![Vx,VC,VT]: ((~vlookup(Vx,VC)=vnoType|~vtcheck(VC,ve2app,VT))|(![VS]: vtcheck(vbind(Vx,VS,VC),ve2app,VT)))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f249])).
% 125.17/16.16 fof(f251,plain,(
% 125.17/16.16 ![X0,X1,X2,X3]: (~vlookup(X0,X1)=vnoType|~vtcheck(X1,ve2app,X2)|vtcheck(vbind(X0,X3,X1),ve2app,X2))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f250])).
% 125.17/16.16 fof(f252,plain,(
% 125.17/16.16 (?[Vx,VS,VC,VT]: ((vlookup(Vx,VC)=vnoType&vtcheck(VC,vapp(ve1app,ve2app),VT))&~vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT)))),
% 125.17/16.16 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 125.17/16.16 fof(f253,plain,(
% 125.17/16.16 ?[Vx,VC,VT]: ((vlookup(Vx,VC)=vnoType&vtcheck(VC,vapp(ve1app,ve2app),VT))&(?[VS]: ~vtcheck(vbind(Vx,VS,VC),vapp(ve1app,ve2app),VT)))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f252])).
% 125.17/16.16 fof(f254,plain,(
% 125.17/16.16 ((vlookup(sK21_skl,sK22_skl)=vnoType&vtcheck(sK22_skl,vapp(ve1app,ve2app),sK23_skl))&~vtcheck(vbind(sK21_skl,sK24_skl,sK22_skl),vapp(ve1app,ve2app),sK23_skl))),
% 125.17/16.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(Vx,sK21_skl),skolemize(VC,sK22_skl),skolemize(VT,sK23_skl),skolemize(VS,sK24_skl)],[f253])).
% 125.17/16.16 fof(f255,plain,(
% 125.17/16.16 vlookup(sK21_skl,sK22_skl)=vnoType),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f254])).
% 125.17/16.16 fof(f256,plain,(
% 125.17/16.16 vtcheck(sK22_skl,vapp(ve1app,ve2app),sK23_skl)),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f254])).
% 125.17/16.16 fof(f257,plain,(
% 125.17/16.16 ~vtcheck(vbind(sK21_skl,sK24_skl,sK22_skl),vapp(ve1app,ve2app),sK23_skl)),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f254])).
% 125.17/16.16 fof(f295,definition,(
% 125.17/16.16 ![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)<=>(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))),
% 125.17/16.16 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 125.17/16.16 fof(f296,plain,(
% 125.17/16.16 ![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)<=>((?[Vx]: sP7_prd(Vx,VC,VT,Ve))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)))))),
% 125.17/16.16 inference(formula_renaming,[status(thm)],[f239,f295])).
% 125.17/16.16 fof(f297,plain,(
% 125.17/16.16 ![Ve,VT,VC]: ((~sP3_prd(VC,VT,Ve)|((?[Vx]: sP7_prd(Vx,VC,VT,Ve))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2)))))&(sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 125.17/16.16 inference(NNF_transformation,[status(thm)],[f296])).
% 125.17/16.16 fof(f298,plain,(
% 125.17/16.16 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|((?[Vx]: sP7_prd(Vx,VC,VT,Ve))|(?[Vx,Ve2,VT1,VT2]: ((Ve=vabs(Vx,VT1,Ve2)&VT=varrow(VT1,VT2))&vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))&(![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f297])).
% 125.17/16.16 fof(f299,plain,(
% 125.17/16.16 (![Ve,VT,VC]: (~sP3_prd(VC,VT,Ve)|(sP7_prd(sK42_skl(VC,VT,Ve),VC,VT,Ve)|((Ve=vabs(sK43_skl(VC,VT,Ve),sK45_skl(VC,VT,Ve),sK44_skl(VC,VT,Ve))&VT=varrow(sK45_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve)))&vtcheck(vbind(sK43_skl(VC,VT,Ve),sK45_skl(VC,VT,Ve),VC),sK44_skl(VC,VT,Ve),sK46_skl(VC,VT,Ve))))))&(![Ve,VT,VC]: (sP3_prd(VC,VT,Ve)|((![Vx]: ~sP7_prd(Vx,VC,VT,Ve))&(![Vx,Ve2,VT1,VT2]: ((~Ve=vabs(Vx,VT1,Ve2)|~VT=varrow(VT1,VT2))|~vtcheck(vbind(Vx,VT1,VC),Ve2,VT2))))))),
% 125.17/16.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK42_skl,sK43_skl,sK44_skl,sK45_skl,sK46_skl]),skolemize(Vx,sK42_skl(VC,VT,Ve)),skolemize(Vx,sK43_skl(VC,VT,Ve)),skolemize(Ve2,sK44_skl(VC,VT,Ve)),skolemize(VT1,sK45_skl(VC,VT,Ve)),skolemize(VT2,sK46_skl(VC,VT,Ve))],[f298])).
% 125.17/16.16 fof(f300,plain,(
% 125.17/16.16 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|sP7_prd(sK42_skl(X0,X1,X2),X0,X1,X2)|X2=vabs(sK43_skl(X0,X1,X2),sK45_skl(X0,X1,X2),sK44_skl(X0,X1,X2)))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f299])).
% 125.17/16.16 fof(f335,plain,(
% 125.17/16.16 ![Ve,VT,VC,Vx]: ((~sP7_prd(Vx,VC,VT,Ve)|(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT)))&(sP7_prd(Vx,VC,VT,Ve)|(~Ve=vvar(Vx)|~vlookup(Vx,VC)=vsomeType(VT))))),
% 125.17/16.16 inference(NNF_transformation,[status(thm)],[f295])).
% 125.17/16.16 fof(f336,plain,(
% 125.17/16.16 (![Ve,VT,VC,Vx]: (~sP7_prd(Vx,VC,VT,Ve)|(Ve=vvar(Vx)&vlookup(Vx,VC)=vsomeType(VT))))&(![Ve,VT,VC,Vx]: (sP7_prd(Vx,VC,VT,Ve)|(~Ve=vvar(Vx)|~vlookup(Vx,VC)=vsomeType(VT))))),
% 125.17/16.16 inference(miniscoping,[status(thm)],[f335])).
% 125.17/16.16 fof(f337,plain,(
% 125.17/16.16 ![X0,X1,X2,X3]: (~sP7_prd(X0,X1,X2,X3)|X3=vvar(X0))),
% 125.17/16.16 inference(cnf_transformation,[status(thm)],[f336])).
% 125.17/16.16 fof(f484,plain,(
% 125.17/16.16 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 125.17/16.16 inference(resolution,[status(thm)],[f243,f256])).
% 125.17/16.16 fof(f500,plain,(
% 125.17/16.16 sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vabs(sK43_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK45_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK44_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 125.17/16.16 inference(resolution,[status(thm)],[f300,f484])).
% 125.17/16.16 fof(f502,plain,(
% 125.17/16.16 sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 125.17/16.16 inference(forward_subsumption_resolution,[status(thm)],[f500,f76])).
% 125.17/16.16 fof(f546,plain,(
% 125.17/16.16 vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|vapp(ve1app,ve2app)=vvar(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 125.17/16.16 inference(resolution,[status(thm)],[f502,f337])).
% 125.17/16.16 fof(f549,plain,(
% 125.17/16.16 vapp(ve1app,ve2app)=vapp(sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 125.17/16.16 inference(forward_subsumption_resolution,[status(thm)],[f546,f75])).
% 125.17/16.16 fof(f556,plain,(
% 125.17/16.16 ve2app=sK18_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))),
% 125.17/16.16 inference(resolution,[status(thm)],[f549,f72])).
% 86.86/16.24 fof(f557,plain,(
% 86.86/16.24 ve1app=sK20_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))),
% 86.86/16.24 inference(resolution,[status(thm)],[f549,f71])).
% 86.86/16.24 fof(f2941,plain,(
% 86.86/16.24 ~vtcheck(sK22_skl,vapp(ve1app,ve2app),sK23_skl)|sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vtcheck(sK22_skl,ve1app,varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl))),
% 86.86/16.24 inference(paramodulation,[status(thm)],[f557,f244])).
% 86.86/16.24 fof(f2942,plain,(
% 86.86/16.24 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vtcheck(sK22_skl,ve1app,varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl))),
% 86.86/16.24 inference(forward_subsumption_resolution,[status(thm)],[f2941,f256])).
% 86.86/16.24 fof(f2952,plain,(
% 86.86/16.24 ~vtcheck(sK22_skl,vapp(ve1app,ve2app),sK23_skl)|sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vtcheck(sK22_skl,ve2app,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 86.86/16.24 inference(paramodulation,[status(thm)],[f556,f245])).
% 86.86/16.24 fof(f2953,plain,(
% 86.86/16.24 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vtcheck(sK22_skl,ve2app,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 86.86/16.24 inference(forward_subsumption_resolution,[status(thm)],[f2952,f256])).
% 86.86/16.24 fof(f2954,plain,(
% 86.86/16.24 ![X0,X1]: (sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(X0,sK22_skl)=vnoType|vtcheck(vbind(X0,X1,sK22_skl),ve2app,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app))))),
% 86.86/16.24 inference(resolution,[status(thm)],[f2953,f251])).
% 86.86/16.24 fof(f2956,plain,(
% 86.86/16.24 ![X0,X1]: (sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(X0,sK22_skl)=vnoType|vtcheck(vbind(X0,X1,sK22_skl),ve1app,varrow(sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK23_skl)))),
% 86.86/16.24 inference(resolution,[status(thm)],[f2942,f248])).
% 86.86/16.24 fof(f3634,plain,(
% 86.86/16.24 ![X0,X1,X2]: (sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(X0,sK22_skl)=vnoType|~vtcheck(vbind(X0,X1,sK22_skl),X2,sK19_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))|vtcheck(vbind(X0,X1,sK22_skl),vapp(ve1app,X2),sK23_skl))),
% 86.86/16.24 inference(resolution,[status(thm)],[f2956,f237])).
% 86.86/16.24 fof(f6093,plain,(
% 86.86/16.24 ![X0,X1]: (sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(X0,sK22_skl)=vnoType|vtcheck(vbind(X0,X1,sK22_skl),vapp(ve1app,ve2app),sK23_skl)|sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(X0,sK22_skl)=vnoType)),
% 86.86/16.24 inference(resolution,[status(thm)],[f3634,f2954])).
% 86.86/16.24 fof(f6104,plain,(
% 86.86/16.24 ![X0,X1]: (sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(X0,sK22_skl)=vnoType|vtcheck(vbind(X0,X1,sK22_skl),vapp(ve1app,ve2app),sK23_skl))),
% 86.86/16.24 inference(duplicate_literals_removal,[status(thm)],[f6093])).
% 86.86/16.24 fof(f6109,plain,(
% 86.86/16.24 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vlookup(sK21_skl,sK22_skl)=vnoType),
% 86.86/16.24 inference(resolution,[status(thm)],[f6104,f257])).
% 86.86/16.24 fof(f6113,plain,(
% 86.86/16.24 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))|~vnoType=vnoType),
% 86.86/16.24 inference(forward_demodulation,[status(thm)],[f255,f6109])).
% 86.86/16.24 fof(f6114,plain,(
% 86.86/16.24 sP3_prd(sK22_skl,sK23_skl,vapp(ve1app,ve2app))),
% 86.86/16.24 inference(trivial_equality_resolution,[status(thm)],[f6113])).
% 86.86/16.24 fof(f6115,plain,(
% 86.86/16.24 sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app))|vapp(ve1app,ve2app)=vabs(sK43_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK45_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK44_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 86.86/16.24 inference(resolution,[status(thm)],[f6114,f300])).
% 86.86/16.24 fof(f6116,plain,(
% 86.86/16.24 sP7_prd(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)),sK22_skl,sK23_skl,vapp(ve1app,ve2app))),
% 86.86/16.24 inference(forward_subsumption_resolution,[status(thm)],[f6115,f76])).
% 86.86/16.24 fof(f6118,plain,(
% 86.86/16.24 vapp(ve1app,ve2app)=vvar(sK42_skl(sK22_skl,sK23_skl,vapp(ve1app,ve2app)))),
% 86.86/16.24 inference(resolution,[status(thm)],[f6116,f337])).
% 86.86/16.24 fof(f6119,plain,(
% 86.86/16.24 $false),
% 86.86/16.24 inference(forward_subsumption_resolution,[status(thm)],[f6118,f75])).
% 86.86/16.24 % SZS output end CNFRefutation for theBenchmark.p
% 23.85/16.30 % Elapsed time: 15.986133 seconds
% 23.85/16.30 % CPU time: 126.664323 seconds
% 23.85/16.30 % Total memory used: 979.501 MB
% 23.85/16.30 % Net memory used: 901.161 MB
%------------------------------------------------------------------------------