%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HAL007+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Satisfiable 0.08s 0.36s
% Output : Saturation 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [Morphism,Dom,Cod] :
( ( morphism(Morphism,Dom,Cod)
& injection(Morphism) )
=> ! [El1,El2] :
( ( apply(Morphism,El1) = apply(Morphism,El2)
& element(El2,Dom)
& element(El1,Dom) )
=> El1 = El2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [Morphism,Dom,Cod] :
( ( ! [El1,El2] :
( ( apply(Morphism,El1) = apply(Morphism,El2)
& element(El2,Dom)
& element(El1,Dom) )
=> El1 = El2 )
& morphism(Morphism,Dom,Cod) )
=> injection(Morphism) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [Morphism,Dom,Cod] :
( ( morphism(Morphism,Dom,Cod)
& surjection(Morphism) )
=> ! [ElCod] :
( element(ElCod,Cod)
=> ? [ElDom] :
( apply(Morphism,ElDom) = ElCod
& element(ElDom,Dom) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [Morphism,Dom,Cod] :
( ( ! [ElCod] :
( element(ElCod,Cod)
=> ? [ElDom] :
( apply(Morphism,ElDom) = ElCod
& element(ElDom,Dom) ) )
& morphism(Morphism,Dom,Cod) )
=> surjection(Morphism) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [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) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] :
( ( ! [ElDom] :
( element(ElDom,Dom)
=> apply(M2,apply(M1,ElDom)) = apply(M4,apply(M3,ElDom)) )
& morphism(M4,DomCod2,Cod)
& morphism(M3,Dom,DomCod2)
& morphism(M2,DomCod1,Cod)
& morphism(M1,Dom,DomCod1) )
=> commute(M1,M2,M3,M4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Dom,El1,El2] :
( ( element(El2,Dom)
& element(El1,Dom) )
=> element(subtract(Dom,El1,El2),Dom) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Dom,El] :
( element(El,Dom)
=> subtract(Dom,El,El) = zero(Dom) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Dom,El1,El2] :
( ( element(El2,Dom)
& element(El1,Dom) )
=> subtract(Dom,El1,subtract(Dom,El1,El2)) = El2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Morphism,Dom,Cod] :
( morphism(Morphism,Dom,Cod)
=> ! [El1,El2] :
( ( element(El2,Dom)
& element(El1,Dom) )
=> apply(Morphism,subtract(Dom,El1,El2)) = subtract(Cod,apply(Morphism,El1),apply(Morphism,El2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,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(f15,plain,
! [X0,X1,X2,X3] :
( element(apply(X0,X3),X2)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f16,plain,
! [X0,X1,X2] :
( apply(X0,zero(X1)) = zero(X2)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f17,plain,
! [Morphism,Dom,Cod] :
( ! [El1,El2] :
( El1 = El2
| apply(Morphism,El1) != apply(Morphism,El2)
| ~ element(El2,Dom)
| ~ element(El1,Dom) )
| ~ morphism(Morphism,Dom,Cod)
| ~ injection(Morphism) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [Morphism,Dom] :
( ! [El1,El2] :
( El1 = El2
| apply(Morphism,El1) != apply(Morphism,El2)
| ~ element(El2,Dom)
| ~ element(El1,Dom) )
| ! [Cod] : ~ morphism(Morphism,Dom,Cod)
| ~ injection(Morphism) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f19,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| apply(X0,X3) != apply(X0,X4)
| ~ element(X4,X1)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2)
| ~ injection(X0) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f20,plain,
! [Morphism,Dom,Cod] :
( injection(Morphism)
| ? [El1,El2] :
( El1 != El2
& apply(Morphism,El1) = apply(Morphism,El2)
& element(El2,Dom)
& element(El1,Dom) )
| ~ morphism(Morphism,Dom,Cod) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f21,plain,
! [Morphism] :
( injection(Morphism)
| ! [Dom] :
( ? [El1,El2] :
( El1 != El2
& apply(Morphism,El1) = apply(Morphism,El2)
& element(El2,Dom)
& element(El1,Dom) )
| ! [Cod] : ~ morphism(Morphism,Dom,Cod) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f22,plain,
! [Morphism] :
( injection(Morphism)
| ! [Dom] :
( ( sK0_skl(Dom,Morphism) != sK1_skl(Dom,Morphism)
& apply(Morphism,sK0_skl(Dom,Morphism)) = apply(Morphism,sK1_skl(Dom,Morphism))
& element(sK1_skl(Dom,Morphism),Dom)
& element(sK0_skl(Dom,Morphism),Dom) )
| ! [Cod] : ~ morphism(Morphism,Dom,Cod) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(El1,sK0_skl(Dom,Morphism)),skolemize(El2,sK1_skl(Dom,Morphism))],[f21]) ).
fof(f23,plain,
! [X0,X1,X2] :
( injection(X0)
| element(sK0_skl(X1,X0),X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X0,X1,X2] :
( injection(X0)
| element(sK1_skl(X1,X0),X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f25,plain,
! [X0,X1,X2] :
( injection(X0)
| apply(X0,sK0_skl(X1,X0)) = apply(X0,sK1_skl(X1,X0))
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f26,plain,
! [X0,X1,X2] :
( injection(X0)
| sK0_skl(X1,X0) != sK1_skl(X1,X0)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f27,plain,
! [Morphism,Dom,Cod] :
( ! [ElCod] :
( ? [ElDom] :
( apply(Morphism,ElDom) = ElCod
& element(ElDom,Dom) )
| ~ element(ElCod,Cod) )
| ~ morphism(Morphism,Dom,Cod)
| ~ surjection(Morphism) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f28,plain,
! [Morphism,Dom,Cod] :
( ! [ElCod] :
( ( apply(Morphism,sK2_skl(ElCod,Cod,Dom,Morphism)) = ElCod
& element(sK2_skl(ElCod,Cod,Dom,Morphism),Dom) )
| ~ element(ElCod,Cod) )
| ~ morphism(Morphism,Dom,Cod)
| ~ surjection(Morphism) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(ElDom,sK2_skl(ElCod,Cod,Dom,Morphism))],[f27]) ).
fof(f29,plain,
! [X0,X1,X2,X3] :
( element(sK2_skl(X3,X2,X1,X0),X1)
| ~ element(X3,X2)
| ~ morphism(X0,X1,X2)
| ~ surjection(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( apply(X0,sK2_skl(X3,X2,X1,X0)) = X3
| ~ element(X3,X2)
| ~ morphism(X0,X1,X2)
| ~ surjection(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f31,plain,
! [Morphism,Dom,Cod] :
( surjection(Morphism)
| ? [ElCod] :
( ! [ElDom] :
( apply(Morphism,ElDom) != ElCod
| ~ element(ElDom,Dom) )
& element(ElCod,Cod) )
| ~ morphism(Morphism,Dom,Cod) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f32,plain,
! [Morphism] :
( surjection(Morphism)
| ! [Dom,Cod] :
( ? [ElCod] :
( ! [ElDom] :
( apply(Morphism,ElDom) != ElCod
| ~ element(ElDom,Dom) )
& element(ElCod,Cod) )
| ~ morphism(Morphism,Dom,Cod) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f33,plain,
! [Morphism] :
( surjection(Morphism)
| ! [Dom,Cod] :
( ( ! [ElDom] :
( apply(Morphism,ElDom) != sK3_skl(Cod,Dom,Morphism)
| ~ element(ElDom,Dom) )
& element(sK3_skl(Cod,Dom,Morphism),Cod) )
| ~ morphism(Morphism,Dom,Cod) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(ElCod,sK3_skl(Cod,Dom,Morphism))],[f32]) ).
fof(f34,plain,
! [X0,X1,X2] :
( surjection(X0)
| element(sK3_skl(X2,X1,X0),X2)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1,X2,X3] :
( surjection(X0)
| apply(X0,X3) != sK3_skl(X2,X1,X0)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f36,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(f37,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)],[f36]) ).
fof(f38,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)],[f37]) ).
fof(f39,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))],[f38]) ).
fof(f40,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)],[f39]) ).
fof(f41,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)],[f39]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( apply(X0,X6) != X5
| ~ element(X6,X2)
| apply(X1,X5) = zero(X4)
| ~ morphism(X1,X3,X4)
| ~ morphism(X0,X2,X3)
| ~ exact(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f44,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( exact(Morphism1,Morphism2)
| ? [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) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f45,definition,
! [Morphism2,CodDom,Cod,ElCodDom] :
( sP0_prd(ElCodDom,Cod,CodDom,Morphism2)
<=> ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f46,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( exact(Morphism1,Morphism2)
| ? [ElCodDom] :
( sP0_prd(ElCodDom,Cod,CodDom,Morphism2)
<~> ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom) ),
inference(formula_renaming,[status(thm)],[f44,f45]) ).
fof(f47,plain,
! [Morphism1,Morphism2,Dom,CodDom,Cod] :
( exact(Morphism1,Morphism2)
| ? [ElCodDom] :
( ( ! [ElDom] :
( apply(Morphism1,ElDom) != ElCodDom
| ~ element(ElDom,Dom) )
| ~ sP0_prd(ElCodDom,Cod,CodDom,Morphism2) )
& ( ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) )
| sP0_prd(ElCodDom,Cod,CodDom,Morphism2) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
! [Morphism1,Morphism2] :
( exact(Morphism1,Morphism2)
| ! [Dom,CodDom,Cod] :
( ? [ElCodDom] :
( ( ! [ElDom] :
( apply(Morphism1,ElDom) != ElCodDom
| ~ element(ElDom,Dom) )
| ~ sP0_prd(ElCodDom,Cod,CodDom,Morphism2) )
& ( ? [ElDom] :
( apply(Morphism1,ElDom) = ElCodDom
& element(ElDom,Dom) )
| sP0_prd(ElCodDom,Cod,CodDom,Morphism2) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom) ) ),
inference(miniscoping,[status(thm)],[f47]) ).
fof(f49,plain,
! [Morphism1,Morphism2] :
( exact(Morphism1,Morphism2)
| ! [Dom,CodDom,Cod] :
( ( ( ! [ElDom] :
( apply(Morphism1,ElDom) != sK5_skl(Cod,CodDom,Dom,Morphism2,Morphism1)
| ~ element(ElDom,Dom) )
| ~ sP0_prd(sK5_skl(Cod,CodDom,Dom,Morphism2,Morphism1),Cod,CodDom,Morphism2) )
& ( ( apply(Morphism1,sK6_skl(Cod,CodDom,Dom,Morphism2,Morphism1)) = sK5_skl(Cod,CodDom,Dom,Morphism2,Morphism1)
& element(sK6_skl(Cod,CodDom,Dom,Morphism2,Morphism1),Dom) )
| sP0_prd(sK5_skl(Cod,CodDom,Dom,Morphism2,Morphism1),Cod,CodDom,Morphism2) ) )
| ~ morphism(Morphism2,CodDom,Cod)
| ~ morphism(Morphism1,Dom,CodDom) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(ElCodDom,sK5_skl(Cod,CodDom,Dom,Morphism2,Morphism1)),skolemize(ElDom,sK6_skl(Cod,CodDom,Dom,Morphism2,Morphism1))],[f48]) ).
fof(f50,plain,
! [X0,X1,X2,X3,X4] :
( exact(X0,X3)
| element(sK6_skl(X4,X2,X1,X3,X0),X1)
| sP0_prd(sK5_skl(X4,X2,X1,X3,X0),X4,X2,X3)
| ~ morphism(X3,X2,X4)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2,X3,X4] :
( exact(X0,X3)
| apply(X0,sK6_skl(X4,X2,X1,X3,X0)) = sK5_skl(X4,X2,X1,X3,X0)
| sP0_prd(sK5_skl(X4,X2,X1,X3,X0),X4,X2,X3)
| ~ morphism(X3,X2,X4)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f52,plain,
! [X0,X1,X2,X3,X4,X5] :
( exact(X0,X3)
| apply(X0,X5) != sK5_skl(X4,X2,X1,X3,X0)
| ~ element(X5,X1)
| ~ sP0_prd(sK5_skl(X4,X2,X1,X3,X0),X4,X2,X3)
| ~ morphism(X3,X2,X4)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f53,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(f54,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)],[f53]) ).
fof(f55,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)],[f54]) ).
fof(f56,plain,
! [M1,M2,M3,M4,Dom,DomCod1,DomCod2,Cod] :
( commute(M1,M2,M3,M4)
| ? [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) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f57,plain,
! [M1,M2,M3,M4] :
( commute(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) ) ) ) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f58,plain,
! [M1,M2,M3,M4] :
( commute(M1,M2,M3,M4)
| ! [Dom] :
( ( apply(M2,apply(M1,sK7_skl(Dom,M4,M3,M2,M1))) != apply(M4,apply(M3,sK7_skl(Dom,M4,M3,M2,M1)))
& element(sK7_skl(Dom,M4,M3,M2,M1),Dom) )
| ! [DomCod2,Cod] :
( ~ morphism(M4,DomCod2,Cod)
| ~ morphism(M3,Dom,DomCod2)
| ! [DomCod1] :
( ~ morphism(M2,DomCod1,Cod)
| ~ morphism(M1,Dom,DomCod1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(ElDom,sK7_skl(Dom,M4,M3,M2,M1))],[f57]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( commute(X0,X3,X5,X7)
| element(sK7_skl(X1,X7,X5,X3,X0),X1)
| ~ morphism(X7,X6,X4)
| ~ morphism(X5,X1,X6)
| ~ morphism(X3,X2,X4)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( commute(X0,X3,X5,X7)
| apply(X3,apply(X0,sK7_skl(X1,X7,X5,X3,X0))) != apply(X7,apply(X5,sK7_skl(X1,X7,X5,X3,X0)))
| ~ morphism(X7,X6,X4)
| ~ morphism(X5,X1,X6)
| ~ morphism(X3,X2,X4)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f61,plain,
! [Dom,El1,El2] :
( element(subtract(Dom,El1,El2),Dom)
| ~ element(El2,Dom)
| ~ element(El1,Dom) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f62,plain,
! [X0,X1,X2] :
( element(subtract(X1,X0,X2),X1)
| ~ element(X2,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [Dom,El] :
( subtract(Dom,El,El) = zero(Dom)
| ~ element(El,Dom) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f64,plain,
! [X0,X1] :
( subtract(X1,X0,X0) = zero(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [Dom,El1,El2] :
( subtract(Dom,El1,subtract(Dom,El1,El2)) = El2
| ~ element(El2,Dom)
| ~ element(El1,Dom) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f66,plain,
! [X0,X1,X2] :
( subtract(X1,X0,subtract(X1,X0,X2)) = X2
| ~ element(X2,X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [Morphism,Dom,Cod] :
( ! [El1,El2] :
( apply(Morphism,subtract(Dom,El1,El2)) = subtract(Cod,apply(Morphism,El1),apply(Morphism,El2))
| ~ element(El2,Dom)
| ~ element(El1,Dom) )
| ~ morphism(Morphism,Dom,Cod) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f68,plain,
! [X0,X1,X2,X3,X4] :
( apply(X0,subtract(X1,X3,X4)) = subtract(X2,apply(X0,X3),apply(X0,X4))
| ~ element(X4,X1)
| ~ element(X3,X1)
| ~ morphism(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [Morphism2,CodDom,Cod,ElCodDom] :
( ( apply(Morphism2,ElCodDom) != zero(Cod)
| ~ element(ElCodDom,CodDom)
| sP0_prd(ElCodDom,Cod,CodDom,Morphism2) )
& ( ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) )
| ~ sP0_prd(ElCodDom,Cod,CodDom,Morphism2) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f70,plain,
( ! [Morphism2,CodDom,Cod,ElCodDom] :
( apply(Morphism2,ElCodDom) != zero(Cod)
| ~ element(ElCodDom,CodDom)
| sP0_prd(ElCodDom,Cod,CodDom,Morphism2) )
& ! [Morphism2,CodDom,Cod,ElCodDom] :
( ( apply(Morphism2,ElCodDom) = zero(Cod)
& element(ElCodDom,CodDom) )
| ~ sP0_prd(ElCodDom,Cod,CodDom,Morphism2) ) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( element(X0,X2)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( apply(X3,X0) = zero(X1)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( apply(X3,X0) != zero(X1)
| ~ element(X0,X2)
| sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f75,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ element(X5,X2)
| apply(X1,apply(X0,X5)) = zero(X4)
| ~ morphism(X1,X3,X4)
| ~ morphism(X0,X2,X3)
| ~ exact(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f43]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HAL007+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:47:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.36 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.08/0.36 % SZS output start Saturation for theBenchmark
% See solution above
% 0.08/0.42 % Elapsed time: 0.056856 seconds
% 0.08/0.42 % CPU time: 0.020551 seconds
% 0.08/0.42 % Total memory used: 248.336 KB
% 0.08/0.42 % Net memory used: 238.832 KB
%------------------------------------------------------------------------------