%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HAL004+1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:45:13 PM UTC 2026
% Result : Theorem 27.46s 3.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HAL004+1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n008.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 20 20:45:24 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.43 % Drodi V4.1.1
% 27.46/3.98 % Refutation found
% 27.46/3.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.46/3.98 % SZS output start CNFRefutation for theBenchmark
% 27.46/3.98 fof(f1,axiom,(
% 27.46/3.98 (! [Morphism,Dom,Cod] :( morphism(Morphism,Dom,Cod)=> ( (! [El] :( element(El,Dom)=> element(apply(Morphism,El),Cod) ))& apply(Morphism,zero(Dom)) = zero(Cod) ) ) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f4,axiom,(
% 27.46/3.98 (! [Morphism,Dom,Cod] :( ( surjection(Morphism)& morphism(Morphism,Dom,Cod) )=> (! [ElCod] :( element(ElCod,Cod)=> (? [ElDom] :( element(ElDom,Dom)& apply(Morphism,ElDom) = ElCod ) )) )) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f8,axiom,(
% 27.46/3.98 (! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] :( ( commute(M1,M2,M3,M4)& morphism(M1,Dom,DomCod1)& morphism(M2,DomCod1,Cod)& morphism(M3,Dom,DomCod2)& morphism(M4,DomCod2,Cod) )=> (! [ElDom] :( element(ElDom,Dom)=> apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom)) ) )) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f10,axiom,(
% 27.46/3.98 (! [Dom,El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> element(subtract(Dom,El1,El2),Dom) ) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f11,axiom,(
% 27.46/3.98 (! [Dom,El] :( element(El,Dom)=> subtract(Dom,El,El) = zero(Dom) ) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f12,axiom,(
% 27.46/3.98 (! [Dom,El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> subtract(Dom,El1,subtract(Dom,El1,El2)) = El2 ) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f13,axiom,(
% 27.46/3.98 (! [Morphism,Dom,Cod] :( morphism(Morphism,Dom,Cod)=> (! [El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> apply(Morphism,subtract(Dom,El1,El2)) = subtract(Cod,apply(Morphism,El1),apply(Morphism,El2)) ) )) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f15,axiom,(
% 27.46/3.98 morphism(beta,b,c) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f17,axiom,(
% 27.46/3.98 morphism(delta,e,r) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f19,axiom,(
% 27.46/3.98 morphism(g,b,e) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f20,axiom,(
% 27.46/3.98 morphism(h,c,r) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f23,axiom,(
% 27.46/3.98 surjection(beta) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f28,axiom,(
% 27.46/3.98 commute(beta,h,g,delta) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f30,hypothesis,(
% 27.46/3.98 surjection(h) ),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f31,conjecture,(
% 27.46/3.98 (! [E] :( element(E,e)=> (? [R,B1] :( element(R,r)& apply(delta,E) = R& element(B1,b)& apply(h,apply(beta,B1)) = R& apply(delta,apply(g,B1)) = R ) )) )),
% 27.46/3.98 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.46/3.98 fof(f32,negated_conjecture,(
% 27.46/3.98 ~((! [E] :( element(E,e)=> (? [R,B1] :( element(R,r)& apply(delta,E) = R& element(B1,b)& apply(h,apply(beta,B1)) = R& apply(delta,apply(g,B1)) = R ) )) ))),
% 27.46/3.98 inference(negated_conjecture,[status(cth)],[f31])).
% 27.46/3.98 fof(f33,plain,(
% 27.46/3.98 ![Morphism,Dom,Cod]: (~morphism(Morphism,Dom,Cod)|((![El]: (~element(El,Dom)|element(apply(Morphism,El),Cod)))&apply(Morphism,zero(Dom))=zero(Cod)))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 27.46/3.98 fof(f34,plain,(
% 27.46/3.98 ![X0,X1,X2,X3]: (~morphism(X0,X1,X2)|~element(X3,X1)|element(apply(X0,X3),X2))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f33])).
% 27.46/3.98 fof(f35,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~morphism(X0,X1,X2)|apply(X0,zero(X1))=zero(X2))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f33])).
% 27.46/3.98 fof(f46,plain,(
% 27.46/3.98 ![Morphism,Dom,Cod]: ((~surjection(Morphism)|~morphism(Morphism,Dom,Cod))|(![ElCod]: (~element(ElCod,Cod)|(?[ElDom]: (element(ElDom,Dom)&apply(Morphism,ElDom)=ElCod)))))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 27.46/3.98 fof(f47,plain,(
% 27.46/3.98 ![Morphism,Dom,Cod]: ((~surjection(Morphism)|~morphism(Morphism,Dom,Cod))|(![ElCod]: (~element(ElCod,Cod)|(element(sK2_skl(ElCod,Cod,Dom,Morphism),Dom)&apply(Morphism,sK2_skl(ElCod,Cod,Dom,Morphism))=ElCod))))),
% 27.46/3.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(ElDom,sK2_skl(ElCod,Cod,Dom,Morphism))],[f46])).
% 27.46/3.98 fof(f48,plain,(
% 27.46/3.98 ![X0,X1,X2,X3]: (~surjection(X0)|~morphism(X0,X1,X2)|~element(X3,X2)|element(sK2_skl(X3,X2,X1,X0),X1))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f47])).
% 27.46/3.98 fof(f49,plain,(
% 27.46/3.98 ![X0,X1,X2,X3]: (~surjection(X0)|~morphism(X0,X1,X2)|~element(X3,X2)|apply(X0,sK2_skl(X3,X2,X1,X0))=X3)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f47])).
% 27.46/3.98 fof(f72,plain,(
% 27.46/3.98 ![M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod]: (((((~commute(M1,M2,M3,M4)|~morphism(M1,Dom,DomCod1))|~morphism(M2,DomCod1,Cod))|~morphism(M3,Dom,DomCod2))|~morphism(M4,DomCod2,Cod))|(![ElDom]: (~element(ElDom,Dom)|apply(M2,apply(M1,ElDom))=apply(M4,apply(M3,ElDom)))))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 27.46/3.98 fof(f73,plain,(
% 27.46/3.98 ![M1,M2,M3,M4,Dom]: ((![DomCod2,Cod]: (((![DomCod1]: ((~commute(M1,M2,M3,M4)|~morphism(M1,Dom,DomCod1))|~morphism(M2,DomCod1,Cod)))|~morphism(M3,Dom,DomCod2))|~morphism(M4,DomCod2,Cod)))|(![ElDom]: (~element(ElDom,Dom)|apply(M2,apply(M1,ElDom))=apply(M4,apply(M3,ElDom)))))),
% 27.46/3.98 inference(miniscoping,[status(thm)],[f72])).
% 27.46/3.98 fof(f74,plain,(
% 27.46/3.98 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~commute(X0,X1,X2,X3)|~morphism(X0,X4,X5)|~morphism(X1,X5,X6)|~morphism(X2,X4,X7)|~morphism(X3,X7,X6)|~element(X8,X4)|apply(X1,apply(X0,X8))=apply(X3,apply(X2,X8)))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f73])).
% 27.46/3.98 fof(f80,plain,(
% 27.46/3.98 ![Dom,El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|element(subtract(Dom,El1,El2),Dom))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 27.46/3.98 fof(f81,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~element(X0,X1)|~element(X2,X1)|element(subtract(X1,X0,X2),X1))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f80])).
% 27.46/3.98 fof(f82,plain,(
% 27.46/3.98 ![Dom,El]: (~element(El,Dom)|subtract(Dom,El,El)=zero(Dom))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 27.46/3.98 fof(f83,plain,(
% 27.46/3.98 ![X0,X1]: (~element(X0,X1)|subtract(X1,X0,X0)=zero(X1))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f82])).
% 27.46/3.98 fof(f84,plain,(
% 27.46/3.98 ![Dom,El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|subtract(Dom,El1,subtract(Dom,El1,El2))=El2)),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 27.46/3.98 fof(f85,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~element(X0,X1)|~element(X2,X1)|subtract(X1,X0,subtract(X1,X0,X2))=X2)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f84])).
% 27.46/3.98 fof(f86,plain,(
% 27.46/3.98 ![Morphism,Dom,Cod]: (~morphism(Morphism,Dom,Cod)|(![El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|apply(Morphism,subtract(Dom,El1,El2))=subtract(Cod,apply(Morphism,El1),apply(Morphism,El2)))))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 27.46/3.98 fof(f87,plain,(
% 27.46/3.98 ![X0,X1,X2,X3,X4]: (~morphism(X0,X1,X2)|~element(X3,X1)|~element(X4,X1)|apply(X0,subtract(X1,X3,X4))=subtract(X2,apply(X0,X3),apply(X0,X4)))),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f86])).
% 27.46/3.98 fof(f89,plain,(
% 27.46/3.98 morphism(beta,b,c)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f15])).
% 27.46/3.98 fof(f91,plain,(
% 27.46/3.98 morphism(delta,e,r)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f17])).
% 27.46/3.98 fof(f93,plain,(
% 27.46/3.98 morphism(g,b,e)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f19])).
% 27.46/3.98 fof(f94,plain,(
% 27.46/3.98 morphism(h,c,r)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f20])).
% 27.46/3.98 fof(f97,plain,(
% 27.46/3.98 surjection(beta)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f23])).
% 27.46/3.98 fof(f102,plain,(
% 27.46/3.98 commute(beta,h,g,delta)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f28])).
% 27.46/3.98 fof(f104,plain,(
% 27.46/3.98 surjection(h)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f30])).
% 27.46/3.98 fof(f105,plain,(
% 27.46/3.98 (?[E]: (element(E,e)&(![R,B1]: ((((~element(R,r)|~apply(delta,E)=R)|~element(B1,b))|~apply(h,apply(beta,B1))=R)|~apply(delta,apply(g,B1))=R))))),
% 27.46/3.98 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 27.46/3.98 fof(f106,plain,(
% 27.46/3.98 (element(sK8_skl,e)&(![R,B1]: ((((~element(R,r)|~apply(delta,sK8_skl)=R)|~element(B1,b))|~apply(h,apply(beta,B1))=R)|~apply(delta,apply(g,B1))=R)))),
% 27.46/3.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(E,sK8_skl)],[f105])).
% 27.46/3.98 fof(f107,plain,(
% 27.46/3.98 element(sK8_skl,e)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f106])).
% 27.46/3.98 fof(f108,plain,(
% 27.46/3.98 ![X0,X1]: (~element(X0,r)|~apply(delta,sK8_skl)=X0|~element(X1,b)|~apply(h,apply(beta,X1))=X0|~apply(delta,apply(g,X1))=X0)),
% 27.46/3.98 inference(cnf_transformation,[status(thm)],[f106])).
% 27.46/3.98 fof(f114,plain,(
% 27.46/3.98 ![X0]: (~element(X0,e)|element(apply(delta,X0),r))),
% 27.46/3.98 inference(resolution,[status(thm)],[f91,f34])).
% 27.46/3.98 fof(f116,plain,(
% 27.46/3.98 ![X0,X1]: (~element(X0,e)|~apply(delta,sK8_skl)=apply(delta,X0)|~element(X1,b)|~apply(h,apply(beta,X1))=apply(delta,X0)|~apply(delta,apply(g,X1))=apply(delta,X0))),
% 27.46/3.98 inference(resolution,[status(thm)],[f114,f108])).
% 27.46/3.98 fof(f118,plain,(
% 27.46/3.98 apply(delta,zero(e))=zero(r)),
% 27.46/3.98 inference(resolution,[status(thm)],[f35,f91])).
% 27.46/3.98 fof(f120,plain,(
% 27.46/3.98 ~element(zero(e),e)|element(zero(r),r)),
% 27.46/3.98 inference(paramodulation,[status(thm)],[f118,f114])).
% 27.46/3.98 fof(f133,plain,(
% 27.46/3.98 ![X0]: (subtract(r,apply(delta,X0),apply(delta,X0))=zero(r)|~element(X0,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f83,f114])).
% 27.46/3.98 fof(f134,plain,(
% 27.46/3.98 subtract(e,sK8_skl,sK8_skl)=zero(e)),
% 27.46/3.98 inference(resolution,[status(thm)],[f83,f107])).
% 27.46/3.98 fof(f136,plain,(
% 27.46/3.98 subtract(r,apply(delta,sK8_skl),apply(delta,sK8_skl))=zero(r)),
% 27.46/3.98 inference(resolution,[status(thm)],[f133,f107])).
% 27.46/3.98 fof(f193,plain,(
% 27.46/3.98 ~element(sK8_skl,e)|~element(sK8_skl,e)|element(zero(e),e)),
% 27.46/3.98 inference(paramodulation,[status(thm)],[f134,f81])).
% 27.46/3.98 fof(f195,plain,(
% 27.46/3.98 ~element(sK8_skl,e)|element(zero(e),e)),
% 27.46/3.98 inference(duplicate_literals_removal,[status(thm)],[f193])).
% 27.46/3.98 fof(f196,plain,(
% 27.46/3.98 element(zero(r),r)),
% 27.46/3.98 inference(backward_subsumption_resolution,[status(thm)],[f120,f197])).
% 27.46/3.98 fof(f197,plain,(
% 27.46/3.98 element(zero(e),e)),
% 27.46/3.98 inference(forward_subsumption_resolution,[status(thm)],[f195,f107])).
% 27.46/3.98 fof(f223,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~morphism(h,X0,X1)|~element(X2,X1)|element(sK2_skl(X2,X1,X0,h),X0))),
% 27.46/3.98 inference(resolution,[status(thm)],[f48,f104])).
% 27.46/3.98 fof(f225,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~morphism(beta,X0,X1)|~element(X2,X1)|element(sK2_skl(X2,X1,X0,beta),X0))),
% 27.46/3.98 inference(resolution,[status(thm)],[f48,f97])).
% 27.46/3.98 fof(f227,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~morphism(h,X0,X1)|~element(X2,X1)|apply(h,sK2_skl(X2,X1,X0,h))=X2)),
% 27.46/3.98 inference(resolution,[status(thm)],[f49,f104])).
% 27.46/3.98 fof(f229,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~morphism(beta,X0,X1)|~element(X2,X1)|apply(beta,sK2_skl(X2,X1,X0,beta))=X2)),
% 27.46/3.98 inference(resolution,[status(thm)],[f49,f97])).
% 27.46/3.98 fof(f261,plain,(
% 27.46/3.98 ![X0]: (~element(X0,r)|element(sK2_skl(X0,r,c,h),c))),
% 27.46/3.98 inference(resolution,[status(thm)],[f223,f94])).
% 27.46/3.98 fof(f273,plain,(
% 27.46/3.98 ![X0]: (~element(X0,c)|element(sK2_skl(X0,c,b,beta),b))),
% 27.46/3.98 inference(resolution,[status(thm)],[f225,f89])).
% 27.46/3.98 fof(f274,plain,(
% 27.46/3.98 ![X0]: (element(sK2_skl(sK2_skl(X0,r,c,h),c,b,beta),b)|~element(X0,r))),
% 27.46/3.98 inference(resolution,[status(thm)],[f273,f261])).
% 27.46/3.98 fof(f280,plain,(
% 27.46/3.98 ![X0,X1]: (element(sK2_skl(sK2_skl(subtract(r,X0,X1),r,c,h),c,b,beta),b)|~element(X0,r)|~element(X1,r))),
% 27.46/3.98 inference(resolution,[status(thm)],[f274,f81])).
% 27.46/3.98 fof(f323,plain,(
% 27.46/3.98 ![X0,X1]: (~element(X0,r)|subtract(r,X0,subtract(r,X0,apply(delta,X1)))=apply(delta,X1)|~element(X1,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f85,f114])).
% 27.46/3.98 fof(f338,plain,(
% 27.46/3.98 ![X0]: (subtract(r,zero(r),subtract(r,zero(r),apply(delta,X0)))=apply(delta,X0)|~element(X0,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f323,f196])).
% 27.46/3.98 fof(f343,plain,(
% 27.46/3.98 ![X0,X1]: (subtract(r,apply(delta,X0),subtract(r,apply(delta,X0),apply(delta,X1)))=apply(delta,X1)|~element(X1,e)|~element(X0,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f323,f114])).
% 27.46/3.98 fof(f353,plain,(
% 27.46/3.98 subtract(r,zero(r),subtract(r,zero(r),apply(delta,sK8_skl)))=apply(delta,sK8_skl)),
% 27.46/3.98 inference(resolution,[status(thm)],[f338,f107])).
% 27.46/3.98 fof(f375,plain,(
% 27.46/3.98 ![X0]: (element(sK2_skl(sK2_skl(subtract(r,X0,zero(r)),r,c,h),c,b,beta),b)|~element(X0,r))),
% 27.46/3.98 inference(resolution,[status(thm)],[f280,f196])).
% 27.46/3.98 fof(f479,plain,(
% 27.46/3.98 ![X0]: (subtract(r,apply(delta,X0),subtract(r,apply(delta,X0),apply(delta,sK8_skl)))=apply(delta,sK8_skl)|~element(X0,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f343,f107])).
% 27.46/3.98 fof(f491,plain,(
% 27.46/3.98 subtract(r,apply(delta,sK8_skl),subtract(r,apply(delta,sK8_skl),apply(delta,sK8_skl)))=apply(delta,sK8_skl)),
% 27.46/3.98 inference(resolution,[status(thm)],[f479,f107])).
% 27.46/3.98 fof(f494,plain,(
% 27.46/3.98 subtract(r,apply(delta,sK8_skl),zero(r))=apply(delta,sK8_skl)),
% 27.46/3.98 inference(forward_demodulation,[status(thm)],[f136,f491])).
% 27.46/3.98 fof(f497,plain,(
% 27.46/3.98 ![X0]: (~element(X0,r)|apply(h,sK2_skl(X0,r,c,h))=X0)),
% 27.46/3.98 inference(resolution,[status(thm)],[f227,f94])).
% 27.46/3.98 fof(f503,plain,(
% 27.46/3.98 ![X0]: (apply(h,sK2_skl(apply(delta,X0),r,c,h))=apply(delta,X0)|~element(X0,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f497,f114])).
% 27.46/3.98 fof(f513,plain,(
% 27.46/3.98 apply(h,sK2_skl(apply(delta,sK8_skl),r,c,h))=apply(delta,sK8_skl)),
% 27.46/3.98 inference(resolution,[status(thm)],[f503,f107])).
% 27.46/3.98 fof(f523,plain,(
% 27.46/3.98 ![X0]: (~element(X0,c)|apply(beta,sK2_skl(X0,c,b,beta))=X0)),
% 27.46/3.98 inference(resolution,[status(thm)],[f229,f89])).
% 27.46/3.98 fof(f597,plain,(
% 27.46/3.98 ![X0]: (apply(beta,sK2_skl(sK2_skl(X0,r,c,h),c,b,beta))=sK2_skl(X0,r,c,h)|~element(X0,r))),
% 27.46/3.98 inference(resolution,[status(thm)],[f523,f261])).
% 27.46/3.98 fof(f616,plain,(
% 27.46/3.98 ![X0]: (apply(beta,sK2_skl(sK2_skl(apply(delta,X0),r,c,h),c,b,beta))=sK2_skl(apply(delta,X0),r,c,h)|~element(X0,e))),
% 27.46/3.98 inference(resolution,[status(thm)],[f597,f114])).
% 27.46/3.98 fof(f841,plain,(
% 27.46/3.98 ![X0,X1,X2,X3,X4]: (~morphism(beta,X0,X1)|~morphism(h,X1,X2)|~morphism(g,X0,X3)|~morphism(delta,X3,X2)|~element(X4,X0)|apply(h,apply(beta,X4))=apply(delta,apply(g,X4)))),
% 27.46/3.98 inference(resolution,[status(thm)],[f74,f102])).
% 27.46/3.98 fof(f871,plain,(
% 27.46/3.98 ~element(zero(r),r)|~element(subtract(r,zero(r),apply(delta,sK8_skl)),r)|element(apply(delta,sK8_skl),r)),
% 27.46/3.98 inference(paramodulation,[status(thm)],[f353,f81])).
% 27.46/3.98 fof(f876,plain,(
% 27.46/3.98 ~element(subtract(r,zero(r),apply(delta,sK8_skl)),r)|element(apply(delta,sK8_skl),r)),
% 27.46/3.98 inference(forward_subsumption_resolution,[status(thm)],[f871,f196])).
% 27.46/3.98 fof(f939,plain,(
% 27.46/3.98 ![X0,X1,X2]: (~morphism(beta,b,X0)|~morphism(h,X0,X1)|~morphism(delta,e,X1)|~element(X2,b)|apply(h,apply(beta,X2))=apply(delta,apply(g,X2)))),
% 27.46/3.98 inference(resolution,[status(thm)],[f841,f93])).
% 27.46/3.98 fof(f1050,plain,(
% 27.46/3.98 ![X0,X1]: (~element(X0,e)|~element(X1,e)|apply(delta,subtract(e,X0,X1))=subtract(r,apply(delta,X0),apply(delta,X1)))),
% 27.46/3.98 inference(resolution,[status(thm)],[f87,f91])).
% 27.46/3.98 fof(f1106,plain,(
% 27.46/3.98 ![X0]: (~element(X0,e)|apply(delta,subtract(e,X0,sK8_skl))=subtract(r,apply(delta,X0),apply(delta,sK8_skl)))),
% 27.46/3.98 inference(resolution,[status(thm)],[f1050,f107])).
% 27.46/3.98 fof(f1125,plain,(
% 27.46/3.98 apply(delta,subtract(e,zero(e),sK8_skl))=subtract(r,apply(delta,zero(e)),apply(delta,sK8_skl))),
% 27.46/3.98 inference(resolution,[status(thm)],[f1106,f197])).
% 27.46/3.98 fof(f1132,plain,(
% 27.46/3.98 ~element(apply(delta,subtract(e,zero(e),sK8_skl)),r)|element(apply(delta,sK8_skl),r)),
% 27.46/3.98 inference(backward_demodulation,[status(thm)],[f1137,f876])).
% 27.46/3.98 fof(f1137,plain,(
% 27.46/3.98 apply(delta,subtract(e,zero(e),sK8_skl))=subtract(r,zero(r),apply(delta,sK8_skl))),
% 27.46/3.98 inference(forward_demodulation,[status(thm)],[f118,f1125])).
% 27.46/3.98 fof(f1422,plain,(
% 27.46/3.98 ~element(zero(r),r)|~element(apply(delta,sK8_skl),r)|element(apply(delta,subtract(e,zero(e),sK8_skl)),r)),
% 27.46/3.98 inference(paramodulation,[status(thm)],[f1137,f81])).
% 27.46/3.98 fof(f1423,plain,(
% 27.46/3.98 ~element(apply(delta,sK8_skl),r)|element(apply(delta,subtract(e,zero(e),sK8_skl)),r)),
% 27.46/3.98 inference(forward_subsumption_resolution,[status(thm)],[f1422,f196])).
% 27.46/3.98 fof(f1456,plain,(
% 27.46/3.98 apply(beta,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta))=sK2_skl(apply(delta,sK8_skl),r,c,h)),
% 27.46/3.98 inference(resolution,[status(thm)],[f616,f107])).
% 27.46/3.98 fof(f1459,plain,(
% 27.46/3.98 ![X0,X1]: (~morphism(beta,b,X0)|~morphism(h,X0,r)|~element(X1,b)|apply(h,apply(beta,X1))=apply(delta,apply(g,X1)))),
% 27.46/3.98 inference(resolution,[status(thm)],[f939,f91])).
% 27.46/3.98 fof(f1460,plain,(
% 27.46/3.98 ![X0]: (~morphism(beta,b,c)|~element(X0,b)|apply(h,apply(beta,X0))=apply(delta,apply(g,X0)))),
% 27.46/3.98 inference(resolution,[status(thm)],[f1459,f94])).
% 27.46/3.98 fof(f1461,plain,(
% 27.46/3.98 ![X0]: (~element(X0,b)|apply(h,apply(beta,X0))=apply(delta,apply(g,X0)))),
% 27.46/3.98 inference(forward_subsumption_resolution,[status(thm)],[f1460,f89])).
% 27.46/3.98 fof(f1638,plain,(
% 27.46/3.98 element(apply(delta,subtract(e,zero(e),sK8_skl)),r)|~element(sK8_skl,e)),
% 27.46/3.98 inference(resolution,[status(thm)],[f1423,f114])).
% 27.46/3.98 fof(f1639,plain,(
% 27.46/3.98 element(apply(delta,sK8_skl),r)),
% 27.46/3.98 inference(backward_subsumption_resolution,[status(thm)],[f1132,f1641])).
% 27.46/3.98 fof(f1641,plain,(
% 27.46/3.98 element(apply(delta,subtract(e,zero(e),sK8_skl)),r)),
% 27.46/3.98 inference(forward_subsumption_resolution,[status(thm)],[f1638,f107])).
% 27.46/4.04 fof(f1660,plain,(
% 27.46/4.04 element(sK2_skl(sK2_skl(subtract(r,apply(delta,sK8_skl),zero(r)),r,c,h),c,b,beta),b)),
% 27.46/4.04 inference(resolution,[status(thm)],[f1639,f375])).
% 27.46/4.04 fof(f1682,plain,(
% 27.46/4.04 element(sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta),b)),
% 27.46/4.04 inference(forward_demodulation,[status(thm)],[f494,f1660])).
% 27.46/4.04 fof(f1778,plain,(
% 27.46/4.04 apply(h,apply(beta,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))=apply(delta,apply(g,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))),
% 27.46/4.04 inference(resolution,[status(thm)],[f1682,f1461])).
% 27.46/4.04 fof(f1806,plain,(
% 27.46/4.04 ![X0]: (~element(X0,e)|~apply(delta,sK8_skl)=apply(delta,X0)|~apply(h,apply(beta,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))=apply(delta,X0)|~apply(delta,apply(g,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))=apply(delta,X0))),
% 27.46/4.04 inference(resolution,[status(thm)],[f1682,f116])).
% 27.46/4.04 fof(f1818,plain,(
% 27.46/4.04 apply(h,sK2_skl(apply(delta,sK8_skl),r,c,h))=apply(delta,apply(g,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))),
% 27.46/4.04 inference(forward_demodulation,[status(thm)],[f1456,f1778])).
% 27.46/4.04 fof(f1819,plain,(
% 27.46/4.04 apply(delta,sK8_skl)=apply(delta,apply(g,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))),
% 27.46/4.04 inference(forward_demodulation,[status(thm)],[f513,f1818])).
% 27.46/4.04 fof(f1851,plain,(
% 27.46/4.04 ![X0]: (~element(X0,e)|~apply(delta,sK8_skl)=apply(delta,X0)|~apply(h,sK2_skl(apply(delta,sK8_skl),r,c,h))=apply(delta,X0)|~apply(delta,apply(g,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))=apply(delta,X0))),
% 27.46/4.04 inference(forward_demodulation,[status(thm)],[f1456,f1806])).
% 27.46/4.04 fof(f1852,plain,(
% 27.46/4.04 ![X0]: (~element(X0,e)|~apply(delta,sK8_skl)=apply(delta,X0)|~apply(delta,sK8_skl)=apply(delta,X0)|~apply(delta,apply(g,sK2_skl(sK2_skl(apply(delta,sK8_skl),r,c,h),c,b,beta)))=apply(delta,X0))),
% 27.46/4.04 inference(forward_demodulation,[status(thm)],[f513,f1851])).
% 27.46/4.04 fof(f1853,plain,(
% 27.46/4.04 ![X0]: (~element(X0,e)|~apply(delta,sK8_skl)=apply(delta,X0)|~apply(delta,sK8_skl)=apply(delta,X0)|~apply(delta,sK8_skl)=apply(delta,X0))),
% 27.46/4.04 inference(forward_demodulation,[status(thm)],[f1819,f1852])).
% 27.46/4.04 fof(f1854,plain,(
% 27.46/4.04 ![X0]: (~element(X0,e)|~apply(delta,sK8_skl)=apply(delta,X0))),
% 27.46/4.04 inference(duplicate_literals_removal,[status(thm)],[f1853])).
% 27.46/4.04 fof(f1867,plain,(
% 27.46/4.04 ~apply(delta,sK8_skl)=apply(delta,sK8_skl)),
% 27.46/4.04 inference(resolution,[status(thm)],[f1854,f107])).
% 27.46/4.04 fof(f1869,plain,(
% 27.46/4.04 $false),
% 27.46/4.04 inference(trivial_equality_resolution,[status(thm)],[f1867])).
% 27.46/4.04 % SZS output end CNFRefutation for theBenchmark.p
% 2.17/4.09 % Elapsed time: 3.661922 seconds
% 2.17/4.09 % CPU time: 28.202804 seconds
% 2.17/4.09 % Total memory used: 320.822 MB
% 2.17/4.09 % Net memory used: 305.026 MB
%------------------------------------------------------------------------------