%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HAL001+2 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 138.90s 18.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HAL001+2 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n006.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Sun Sep 20 20:43:58 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 138.90/18.11 % Refutation found
% 138.90/18.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 138.90/18.11 % SZS output start CNFRefutation for theBenchmark
% 138.90/18.11 fof(f1,axiom,(
% 138.90/18.11 (! [Morphism,Dom,Cod] :( morphism(Morphism,Dom,Cod)=> ( (! [El] :( element(El,Dom)=> element(apply(Morphism,El),Cod) ))& apply(Morphism,zero(Dom)) = zero(Cod) ) ) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f2,axiom,(
% 138.90/18.11 (! [Morphism,Dom,Cod] :( ( injection(Morphism)& morphism(Morphism,Dom,Cod) )=> (! [El1,El2] :( ( element(El1,Dom)& element(El2,Dom)& apply(Morphism,El1) = apply(Morphism,El2) )=> El1 = El2 ) )) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f3,axiom,(
% 138.90/18.11 (! [Morphism,Dom,Cod] :( ( morphism(Morphism,Dom,Cod)& (! [El1,El2] :( ( element(El1,Dom)& element(El2,Dom)& apply(Morphism,El1) = apply(Morphism,El2) )=> El1 = El2 ) ))=> injection(Morphism) ) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f6,axiom,(
% 138.90/18.11 (! [Morphism1,Morphism2,Dom,CodDom,Cod] :( ( exact(Morphism1,Morphism2)& morphism(Morphism1,Dom,CodDom)& morphism(Morphism2,CodDom,Cod) )=> (! [ElCodDom] :( ( element(ElCodDom,CodDom)& apply(Morphism2,ElCodDom) = zero(Cod) )<=> (? [ElDom] :( element(ElDom,Dom)& apply(Morphism1,ElDom) = ElCodDom ) )) )) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f8,axiom,(
% 138.90/18.11 (! [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)) ) )) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f10,axiom,(
% 138.90/18.11 (! [Dom,El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> element(subtract(Dom,El1,El2),Dom) ) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f11,axiom,(
% 138.90/18.11 (! [Dom,El] :( element(El,Dom)=> subtract(Dom,El,El) = zero(Dom) ) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f12,axiom,(
% 138.90/18.11 (! [Dom,El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> subtract(Dom,El1,subtract(Dom,El1,El2)) = El2 ) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f13,axiom,(
% 138.90/18.11 (! [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)) ) )) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f14,axiom,(
% 138.90/18.11 (! [Morphism,Dom,Cod] :( ( injection(Morphism)& morphism(Morphism,Dom,Cod) )=> (! [El] :( ( element(El,Dom)& apply(Morphism,El) = zero(Cod) )=> El = zero(Dom) ) )) )),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f16,axiom,(
% 138.90/18.11 morphism(alpha,a,b) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f17,axiom,(
% 138.90/18.11 morphism(beta,b,c) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f18,axiom,(
% 138.90/18.11 morphism(gamma,d,e) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f19,axiom,(
% 138.90/18.11 morphism(delta,e,r) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f20,axiom,(
% 138.90/18.11 morphism(f,a,d) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f21,axiom,(
% 138.90/18.11 morphism(g,b,e) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f22,axiom,(
% 138.90/18.11 morphism(h,c,r) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f24,axiom,(
% 138.90/18.11 injection(gamma) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f26,axiom,(
% 138.90/18.11 surjection(delta) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f27,axiom,(
% 138.90/18.11 exact(alpha,beta) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f29,axiom,(
% 138.90/18.11 commute(alpha,g,f,gamma) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f30,axiom,(
% 138.90/18.11 commute(beta,h,g,delta) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f31,hypothesis,(
% 138.90/18.11 injection(f) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f32,hypothesis,(
% 138.90/18.11 injection(h) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f33,conjecture,(
% 138.90/18.11 injection(g) ),
% 138.90/18.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 138.90/18.11 fof(f34,negated_conjecture,(
% 138.90/18.11 ~(injection(g) )),
% 138.90/18.11 inference(negated_conjecture,[status(cth)],[f33])).
% 138.90/18.11 fof(f35,plain,(
% 138.90/18.11 ![Morphism,Dom,Cod]: (~morphism(Morphism,Dom,Cod)|((![El]: (~element(El,Dom)|element(apply(Morphism,El),Cod)))&apply(Morphism,zero(Dom))=zero(Cod)))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 138.90/18.11 fof(f36,plain,(
% 138.90/18.11 ![X0,X1,X2,X3]: (~morphism(X0,X1,X2)|~element(X3,X1)|element(apply(X0,X3),X2))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f35])).
% 138.90/18.11 fof(f37,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(X0,X1,X2)|apply(X0,zero(X1))=zero(X2))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f35])).
% 138.90/18.11 fof(f38,plain,(
% 138.90/18.11 ![Morphism,Dom,Cod]: ((~injection(Morphism)|~morphism(Morphism,Dom,Cod))|(![El1,El2]: (((~element(El1,Dom)|~element(El2,Dom))|~apply(Morphism,El1)=apply(Morphism,El2))|El1=El2)))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 138.90/18.11 fof(f39,plain,(
% 138.90/18.11 ![Morphism,Dom]: ((~injection(Morphism)|(![Cod]: ~morphism(Morphism,Dom,Cod)))|(![El1,El2]: (((~element(El1,Dom)|~element(El2,Dom))|~apply(Morphism,El1)=apply(Morphism,El2))|El1=El2)))),
% 138.90/18.11 inference(miniscoping,[status(thm)],[f38])).
% 138.90/18.11 fof(f40,plain,(
% 138.90/18.11 ![X0,X1,X2,X3,X4]: (~injection(X0)|~morphism(X0,X1,X2)|~element(X3,X1)|~element(X4,X1)|~apply(X0,X3)=apply(X0,X4)|X3=X4)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f39])).
% 138.90/18.11 fof(f41,plain,(
% 138.90/18.11 ![Morphism,Dom,Cod]: ((~morphism(Morphism,Dom,Cod)|(?[El1,El2]: (((element(El1,Dom)&element(El2,Dom))&apply(Morphism,El1)=apply(Morphism,El2))&~El1=El2)))|injection(Morphism))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 138.90/18.11 fof(f42,plain,(
% 138.90/18.11 ![Morphism]: ((![Dom]: ((![Cod]: ~morphism(Morphism,Dom,Cod))|(?[El1,El2]: (((element(El1,Dom)&element(El2,Dom))&apply(Morphism,El1)=apply(Morphism,El2))&~El1=El2))))|injection(Morphism))),
% 138.90/18.11 inference(miniscoping,[status(thm)],[f41])).
% 138.90/18.11 fof(f43,plain,(
% 138.90/18.11 ![Morphism]: ((![Dom]: ((![Cod]: ~morphism(Morphism,Dom,Cod))|(((element(sK0_skl(Dom,Morphism),Dom)&element(sK1_skl(Dom,Morphism),Dom))&apply(Morphism,sK0_skl(Dom,Morphism))=apply(Morphism,sK1_skl(Dom,Morphism)))&~sK0_skl(Dom,Morphism)=sK1_skl(Dom,Morphism))))|injection(Morphism))),
% 138.90/18.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(El1,sK0_skl(Dom,Morphism)),skolemize(El2,sK1_skl(Dom,Morphism))],[f42])).
% 138.90/18.11 fof(f44,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(X0,X1,X2)|element(sK0_skl(X1,X0),X1)|injection(X0))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f43])).
% 138.90/18.11 fof(f45,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(X0,X1,X2)|element(sK1_skl(X1,X0),X1)|injection(X0))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f43])).
% 138.90/18.11 fof(f46,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(X0,X1,X2)|apply(X0,sK0_skl(X1,X0))=apply(X0,sK1_skl(X1,X0))|injection(X0))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f43])).
% 138.90/18.11 fof(f47,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(X0,X1,X2)|~sK0_skl(X1,X0)=sK1_skl(X1,X0)|injection(X0))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f43])).
% 138.90/18.11 fof(f57,plain,(
% 138.90/18.11 ![Morphism1,Morphism2,Dom,CodDom,Cod]: (((~exact(Morphism1,Morphism2)|~morphism(Morphism1,Dom,CodDom))|~morphism(Morphism2,CodDom,Cod))|(![ElCodDom]: ((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))<=>(?[ElDom]: (element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom)))))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 138.90/18.11 fof(f58,plain,(
% 138.90/18.11 ![Morphism1,Morphism2,Dom,CodDom,Cod]: (((~exact(Morphism1,Morphism2)|~morphism(Morphism1,Dom,CodDom))|~morphism(Morphism2,CodDom,Cod))|(![ElCodDom]: (((~element(ElCodDom,CodDom)|~apply(Morphism2,ElCodDom)=zero(Cod))|(?[ElDom]: (element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom)))&((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))|(![ElDom]: (~element(ElDom,Dom)|~apply(Morphism1,ElDom)=ElCodDom))))))),
% 138.90/18.11 inference(NNF_transformation,[status(thm)],[f57])).
% 138.90/18.11 fof(f59,plain,(
% 138.90/18.11 ![Morphism1,Morphism2,Dom,CodDom,Cod]: (((~exact(Morphism1,Morphism2)|~morphism(Morphism1,Dom,CodDom))|~morphism(Morphism2,CodDom,Cod))|((![ElCodDom]: ((~element(ElCodDom,CodDom)|~apply(Morphism2,ElCodDom)=zero(Cod))|(?[ElDom]: (element(ElDom,Dom)&apply(Morphism1,ElDom)=ElCodDom))))&(![ElCodDom]: ((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))|(![ElDom]: (~element(ElDom,Dom)|~apply(Morphism1,ElDom)=ElCodDom))))))),
% 138.90/18.11 inference(miniscoping,[status(thm)],[f58])).
% 138.90/18.11 fof(f60,plain,(
% 138.90/18.11 ![Morphism1,Morphism2,Dom,CodDom,Cod]: (((~exact(Morphism1,Morphism2)|~morphism(Morphism1,Dom,CodDom))|~morphism(Morphism2,CodDom,Cod))|((![ElCodDom]: ((~element(ElCodDom,CodDom)|~apply(Morphism2,ElCodDom)=zero(Cod))|(element(sK4_skl(ElCodDom,Cod,CodDom,Dom,Morphism2,Morphism1),Dom)&apply(Morphism1,sK4_skl(ElCodDom,Cod,CodDom,Dom,Morphism2,Morphism1))=ElCodDom)))&(![ElCodDom]: ((element(ElCodDom,CodDom)&apply(Morphism2,ElCodDom)=zero(Cod))|(![ElDom]: (~element(ElDom,Dom)|~apply(Morphism1,ElDom)=ElCodDom))))))),
% 138.90/18.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(ElDom,sK4_skl(ElCodDom,Cod,CodDom,Dom,Morphism2,Morphism1))],[f59])).
% 138.90/18.11 fof(f61,plain,(
% 138.90/18.11 ![X0,X1,X2,X3,X4,X5]: (~exact(X0,X1)|~morphism(X0,X2,X3)|~morphism(X1,X3,X4)|~element(X5,X3)|~apply(X1,X5)=zero(X4)|element(sK4_skl(X5,X4,X3,X2,X1,X0),X2))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f60])).
% 138.90/18.11 fof(f62,plain,(
% 138.90/18.11 ![X0,X1,X2,X3,X4,X5]: (~exact(X0,X1)|~morphism(X0,X2,X3)|~morphism(X1,X3,X4)|~element(X5,X3)|~apply(X1,X5)=zero(X4)|apply(X0,sK4_skl(X5,X4,X3,X2,X1,X0))=X5)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f60])).
% 138.90/18.11 fof(f74,plain,(
% 138.90/18.11 ![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)))))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 138.90/18.11 fof(f75,plain,(
% 138.90/18.11 ![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)))))),
% 138.90/18.11 inference(miniscoping,[status(thm)],[f74])).
% 138.90/18.11 fof(f76,plain,(
% 138.90/18.11 ![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)))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f75])).
% 138.90/18.11 fof(f82,plain,(
% 138.90/18.11 ![Dom,El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|element(subtract(Dom,El1,El2),Dom))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 138.90/18.11 fof(f83,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~element(X0,X1)|~element(X2,X1)|element(subtract(X1,X0,X2),X1))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f82])).
% 138.90/18.11 fof(f84,plain,(
% 138.90/18.11 ![Dom,El]: (~element(El,Dom)|subtract(Dom,El,El)=zero(Dom))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 138.90/18.11 fof(f85,plain,(
% 138.90/18.11 ![X0,X1]: (~element(X0,X1)|subtract(X1,X0,X0)=zero(X1))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f84])).
% 138.90/18.11 fof(f86,plain,(
% 138.90/18.11 ![Dom,El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|subtract(Dom,El1,subtract(Dom,El1,El2))=El2)),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 138.90/18.11 fof(f87,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~element(X0,X1)|~element(X2,X1)|subtract(X1,X0,subtract(X1,X0,X2))=X2)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f86])).
% 138.90/18.11 fof(f88,plain,(
% 138.90/18.11 ![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)))))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 138.90/18.11 fof(f89,plain,(
% 138.90/18.11 ![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)))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f88])).
% 138.90/18.11 fof(f90,plain,(
% 138.90/18.11 ![Morphism,Dom,Cod]: ((~injection(Morphism)|~morphism(Morphism,Dom,Cod))|(![El]: ((~element(El,Dom)|~apply(Morphism,El)=zero(Cod))|El=zero(Dom))))),
% 138.90/18.11 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 138.90/18.11 fof(f91,plain,(
% 138.90/18.11 ![X0,X1,X2,X3]: (~injection(X0)|~morphism(X0,X1,X2)|~element(X3,X1)|~apply(X0,X3)=zero(X2)|X3=zero(X1))),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f90])).
% 138.90/18.11 fof(f98,plain,(
% 138.90/18.11 morphism(alpha,a,b)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f16])).
% 138.90/18.11 fof(f99,plain,(
% 138.90/18.11 morphism(beta,b,c)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f17])).
% 138.90/18.11 fof(f100,plain,(
% 138.90/18.11 morphism(gamma,d,e)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f18])).
% 138.90/18.11 fof(f101,plain,(
% 138.90/18.11 morphism(delta,e,r)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f19])).
% 138.90/18.11 fof(f102,plain,(
% 138.90/18.11 morphism(f,a,d)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f20])).
% 138.90/18.11 fof(f103,plain,(
% 138.90/18.11 morphism(g,b,e)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f21])).
% 138.90/18.11 fof(f104,plain,(
% 138.90/18.11 morphism(h,c,r)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f22])).
% 138.90/18.11 fof(f106,plain,(
% 138.90/18.11 injection(gamma)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f24])).
% 138.90/18.11 fof(f108,plain,(
% 138.90/18.11 surjection(delta)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f26])).
% 138.90/18.11 fof(f109,plain,(
% 138.90/18.11 exact(alpha,beta)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f27])).
% 138.90/18.11 fof(f111,plain,(
% 138.90/18.11 commute(alpha,g,f,gamma)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f29])).
% 138.90/18.11 fof(f112,plain,(
% 138.90/18.11 commute(beta,h,g,delta)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f30])).
% 138.90/18.11 fof(f113,plain,(
% 138.90/18.11 injection(f)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f31])).
% 138.90/18.11 fof(f114,plain,(
% 138.90/18.11 injection(h)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f32])).
% 138.90/18.11 fof(f115,plain,(
% 138.90/18.11 ~injection(g)),
% 138.90/18.11 inference(cnf_transformation,[status(thm)],[f34])).
% 138.90/18.11 fof(f122,plain,(
% 138.90/18.11 ![X0,X1,X2,X3]: (~morphism(alpha,X0,X1)|~morphism(beta,X1,X2)|~element(X3,X1)|~apply(beta,X3)=zero(X2)|apply(alpha,sK4_skl(X3,X2,X1,X0,beta,alpha))=X3)),
% 138.90/18.11 inference(resolution,[status(thm)],[f109,f62])).
% 138.90/18.11 fof(f123,plain,(
% 138.90/18.11 ![X0,X1,X2,X3]: (~morphism(alpha,X0,X1)|~morphism(beta,X1,X2)|~element(X3,X1)|~apply(beta,X3)=zero(X2)|element(sK4_skl(X3,X2,X1,X0,beta,alpha),X0))),
% 138.90/18.11 inference(resolution,[status(thm)],[f109,f61])).
% 138.90/18.11 fof(f139,plain,(
% 138.90/18.11 apply(alpha,zero(a))=zero(b)),
% 138.90/18.11 inference(resolution,[status(thm)],[f98,f37])).
% 138.90/18.11 fof(f196,plain,(
% 138.90/18.11 apply(beta,zero(b))=zero(c)),
% 138.90/18.11 inference(resolution,[status(thm)],[f99,f37])).
% 138.90/18.11 fof(f197,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|element(apply(beta,X0),c))),
% 138.90/18.11 inference(resolution,[status(thm)],[f99,f36])).
% 138.90/18.11 fof(f245,plain,(
% 138.90/18.11 ![X0,X1]: (~element(X0,b)|~element(X1,b)|apply(beta,subtract(b,X0,X1))=subtract(c,apply(beta,X0),apply(beta,X1)))),
% 138.90/18.11 inference(resolution,[status(thm)],[f89,f99])).
% 138.90/18.11 fof(f257,plain,(
% 138.90/18.11 ![X0]: (~injection(gamma)|~element(X0,d)|~apply(gamma,X0)=zero(e)|X0=zero(d))),
% 138.90/18.11 inference(resolution,[status(thm)],[f100,f91])).
% 138.90/18.11 fof(f271,plain,(
% 138.90/18.11 apply(gamma,zero(d))=zero(e)),
% 138.90/18.11 inference(resolution,[status(thm)],[f100,f37])).
% 138.90/18.11 fof(f274,definition,(
% 138.90/18.11 sQ24_spl <=> (injection(gamma))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f276,plain,(
% 138.90/18.11 ~injection(gamma)|sQ24_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f274])).
% 138.90/18.11 fof(f277,definition,(
% 138.90/18.11 ![X0]: (sQ25_spl <=> (~element(X0,d)|~apply(gamma,X0)=zero(e)|X0=zero(d)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f278,plain,(
% 138.90/18.11 ![X0]: (~element(X0,d)|~apply(gamma,X0)=zero(e)|X0=zero(d)|~sQ25_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f277])).
% 138.90/18.11 fof(f280,plain,(
% 138.90/18.11 ~sQ24_spl|sQ25_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f257,f274,f277])).
% 138.90/18.11 fof(f320,plain,(
% 138.90/18.11 $false|sQ24_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f276,f106])).
% 138.90/18.11 fof(f321,plain,(
% 138.90/18.11 sQ24_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f320])).
% 138.90/18.11 fof(f384,plain,(
% 138.90/18.11 apply(delta,zero(e))=zero(r)),
% 138.90/18.11 inference(resolution,[status(thm)],[f101,f37])).
% 138.90/18.11 fof(f409,definition,(
% 138.90/18.11 sQ51_spl <=> (surjection(delta))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f411,plain,(
% 138.90/18.11 ~surjection(delta)|sQ51_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f409])).
% 138.90/18.11 fof(f448,plain,(
% 138.90/18.11 ![X0]: (~injection(f)|~element(X0,a)|~apply(f,X0)=zero(d)|X0=zero(a))),
% 138.90/18.11 inference(resolution,[status(thm)],[f102,f91])).
% 138.90/18.11 fof(f462,plain,(
% 138.90/18.11 apply(f,zero(a))=zero(d)),
% 138.90/18.11 inference(resolution,[status(thm)],[f102,f37])).
% 138.90/18.11 fof(f463,plain,(
% 138.90/18.11 ![X0]: (~element(X0,a)|element(apply(f,X0),d))),
% 138.90/18.11 inference(resolution,[status(thm)],[f102,f36])).
% 138.90/18.11 fof(f468,definition,(
% 138.90/18.11 sQ61_spl <=> (injection(f))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f470,plain,(
% 138.90/18.11 ~injection(f)|sQ61_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f468])).
% 138.90/18.11 fof(f480,definition,(
% 138.90/18.11 ![X0]: (sQ64_spl <=> (~element(X0,a)|~apply(f,X0)=zero(d)|X0=zero(a)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f481,plain,(
% 138.90/18.11 ![X0]: (~element(X0,a)|~apply(f,X0)=zero(d)|X0=zero(a)|~sQ64_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f480])).
% 138.90/18.11 fof(f483,plain,(
% 138.90/18.11 ~sQ61_spl|sQ64_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f448,f468,f480])).
% 138.90/18.11 fof(f523,plain,(
% 138.90/18.11 $false|sQ61_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f470,f113])).
% 138.90/18.11 fof(f524,plain,(
% 138.90/18.11 sQ61_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f523])).
% 138.90/18.11 fof(f529,plain,(
% 138.90/18.11 ![X0,X1]: (~element(X0,b)|~element(X1,b)|apply(g,subtract(b,X0,X1))=subtract(e,apply(g,X0),apply(g,X1)))),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f89])).
% 138.90/18.11 fof(f538,plain,(
% 138.90/18.11 ~sK0_skl(b,g)=sK1_skl(b,g)|injection(g)),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f47])).
% 138.90/18.11 fof(f539,plain,(
% 138.90/18.11 apply(g,sK0_skl(b,g))=apply(g,sK1_skl(b,g))|injection(g)),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f46])).
% 138.90/18.11 fof(f540,plain,(
% 138.90/18.11 element(sK1_skl(b,g),b)|injection(g)),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f45])).
% 138.90/18.11 fof(f541,plain,(
% 138.90/18.11 element(sK0_skl(b,g),b)|injection(g)),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f44])).
% 138.90/18.11 fof(f542,plain,(
% 138.90/18.11 apply(g,zero(b))=zero(e)),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f37])).
% 138.90/18.11 fof(f543,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|element(apply(g,X0),e))),
% 138.90/18.11 inference(resolution,[status(thm)],[f103,f36])).
% 138.90/18.11 fof(f548,definition,(
% 138.90/18.11 sQ76_spl <=> (injection(g))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f549,plain,(
% 138.90/18.11 injection(g)|~sQ76_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f548])).
% 138.90/18.11 fof(f583,definition,(
% 138.90/18.11 sQ85_spl <=> (sK0_skl(b,g)=sK1_skl(b,g))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f585,plain,(
% 138.90/18.11 ~sK0_skl(b,g)=sK1_skl(b,g)|sQ85_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f583])).
% 138.90/18.11 fof(f586,plain,(
% 138.90/18.11 ~sQ85_spl|sQ76_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f538,f583,f548])).
% 138.90/18.11 fof(f587,definition,(
% 138.90/18.11 sQ86_spl <=> (apply(g,sK0_skl(b,g))=apply(g,sK1_skl(b,g)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f588,plain,(
% 138.90/18.11 apply(g,sK0_skl(b,g))=apply(g,sK1_skl(b,g))|~sQ86_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f587])).
% 138.90/18.11 fof(f590,plain,(
% 138.90/18.11 sQ86_spl|sQ76_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f539,f587,f548])).
% 138.90/18.11 fof(f591,definition,(
% 138.90/18.11 sQ87_spl <=> (element(sK1_skl(b,g),b))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f592,plain,(
% 138.90/18.11 element(sK1_skl(b,g),b)|~sQ87_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f591])).
% 138.90/18.11 fof(f594,plain,(
% 138.90/18.11 sQ87_spl|sQ76_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f540,f591,f548])).
% 138.90/18.11 fof(f595,definition,(
% 138.90/18.11 sQ88_spl <=> (element(sK0_skl(b,g),b))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f596,plain,(
% 138.90/18.11 element(sK0_skl(b,g),b)|~sQ88_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f595])).
% 138.90/18.11 fof(f598,plain,(
% 138.90/18.11 sQ88_spl|sQ76_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f541,f595,f548])).
% 138.90/18.11 fof(f622,plain,(
% 138.90/18.11 ![X0,X1]: (~injection(h)|~element(X0,c)|~element(X1,c)|~apply(h,X0)=apply(h,X1)|X0=X1)),
% 138.90/18.11 inference(resolution,[status(thm)],[f104,f40])).
% 138.90/18.11 fof(f626,definition,(
% 138.90/18.11 sQ91_spl <=> (injection(h))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f628,plain,(
% 138.90/18.11 ~injection(h)|sQ91_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f626])).
% 138.90/18.11 fof(f677,definition,(
% 138.90/18.11 ![X0,X1]: (sQ104_spl <=> (~element(X0,c)|~element(X1,c)|~apply(h,X0)=apply(h,X1)|X0=X1))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f678,plain,(
% 138.90/18.11 ![X0,X1]: (~element(X0,c)|~element(X1,c)|~apply(h,X0)=apply(h,X1)|X0=X1|~sQ104_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f677])).
% 138.90/18.11 fof(f680,plain,(
% 138.90/18.11 ~sQ91_spl|sQ104_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f622,f626,f677])).
% 138.90/18.11 fof(f681,plain,(
% 138.90/18.11 $false|sQ91_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f628,f114])).
% 138.90/18.11 fof(f682,plain,(
% 138.90/18.11 sQ91_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f681])).
% 138.90/18.11 fof(f683,plain,(
% 138.90/18.11 $false|~sQ76_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f549,f115])).
% 138.90/18.11 fof(f684,plain,(
% 138.90/18.11 ~sQ76_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f683])).
% 138.90/18.11 fof(f685,plain,(
% 138.90/18.11 ![X0,X1,X2,X3,X4]: (~morphism(alpha,X0,X1)|~morphism(g,X1,X2)|~morphism(f,X0,X3)|~morphism(gamma,X3,X2)|~element(X4,X0)|apply(g,apply(alpha,X4))=apply(gamma,apply(f,X4)))),
% 138.90/18.11 inference(resolution,[status(thm)],[f111,f76])).
% 138.90/18.11 fof(f686,plain,(
% 138.90/18.11 ![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)))),
% 138.90/18.11 inference(resolution,[status(thm)],[f112,f76])).
% 138.90/18.11 fof(f689,plain,(
% 138.90/18.11 subtract(b,sK1_skl(b,g),sK1_skl(b,g))=zero(b)|~sQ87_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f592,f85])).
% 138.90/18.11 fof(f748,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|subtract(b,sK0_skl(b,g),subtract(b,sK0_skl(b,g),X0))=X0|~sQ88_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f87])).
% 138.90/18.11 fof(f751,definition,(
% 138.90/18.11 sQ109_spl <=> (apply(beta,sK1_skl(b,g))=apply(beta,sK0_skl(b,g)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f752,plain,(
% 138.90/18.11 apply(beta,sK1_skl(b,g))=apply(beta,sK0_skl(b,g))|~sQ109_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f751])).
% 138.90/18.11 fof(f755,plain,(
% 138.90/18.11 ![X0,X1]: (~morphism(beta,b,X0)|~element(X1,b)|~apply(beta,X1)=zero(X0)|apply(alpha,sK4_skl(X1,X0,b,a,beta,alpha))=X1)),
% 138.90/18.11 inference(resolution,[status(thm)],[f122,f98])).
% 138.90/18.11 fof(f756,plain,(
% 138.90/18.11 ![X0,X1]: (~morphism(beta,b,X0)|~element(X1,b)|~apply(beta,X1)=zero(X0)|element(sK4_skl(X1,X0,b,a,beta,alpha),a))),
% 138.90/18.11 inference(resolution,[status(thm)],[f123,f98])).
% 138.90/18.11 fof(f1131,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(g,b,X0)|~morphism(f,a,X1)|~morphism(gamma,X1,X0)|~element(X2,a)|apply(g,apply(alpha,X2))=apply(gamma,apply(f,X2)))),
% 138.90/18.11 inference(resolution,[status(thm)],[f685,f98])).
% 138.90/18.11 fof(f1132,definition,(
% 138.90/18.11 ![X0,X1]: (sQ150_spl <=> (~morphism(g,b,X0)|~morphism(f,a,X1)|~morphism(gamma,X1,X0)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1133,plain,(
% 138.90/18.11 ![X0,X1]: (~morphism(g,b,X0)|~morphism(f,a,X1)|~morphism(gamma,X1,X0)|~sQ150_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1132])).
% 138.90/18.11 fof(f1135,definition,(
% 138.90/18.11 ![X2]: (sQ151_spl <=> (~element(X2,a)|apply(g,apply(alpha,X2))=apply(gamma,apply(f,X2))))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1136,plain,(
% 138.90/18.11 ![X0]: (~element(X0,a)|apply(g,apply(alpha,X0))=apply(gamma,apply(f,X0))|~sQ151_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1135])).
% 138.90/18.11 fof(f1138,plain,(
% 138.90/18.11 sQ150_spl|sQ151_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f1131,f1132,f1135])).
% 138.90/18.11 fof(f1139,plain,(
% 138.90/18.11 ![X0,X1,X2]: (~morphism(h,c,X0)|~morphism(g,b,X1)|~morphism(delta,X1,X0)|~element(X2,b)|apply(h,apply(beta,X2))=apply(delta,apply(g,X2)))),
% 138.90/18.11 inference(resolution,[status(thm)],[f686,f99])).
% 138.90/18.11 fof(f1140,definition,(
% 138.90/18.11 ![X0,X1]: (sQ152_spl <=> (~morphism(h,c,X0)|~morphism(g,b,X1)|~morphism(delta,X1,X0)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1141,plain,(
% 138.90/18.11 ![X0,X1]: (~morphism(h,c,X0)|~morphism(g,b,X1)|~morphism(delta,X1,X0)|~sQ152_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1140])).
% 138.90/18.11 fof(f1143,definition,(
% 138.90/18.11 ![X2]: (sQ153_spl <=> (~element(X2,b)|apply(h,apply(beta,X2))=apply(delta,apply(g,X2))))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1144,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|apply(h,apply(beta,X0))=apply(delta,apply(g,X0))|~sQ153_spl)),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1143])).
% 138.90/18.11 fof(f1146,plain,(
% 138.90/18.11 sQ152_spl|sQ153_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f1139,f1140,f1143])).
% 138.90/18.11 fof(f1253,definition,(
% 138.90/18.11 sQ170_spl <=> (apply(h,apply(beta,sK1_skl(b,g)))=apply(h,apply(beta,sK1_skl(b,g))))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1255,plain,(
% 138.90/18.11 ~apply(h,apply(beta,sK1_skl(b,g)))=apply(h,apply(beta,sK1_skl(b,g)))|sQ170_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1253])).
% 138.90/18.11 fof(f1318,plain,(
% 138.90/18.11 subtract(b,sK0_skl(b,g),subtract(b,sK0_skl(b,g),sK0_skl(b,g)))=sK0_skl(b,g)|~sQ88_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f748,f596])).
% 138.90/18.11 fof(f1384,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|~apply(beta,X0)=zero(c)|apply(alpha,sK4_skl(X0,c,b,a,beta,alpha))=X0)),
% 138.90/18.11 inference(resolution,[status(thm)],[f755,f99])).
% 138.90/18.11 fof(f1385,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|~apply(beta,X0)=zero(c)|element(sK4_skl(X0,c,b,a,beta,alpha),a))),
% 138.90/18.11 inference(resolution,[status(thm)],[f756,f99])).
% 138.90/18.11 fof(f1416,definition,(
% 138.90/18.11 sQ176_spl <=> (morphism(alpha,a,b))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1418,plain,(
% 138.90/18.11 ~morphism(alpha,a,b)|sQ176_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1416])).
% 138.90/18.11 fof(f1419,definition,(
% 138.90/18.11 sQ177_spl <=> (morphism(g,b,e))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1421,plain,(
% 138.90/18.11 ~morphism(g,b,e)|sQ177_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1419])).
% 138.90/18.11 fof(f1680,definition,(
% 138.90/18.11 sQ205_spl <=> (morphism(beta,b,c))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1682,plain,(
% 138.90/18.11 ~morphism(beta,b,c)|sQ205_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1680])).
% 138.90/18.11 fof(f1683,definition,(
% 138.90/18.11 sQ206_spl <=> (morphism(h,c,r))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1685,plain,(
% 138.90/18.11 ~morphism(h,c,r)|sQ206_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1683])).
% 138.90/18.11 fof(f1928,definition,(
% 138.90/18.11 sQ208_spl <=> (morphism(gamma,d,e))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1930,plain,(
% 138.90/18.11 ~morphism(gamma,d,e)|sQ208_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1928])).
% 138.90/18.11 fof(f1931,definition,(
% 138.90/18.11 sQ209_spl <=> (morphism(delta,e,r))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f1933,plain,(
% 138.90/18.11 ~morphism(delta,e,r)|sQ209_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f1931])).
% 138.90/18.11 fof(f2314,definition,(
% 138.90/18.11 sQ238_spl <=> (morphism(f,a,d))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f2316,plain,(
% 138.90/18.11 ~morphism(f,a,d)|sQ238_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f2314])).
% 138.90/18.11 fof(f2321,plain,(
% 138.90/18.11 $false|sQ208_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f1930,f100])).
% 138.90/18.11 fof(f2322,plain,(
% 138.90/18.11 sQ208_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f2321])).
% 138.90/18.11 fof(f2608,plain,(
% 138.90/18.11 $false|sQ209_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f1933,f101])).
% 138.90/18.11 fof(f2609,plain,(
% 138.90/18.11 sQ209_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f2608])).
% 138.90/18.11 fof(f2610,plain,(
% 138.90/18.11 $false|sQ177_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f1421,f103])).
% 138.90/18.11 fof(f2611,plain,(
% 138.90/18.11 sQ177_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f2610])).
% 138.90/18.11 fof(f2967,plain,(
% 138.90/18.11 ![X0]: (~morphism(f,a,X0)|~morphism(gamma,X0,e)|~sQ150_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f1133,f103])).
% 138.90/18.11 fof(f2968,plain,(
% 138.90/18.11 ~morphism(gamma,d,e)|~sQ150_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f2967,f102])).
% 138.90/18.11 fof(f2969,plain,(
% 138.90/18.11 ~sQ208_spl|~sQ150_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f2968,f1928,f1132])).
% 138.90/18.11 fof(f2982,plain,(
% 138.90/18.11 ![X0]: (~morphism(g,b,X0)|~morphism(delta,X0,r)|~sQ152_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f1141,f104])).
% 138.90/18.11 fof(f3052,plain,(
% 138.90/18.11 ~morphism(delta,e,r)|~sQ152_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f2982,f103])).
% 138.90/18.11 fof(f3053,plain,(
% 138.90/18.11 ~sQ209_spl|~sQ152_spl),
% 138.90/18.11 inference(split_clause,[status(thm)],[f3052,f1931,f1140])).
% 138.90/18.11 fof(f3546,definition,(
% 138.90/18.11 sQ273_spl <=> (apply(beta,zero(b))=zero(c))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f3548,plain,(
% 138.90/18.11 ~apply(beta,zero(b))=zero(c)|sQ273_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f3546])).
% 138.90/18.11 fof(f3562,plain,(
% 138.90/18.11 ~zero(c)=zero(c)|sQ273_spl),
% 138.90/18.11 inference(forward_demodulation,[status(thm)],[f196,f3548])).
% 138.90/18.11 fof(f3563,plain,(
% 138.90/18.11 $false|sQ273_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f3562])).
% 138.90/18.11 fof(f3564,plain,(
% 138.90/18.11 sQ273_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f3563])).
% 138.90/18.11 fof(f3611,definition,(
% 138.90/18.11 sQ278_spl <=> (sK0_skl(b,g)=subtract(b,sK0_skl(b,g),zero(b)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f3612,plain,(
% 138.90/18.11 sK0_skl(b,g)=subtract(b,sK0_skl(b,g),zero(b))|~sQ278_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f3611])).
% 138.90/18.11 fof(f3613,plain,(
% 138.90/18.11 ~sK0_skl(b,g)=subtract(b,sK0_skl(b,g),zero(b))|sQ278_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f3611])).
% 138.90/18.11 fof(f3719,definition,(
% 138.90/18.11 sQ298_spl <=> (sK1_skl(b,g)=subtract(b,sK0_skl(b,g),zero(b)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f3720,plain,(
% 138.90/18.11 sK1_skl(b,g)=subtract(b,sK0_skl(b,g),zero(b))|~sQ298_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f3719])).
% 138.90/18.11 fof(f3805,definition,(
% 138.90/18.11 sQ316_spl <=> (apply(f,zero(a))=zero(d))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f3807,plain,(
% 138.90/18.11 ~apply(f,zero(a))=zero(d)|sQ316_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f3805])).
% 138.90/18.11 fof(f3814,definition,(
% 138.90/18.11 sQ318_spl <=> (apply(alpha,zero(a))=zero(b))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f3816,plain,(
% 138.90/18.11 ~apply(alpha,zero(a))=zero(b)|sQ318_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f3814])).
% 138.90/18.11 fof(f4012,plain,(
% 138.90/18.11 apply(h,apply(beta,sK1_skl(b,g)))=apply(delta,apply(g,sK1_skl(b,g)))|~sQ87_spl|~sQ153_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f592,f1144])).
% 138.90/18.11 fof(f4250,definition,(
% 138.90/18.11 sQ344_spl <=> (apply(beta,sK2_skl(sK8_skl(r,e,delta),e,b,g))=apply(beta,sK2_skl(sK8_skl(r,e,delta),e,b,g)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f4252,plain,(
% 138.90/18.11 ~apply(beta,sK2_skl(sK8_skl(r,e,delta),e,b,g))=apply(beta,sK2_skl(sK8_skl(r,e,delta),e,b,g))|sQ344_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f4250])).
% 138.90/18.11 fof(f4304,plain,(
% 138.90/18.11 $false|sQ344_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f4252])).
% 138.90/18.11 fof(f4305,plain,(
% 138.90/18.11 sQ344_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f4304])).
% 138.90/18.11 fof(f4350,definition,(
% 138.90/18.11 sQ365_spl <=> (apply(delta,zero(e))=zero(r))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f4352,plain,(
% 138.90/18.11 ~apply(delta,zero(e))=zero(r)|sQ365_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f4350])).
% 138.90/18.11 fof(f4357,plain,(
% 138.90/18.11 ~zero(r)=zero(r)|sQ365_spl),
% 138.90/18.11 inference(forward_demodulation,[status(thm)],[f384,f4352])).
% 138.90/18.11 fof(f4358,plain,(
% 138.90/18.11 $false|sQ365_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f4357])).
% 138.90/18.11 fof(f4359,plain,(
% 138.90/18.11 sQ365_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f4358])).
% 138.90/18.11 fof(f4406,plain,(
% 138.90/18.11 element(apply(g,sK0_skl(b,g)),e)|~sQ88_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f543])).
% 138.90/18.11 fof(f4408,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|apply(beta,subtract(b,sK0_skl(b,g),X0))=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,X0))|~sQ88_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f245])).
% 138.90/18.11 fof(f4409,plain,(
% 138.90/18.11 element(apply(beta,sK0_skl(b,g)),c)|~sQ88_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f197])).
% 138.90/18.11 fof(f4411,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|subtract(b,sK0_skl(b,g),subtract(b,sK0_skl(b,g),X0))=X0|~sQ88_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f87])).
% 138.90/18.11 fof(f4412,plain,(
% 138.90/18.11 subtract(b,sK0_skl(b,g),sK0_skl(b,g))=zero(b)|~sQ88_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f85])).
% 138.90/18.11 fof(f4413,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|element(subtract(b,sK0_skl(b,g),X0),b)|~sQ88_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f83])).
% 138.90/18.11 fof(f4581,definition,(
% 138.90/18.11 sQ371_spl <=> (apply(f,sK2_skl(sK0_skl(b,g),b,a,alpha))=apply(f,sK2_skl(sK0_skl(b,g),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f4583,plain,(
% 138.90/18.11 ~apply(f,sK2_skl(sK0_skl(b,g),b,a,alpha))=apply(f,sK2_skl(sK0_skl(b,g),b,a,alpha))|sQ371_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f4581])).
% 138.90/18.11 fof(f4592,definition,(
% 138.90/18.11 sQ373_spl <=> (apply(f,sK2_skl(sK1_skl(b,g),b,a,alpha))=apply(f,sK2_skl(sK1_skl(b,g),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f4594,plain,(
% 138.90/18.11 ~apply(f,sK2_skl(sK1_skl(b,g),b,a,alpha))=apply(f,sK2_skl(sK1_skl(b,g),b,a,alpha))|sQ373_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f4592])).
% 138.90/18.11 fof(f4599,plain,(
% 138.90/18.11 $false|sQ373_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f4594])).
% 138.90/18.11 fof(f4600,plain,(
% 138.90/18.11 sQ373_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f4599])).
% 138.90/18.11 fof(f4908,plain,(
% 138.90/18.11 apply(h,apply(beta,sK0_skl(b,g)))=apply(delta,apply(g,sK0_skl(b,g)))|~sQ88_spl|~sQ153_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f1144])).
% 138.90/18.11 fof(f5058,definition,(
% 138.90/18.11 sQ399_spl <=> (apply(f,sK2_skl(sK8_skl(e,b,g),b,a,alpha))=apply(f,sK2_skl(sK8_skl(e,b,g),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f5060,plain,(
% 138.90/18.11 ~apply(f,sK2_skl(sK8_skl(e,b,g),b,a,alpha))=apply(f,sK2_skl(sK8_skl(e,b,g),b,a,alpha))|sQ399_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f5058])).
% 138.90/18.11 fof(f5124,definition,(
% 138.90/18.11 sQ403_spl <=> (apply(alpha,sK2_skl(sK0_skl(b,g),b,a,alpha))=apply(alpha,sK2_skl(sK0_skl(b,g),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f5126,plain,(
% 138.90/18.11 ~apply(alpha,sK2_skl(sK0_skl(b,g),b,a,alpha))=apply(alpha,sK2_skl(sK0_skl(b,g),b,a,alpha))|sQ403_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f5124])).
% 138.90/18.11 fof(f5151,plain,(
% 138.90/18.11 $false|sQ371_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f4583])).
% 138.90/18.11 fof(f5152,plain,(
% 138.90/18.11 sQ371_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f5151])).
% 138.90/18.11 fof(f5154,plain,(
% 138.90/18.11 $false|sQ403_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f5126])).
% 138.90/18.11 fof(f5155,plain,(
% 138.90/18.11 sQ403_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f5154])).
% 138.90/18.11 fof(f5169,definition,(
% 138.90/18.11 sQ409_spl <=> (apply(gamma,zero(d))=zero(e))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f5171,plain,(
% 138.90/18.11 ~apply(gamma,zero(d))=zero(e)|sQ409_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f5169])).
% 138.90/18.11 fof(f5306,plain,(
% 138.90/18.11 ~zero(e)=zero(e)|sQ409_spl),
% 138.90/18.11 inference(forward_demodulation,[status(thm)],[f271,f5171])).
% 138.90/18.11 fof(f5307,plain,(
% 138.90/18.11 $false|sQ409_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f5306])).
% 138.90/18.11 fof(f5308,plain,(
% 138.90/18.11 sQ409_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f5307])).
% 138.90/18.11 fof(f5773,plain,(
% 138.90/18.11 ![X0]: (~element(X0,b)|apply(g,subtract(b,sK0_skl(b,g),X0))=subtract(e,apply(g,sK0_skl(b,g)),apply(g,X0))|~sQ88_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f596,f529])).
% 138.90/18.11 fof(f5832,plain,(
% 138.90/18.11 subtract(e,apply(g,sK0_skl(b,g)),apply(g,sK0_skl(b,g)))=zero(e)|~sQ88_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f4406,f85])).
% 138.90/18.11 fof(f6069,plain,(
% 138.90/18.11 $false|sQ399_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f5060])).
% 138.90/18.11 fof(f6070,plain,(
% 138.90/18.11 sQ399_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6069])).
% 138.90/18.11 fof(f6075,plain,(
% 138.90/18.11 ~zero(b)=zero(b)|sQ318_spl),
% 138.90/18.11 inference(forward_demodulation,[status(thm)],[f139,f3816])).
% 138.90/18.11 fof(f6076,plain,(
% 138.90/18.11 $false|sQ318_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f6075])).
% 138.90/18.11 fof(f6077,plain,(
% 138.90/18.11 sQ318_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6076])).
% 138.90/18.11 fof(f6078,plain,(
% 138.90/18.11 ~zero(d)=zero(d)|sQ316_spl),
% 138.90/18.11 inference(forward_demodulation,[status(thm)],[f462,f3807])).
% 138.90/18.11 fof(f6079,plain,(
% 138.90/18.11 $false|sQ316_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f6078])).
% 138.90/18.11 fof(f6080,plain,(
% 138.90/18.11 sQ316_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6079])).
% 138.90/18.11 fof(f6098,plain,(
% 138.90/18.11 $false|sQ238_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f2316,f102])).
% 138.90/18.11 fof(f6099,plain,(
% 138.90/18.11 sQ238_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6098])).
% 138.90/18.11 fof(f6100,plain,(
% 138.90/18.11 $false|sQ206_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f1685,f104])).
% 138.90/18.11 fof(f6101,plain,(
% 138.90/18.11 sQ206_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6100])).
% 138.90/18.11 fof(f6102,plain,(
% 138.90/18.11 $false|sQ205_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f1682,f99])).
% 138.90/18.11 fof(f6103,plain,(
% 138.90/18.11 sQ205_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6102])).
% 138.90/18.11 fof(f6104,plain,(
% 138.90/18.11 $false|sQ176_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f1418,f98])).
% 138.90/18.11 fof(f6105,plain,(
% 138.90/18.11 sQ176_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6104])).
% 138.90/18.11 fof(f6106,plain,(
% 138.90/18.11 $false|sQ170_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f1255])).
% 138.90/18.11 fof(f6107,plain,(
% 138.90/18.11 sQ170_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6106])).
% 138.90/18.11 fof(f6178,definition,(
% 138.90/18.11 sQ425_spl <=> (zero(e)=apply(g,zero(b)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f6180,plain,(
% 138.90/18.11 ~zero(e)=apply(g,zero(b))|sQ425_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f6178])).
% 138.90/18.11 fof(f6194,plain,(
% 138.90/18.11 ~zero(e)=zero(e)|sQ425_spl),
% 138.90/18.11 inference(forward_demodulation,[status(thm)],[f542,f6180])).
% 138.90/18.11 fof(f6195,plain,(
% 138.90/18.11 $false|sQ425_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f6194])).
% 138.90/18.11 fof(f6196,plain,(
% 138.90/18.11 sQ425_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6195])).
% 138.90/18.11 fof(f6883,definition,(
% 138.90/18.11 sQ522_spl <=> (apply(gamma,sK8_skl(e,d,gamma))=apply(gamma,sK8_skl(e,d,gamma)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ522_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f6885,plain,(
% 138.90/18.11 ~apply(gamma,sK8_skl(e,d,gamma))=apply(gamma,sK8_skl(e,d,gamma))|sQ522_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f6883])).
% 138.90/18.11 fof(f6890,plain,(
% 138.90/18.11 $false|sQ522_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f6885])).
% 138.90/18.11 fof(f6891,plain,(
% 138.90/18.11 sQ522_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6890])).
% 138.90/18.11 fof(f6986,definition,(
% 138.90/18.11 sQ524_spl <=> (apply(h,sK1_skl(c,h))=apply(h,sK1_skl(c,h)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ524_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f6988,plain,(
% 138.90/18.11 ~apply(h,sK1_skl(c,h))=apply(h,sK1_skl(c,h))|sQ524_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f6986])).
% 138.90/18.11 fof(f6996,plain,(
% 138.90/18.11 $false|sQ524_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f6988])).
% 138.90/18.11 fof(f6997,plain,(
% 138.90/18.11 sQ524_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f6996])).
% 138.90/18.11 fof(f7014,definition,(
% 138.90/18.11 sQ526_spl <=> (apply(h,sK0_skl(c,h))=apply(h,sK0_skl(c,h)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f7016,plain,(
% 138.90/18.11 ~apply(h,sK0_skl(c,h))=apply(h,sK0_skl(c,h))|sQ526_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f7014])).
% 138.90/18.11 fof(f7025,plain,(
% 138.90/18.11 $false|sQ526_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f7016])).
% 138.90/18.11 fof(f7026,plain,(
% 138.90/18.11 sQ526_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f7025])).
% 138.90/18.11 fof(f7689,plain,(
% 138.90/18.11 apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,sK1_skl(b,g)))|~sQ88_spl|~sQ87_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f4408,f592])).
% 138.90/18.11 fof(f7749,plain,(
% 138.90/18.11 subtract(b,sK0_skl(b,g),subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=sK1_skl(b,g)|~sQ88_spl|~sQ87_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f4411,f592])).
% 138.90/18.11 fof(f7757,plain,(
% 138.90/18.11 element(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),b)|~sQ88_spl|~sQ87_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f4413,f592])).
% 138.90/18.11 fof(f7954,plain,(
% 138.90/18.11 ![X0]: (~element(X0,c)|~apply(h,apply(beta,sK0_skl(b,g)))=apply(h,X0)|apply(beta,sK0_skl(b,g))=X0|~sQ88_spl|~sQ104_spl)),
% 138.90/18.11 inference(resolution,[status(thm)],[f4409,f678])).
% 138.90/18.11 fof(f8718,definition,(
% 138.90/18.11 sQ557_spl <=> (apply(f,sK2_skl(sK8_skl(c,b,beta),b,a,alpha))=apply(f,sK2_skl(sK8_skl(c,b,beta),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f8720,plain,(
% 138.90/18.11 ~apply(f,sK2_skl(sK8_skl(c,b,beta),b,a,alpha))=apply(f,sK2_skl(sK8_skl(c,b,beta),b,a,alpha))|sQ557_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f8718])).
% 138.90/18.11 fof(f8726,plain,(
% 138.90/18.11 $false|sQ557_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f8720])).
% 138.90/18.11 fof(f8727,plain,(
% 138.90/18.11 sQ557_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f8726])).
% 138.90/18.11 fof(f9219,plain,(
% 138.90/18.11 sK1_skl(b,g)=sK0_skl(b,g)|~sQ278_spl|~sQ298_spl),
% 138.90/18.11 inference(backward_demodulation,[status(thm)],[f3612,f3720])).
% 138.90/18.11 fof(f9220,plain,(
% 138.90/18.11 $false|sQ85_spl|~sQ278_spl|~sQ298_spl),
% 138.90/18.11 inference(forward_subsumption_resolution,[status(thm)],[f9219,f585])).
% 138.90/18.11 fof(f9221,plain,(
% 138.90/18.11 sQ85_spl|~sQ278_spl|~sQ298_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f9220])).
% 138.90/18.11 fof(f9393,definition,(
% 138.90/18.11 sQ566_spl <=> (apply(alpha,sK2_skl(sK0_skl(b,beta),b,a,alpha))=apply(alpha,sK2_skl(sK0_skl(b,beta),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f9395,plain,(
% 138.90/18.11 ~apply(alpha,sK2_skl(sK0_skl(b,beta),b,a,alpha))=apply(alpha,sK2_skl(sK0_skl(b,beta),b,a,alpha))|sQ566_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f9393])).
% 138.90/18.11 fof(f9409,plain,(
% 138.90/18.11 $false|sQ566_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f9395])).
% 138.90/18.11 fof(f9410,plain,(
% 138.90/18.11 sQ566_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f9409])).
% 138.90/18.11 fof(f9490,definition,(
% 138.90/18.11 sQ578_spl <=> (apply(alpha,sK1_skl(a,f))=apply(alpha,sK1_skl(a,f)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f9492,plain,(
% 138.90/18.11 ~apply(alpha,sK1_skl(a,f))=apply(alpha,sK1_skl(a,f))|sQ578_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f9490])).
% 138.90/18.11 fof(f9497,definition,(
% 138.90/18.11 sQ580_spl <=> (apply(f,sK1_skl(a,f))=apply(f,sK1_skl(a,f)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f9499,plain,(
% 138.90/18.11 ~apply(f,sK1_skl(a,f))=apply(f,sK1_skl(a,f))|sQ580_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f9497])).
% 138.90/18.11 fof(f9534,plain,(
% 138.90/18.11 $false|sQ580_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f9499])).
% 138.90/18.11 fof(f9535,plain,(
% 138.90/18.11 sQ580_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f9534])).
% 138.90/18.11 fof(f9536,plain,(
% 138.90/18.11 $false|sQ578_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f9492])).
% 138.90/18.11 fof(f9537,plain,(
% 138.90/18.11 sQ578_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f9536])).
% 138.90/18.11 fof(f11246,plain,(
% 138.90/18.11 element(apply(beta,sK1_skl(b,g)),c)|~sQ87_spl),
% 138.90/18.11 inference(resolution,[status(thm)],[f592,f197])).
% 138.90/18.11 fof(f12398,definition,(
% 138.90/18.11 sQ651_spl <=> (apply(f,sK2_skl(sK1_skl(b,beta),b,a,alpha))=apply(f,sK2_skl(sK1_skl(b,beta),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f12400,plain,(
% 138.90/18.11 ~apply(f,sK2_skl(sK1_skl(b,beta),b,a,alpha))=apply(f,sK2_skl(sK1_skl(b,beta),b,a,alpha))|sQ651_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f12398])).
% 138.90/18.11 fof(f12414,plain,(
% 138.90/18.11 $false|sQ651_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f12400])).
% 138.90/18.11 fof(f12415,plain,(
% 138.90/18.11 sQ651_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f12414])).
% 138.90/18.11 fof(f13373,definition,(
% 138.90/18.11 sQ663_spl <=> (apply(f,sK0_skl(a,f))=apply(f,sK0_skl(a,f)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f13375,plain,(
% 138.90/18.11 ~apply(f,sK0_skl(a,f))=apply(f,sK0_skl(a,f))|sQ663_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f13373])).
% 138.90/18.11 fof(f13392,plain,(
% 138.90/18.11 $false|sQ663_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f13375])).
% 138.90/18.11 fof(f13393,plain,(
% 138.90/18.11 sQ663_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f13392])).
% 138.90/18.11 fof(f13414,definition,(
% 138.90/18.11 sQ667_spl <=> (apply(alpha,sK0_skl(a,f))=apply(alpha,sK0_skl(a,f)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f13416,plain,(
% 138.90/18.11 ~apply(alpha,sK0_skl(a,f))=apply(alpha,sK0_skl(a,f))|sQ667_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f13414])).
% 138.90/18.11 fof(f13421,plain,(
% 138.90/18.11 $false|sQ667_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f13416])).
% 138.90/18.11 fof(f13422,plain,(
% 138.90/18.11 sQ667_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f13421])).
% 138.90/18.11 fof(f13520,definition,(
% 138.90/18.11 sQ674_spl <=> (apply(f,sK0_skl(a,alpha))=apply(f,sK0_skl(a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ674_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f13522,plain,(
% 138.90/18.11 ~apply(f,sK0_skl(a,alpha))=apply(f,sK0_skl(a,alpha))|sQ674_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f13520])).
% 138.90/18.11 fof(f13533,plain,(
% 138.90/18.11 $false|sQ674_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f13522])).
% 138.90/18.11 fof(f13534,plain,(
% 138.90/18.11 sQ674_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f13533])).
% 138.90/18.11 fof(f13540,definition,(
% 138.90/18.11 sQ677_spl <=> (apply(alpha,sK0_skl(a,alpha))=apply(alpha,sK0_skl(a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ677_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f13542,plain,(
% 138.90/18.11 ~apply(alpha,sK0_skl(a,alpha))=apply(alpha,sK0_skl(a,alpha))|sQ677_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f13540])).
% 138.90/18.11 fof(f13559,plain,(
% 138.90/18.11 $false|sQ677_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f13542])).
% 138.90/18.11 fof(f13560,plain,(
% 138.90/18.11 sQ677_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f13559])).
% 138.90/18.11 fof(f15228,definition,(
% 138.90/18.11 sQ725_spl <=> (apply(alpha,sK2_skl(sK1_skl(b,g),b,a,alpha))=apply(alpha,sK2_skl(sK1_skl(b,g),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ725_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f15230,plain,(
% 138.90/18.11 ~apply(alpha,sK2_skl(sK1_skl(b,g),b,a,alpha))=apply(alpha,sK2_skl(sK1_skl(b,g),b,a,alpha))|sQ725_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f15228])).
% 138.90/18.11 fof(f15243,plain,(
% 138.90/18.11 $false|sQ725_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f15230])).
% 138.90/18.11 fof(f15244,plain,(
% 138.90/18.11 sQ725_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f15243])).
% 138.90/18.11 fof(f15376,definition,(
% 138.90/18.11 sQ726_spl <=> (apply(alpha,sK2_skl(sK8_skl(c,b,beta),b,a,alpha))=apply(alpha,sK2_skl(sK8_skl(c,b,beta),b,a,alpha)))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f15378,plain,(
% 138.90/18.11 ~apply(alpha,sK2_skl(sK8_skl(c,b,beta),b,a,alpha))=apply(alpha,sK2_skl(sK8_skl(c,b,beta),b,a,alpha))|sQ726_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f15376])).
% 138.90/18.11 fof(f15388,plain,(
% 138.90/18.11 $false|sQ726_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f15378])).
% 138.90/18.11 fof(f15389,plain,(
% 138.90/18.11 sQ726_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f15388])).
% 138.90/18.11 fof(f15448,definition,(
% 138.90/18.11 sQ728_spl <=> (apply(gamma,apply(f,sK1_skl(a,f)))=apply(gamma,apply(f,sK1_skl(a,f))))),
% 138.90/18.11 introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition])).
% 138.90/18.11 fof(f15450,plain,(
% 138.90/18.11 ~apply(gamma,apply(f,sK1_skl(a,f)))=apply(gamma,apply(f,sK1_skl(a,f)))|sQ728_spl),
% 138.90/18.11 inference(component_clause,[status(thm)],[f15448])).
% 138.90/18.11 fof(f15453,plain,(
% 138.90/18.11 $false|sQ728_spl),
% 138.90/18.11 inference(trivial_equality_resolution,[status(thm)],[f15450])).
% 138.90/18.11 fof(f15454,plain,(
% 138.90/18.11 sQ728_spl),
% 138.90/18.11 inference(contradiction_clause,[status(thm)],[f15453])).
% 138.90/18.11 fof(f17169,definition,(
% 138.90/18.11 ![X0]: (sQ756_spl <=> (~morphism(g,b,X0)))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ756_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f17170,plain,(
% 138.90/18.12 ![X0]: (~morphism(g,b,X0)|~sQ756_spl)),
% 138.90/18.12 inference(component_clause,[status(thm)],[f17169])).
% 138.90/18.12 fof(f17177,definition,(
% 138.90/18.12 ![X0]: (sQ757_spl <=> (~morphism(h,c,X0)))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ757_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f17178,plain,(
% 138.90/18.12 ![X0]: (~morphism(h,c,X0)|~sQ757_spl)),
% 138.90/18.12 inference(component_clause,[status(thm)],[f17177])).
% 138.90/18.12 fof(f17208,plain,(
% 138.90/18.12 $false|~sQ756_spl),
% 138.90/18.12 inference(backward_subsumption_resolution,[status(thm)],[f103,f17170])).
% 138.90/18.12 fof(f17209,plain,(
% 138.90/18.12 ~sQ756_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f17208])).
% 138.90/18.12 fof(f17210,plain,(
% 138.90/18.12 $false|~sQ757_spl),
% 138.90/18.12 inference(backward_subsumption_resolution,[status(thm)],[f104,f17178])).
% 138.90/18.12 fof(f17211,plain,(
% 138.90/18.12 ~sQ757_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f17210])).
% 138.90/18.12 fof(f18068,definition,(
% 138.90/18.12 ![X0]: (sQ791_spl <=> (~morphism(delta,e,X0)))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ791_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f18069,plain,(
% 138.90/18.12 ![X0]: (~morphism(delta,e,X0)|~sQ791_spl)),
% 138.90/18.12 inference(component_clause,[status(thm)],[f18068])).
% 138.90/18.12 fof(f18077,plain,(
% 138.90/18.12 $false|~sQ791_spl),
% 138.90/18.12 inference(backward_subsumption_resolution,[status(thm)],[f101,f18069])).
% 138.90/18.12 fof(f18078,plain,(
% 138.90/18.12 ~sQ791_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f18077])).
% 138.90/18.12 fof(f18130,definition,(
% 138.90/18.12 ![X0]: (sQ793_spl <=> (~morphism(gamma,d,X0)))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ793_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f18131,plain,(
% 138.90/18.12 ![X0]: (~morphism(gamma,d,X0)|~sQ793_spl)),
% 138.90/18.12 inference(component_clause,[status(thm)],[f18130])).
% 138.90/18.12 fof(f18145,plain,(
% 138.90/18.12 $false|~sQ793_spl),
% 138.90/18.12 inference(backward_subsumption_resolution,[status(thm)],[f100,f18131])).
% 138.90/18.12 fof(f18146,plain,(
% 138.90/18.12 ~sQ793_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f18145])).
% 138.90/18.12 fof(f18780,plain,(
% 138.90/18.12 subtract(b,sK0_skl(b,g),zero(b))=sK0_skl(b,g)|~sQ88_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f4412,f1318])).
% 138.90/18.12 fof(f18781,plain,(
% 138.90/18.12 $false|sQ278_spl|~sQ88_spl),
% 138.90/18.12 inference(forward_subsumption_resolution,[status(thm)],[f18780,f3613])).
% 138.90/18.12 fof(f18782,plain,(
% 138.90/18.12 sQ278_spl|~sQ88_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f18781])).
% 138.90/18.12 fof(f19020,definition,(
% 138.90/18.12 sQ816_spl <=> (apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=zero(c))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ816_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f19022,plain,(
% 138.90/18.12 ~apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=zero(c)|sQ816_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f19020])).
% 138.90/18.12 fof(f19023,definition,(
% 138.90/18.12 sQ817_spl <=> (apply(alpha,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha))=subtract(b,sK0_skl(b,g),sK1_skl(b,g)))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ817_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f19024,plain,(
% 138.90/18.12 apply(alpha,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha))=subtract(b,sK0_skl(b,g),sK1_skl(b,g))|~sQ817_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f19023])).
% 138.90/18.12 fof(f19267,definition,(
% 138.90/18.12 sQ847_spl <=> (element(sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha),a))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ847_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f19268,plain,(
% 138.90/18.12 element(sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha),a)|~sQ847_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f19267])).
% 138.90/18.12 fof(f20357,definition,(
% 138.90/18.12 sQ905_spl <=> (apply(h,apply(beta,sK7_skl(b,h,beta,h,beta)))=apply(h,apply(beta,sK7_skl(b,h,beta,h,beta))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ905_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f20359,plain,(
% 138.90/18.12 ~apply(h,apply(beta,sK7_skl(b,h,beta,h,beta)))=apply(h,apply(beta,sK7_skl(b,h,beta,h,beta)))|sQ905_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f20357])).
% 138.90/18.12 fof(f20361,plain,(
% 138.90/18.12 $false|sQ905_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f20359])).
% 138.90/18.12 fof(f20362,plain,(
% 138.90/18.12 sQ905_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f20361])).
% 138.90/18.12 fof(f20726,plain,(
% 138.90/18.12 apply(g,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=subtract(e,apply(g,sK0_skl(b,g)),apply(g,sK1_skl(b,g)))|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f5773,f592])).
% 138.90/18.12 fof(f20732,plain,(
% 138.90/18.12 apply(g,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=subtract(e,apply(g,sK0_skl(b,g)),apply(g,sK0_skl(b,g)))|~sQ86_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f588,f20726])).
% 138.90/18.12 fof(f21201,plain,(
% 138.90/18.12 ![X0]: (~element(X0,b)|apply(beta,subtract(b,sK1_skl(b,g),X0))=subtract(c,apply(beta,sK1_skl(b,g)),apply(beta,X0))|~sQ87_spl)),
% 138.90/18.12 inference(resolution,[status(thm)],[f592,f245])).
% 138.90/18.12 fof(f23220,definition,(
% 138.90/18.12 sQ929_spl <=> (apply(f,sK2_skl(zero(b),b,a,alpha))=apply(f,sK2_skl(zero(b),b,a,alpha)))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ929_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f23222,plain,(
% 138.90/18.12 ~apply(f,sK2_skl(zero(b),b,a,alpha))=apply(f,sK2_skl(zero(b),b,a,alpha))|sQ929_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f23220])).
% 138.90/18.12 fof(f23231,plain,(
% 138.90/18.12 $false|sQ929_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f23222])).
% 138.90/18.12 fof(f23232,plain,(
% 138.90/18.12 sQ929_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f23231])).
% 138.90/18.12 fof(f23475,definition,(
% 138.90/18.12 sQ933_spl <=> (apply(beta,apply(alpha,sK7_skl(a,beta,alpha,beta,alpha)))=apply(beta,apply(alpha,sK7_skl(a,beta,alpha,beta,alpha))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ933_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f23477,plain,(
% 138.90/18.12 ~apply(beta,apply(alpha,sK7_skl(a,beta,alpha,beta,alpha)))=apply(beta,apply(alpha,sK7_skl(a,beta,alpha,beta,alpha)))|sQ933_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f23475])).
% 138.90/18.12 fof(f23479,plain,(
% 138.90/18.12 $false|sQ933_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f23477])).
% 138.90/18.12 fof(f23480,plain,(
% 138.90/18.12 sQ933_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f23479])).
% 138.90/18.12 fof(f23487,definition,(
% 138.90/18.12 sQ935_spl <=> (apply(g,apply(alpha,sK7_skl(a,g,alpha,g,alpha)))=apply(g,apply(alpha,sK7_skl(a,g,alpha,g,alpha))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ935_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f23489,plain,(
% 138.90/18.12 ~apply(g,apply(alpha,sK7_skl(a,g,alpha,g,alpha)))=apply(g,apply(alpha,sK7_skl(a,g,alpha,g,alpha)))|sQ935_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f23487])).
% 138.90/18.12 fof(f23491,plain,(
% 138.90/18.12 $false|sQ935_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f23489])).
% 138.90/18.12 fof(f23492,plain,(
% 138.90/18.12 sQ935_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f23491])).
% 138.90/18.12 fof(f23554,definition,(
% 138.90/18.12 sQ936_spl <=> (apply(delta,apply(gamma,sK7_skl(d,delta,gamma,delta,gamma)))=apply(delta,apply(gamma,sK7_skl(d,delta,gamma,delta,gamma))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ936_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f23556,plain,(
% 138.90/18.12 ~apply(delta,apply(gamma,sK7_skl(d,delta,gamma,delta,gamma)))=apply(delta,apply(gamma,sK7_skl(d,delta,gamma,delta,gamma)))|sQ936_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f23554])).
% 138.90/18.12 fof(f23561,plain,(
% 138.90/18.12 $false|sQ936_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f23556])).
% 138.90/18.12 fof(f23562,plain,(
% 138.90/18.12 sQ936_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f23561])).
% 138.90/18.12 fof(f23642,plain,(
% 138.90/18.12 $false|sQ51_spl),
% 138.90/18.12 inference(forward_subsumption_resolution,[status(thm)],[f411,f108])).
% 138.90/18.12 fof(f23643,plain,(
% 138.90/18.12 sQ51_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f23642])).
% 138.90/18.12 fof(f23693,definition,(
% 138.90/18.12 sQ939_spl <=> (apply(gamma,apply(f,sK7_skl(a,gamma,f,gamma,f)))=apply(gamma,apply(f,sK7_skl(a,gamma,f,gamma,f))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ939_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f23695,plain,(
% 138.90/18.12 ~apply(gamma,apply(f,sK7_skl(a,gamma,f,gamma,f)))=apply(gamma,apply(f,sK7_skl(a,gamma,f,gamma,f)))|sQ939_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f23693])).
% 138.90/18.12 fof(f23700,plain,(
% 138.90/18.12 $false|sQ939_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f23695])).
% 138.90/18.12 fof(f23701,plain,(
% 138.90/18.12 sQ939_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f23700])).
% 138.90/18.12 fof(f24541,definition,(
% 138.90/18.12 sQ1008_spl <=> (apply(delta,apply(g,sK7_skl(b,delta,g,delta,g)))=apply(delta,apply(g,sK7_skl(b,delta,g,delta,g))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ1008_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f24543,plain,(
% 138.90/18.12 ~apply(delta,apply(g,sK7_skl(b,delta,g,delta,g)))=apply(delta,apply(g,sK7_skl(b,delta,g,delta,g)))|sQ1008_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f24541])).
% 138.90/18.12 fof(f24548,plain,(
% 138.90/18.12 $false|sQ1008_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f24543])).
% 138.90/18.12 fof(f24549,plain,(
% 138.90/18.12 sQ1008_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f24548])).
% 138.90/18.12 fof(f27335,plain,(
% 138.90/18.12 apply(h,apply(beta,sK1_skl(b,g)))=apply(delta,apply(g,sK0_skl(b,g)))|~sQ86_spl|~sQ87_spl|~sQ153_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f588,f4012])).
% 138.90/18.12 fof(f27653,definition,(
% 138.90/18.12 sQ1048_spl <=> (apply(delta,apply(g,sK0_skl(b,g)))=apply(h,apply(beta,sK1_skl(b,g))))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ1048_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f27655,plain,(
% 138.90/18.12 ~apply(delta,apply(g,sK0_skl(b,g)))=apply(h,apply(beta,sK1_skl(b,g)))|sQ1048_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f27653])).
% 138.90/18.12 fof(f27666,plain,(
% 138.90/18.12 ~apply(delta,apply(g,sK0_skl(b,g)))=apply(delta,apply(g,sK0_skl(b,g)))|~sQ86_spl|~sQ87_spl|~sQ153_spl|sQ1048_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f27335,f27655])).
% 138.90/18.12 fof(f27667,plain,(
% 138.90/18.12 $false|~sQ86_spl|~sQ87_spl|~sQ153_spl|sQ1048_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f27666])).
% 138.90/18.12 fof(f27668,plain,(
% 138.90/18.12 ~sQ86_spl|~sQ87_spl|~sQ153_spl|sQ1048_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f27667])).
% 138.90/18.12 fof(f27792,plain,(
% 138.90/18.12 ![X0]: (~element(X0,b)|apply(beta,subtract(b,sK1_skl(b,g),X0))=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,X0))|~sQ109_spl|~sQ87_spl)),
% 138.90/18.12 inference(backward_demodulation,[status(thm)],[f752,f21201])).
% 138.90/18.12 fof(f27813,plain,(
% 138.90/18.12 apply(beta,subtract(b,sK1_skl(b,g),sK1_skl(b,g)))=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,sK1_skl(b,g)))|~sQ109_spl|~sQ87_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f27792,f592])).
% 138.90/18.12 fof(f27822,plain,(
% 138.90/18.12 apply(beta,zero(b))=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,sK1_skl(b,g)))|~sQ109_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f689,f27813])).
% 138.90/18.12 fof(f27823,plain,(
% 138.90/18.12 zero(c)=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,sK1_skl(b,g)))|~sQ109_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f196,f27822])).
% 138.90/18.12 fof(f27824,plain,(
% 138.90/18.12 zero(c)=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,sK0_skl(b,g)))|~sQ109_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f752,f27823])).
% 138.90/18.12 fof(f29190,plain,(
% 138.90/18.12 ![X0]: (~element(X0,c)|~apply(delta,apply(g,sK0_skl(b,g)))=apply(h,X0)|apply(beta,sK0_skl(b,g))=X0|~sQ153_spl|~sQ88_spl|~sQ104_spl)),
% 138.90/18.12 inference(backward_demodulation,[status(thm)],[f4908,f7954])).
% 138.90/18.12 fof(f29193,plain,(
% 138.90/18.12 ~apply(delta,apply(g,sK0_skl(b,g)))=apply(h,apply(beta,sK1_skl(b,g)))|apply(beta,sK0_skl(b,g))=apply(beta,sK1_skl(b,g))|~sQ153_spl|~sQ88_spl|~sQ104_spl|~sQ87_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f29190,f11246])).
% 138.90/18.12 fof(f29196,plain,(
% 138.90/18.12 ~sQ1048_spl|sQ109_spl|~sQ153_spl|~sQ88_spl|~sQ104_spl|~sQ87_spl),
% 138.90/18.12 inference(split_clause,[status(thm)],[f29193,f27653,f751,f1143,f595,f677,f591])).
% 138.90/18.12 fof(f32362,plain,(
% 138.90/18.12 apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=subtract(c,apply(beta,sK0_skl(b,g)),apply(beta,sK0_skl(b,g)))|~sQ109_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f752,f7689])).
% 138.90/18.12 fof(f32363,plain,(
% 138.90/18.12 apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=zero(c)|~sQ109_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f27824,f32362])).
% 138.90/18.12 fof(f32473,plain,(
% 138.90/18.12 ~apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=zero(c)|element(sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha),a)|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f7757,f1385])).
% 138.90/18.12 fof(f32474,plain,(
% 138.90/18.12 ~apply(beta,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=zero(c)|apply(alpha,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha))=subtract(b,sK0_skl(b,g),sK1_skl(b,g))|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f7757,f1384])).
% 138.90/18.12 fof(f32505,plain,(
% 138.90/18.12 ~sQ816_spl|sQ847_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(split_clause,[status(thm)],[f32473,f19020,f19267,f595,f591])).
% 138.90/18.12 fof(f32506,plain,(
% 138.90/18.12 ~sQ816_spl|sQ817_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(split_clause,[status(thm)],[f32474,f19020,f19023,f595,f591])).
% 138.90/18.12 fof(f34692,plain,(
% 138.90/18.12 ~zero(c)=zero(c)|~sQ109_spl|~sQ88_spl|~sQ87_spl|sQ816_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f32363,f19022])).
% 138.90/18.12 fof(f34693,plain,(
% 138.90/18.12 $false|~sQ109_spl|~sQ88_spl|~sQ87_spl|sQ816_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f34692])).
% 138.90/18.12 fof(f34694,plain,(
% 138.90/18.12 ~sQ109_spl|~sQ88_spl|~sQ87_spl|sQ816_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f34693])).
% 138.90/18.12 fof(f34808,plain,(
% 138.90/18.12 ~apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha))=zero(d)|sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)=zero(a)|~sQ847_spl|~sQ64_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f19268,f481])).
% 138.90/18.12 fof(f34812,plain,(
% 138.90/18.12 apply(g,apply(alpha,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))=apply(gamma,apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))|~sQ847_spl|~sQ151_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f19268,f1136])).
% 138.90/18.12 fof(f34814,plain,(
% 138.90/18.12 element(apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)),d)|~sQ847_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f19268,f463])).
% 138.90/18.12 fof(f34827,definition,(
% 138.90/18.12 sQ1114_spl <=> (apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha))=zero(d))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ1114_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f34830,definition,(
% 138.90/18.12 sQ1115_spl <=> (sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)=zero(a))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ1115_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f34831,plain,(
% 138.90/18.12 sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)=zero(a)|~sQ1115_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f34830])).
% 138.90/18.12 fof(f34833,plain,(
% 138.90/18.12 ~sQ1114_spl|sQ1115_spl|~sQ847_spl|~sQ64_spl),
% 138.90/18.12 inference(split_clause,[status(thm)],[f34808,f34827,f34830,f19267,f480])).
% 138.90/18.12 fof(f34836,plain,(
% 138.90/18.12 apply(g,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=apply(gamma,apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))|~sQ817_spl|~sQ847_spl|~sQ151_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f19024,f34812])).
% 138.90/18.12 fof(f35326,plain,(
% 138.90/18.12 apply(g,subtract(b,sK0_skl(b,g),sK1_skl(b,g)))=zero(e)|~sQ86_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f5832,f20732])).
% 138.90/18.12 fof(f53823,plain,(
% 138.90/18.12 apply(alpha,zero(a))=subtract(b,sK0_skl(b,g),sK1_skl(b,g))|~sQ1115_spl|~sQ817_spl),
% 138.90/18.12 inference(backward_demodulation,[status(thm)],[f34831,f19024])).
% 138.90/18.12 fof(f53824,plain,(
% 138.90/18.12 zero(b)=subtract(b,sK0_skl(b,g),sK1_skl(b,g))|~sQ1115_spl|~sQ817_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f139,f53823])).
% 138.90/18.12 fof(f56406,plain,(
% 138.90/18.12 zero(e)=apply(gamma,apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))|~sQ86_spl|~sQ88_spl|~sQ87_spl|~sQ817_spl|~sQ847_spl|~sQ151_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f35326,f34836])).
% 138.90/18.12 fof(f56418,plain,(
% 138.90/18.12 ~apply(gamma,apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))=zero(e)|apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha))=zero(d)|~sQ847_spl|~sQ25_spl),
% 138.90/18.12 inference(resolution,[status(thm)],[f34814,f278])).
% 138.90/18.12 fof(f56437,definition,(
% 138.90/18.12 sQ1406_spl <=> (apply(gamma,apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))=zero(e))),
% 138.90/18.12 introduced(definition,[new_symbols(definition,[sQ1406_spl])],[split_symbol_definition])).
% 138.90/18.12 fof(f56439,plain,(
% 138.90/18.12 ~apply(gamma,apply(f,sK4_skl(subtract(b,sK0_skl(b,g),sK1_skl(b,g)),c,b,a,beta,alpha)))=zero(e)|sQ1406_spl),
% 138.90/18.12 inference(component_clause,[status(thm)],[f56437])).
% 138.90/18.12 fof(f56440,plain,(
% 138.90/18.12 ~sQ1406_spl|sQ1114_spl|~sQ847_spl|~sQ25_spl),
% 138.90/18.12 inference(split_clause,[status(thm)],[f56418,f56437,f34827,f19267,f277])).
% 138.90/18.12 fof(f56444,plain,(
% 138.90/18.12 ~zero(e)=zero(e)|~sQ86_spl|~sQ88_spl|~sQ87_spl|~sQ817_spl|~sQ847_spl|~sQ151_spl|sQ1406_spl),
% 138.90/18.12 inference(forward_demodulation,[status(thm)],[f56406,f56439])).
% 138.90/18.12 fof(f56445,plain,(
% 138.90/18.12 $false|~sQ86_spl|~sQ88_spl|~sQ87_spl|~sQ817_spl|~sQ847_spl|~sQ151_spl|sQ1406_spl),
% 138.90/18.12 inference(trivial_equality_resolution,[status(thm)],[f56444])).
% 138.90/18.12 fof(f56446,plain,(
% 138.90/18.12 ~sQ86_spl|~sQ88_spl|~sQ87_spl|~sQ817_spl|~sQ847_spl|~sQ151_spl|sQ1406_spl),
% 138.90/18.12 inference(contradiction_clause,[status(thm)],[f56445])).
% 138.90/18.12 fof(f56468,plain,(
% 138.90/18.12 subtract(b,sK0_skl(b,g),zero(b))=sK1_skl(b,g)|~sQ1115_spl|~sQ817_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(backward_demodulation,[status(thm)],[f53824,f7749])).
% 138.90/18.12 fof(f56489,plain,(
% 138.90/18.12 sQ298_spl|~sQ1115_spl|~sQ817_spl|~sQ88_spl|~sQ87_spl),
% 138.90/18.12 inference(split_clause,[status(thm)],[f56468,f3719,f34830,f19023,f595,f591])).
% 138.90/18.12 fof(f56707,plain,(
% 138.90/18.12 $false),
% 138.90/18.12 inference(sat_refutation,[status(thm)],[f280,f321,f483,f524,f586,f590,f594,f598,f680,f682,f684,f1138,f1146,f2322,f2609,f2611,f2969,f3053,f3564,f4305,f4359,f4600,f5152,f5155,f5308,f6070,f6077,f6080,f6099,f6101,f6103,f6105,f6107,f6196,f6891,f6997,f7026,f8727,f9221,f9410,f9535,f9537,f12415,f13393,f13422,f13534,f13560,f15244,f15389,f15454,f17209,f17211,f18078,f18146,f18782,f20362,f23232,f23480,f23492,f23562,f23643,f23701,f24549,f27668,f29196,f32505,f32506,f34694,f34833,f56440,f56446,f56489])).
% 138.90/18.22 % SZS output end CNFRefutation for theBenchmark.p
% 35.20/18.26 % Elapsed time: 17.807560 seconds
% 35.20/18.26 % CPU time: 140.548765 seconds
% 35.20/18.26 % Total memory used: 796.670 MB
% 35.20/18.26 % Net memory used: 754.896 MB
%------------------------------------------------------------------------------