%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HAL003+3 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 3.95s 0.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HAL003+3 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Sun Sep 20 20:42:21 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.37 % Drodi V4.1.1
% 3.95/0.94 % Refutation found
% 3.95/0.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.95/0.94 % SZS output start CNFRefutation for theBenchmark
% 3.95/0.94 fof(f1,axiom,(
% 3.95/0.94 (! [Morphism,Dom,Cod] :( morphism(Morphism,Dom,Cod)=> ( (! [El] :( element(El,Dom)=> element(apply(Morphism,El),Cod) ))& apply(Morphism,zero(Dom)) = zero(Cod) ) ) )),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f5,axiom,(
% 3.95/0.94 (! [Morphism,Dom,Cod] :( ( morphism(Morphism,Dom,Cod)& (! [ElCod] :( element(ElCod,Cod)=> (? [ElDom] :( element(ElDom,Dom)& apply(Morphism,ElDom) = ElCod ) )) ))=> surjection(Morphism) ) )),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f10,axiom,(
% 3.95/0.94 (! [Dom,El1,El2] :( ( element(El1,Dom)& element(El2,Dom) )=> element(subtract(Dom,El1,El2),Dom) ) )),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f14,axiom,(
% 3.95/0.94 morphism(alpha,a,b) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f15,axiom,(
% 3.95/0.94 morphism(beta,b,c) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f16,axiom,(
% 3.95/0.94 morphism(gamma,d,e) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f17,axiom,(
% 3.95/0.94 morphism(delta,e,r) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f19,axiom,(
% 3.95/0.94 morphism(g,b,e) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f25,axiom,(
% 3.95/0.94 exact(alpha,beta) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f33,axiom,(
% 3.95/0.94 (! [E] :( element(E,e)=> (? [B1,B2] :( element(B1,b)& element(B2,b)& apply(g,subtract(b,B1,B2)) = E ) )) )),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f34,conjecture,(
% 3.95/0.94 surjection(g) ),
% 3.95/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.95/0.94 fof(f35,negated_conjecture,(
% 3.95/0.94 ~(surjection(g) )),
% 3.95/0.94 inference(negated_conjecture,[status(cth)],[f34])).
% 3.95/0.94 fof(f36,plain,(
% 3.95/0.94 ![Morphism,Dom,Cod]: (~morphism(Morphism,Dom,Cod)|((![El]: (~element(El,Dom)|element(apply(Morphism,El),Cod)))&apply(Morphism,zero(Dom))=zero(Cod)))),
% 3.95/0.94 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 3.95/0.94 fof(f38,plain,(
% 3.95/0.94 ![X0,X1,X2]: (~morphism(X0,X1,X2)|apply(X0,zero(X1))=zero(X2))),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f36])).
% 3.95/0.94 fof(f53,plain,(
% 3.95/0.94 ![Morphism,Dom,Cod]: ((~morphism(Morphism,Dom,Cod)|(?[ElCod]: (element(ElCod,Cod)&(![ElDom]: (~element(ElDom,Dom)|~apply(Morphism,ElDom)=ElCod)))))|surjection(Morphism))),
% 3.95/0.94 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 3.95/0.94 fof(f54,plain,(
% 3.95/0.94 ![Morphism]: ((![Dom,Cod]: (~morphism(Morphism,Dom,Cod)|(?[ElCod]: (element(ElCod,Cod)&(![ElDom]: (~element(ElDom,Dom)|~apply(Morphism,ElDom)=ElCod))))))|surjection(Morphism))),
% 3.95/0.94 inference(miniscoping,[status(thm)],[f53])).
% 3.95/0.94 fof(f55,plain,(
% 3.95/0.94 ![Morphism]: ((![Dom,Cod]: (~morphism(Morphism,Dom,Cod)|(element(sK3_skl(Cod,Dom,Morphism),Cod)&(![ElDom]: (~element(ElDom,Dom)|~apply(Morphism,ElDom)=sK3_skl(Cod,Dom,Morphism))))))|surjection(Morphism))),
% 3.95/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(ElCod,sK3_skl(Cod,Dom,Morphism))],[f54])).
% 3.95/0.94 fof(f56,plain,(
% 3.95/0.94 ![X0,X1,X2]: (~morphism(X0,X1,X2)|element(sK3_skl(X2,X1,X0),X2)|surjection(X0))),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f55])).
% 3.95/0.94 fof(f57,plain,(
% 3.95/0.94 ![X0,X1,X2,X3]: (~morphism(X0,X1,X2)|~element(X3,X1)|~apply(X0,X3)=sK3_skl(X2,X1,X0)|surjection(X0))),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f55])).
% 3.95/0.94 fof(f83,plain,(
% 3.95/0.94 ![Dom,El1,El2]: ((~element(El1,Dom)|~element(El2,Dom))|element(subtract(Dom,El1,El2),Dom))),
% 3.95/0.94 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 3.95/0.94 fof(f84,plain,(
% 3.95/0.94 ![X0,X1,X2]: (~element(X0,X1)|~element(X2,X1)|element(subtract(X1,X0,X2),X1))),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f83])).
% 3.95/0.94 fof(f91,plain,(
% 3.95/0.94 morphism(alpha,a,b)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f14])).
% 3.95/0.94 fof(f92,plain,(
% 3.95/0.94 morphism(beta,b,c)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f15])).
% 3.95/0.94 fof(f93,plain,(
% 3.95/0.94 morphism(gamma,d,e)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f16])).
% 3.95/0.94 fof(f94,plain,(
% 3.95/0.94 morphism(delta,e,r)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f17])).
% 3.95/0.94 fof(f96,plain,(
% 3.95/0.94 morphism(g,b,e)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f19])).
% 3.95/0.94 fof(f102,plain,(
% 3.95/0.94 exact(alpha,beta)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f25])).
% 3.95/0.94 fof(f124,plain,(
% 3.95/0.94 ![E]: (~element(E,e)|(?[B1,B2]: ((element(B1,b)&element(B2,b))&apply(g,subtract(b,B1,B2))=E)))),
% 3.95/0.94 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 3.95/0.94 fof(f125,plain,(
% 3.95/0.94 ![E]: (~element(E,e)|((element(sK13_skl(E),b)&element(sK14_skl(E),b))&apply(g,subtract(b,sK13_skl(E),sK14_skl(E)))=E))),
% 3.95/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(B1,sK13_skl(E)),skolemize(B2,sK14_skl(E))],[f124])).
% 3.95/0.94 fof(f126,plain,(
% 3.95/0.94 ![X0]: (~element(X0,e)|element(sK13_skl(X0),b))),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f125])).
% 3.95/0.94 fof(f127,plain,(
% 3.95/0.94 ![X0]: (~element(X0,e)|element(sK14_skl(X0),b))),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f125])).
% 3.95/0.94 fof(f128,plain,(
% 3.95/0.94 ![X0]: (~element(X0,e)|apply(g,subtract(b,sK13_skl(X0),sK14_skl(X0)))=X0)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f125])).
% 3.95/0.94 fof(f129,plain,(
% 3.95/0.94 ~surjection(g)),
% 3.95/0.94 inference(cnf_transformation,[status(thm)],[f35])).
% 3.95/0.95 fof(f138,plain,(
% 3.95/0.95 apply(g,zero(b))=zero(e)),
% 3.95/0.95 inference(resolution,[status(thm)],[f38,f96])).
% 3.95/0.95 fof(f166,definition,(
% 3.95/0.95 sQ5_spl <=> (surjection(g))),
% 3.95/0.95 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 3.95/0.95 fof(f167,plain,(
% 3.95/0.95 surjection(g)|~sQ5_spl),
% 3.95/0.95 inference(component_clause,[status(thm)],[f166])).
% 3.95/0.95 fof(f225,plain,(
% 3.95/0.95 element(sK3_skl(e,b,g),e)|surjection(g)),
% 3.95/0.95 inference(resolution,[status(thm)],[f56,f96])).
% 3.95/0.95 fof(f226,definition,(
% 3.95/0.95 sQ14_spl <=> (element(sK3_skl(e,b,g),e))),
% 3.95/0.95 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 3.95/0.95 fof(f227,plain,(
% 3.95/0.95 element(sK3_skl(e,b,g),e)|~sQ14_spl),
% 3.95/0.95 inference(component_clause,[status(thm)],[f226])).
% 3.95/0.95 fof(f229,plain,(
% 3.95/0.95 sQ14_spl|sQ5_spl),
% 3.95/0.95 inference(split_clause,[status(thm)],[f225,f226,f166])).
% 3.95/0.95 fof(f448,plain,(
% 3.95/0.95 apply(delta,zero(e))=zero(r)),
% 3.95/0.95 inference(resolution,[status(thm)],[f94,f38])).
% 3.95/0.95 fof(f675,plain,(
% 3.95/0.95 $false|~sQ5_spl),
% 3.95/0.95 inference(forward_subsumption_resolution,[status(thm)],[f167,f129])).
% 3.95/0.95 fof(f676,plain,(
% 3.95/0.95 ~sQ5_spl),
% 3.95/0.95 inference(contradiction_clause,[status(thm)],[f675])).
% 3.95/0.95 fof(f781,plain,(
% 3.95/0.95 element(sK13_skl(sK3_skl(e,b,g)),b)|~sQ14_spl),
% 3.95/0.95 inference(resolution,[status(thm)],[f126,f227])).
% 3.95/0.95 fof(f785,plain,(
% 3.95/0.95 element(sK14_skl(sK3_skl(e,b,g)),b)|~sQ14_spl),
% 3.95/0.95 inference(resolution,[status(thm)],[f127,f227])).
% 3.95/0.95 fof(f789,plain,(
% 3.95/0.95 apply(g,subtract(b,sK13_skl(sK3_skl(e,b,g)),sK14_skl(sK3_skl(e,b,g))))=sK3_skl(e,b,g)|~sQ14_spl),
% 3.95/0.95 inference(resolution,[status(thm)],[f128,f227])).
% 3.95/0.95 fof(f891,definition,(
% 3.95/0.95 sQ82_spl <=> (exact(alpha,beta))),
% 3.95/0.95 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 3.95/0.95 fof(f893,plain,(
% 3.95/0.95 ~exact(alpha,beta)|sQ82_spl),
% 3.95/0.95 inference(component_clause,[status(thm)],[f891])).
% 3.95/0.95 fof(f994,plain,(
% 3.95/0.95 ![X0]: (~element(X0,b)|element(subtract(b,sK13_skl(sK3_skl(e,b,g)),X0),b)|~sQ14_spl)),
% 3.95/0.95 inference(resolution,[status(thm)],[f781,f84])).
% 3.95/0.95 fof(f1031,plain,(
% 3.95/0.95 ~morphism(g,b,e)|~element(subtract(b,sK13_skl(sK3_skl(e,b,g)),sK14_skl(sK3_skl(e,b,g))),b)|surjection(g)|~sQ14_spl),
% 3.95/0.95 inference(resolution,[status(thm)],[f789,f57])).
% 3.95/0.95 fof(f1035,definition,(
% 3.95/0.95 sQ95_spl <=> (morphism(g,b,e))),
% 3.95/0.95 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 3.95/0.95 fof(f1037,plain,(
% 3.95/0.95 ~morphism(g,b,e)|sQ95_spl),
% 3.95/0.95 inference(component_clause,[status(thm)],[f1035])).
% 3.95/0.95 fof(f1038,definition,(
% 3.95/0.95 sQ96_spl <=> (element(subtract(b,sK13_skl(sK3_skl(e,b,g)),sK14_skl(sK3_skl(e,b,g))),b))),
% 3.95/0.95 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 3.95/0.95 fof(f1040,plain,(
% 3.95/0.95 ~element(subtract(b,sK13_skl(sK3_skl(e,b,g)),sK14_skl(sK3_skl(e,b,g))),b)|sQ96_spl),
% 3.95/0.95 inference(component_clause,[status(thm)],[f1038])).
% 3.95/0.95 fof(f1041,plain,(
% 3.95/0.95 ~sQ95_spl|~sQ96_spl|sQ5_spl|~sQ14_spl),
% 3.95/0.95 inference(split_clause,[status(thm)],[f1031,f1035,f1038,f166,f226])).
% 3.95/0.95 fof(f1051,plain,(
% 3.95/0.95 $false|sQ95_spl),
% 3.95/0.95 inference(forward_subsumption_resolution,[status(thm)],[f1037,f96])).
% 3.95/0.95 fof(f1052,plain,(
% 3.95/0.95 sQ95_spl),
% 3.95/0.95 inference(contradiction_clause,[status(thm)],[f1051])).
% 3.95/0.97 fof(f1068,definition,(
% 3.95/0.97 sQ99_spl <=> (morphism(alpha,a,b))),
% 3.95/0.97 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 3.95/0.97 fof(f1070,plain,(
% 3.95/0.97 ~morphism(alpha,a,b)|sQ99_spl),
% 3.95/0.97 inference(component_clause,[status(thm)],[f1068])).
% 3.95/0.97 fof(f1075,plain,(
% 3.95/0.97 $false|sQ99_spl),
% 3.95/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1070,f91])).
% 3.95/0.97 fof(f1076,plain,(
% 3.95/0.97 sQ99_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f1075])).
% 3.95/0.97 fof(f1433,definition,(
% 3.95/0.97 sQ150_spl <=> (morphism(delta,e,r))),
% 3.95/0.97 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 3.95/0.97 fof(f1435,plain,(
% 3.95/0.97 ~morphism(delta,e,r)|sQ150_spl),
% 3.95/0.97 inference(component_clause,[status(thm)],[f1433])).
% 3.95/0.97 fof(f1440,plain,(
% 3.95/0.97 $false|sQ150_spl),
% 3.95/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1435,f94])).
% 3.95/0.97 fof(f1441,plain,(
% 3.95/0.97 sQ150_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f1440])).
% 3.95/0.97 fof(f1510,plain,(
% 3.95/0.97 $false|sQ82_spl),
% 3.95/0.97 inference(forward_subsumption_resolution,[status(thm)],[f893,f102])).
% 3.95/0.97 fof(f1511,plain,(
% 3.95/0.97 sQ82_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f1510])).
% 3.95/0.97 fof(f1559,definition,(
% 3.95/0.97 sQ158_spl <=> (apply(g,zero(b))=zero(e))),
% 3.95/0.97 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 3.95/0.97 fof(f1561,plain,(
% 3.95/0.97 ~apply(g,zero(b))=zero(e)|sQ158_spl),
% 3.95/0.97 inference(component_clause,[status(thm)],[f1559])).
% 3.95/0.97 fof(f1569,plain,(
% 3.95/0.97 ~zero(e)=zero(e)|sQ158_spl),
% 3.95/0.97 inference(forward_demodulation,[status(thm)],[f138,f1561])).
% 3.95/0.97 fof(f1570,plain,(
% 3.95/0.97 $false|sQ158_spl),
% 3.95/0.97 inference(trivial_equality_resolution,[status(thm)],[f1569])).
% 3.95/0.97 fof(f1571,plain,(
% 3.95/0.97 sQ158_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f1570])).
% 3.95/0.97 fof(f2324,definition,(
% 3.95/0.97 sQ199_spl <=> (apply(delta,zero(e))=zero(r))),
% 3.95/0.97 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 3.95/0.97 fof(f2326,plain,(
% 3.95/0.97 ~apply(delta,zero(e))=zero(r)|sQ199_spl),
% 3.95/0.97 inference(component_clause,[status(thm)],[f2324])).
% 3.95/0.97 fof(f2348,plain,(
% 3.95/0.97 ~zero(r)=zero(r)|sQ199_spl),
% 3.95/0.97 inference(forward_demodulation,[status(thm)],[f448,f2326])).
% 3.95/0.97 fof(f2349,plain,(
% 3.95/0.97 $false|sQ199_spl),
% 3.95/0.97 inference(trivial_equality_resolution,[status(thm)],[f2348])).
% 3.95/0.97 fof(f2350,plain,(
% 3.95/0.97 sQ199_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f2349])).
% 3.95/0.97 fof(f3064,definition,(
% 3.95/0.97 sQ222_spl <=> (morphism(gamma,d,e))),
% 3.95/0.97 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 3.95/0.97 fof(f3066,plain,(
% 3.95/0.97 ~morphism(gamma,d,e)|sQ222_spl),
% 3.95/0.97 inference(component_clause,[status(thm)],[f3064])).
% 3.95/0.97 fof(f3068,plain,(
% 3.95/0.97 $false|sQ222_spl),
% 3.95/0.97 inference(forward_subsumption_resolution,[status(thm)],[f3066,f93])).
% 3.95/0.97 fof(f3069,plain,(
% 3.95/0.97 sQ222_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f3068])).
% 3.95/0.97 fof(f3072,definition,(
% 3.95/0.97 sQ223_spl <=> (morphism(beta,b,c))),
% 3.95/0.97 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 3.95/0.97 fof(f3074,plain,(
% 3.95/0.97 ~morphism(beta,b,c)|sQ223_spl),
% 3.95/0.97 inference(component_clause,[status(thm)],[f3072])).
% 3.95/0.97 fof(f3076,plain,(
% 3.95/0.97 $false|sQ223_spl),
% 3.95/0.97 inference(forward_subsumption_resolution,[status(thm)],[f3074,f92])).
% 3.95/0.97 fof(f3077,plain,(
% 3.95/0.97 sQ223_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f3076])).
% 3.95/0.97 fof(f3479,plain,(
% 3.95/0.97 element(subtract(b,sK13_skl(sK3_skl(e,b,g)),sK14_skl(sK3_skl(e,b,g))),b)|~sQ14_spl),
% 3.95/0.97 inference(resolution,[status(thm)],[f994,f785])).
% 3.95/0.97 fof(f3495,plain,(
% 3.95/0.97 $false|sQ96_spl|~sQ14_spl),
% 3.95/0.97 inference(forward_subsumption_resolution,[status(thm)],[f3479,f1040])).
% 3.95/0.97 fof(f3496,plain,(
% 3.95/0.97 sQ96_spl|~sQ14_spl),
% 3.95/0.97 inference(contradiction_clause,[status(thm)],[f3495])).
% 3.95/0.97 fof(f3497,plain,(
% 3.95/0.97 $false),
% 3.95/0.97 inference(sat_refutation,[status(thm)],[f229,f676,f1041,f1052,f1076,f1441,f1511,f1571,f2350,f3069,f3077,f3496])).
% 3.95/0.97 % SZS output end CNFRefutation for theBenchmark.p
% 3.95/1.00 % Elapsed time: 0.626085 seconds
% 3.95/1.00 % CPU time: 4.580126 seconds
% 3.95/1.00 % Total memory used: 164.789 MB
% 3.95/1.00 % Net memory used: 160.127 MB
%------------------------------------------------------------------------------