%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HAL006+1 : 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 : n003.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 89.67s 12.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HAL006+1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n003.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 20:46:31 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 89.67/12.12 % Refutation found
% 89.67/12.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 89.67/12.12 % SZS output start CNFRefutation for theBenchmark
% 89.67/12.12 fof(f1,axiom,(
% 89.67/12.12 (! [Morphism,Dom,Cod] :( morphism(Morphism,Dom,Cod)=> ( (! [El] :( element(El,Dom)=> element(apply(Morphism,El),Cod) ))& apply(Morphism,zero(Dom)) = zero(Cod) ) ) )),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f12,axiom,(
% 89.67/12.12 (! [Dom,El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> subtract(Dom,El1,subtract(Dom,El1,El2)) = El2 ) )),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f13,axiom,(
% 89.67/12.12 (! [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)) ) )) )),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f14,axiom,(
% 89.67/12.12 morphism(alpha,a,b) ),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f19,axiom,(
% 89.67/12.12 morphism(g,b,e) ),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f32,axiom,(
% 89.67/12.12 (! [E] :( element(E,e)=> (? [B1,E1,A] :( element(B1,b)& element(E1,e)& subtract(e,apply(g,B1),E) = E1& element(A,a)& apply(gamma,apply(f,A)) = E1& apply(g,apply(alpha,A)) = E1 ) )) )),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f33,conjecture,(
% 89.67/12.12 (! [E] :( element(E,e)=> (? [B1,B2] :( element(B1,b)& element(B2,b)& apply(g,subtract(b,B1,B2)) = E ) )) )),
% 89.67/12.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 89.67/12.12 fof(f34,negated_conjecture,(
% 89.67/12.12 ~((! [E] :( element(E,e)=> (? [B1,B2] :( element(B1,b)& element(B2,b)& apply(g,subtract(b,B1,B2)) = E ) )) ))),
% 89.67/12.12 inference(negated_conjecture,[status(cth)],[f33])).
% 89.67/12.12 fof(f35,plain,(
% 89.67/12.12 ![Morphism,Dom,Cod]: (~morphism(Morphism,Dom,Cod)|((![El]: (~element(El,Dom)|element(apply(Morphism,El),Cod)))&apply(Morphism,zero(Dom))=zero(Cod)))),
% 89.67/12.12 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 89.67/12.12 fof(f36,plain,(
% 89.67/12.12 ![X0,X1,X2,X3]: (~morphism(X0,X1,X2)|~element(X3,X1)|element(apply(X0,X3),X2))),
% 89.67/12.12 inference(cnf_transformation,[status(thm)],[f35])).
% 89.67/12.12 fof(f86,plain,(
% 89.67/12.12 ![Dom,El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|subtract(Dom,El1,subtract(Dom,El1,El2))=El2)),
% 89.67/12.12 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 89.67/12.12 fof(f87,plain,(
% 89.67/12.12 ![X0,X1,X2]: (~element(X0,X1)|~element(X2,X1)|subtract(X1,X0,subtract(X1,X0,X2))=X2)),
% 89.67/12.12 inference(cnf_transformation,[status(thm)],[f86])).
% 89.67/12.12 fof(f88,plain,(
% 89.67/12.12 ![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)))))),
% 89.67/12.12 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 89.67/12.12 fof(f89,plain,(
% 89.67/12.12 ![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)))),
% 89.67/12.12 inference(cnf_transformation,[status(thm)],[f88])).
% 89.67/12.12 fof(f90,plain,(
% 89.67/12.12 morphism(alpha,a,b)),
% 89.67/12.12 inference(cnf_transformation,[status(thm)],[f14])).
% 89.67/12.12 fof(f95,plain,(
% 89.67/12.12 morphism(g,b,e)),
% 89.67/12.12 inference(cnf_transformation,[status(thm)],[f19])).
% 89.67/12.12 fof(f114,plain,(
% 89.67/12.12 ![E]: (~element(E,e)|(?[B1,E1,A]: (((((element(B1,b)&element(E1,e))&subtract(e,apply(g,B1),E)=E1)&element(A,a))&apply(gamma,apply(f,A))=E1)&apply(g,apply(alpha,A))=E1)))),
% 89.67/12.12 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 89.67/12.12 fof(f115,plain,(
% 89.67/12.12 ![E]: (~element(E,e)|(?[E1,A]: ((((?[B1]: ((element(B1,b)&element(E1,e))&subtract(e,apply(g,B1),E)=E1))&element(A,a))&apply(gamma,apply(f,A))=E1)&apply(g,apply(alpha,A))=E1)))),
% 89.67/12.12 inference(miniscoping,[status(thm)],[f114])).
% 89.67/12.12 fof(f116,plain,(
% 89.67/12.12 ![E]: (~element(E,e)|(((((element(sK12_skl(E),b)&element(sK10_skl(E),e))&subtract(e,apply(g,sK12_skl(E)),E)=sK10_skl(E))&element(sK11_skl(E),a))&apply(gamma,apply(f,sK11_skl(E)))=sK10_skl(E))&apply(g,apply(alpha,sK11_skl(E)))=sK10_skl(E)))),
% 89.67/12.12 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(E1,sK10_skl(E)),skolemize(A,sK11_skl(E)),skolemize(B1,sK12_skl(E))],[f115])).
% 89.67/12.12 fof(f117,plain,(
% 89.67/12.12 ![X0]: (~element(X0,e)|element(sK12_skl(X0),b))),
% 32.63/12.29 inference(cnf_transformation,[status(thm)],[f116])).
% 32.63/12.29 fof(f119,plain,(
% 32.63/12.29 ![X0]: (~element(X0,e)|subtract(e,apply(g,sK12_skl(X0)),X0)=sK10_skl(X0))),
% 32.63/12.29 inference(cnf_transformation,[status(thm)],[f116])).
% 32.63/12.29 fof(f120,plain,(
% 32.63/12.29 ![X0]: (~element(X0,e)|element(sK11_skl(X0),a))),
% 32.63/12.29 inference(cnf_transformation,[status(thm)],[f116])).
% 32.63/12.29 fof(f122,plain,(
% 32.63/12.29 ![X0]: (~element(X0,e)|apply(g,apply(alpha,sK11_skl(X0)))=sK10_skl(X0))),
% 32.63/12.29 inference(cnf_transformation,[status(thm)],[f116])).
% 32.63/12.29 fof(f123,plain,(
% 32.63/12.29 (?[E]: (element(E,e)&(![B1,B2]: ((~element(B1,b)|~element(B2,b))|~apply(g,subtract(b,B1,B2))=E))))),
% 32.63/12.29 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 32.63/12.29 fof(f124,plain,(
% 32.63/12.29 (element(sK13_skl,e)&(![B1,B2]: ((~element(B1,b)|~element(B2,b))|~apply(g,subtract(b,B1,B2))=sK13_skl)))),
% 32.63/12.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(E,sK13_skl)],[f123])).
% 32.63/12.29 fof(f125,plain,(
% 32.63/12.29 element(sK13_skl,e)),
% 32.63/12.29 inference(cnf_transformation,[status(thm)],[f124])).
% 32.63/12.29 fof(f126,plain,(
% 32.63/12.29 ![X0,X1]: (~element(X0,b)|~element(X1,b)|~apply(g,subtract(b,X0,X1))=sK13_skl)),
% 32.63/12.29 inference(cnf_transformation,[status(thm)],[f124])).
% 32.63/12.29 fof(f134,plain,(
% 32.63/12.29 ![X0]: (~element(X0,b)|element(apply(g,X0),e))),
% 32.63/12.29 inference(resolution,[status(thm)],[f95,f36])).
% 32.63/12.29 fof(f138,plain,(
% 32.63/12.29 ![X0,X1]: (~element(X0,b)|~element(X1,b)|apply(g,subtract(b,X0,X1))=subtract(e,apply(g,X0),apply(g,X1)))),
% 32.63/12.29 inference(resolution,[status(thm)],[f89,f95])).
% 32.63/12.29 fof(f1657,plain,(
% 32.63/12.29 ![X0]: (~element(X0,a)|element(apply(alpha,X0),b))),
% 32.63/12.29 inference(resolution,[status(thm)],[f90,f36])).
% 32.63/12.29 fof(f3965,plain,(
% 32.63/12.29 element(sK12_skl(sK13_skl),b)),
% 32.63/12.29 inference(resolution,[status(thm)],[f117,f125])).
% 32.63/12.29 fof(f4067,plain,(
% 32.63/12.29 subtract(e,apply(g,sK12_skl(sK13_skl)),sK13_skl)=sK10_skl(sK13_skl)),
% 32.63/12.29 inference(resolution,[status(thm)],[f119,f125])).
% 32.63/12.29 fof(f4118,plain,(
% 32.63/12.29 element(sK11_skl(sK13_skl),a)),
% 32.63/12.29 inference(resolution,[status(thm)],[f120,f125])).
% 32.63/12.29 fof(f4188,plain,(
% 32.63/12.29 ![X0]: (~element(X0,b)|apply(g,subtract(b,sK12_skl(sK13_skl),X0))=subtract(e,apply(g,sK12_skl(sK13_skl)),apply(g,X0)))),
% 32.63/12.29 inference(resolution,[status(thm)],[f3965,f138])).
% 32.63/12.29 fof(f4189,plain,(
% 32.63/12.29 element(apply(g,sK12_skl(sK13_skl)),e)),
% 32.63/12.29 inference(resolution,[status(thm)],[f3965,f134])).
% 32.63/12.29 fof(f4190,plain,(
% 32.63/12.29 ![X0]: (~element(X0,b)|~apply(g,subtract(b,sK12_skl(sK13_skl),X0))=sK13_skl)),
% 32.63/12.29 inference(resolution,[status(thm)],[f3965,f126])).
% 32.63/12.29 fof(f4235,plain,(
% 32.63/12.29 element(apply(alpha,sK11_skl(sK13_skl)),b)),
% 32.63/12.29 inference(resolution,[status(thm)],[f4118,f1657])).
% 32.63/12.29 fof(f4652,plain,(
% 32.63/12.29 ![X0]: (~element(X0,e)|subtract(e,apply(g,sK12_skl(sK13_skl)),subtract(e,apply(g,sK12_skl(sK13_skl)),X0))=X0)),
% 32.63/12.29 inference(resolution,[status(thm)],[f4189,f87])).
% 32.63/12.29 fof(f4881,plain,(
% 32.63/12.29 ~apply(g,subtract(b,sK12_skl(sK13_skl),apply(alpha,sK11_skl(sK13_skl))))=sK13_skl),
% 32.63/12.29 inference(resolution,[status(thm)],[f4235,f4190])).
% 32.63/12.29 fof(f4882,plain,(
% 32.63/12.29 apply(g,subtract(b,sK12_skl(sK13_skl),apply(alpha,sK11_skl(sK13_skl))))=subtract(e,apply(g,sK12_skl(sK13_skl)),apply(g,apply(alpha,sK11_skl(sK13_skl))))),
% 32.63/12.29 inference(resolution,[status(thm)],[f4235,f4188])).
% 32.63/12.29 fof(f6396,plain,(
% 32.63/12.29 apply(g,apply(alpha,sK11_skl(sK13_skl)))=sK10_skl(sK13_skl)),
% 32.63/12.29 inference(resolution,[status(thm)],[f122,f125])).
% 32.63/12.29 fof(f6402,plain,(
% 32.63/12.29 apply(g,subtract(b,sK12_skl(sK13_skl),apply(alpha,sK11_skl(sK13_skl))))=subtract(e,apply(g,sK12_skl(sK13_skl)),sK10_skl(sK13_skl))),
% 32.63/12.29 inference(backward_demodulation,[status(thm)],[f6396,f4882])).
% 32.63/12.29 fof(f6405,plain,(
% 32.63/12.29 ~subtract(e,apply(g,sK12_skl(sK13_skl)),sK10_skl(sK13_skl))=sK13_skl),
% 32.63/12.29 inference(backward_demodulation,[status(thm)],[f6402,f4881])).
% 32.63/12.29 fof(f9313,plain,(
% 32.63/12.29 subtract(e,apply(g,sK12_skl(sK13_skl)),subtract(e,apply(g,sK12_skl(sK13_skl)),sK13_skl))=sK13_skl),
% 32.63/12.29 inference(resolution,[status(thm)],[f4652,f125])).
% 32.63/12.29 fof(f9323,plain,(
% 32.63/12.29 subtract(e,apply(g,sK12_skl(sK13_skl)),sK10_skl(sK13_skl))=sK13_skl),
% 32.63/12.29 inference(forward_demodulation,[status(thm)],[f4067,f9313])).
% 32.63/12.29 fof(f9324,plain,(
% 32.63/12.29 $false),
% 32.63/12.29 inference(forward_subsumption_resolution,[status(thm)],[f9323,f6405])).
% 32.63/12.29 % SZS output end CNFRefutation for theBenchmark.p
% 4.90/12.35 % Elapsed time: 11.895529 seconds
% 4.90/12.35 % CPU time: 92.928659 seconds
% 4.90/12.35 % Total memory used: 752.997 MB
% 4.90/12.35 % Net memory used: 696.728 MB
%------------------------------------------------------------------------------