%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HAL001+2 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:45:12 PM UTC 2026
% Result : Theorem 53.53s 7.10s
% Output : CNFRefutation 4.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 43
% Syntax : Number of formulae : 176 ( 43 unt; 24 def)
% Number of atoms : 498 ( 101 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 580 ( 258 ~; 256 |; 31 &)
% ( 26 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 25 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 13 con; 0-6 aty)
% Number of variables : 190 ( 184 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Morphism,Dom,Cod] :
( morphism(Morphism,Dom,Cod)
=> ( apply(Morphism,zero(Dom)) = zero(Cod)
& ! [El] :
( element(El,Dom)
=> element(apply(Morphism,El),Cod) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( ( morphism(Morphism2,CodDom,Cod)
& morphism(Morphism1,Dom,CodDom)
& exact(Morphism1,Morphism2) )
=> ! [ElCodDom] :
( ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) )
<=> ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] :
( ( morphism(M4,DomCod2,Cod)
& morphism(M3,Dom,DomCod2)
& morphism(M2,DomCod1,Cod)
& morphism(M1,Dom,DomCod1)
& commute(M1,M2,M3,M4) )
=> ! [ElDom] :
( element(ElDom,Dom)
=> apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Morphism,Dom,Cod] :
( ( morphism(Morphism,Dom,Cod)
& injection(Morphism) )
=> ! [El] :
( ( apply(Morphism,El) = zero(Cod)
& element(El,Dom) )
=> El = zero(Dom) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Morphism,Dom,Cod] :
( ( ! [El] :
( ( apply(Morphism,El) = zero(Cod)
& element(El,Dom) )
=> El = zero(Dom) )
& morphism(Morphism,Dom,Cod) )
=> injection(Morphism) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
morphism(alpha,a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
morphism(beta,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
morphism(gamma,d,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
morphism(delta,e,r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
morphism(f,a,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
morphism(g,b,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
morphism(h,c,r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
injection(gamma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
exact(alpha,beta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
commute(alpha,g,f,gamma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
commute(beta,h,g,delta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
injection(f),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
injection(h),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,conjecture,
injection(g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ injection(g),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f35,plain,
! [Morphism,Dom,Cod] :
( ( apply(Morphism,zero(Dom)) = zero(Cod)
& ! [El] :
( element(apply(Morphism,El),Cod)
| ~ element(El,Dom) ) )
| ~ morphism(Morphism,Dom,Cod) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f36,plain,
! [X0,X1,X2,X3] :
( element(apply(X0,X3),X2)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0,X1,X2] :
( apply(X0,zero(X1)) = zero(X2)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f57,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( ! [ElCodDom] :
( ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) )
<=> ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom)
| ~ exact(Morphism1,Morphism2) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f58,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( ! [ElCodDom] :
( ( ! [ElDom] :
( apply(Morphism1,ElDom) != ElCodDom
| ~ element(ElDom,Dom) )
| ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) ) )
& ( ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) )
| apply(Morphism2,ElCodDom) != zero(Cod)
| ~ element(ElCodDom,CodDom) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom)
| ~ exact(Morphism1,Morphism2) ),
inference(NNF_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( ( ! [ElCodDom] :
( ! [ElDom] :
( apply(Morphism1,ElDom) != ElCodDom
| ~ element(ElDom,Dom) )
| ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) ) )
& ! [ElCodDom] :
( ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) )
| apply(Morphism2,ElCodDom) != zero(Cod)
| ~ element(ElCodDom,CodDom) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom)
| ~ exact(Morphism1,Morphism2) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f60,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( ( ! [ElCodDom] :
( ! [ElDom] :
( apply(Morphism1,ElDom) != ElCodDom
| ~ element(ElDom,Dom) )
| ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) ) )
& ! [ElCodDom] :
( ( apply(Morphism1,sK4_skl(ElCodDom,Cod,CodDom,Dom,Morphism2,Morphism1)) = ElCodDom
& element(sK4_skl(ElCodDom,Cod,CodDom,Dom,Morphism2,Morphism1),Dom) )
| apply(Morphism2,ElCodDom) != zero(Cod)
| ~ element(ElCodDom,CodDom) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom)
| ~ exact(Morphism1,Morphism2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(ElDom,sK4_skl(ElCodDom,Cod,CodDom,Dom,Morphism2,Morphism1))],[f59]) ).
fof(f61,plain,
! [X0,X1,X2,X3,X4,X5] :
( element(sK4_skl(X5,X4,X3,X2,X1,X0),X2)
| apply(X1,X5) != zero(X4)
| ~ element(X5,X3)
| ~ morphism(X1,X3,X4)
| ~ morphism(X0,X2,X3)
| ~ exact(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1,X2,X3,X4,X5] :
( apply(X0,sK4_skl(X5,X4,X3,X2,X1,X0)) = X5
| apply(X1,X5) != zero(X4)
| ~ element(X5,X3)
| ~ morphism(X1,X3,X4)
| ~ morphism(X0,X2,X3)
| ~ exact(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f74,plain,
! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] :
( ! [ElDom] :
( apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom))
| ~ element(ElDom,Dom) )
| ~ morphism(M4,DomCod2,Cod)
| ~ morphism(M3,Dom,DomCod2)
| ~ morphism(M2,DomCod1,Cod)
| ~ morphism(M1,Dom,DomCod1)
| ~ commute(M1,M2,M3,M4) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f75,plain,
! [M1,M2,M3,M4,Dom] :
( ! [ElDom] :
( apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom))
| ~ element(ElDom,Dom) )
| ! [DomCod2,Cod] :
( ~ morphism(M4,DomCod2,Cod)
| ~ morphism(M3,Dom,DomCod2)
| ! [DomCod1] :
( ~ morphism(M2,DomCod1,Cod)
| ~ morphism(M1,Dom,DomCod1)
| ~ commute(M1,M2,M3,M4) ) ) ),
inference(miniscoping,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( apply(X1,apply(X0,X8)) = apply(X3,apply(X2,X8))
| ~ element(X8,X4)
| ~ morphism(X3,X7,X6)
| ~ morphism(X2,X4,X7)
| ~ morphism(X1,X5,X6)
| ~ morphism(X0,X4,X5)
| ~ commute(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f90,plain,
! [Morphism,Dom,Cod] :
( ! [El] :
( El = zero(Dom)
| apply(Morphism,El) != zero(Cod)
| ~ element(El,Dom) )
| ~ morphism(Morphism,Dom,Cod)
| ~ injection(Morphism) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( X3 = zero(X1)
| apply(X0,X3) != zero(X2)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2)
| ~ injection(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [Morphism,Dom,Cod] :
( injection(Morphism)
| ? [El] :
( El != zero(Dom)
& apply(Morphism,El) = zero(Cod)
& element(El,Dom) )
| ~ morphism(Morphism,Dom,Cod) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f93,plain,
! [Morphism] :
( injection(Morphism)
| ! [Dom,Cod] :
( ? [El] :
( El != zero(Dom)
& apply(Morphism,El) = zero(Cod)
& element(El,Dom) )
| ~ morphism(Morphism,Dom,Cod) ) ),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f94,plain,
! [Morphism] :
( injection(Morphism)
| ! [Dom,Cod] :
( ( sK8_skl(Cod,Dom,Morphism) != zero(Dom)
& apply(Morphism,sK8_skl(Cod,Dom,Morphism)) = zero(Cod)
& element(sK8_skl(Cod,Dom,Morphism),Dom) )
| ~ morphism(Morphism,Dom,Cod) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(El,sK8_skl(Cod,Dom,Morphism))],[f93]) ).
fof(f95,plain,
! [X0,X1,X2] :
( injection(X0)
| element(sK8_skl(X2,X1,X0),X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
! [X0,X1,X2] :
( injection(X0)
| apply(X0,sK8_skl(X2,X1,X0)) = zero(X2)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f97,plain,
! [X0,X1,X2] :
( injection(X0)
| sK8_skl(X2,X1,X0) != zero(X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
morphism(alpha,a,b),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f99,plain,
morphism(beta,b,c),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f100,plain,
morphism(gamma,d,e),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f101,plain,
morphism(delta,e,r),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f102,plain,
morphism(f,a,d),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f103,plain,
morphism(g,b,e),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f104,plain,
morphism(h,c,r),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f106,plain,
injection(gamma),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f109,plain,
exact(alpha,beta),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f111,plain,
commute(alpha,g,f,gamma),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f112,plain,
commute(beta,h,g,delta),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f113,plain,
injection(f),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f114,plain,
injection(h),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f115,plain,
~ injection(g),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f125,plain,
apply(alpha,zero(a)) = zero(b),
inference(resolution,[status(thm)],[f37,f98]) ).
fof(f127,plain,
apply(delta,zero(e)) = zero(r),
inference(resolution,[status(thm)],[f101,f37]) ).
fof(f163,definition,
( sQ4_spl
<=> injection(g) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( ~ sQ4_spl
| injection(g) ),
inference(component_clause,[status(thm)],[f163]) ).
fof(f202,definition,
( sQ11_spl
<=> injection(gamma) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f204,plain,
( sQ11_spl
| ~ injection(gamma) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f210,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f204,f106]) ).
fof(f211,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f210]) ).
fof(f247,definition,
( sQ18_spl
<=> injection(f) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( sQ18_spl
| ~ injection(f) ),
inference(component_clause,[status(thm)],[f247]) ).
fof(f255,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f249,f113]) ).
fof(f256,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f255]) ).
fof(f268,definition,
( sQ21_spl
<=> injection(h) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f270,plain,
( sQ21_spl
| ~ injection(h) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f276,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f270,f114]) ).
fof(f277,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f276]) ).
fof(f280,plain,
! [X0,X1] :
( sK8_skl(X1,X0,g) != zero(X0)
| ~ morphism(g,X0,X1) ),
inference(resolution,[status(thm)],[f97,f115]) ).
fof(f287,plain,
sK8_skl(e,b,g) != zero(b),
inference(resolution,[status(thm)],[f280,f103]) ).
fof(f346,plain,
! [X0,X1] :
( apply(g,sK8_skl(X1,X0,g)) = zero(X1)
| ~ morphism(g,X0,X1) ),
inference(resolution,[status(thm)],[f96,f115]) ).
fof(f372,plain,
apply(g,sK8_skl(e,b,g)) = zero(e),
inference(resolution,[status(thm)],[f346,f103]) ).
fof(f386,plain,
! [X0,X1,X2,X3] :
( apply(alpha,sK4_skl(X3,X2,X1,X0,beta,alpha)) = X3
| apply(beta,X3) != zero(X2)
| ~ element(X3,X1)
| ~ morphism(beta,X1,X2)
| ~ morphism(alpha,X0,X1) ),
inference(resolution,[status(thm)],[f62,f109]) ).
fof(f388,definition,
( sQ36_spl
<=> element(sK8_skl(e,b,g),b) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( ~ sQ36_spl
| element(sK8_skl(e,b,g),b) ),
inference(component_clause,[status(thm)],[f388]) ).
fof(f390,plain,
( sQ36_spl
| ~ element(sK8_skl(e,b,g),b) ),
inference(component_clause,[status(thm)],[f388]) ).
fof(f392,plain,
( sQ36_spl
| injection(g)
| ~ morphism(g,b,e) ),
inference(resolution,[status(thm)],[f390,f95]) ).
fof(f394,definition,
( sQ37_spl
<=> morphism(g,b,e) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( sQ37_spl
| ~ morphism(g,b,e) ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f397,plain,
( sQ36_spl
| sQ4_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f392,f394,f163,f388]) ).
fof(f398,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f164,f115]) ).
fof(f399,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f398]) ).
fof(f400,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f396,f103]) ).
fof(f401,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f400]) ).
fof(f429,definition,
! [X1] :
( sQ43_spl
<=> ( X1 = zero(c)
| apply(h,X1) != zero(r)
| ~ element(X1,c) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f430,plain,
! [X0] :
( ~ sQ43_spl
| X0 = zero(c)
| apply(h,X0) != zero(r)
| ~ element(X0,c) ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f437,definition,
( sQ44_spl
<=> morphism(beta,b,c) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ44_spl
| ~ morphism(beta,b,c) ),
inference(component_clause,[status(thm)],[f437]) ).
fof(f441,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f99]) ).
fof(f442,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f441]) ).
fof(f473,definition,
( sQ48_spl
<=> apply(beta,sK8_skl(e,b,g)) = zero(c) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f654,plain,
! [X0,X1,X2,X3,X4] :
( apply(h,apply(beta,X4)) = apply(delta,apply(g,X4))
| ~ element(X4,X0)
| ~ morphism(delta,X3,X2)
| ~ morphism(g,X0,X3)
| ~ morphism(h,X1,X2)
| ~ morphism(beta,X0,X1) ),
inference(resolution,[status(thm)],[f76,f112]) ).
fof(f655,plain,
! [X0,X1,X2,X3,X4] :
( apply(g,apply(alpha,X4)) = apply(gamma,apply(f,X4))
| ~ element(X4,X0)
| ~ morphism(gamma,X3,X2)
| ~ morphism(f,X0,X3)
| ~ morphism(g,X1,X2)
| ~ morphism(alpha,X0,X1) ),
inference(resolution,[status(thm)],[f76,f111]) ).
fof(f781,plain,
! [X0] :
( X0 = zero(c)
| apply(h,X0) != zero(r)
| ~ element(X0,c)
| ~ injection(h) ),
inference(resolution,[status(thm)],[f91,f104]) ).
fof(f783,plain,
! [X0] :
( X0 = zero(a)
| apply(f,X0) != zero(d)
| ~ element(X0,a)
| ~ injection(f) ),
inference(resolution,[status(thm)],[f91,f102]) ).
fof(f784,plain,
! [X0] :
( X0 = zero(d)
| apply(gamma,X0) != zero(e)
| ~ element(X0,d)
| ~ injection(gamma) ),
inference(resolution,[status(thm)],[f91,f100]) ).
fof(f791,plain,
( sQ43_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f781,f268,f429]) ).
fof(f793,definition,
! [X0] :
( sQ81_spl
<=> ( X0 = zero(a)
| apply(f,X0) != zero(d)
| ~ element(X0,a) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f794,plain,
! [X0] :
( ~ sQ81_spl
| X0 = zero(a)
| apply(f,X0) != zero(d)
| ~ element(X0,a) ),
inference(component_clause,[status(thm)],[f793]) ).
fof(f796,plain,
( sQ81_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f783,f247,f793]) ).
fof(f797,definition,
! [X0] :
( sQ82_spl
<=> ( X0 = zero(d)
| apply(gamma,X0) != zero(e)
| ~ element(X0,d) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f798,plain,
! [X0] :
( ~ sQ82_spl
| X0 = zero(d)
| apply(gamma,X0) != zero(e)
| ~ element(X0,d) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f800,plain,
( sQ82_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f784,f202,f797]) ).
fof(f1327,plain,
! [X0,X1] :
( apply(alpha,sK4_skl(X1,X0,b,a,beta,alpha)) = X1
| apply(beta,X1) != zero(X0)
| ~ element(X1,b)
| ~ morphism(beta,b,X0) ),
inference(resolution,[status(thm)],[f386,f98]) ).
fof(f1432,definition,
( sQ128_spl
<=> morphism(h,c,r) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( sQ128_spl
| ~ morphism(h,c,r) ),
inference(component_clause,[status(thm)],[f1432]) ).
fof(f1436,plain,
( sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1434,f104]) ).
fof(f1437,plain,
sQ128_spl,
inference(contradiction_clause,[status(thm)],[f1436]) ).
fof(f1638,plain,
! [X0,X1,X2] :
( apply(h,apply(beta,X2)) = apply(delta,apply(g,X2))
| ~ element(X2,b)
| ~ morphism(delta,X1,X0)
| ~ morphism(g,b,X1)
| ~ morphism(h,c,X0) ),
inference(resolution,[status(thm)],[f654,f99]) ).
fof(f1639,definition,
! [X0,X1] :
( sQ141_spl
<=> ( ~ morphism(delta,X1,X0)
| ~ morphism(g,b,X1)
| ~ morphism(h,c,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1640,plain,
! [X0,X1] :
( ~ sQ141_spl
| ~ morphism(delta,X1,X0)
| ~ morphism(g,b,X1)
| ~ morphism(h,c,X0) ),
inference(component_clause,[status(thm)],[f1639]) ).
fof(f1642,definition,
! [X2] :
( sQ142_spl
<=> ( apply(h,apply(beta,X2)) = apply(delta,apply(g,X2))
| ~ element(X2,b) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1643,plain,
! [X0] :
( ~ sQ142_spl
| apply(h,apply(beta,X0)) = apply(delta,apply(g,X0))
| ~ element(X0,b) ),
inference(component_clause,[status(thm)],[f1642]) ).
fof(f1645,plain,
( sQ142_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f1638,f1639,f1642]) ).
fof(f1646,plain,
! [X0,X1,X2] :
( apply(g,apply(alpha,X2)) = apply(gamma,apply(f,X2))
| ~ element(X2,a)
| ~ morphism(gamma,X1,X0)
| ~ morphism(f,a,X1)
| ~ morphism(g,b,X0) ),
inference(resolution,[status(thm)],[f655,f98]) ).
fof(f1647,definition,
! [X0,X1] :
( sQ143_spl
<=> ( ~ morphism(gamma,X1,X0)
| ~ morphism(f,a,X1)
| ~ morphism(g,b,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1648,plain,
! [X0,X1] :
( ~ sQ143_spl
| ~ morphism(gamma,X1,X0)
| ~ morphism(f,a,X1)
| ~ morphism(g,b,X0) ),
inference(component_clause,[status(thm)],[f1647]) ).
fof(f1650,definition,
! [X2] :
( sQ144_spl
<=> ( apply(g,apply(alpha,X2)) = apply(gamma,apply(f,X2))
| ~ element(X2,a) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1651,plain,
! [X0] :
( ~ sQ144_spl
| apply(g,apply(alpha,X0)) = apply(gamma,apply(f,X0))
| ~ element(X0,a) ),
inference(component_clause,[status(thm)],[f1650]) ).
fof(f1653,plain,
( sQ144_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f1646,f1647,f1650]) ).
fof(f2058,plain,
! [X0] :
( ~ sQ141_spl
| ~ morphism(delta,e,X0)
| ~ morphism(h,c,X0) ),
inference(resolution,[status(thm)],[f1640,f103]) ).
fof(f2059,plain,
( ~ sQ141_spl
| ~ morphism(h,c,r) ),
inference(resolution,[status(thm)],[f2058,f101]) ).
fof(f2060,plain,
( ~ sQ141_spl
| ~ sQ128_spl ),
inference(split_clause,[status(thm)],[f2059,f1432,f1639]) ).
fof(f2061,plain,
! [X0] :
( ~ sQ143_spl
| ~ morphism(gamma,d,X0)
| ~ morphism(g,b,X0) ),
inference(resolution,[status(thm)],[f1648,f102]) ).
fof(f2062,plain,
( ~ sQ143_spl
| ~ morphism(g,b,e) ),
inference(resolution,[status(thm)],[f2061,f100]) ).
fof(f2063,plain,
( ~ sQ143_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f2062,f394,f1647]) ).
fof(f2591,definition,
( sQ217_spl
<=> morphism(alpha,a,b) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f2593,plain,
( sQ217_spl
| ~ morphism(alpha,a,b) ),
inference(component_clause,[status(thm)],[f2591]) ).
fof(f2595,plain,
( sQ217_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2593,f98]) ).
fof(f2596,plain,
sQ217_spl,
inference(contradiction_clause,[status(thm)],[f2595]) ).
fof(f4367,plain,
( ~ sQ36_spl
| ~ sQ142_spl
| apply(h,apply(beta,sK8_skl(e,b,g))) = apply(delta,apply(g,sK8_skl(e,b,g))) ),
inference(resolution,[status(thm)],[f1643,f389]) ).
fof(f4379,plain,
( ~ sQ36_spl
| ~ sQ142_spl
| apply(h,apply(beta,sK8_skl(e,b,g))) = apply(delta,zero(e)) ),
inference(forward_demodulation,[status(thm)],[f372,f4367]) ).
fof(f4380,plain,
( ~ sQ36_spl
| ~ sQ142_spl
| apply(h,apply(beta,sK8_skl(e,b,g))) = zero(r) ),
inference(forward_demodulation,[status(thm)],[f127,f4379]) ).
fof(f4382,plain,
( ~ sQ43_spl
| ~ sQ36_spl
| ~ sQ142_spl
| apply(beta,sK8_skl(e,b,g)) = zero(c)
| ~ element(apply(beta,sK8_skl(e,b,g)),c) ),
inference(resolution,[status(thm)],[f4380,f430]) ).
fof(f4388,definition,
( sQ348_spl
<=> element(apply(beta,sK8_skl(e,b,g)),c) ),
introduced(definition,[new_symbols(definition,[sQ348_spl])],[split_symbol_definition]) ).
fof(f4390,plain,
( sQ348_spl
| ~ element(apply(beta,sK8_skl(e,b,g)),c) ),
inference(component_clause,[status(thm)],[f4388]) ).
fof(f4391,plain,
( ~ sQ43_spl
| ~ sQ36_spl
| ~ sQ142_spl
| sQ48_spl
| ~ sQ348_spl ),
inference(split_clause,[status(thm)],[f4382,f4388,f473,f1642,f388,f429]) ).
fof(f4399,plain,
! [X0] :
( sQ348_spl
| ~ element(sK8_skl(e,b,g),X0)
| ~ morphism(beta,X0,c) ),
inference(resolution,[status(thm)],[f4390,f36]) ).
fof(f4420,plain,
( sQ348_spl
| ~ element(sK8_skl(e,b,g),b) ),
inference(resolution,[status(thm)],[f4399,f99]) ).
fof(f4421,plain,
( sQ348_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f4420,f388,f4388]) ).
fof(f5426,plain,
! [X0] :
( apply(alpha,sK4_skl(X0,c,b,a,beta,alpha)) = X0
| apply(beta,X0) != zero(c)
| ~ element(X0,b) ),
inference(resolution,[status(thm)],[f1327,f99]) ).
fof(f14284,plain,
( ~ sQ36_spl
| apply(alpha,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)) = sK8_skl(e,b,g)
| apply(beta,sK8_skl(e,b,g)) != zero(c) ),
inference(resolution,[status(thm)],[f5426,f389]) ).
fof(f14312,definition,
( sQ658_spl
<=> apply(alpha,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)) = sK8_skl(e,b,g) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f14313,plain,
( ~ sQ658_spl
| apply(alpha,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)) = sK8_skl(e,b,g) ),
inference(component_clause,[status(thm)],[f14312]) ).
fof(f14315,plain,
( ~ sQ36_spl
| sQ658_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f14284,f473,f14312,f388]) ).
fof(f14418,definition,
( sQ682_spl
<=> exact(alpha,beta) ),
introduced(definition,[new_symbols(definition,[sQ682_spl])],[split_symbol_definition]) ).
fof(f14420,plain,
( sQ682_spl
| ~ exact(alpha,beta) ),
inference(component_clause,[status(thm)],[f14418]) ).
fof(f14422,plain,
( sQ682_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14420,f109]) ).
fof(f14423,plain,
sQ682_spl,
inference(contradiction_clause,[status(thm)],[f14422]) ).
fof(f19228,definition,
( sQ856_spl
<=> element(sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha),a) ),
introduced(definition,[new_symbols(definition,[sQ856_spl])],[split_symbol_definition]) ).
fof(f19229,plain,
( ~ sQ856_spl
| element(sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha),a) ),
inference(component_clause,[status(thm)],[f19228]) ).
fof(f19230,plain,
( sQ856_spl
| ~ element(sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha),a) ),
inference(component_clause,[status(thm)],[f19228]) ).
fof(f19246,plain,
( sQ856_spl
| apply(beta,sK8_skl(e,b,g)) != zero(c)
| ~ element(sK8_skl(e,b,g),b)
| ~ morphism(beta,b,c)
| ~ morphism(alpha,a,b)
| ~ exact(alpha,beta) ),
inference(resolution,[status(thm)],[f19230,f61]) ).
fof(f19248,plain,
( sQ856_spl
| ~ sQ48_spl
| ~ sQ36_spl
| ~ sQ44_spl
| ~ sQ217_spl
| ~ sQ682_spl ),
inference(split_clause,[status(thm)],[f19246,f14418,f2591,f437,f388,f473,f19228]) ).
fof(f19257,plain,
( ~ sQ144_spl
| ~ sQ856_spl
| apply(g,apply(alpha,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha))) = apply(gamma,apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha))) ),
inference(resolution,[status(thm)],[f19229,f1651]) ).
fof(f19260,plain,
( ~ sQ81_spl
| ~ sQ856_spl
| sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha) = zero(a)
| apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)) != zero(d) ),
inference(resolution,[status(thm)],[f19229,f794]) ).
fof(f19289,plain,
( ~ sQ144_spl
| ~ sQ856_spl
| ~ sQ658_spl
| apply(g,sK8_skl(e,b,g)) = apply(gamma,apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha))) ),
inference(forward_demodulation,[status(thm)],[f14313,f19257]) ).
fof(f19290,plain,
( ~ sQ144_spl
| ~ sQ856_spl
| ~ sQ658_spl
| zero(e) = apply(gamma,apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha))) ),
inference(forward_demodulation,[status(thm)],[f372,f19289]) ).
fof(f19291,definition,
( sQ860_spl
<=> apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)) = zero(d) ),
introduced(definition,[new_symbols(definition,[sQ860_spl])],[split_symbol_definition]) ).
fof(f19294,definition,
( sQ861_spl
<=> sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha) = zero(a) ),
introduced(definition,[new_symbols(definition,[sQ861_spl])],[split_symbol_definition]) ).
fof(f19295,plain,
( ~ sQ861_spl
| sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha) = zero(a) ),
inference(component_clause,[status(thm)],[f19294]) ).
fof(f19297,plain,
( ~ sQ81_spl
| ~ sQ856_spl
| sQ861_spl
| ~ sQ860_spl ),
inference(split_clause,[status(thm)],[f19260,f19291,f19294,f19228,f793]) ).
fof(f19304,plain,
( ~ sQ658_spl
| ~ sQ861_spl
| apply(alpha,zero(a)) = sK8_skl(e,b,g) ),
inference(backward_demodulation,[status(thm)],[f19295,f14313]) ).
fof(f19308,plain,
( ~ sQ658_spl
| ~ sQ861_spl
| zero(b) = sK8_skl(e,b,g) ),
inference(forward_demodulation,[status(thm)],[f125,f19304]) ).
fof(f19309,plain,
( ~ sQ658_spl
| ~ sQ861_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19308,f287]) ).
fof(f19310,plain,
( ~ sQ658_spl
| ~ sQ861_spl ),
inference(contradiction_clause,[status(thm)],[f19309]) ).
fof(f20474,plain,
( ~ sQ82_spl
| ~ sQ144_spl
| ~ sQ856_spl
| ~ sQ658_spl
| apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)) = zero(d)
| ~ element(apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)),d) ),
inference(resolution,[status(thm)],[f19290,f798]) ).
fof(f20481,definition,
( sQ918_spl
<=> element(apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)),d) ),
introduced(definition,[new_symbols(definition,[sQ918_spl])],[split_symbol_definition]) ).
fof(f20483,plain,
( sQ918_spl
| ~ element(apply(f,sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha)),d) ),
inference(component_clause,[status(thm)],[f20481]) ).
fof(f20484,plain,
( ~ sQ82_spl
| ~ sQ144_spl
| ~ sQ856_spl
| ~ sQ658_spl
| sQ860_spl
| ~ sQ918_spl ),
inference(split_clause,[status(thm)],[f20474,f20481,f19291,f14312,f19228,f1650,f797]) ).
fof(f20562,plain,
! [X0] :
( sQ918_spl
| ~ element(sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha),X0)
| ~ morphism(f,X0,d) ),
inference(resolution,[status(thm)],[f20483,f36]) ).
fof(f20613,plain,
( sQ918_spl
| ~ element(sK4_skl(sK8_skl(e,b,g),c,b,a,beta,alpha),a) ),
inference(resolution,[status(thm)],[f20562,f102]) ).
fof(f20614,plain,
( sQ918_spl
| ~ sQ856_spl ),
inference(split_clause,[status(thm)],[f20613,f19228,f20481]) ).
fof(f20615,plain,
$false,
inference(sat_refutation,[status(thm)],[f211,f256,f277,f397,f399,f401,f442,f791,f796,f800,f1437,f1645,f1653,f2060,f2063,f2596,f4391,f4421,f14315,f14423,f19248,f19297,f19310,f20484,f20614]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : HAL001+2 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sun Sep 20 20:43:52 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 53.53/7.10 % Refutation found
% 53.53/7.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 53.53/7.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.18/7.86 % Elapsed time: 7.551543 seconds
% 4.18/7.86 % CPU time: 55.414077 seconds
% 4.18/7.86 % Total memory used: 581.951 MB
% 4.18/7.86 % Net memory used: 521.280 MB
%------------------------------------------------------------------------------