%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU236+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 02:22:06 PM UTC 2026
% Result : Theorem 105.51s 13.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU236+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n026.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 21 06:04:52 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 105.51/13.72 % Refutation found
% 105.51/13.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 105.51/13.72 % SZS output start CNFRefutation for theBenchmark
% 105.51/13.72 fof(f3,axiom,(
% 105.51/13.72 (! [A] :( ordinal(A)=> ( epsilon_transitive(A)& epsilon_connected(A) ) ) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f10,axiom,(
% 105.51/13.72 (! [A] : succ(A) = set_union2(A,singleton(A)) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f11,axiom,(
% 105.51/13.72 (! [A,B] :( B = singleton(A)<=> (! [C] :( in(C,B)<=> C = A ) )) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f12,axiom,(
% 105.51/13.72 (! [A] :( epsilon_transitive(A)<=> (! [B] :( in(B,A)=> subset(B,A) ) )) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f13,axiom,(
% 105.51/13.72 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f21,axiom,(
% 105.51/13.72 (! [A] :( ordinal(A)=> ( ~ empty(succ(A))& epsilon_transitive(succ(A))& epsilon_connected(succ(A))& ordinal(succ(A)) ) ) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f38,axiom,(
% 105.51/13.72 (! [A,B] :( ( ordinal(A)& ordinal(B) )=> ( ordinal_subset(A,B)<=> subset(A,B) ) ) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f41,axiom,(
% 105.51/13.72 (! [A] : in(A,succ(A)) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f45,conjecture,(
% 105.51/13.72 (! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ( in(A,B)<=> ordinal_subset(succ(A),B) ) ) )) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f46,negated_conjecture,(
% 105.51/13.72 ~((! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ( in(A,B)<=> ordinal_subset(succ(A),B) ) ) )) ))),
% 105.51/13.72 inference(negated_conjecture,[status(cth)],[f45])).
% 105.51/13.72 fof(f53,axiom,(
% 105.51/13.72 (! [A,B,C] :( ( subset(A,B)& subset(C,B) )=> subset(set_union2(A,C),B) ) )),
% 105.51/13.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.51/13.72 fof(f58,plain,(
% 105.51/13.72 ![A]: (~ordinal(A)|(epsilon_transitive(A)&epsilon_connected(A)))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 105.51/13.72 fof(f59,plain,(
% 105.51/13.72 ![X0]: (~ordinal(X0)|epsilon_transitive(X0))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f58])).
% 105.51/13.72 fof(f76,plain,(
% 105.51/13.72 ![X0]: (succ(X0)=set_union2(X0,singleton(X0)))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f10])).
% 105.51/13.72 fof(f77,plain,(
% 105.51/13.72 ![A,B]: ((~B=singleton(A)|(![C]: ((~in(C,B)|C=A)&(in(C,B)|~C=A))))&(B=singleton(A)|(?[C]: ((~in(C,B)|~C=A)&(in(C,B)|C=A)))))),
% 105.51/13.72 inference(NNF_transformation,[status(thm)],[f11])).
% 105.51/13.72 fof(f78,plain,(
% 105.51/13.72 (![A,B]: (~B=singleton(A)|((![C]: (~in(C,B)|C=A))&(![C]: (in(C,B)|~C=A)))))&(![A,B]: (B=singleton(A)|(?[C]: ((~in(C,B)|~C=A)&(in(C,B)|C=A)))))),
% 105.51/13.72 inference(miniscoping,[status(thm)],[f77])).
% 105.51/13.72 fof(f79,plain,(
% 105.51/13.72 (![A,B]: (~B=singleton(A)|((![C]: (~in(C,B)|C=A))&(![C]: (in(C,B)|~C=A)))))&(![A,B]: (B=singleton(A)|((~in(sK0_skl(B,A),B)|~sK0_skl(B,A)=A)&(in(sK0_skl(B,A),B)|sK0_skl(B,A)=A))))),
% 105.51/13.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f78])).
% 105.51/13.72 fof(f80,plain,(
% 105.51/13.72 ![X0,X1,X2]: (~X0=singleton(X1)|~in(X2,X0)|X2=X1)),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f79])).
% 105.51/13.72 fof(f84,plain,(
% 105.51/13.72 ![A]: (epsilon_transitive(A)<=>(![B]: (~in(B,A)|subset(B,A))))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 105.51/13.72 fof(f85,plain,(
% 105.51/13.72 ![A]: ((~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A))))&(epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 105.51/13.72 inference(NNF_transformation,[status(thm)],[f84])).
% 105.51/13.72 fof(f86,plain,(
% 105.51/13.72 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 105.51/13.72 inference(miniscoping,[status(thm)],[f85])).
% 105.51/13.72 fof(f87,plain,(
% 105.51/13.72 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(in(sK1_skl(A),A)&~subset(sK1_skl(A),A))))),
% 105.51/13.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f86])).
% 105.51/13.72 fof(f88,plain,(
% 105.51/13.72 ![X0,X1]: (~epsilon_transitive(X0)|~in(X1,X0)|subset(X1,X0))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f87])).
% 105.51/13.72 fof(f91,plain,(
% 105.51/13.72 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 105.51/13.72 fof(f92,plain,(
% 105.51/13.72 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 105.51/13.72 inference(NNF_transformation,[status(thm)],[f91])).
% 105.51/13.72 fof(f93,plain,(
% 105.51/13.72 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 105.51/13.72 inference(miniscoping,[status(thm)],[f92])).
% 105.51/13.72 fof(f94,plain,(
% 105.51/13.72 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK2_skl(B,A),A)&~in(sK2_skl(B,A),B))))),
% 105.51/13.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f93])).
% 105.51/13.72 fof(f95,plain,(
% 105.51/13.72 ![X0,X1,X2]: (~subset(X0,X1)|~in(X2,X0)|in(X2,X1))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f94])).
% 105.51/13.72 fof(f96,plain,(
% 105.51/13.72 ![X0,X1]: (subset(X0,X1)|in(sK2_skl(X1,X0),X0))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f94])).
% 105.51/13.72 fof(f97,plain,(
% 105.51/13.72 ![X0,X1]: (subset(X0,X1)|~in(sK2_skl(X1,X0),X1))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f94])).
% 105.51/13.72 fof(f118,plain,(
% 105.51/13.72 ![A]: (~ordinal(A)|(((~empty(succ(A))&epsilon_transitive(succ(A)))&epsilon_connected(succ(A)))&ordinal(succ(A))))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 105.51/13.72 fof(f122,plain,(
% 105.51/13.72 ![X0]: (~ordinal(X0)|ordinal(succ(X0)))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f118])).
% 105.51/13.72 fof(f179,plain,(
% 105.51/13.72 ![A,B]: ((~ordinal(A)|~ordinal(B))|(ordinal_subset(A,B)<=>subset(A,B)))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 105.51/13.72 fof(f180,plain,(
% 105.51/13.72 ![A,B]: ((~ordinal(A)|~ordinal(B))|((~ordinal_subset(A,B)|subset(A,B))&(ordinal_subset(A,B)|~subset(A,B))))),
% 105.51/13.72 inference(NNF_transformation,[status(thm)],[f179])).
% 105.51/13.72 fof(f181,plain,(
% 105.51/13.72 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|~ordinal_subset(X0,X1)|subset(X0,X1))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f180])).
% 105.51/13.72 fof(f182,plain,(
% 105.51/13.72 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|ordinal_subset(X0,X1)|~subset(X0,X1))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f180])).
% 105.51/13.72 fof(f188,plain,(
% 105.51/13.72 ![X0]: (in(X0,succ(X0)))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f41])).
% 105.51/13.72 fof(f194,plain,(
% 105.51/13.72 (?[A]: (ordinal(A)&(?[B]: (ordinal(B)&(in(A,B)<~>ordinal_subset(succ(A),B))))))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 105.51/13.72 fof(f195,plain,(
% 105.51/13.72 ?[A]: (ordinal(A)&(?[B]: (ordinal(B)&((in(A,B)|ordinal_subset(succ(A),B))&(~in(A,B)|~ordinal_subset(succ(A),B))))))),
% 105.51/13.72 inference(NNF_transformation,[status(thm)],[f194])).
% 105.51/13.72 fof(f196,plain,(
% 105.51/13.72 (ordinal(sK17_skl)&(ordinal(sK18_skl)&((in(sK17_skl,sK18_skl)|ordinal_subset(succ(sK17_skl),sK18_skl))&(~in(sK17_skl,sK18_skl)|~ordinal_subset(succ(sK17_skl),sK18_skl)))))),
% 105.51/13.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(A,sK17_skl),skolemize(B,sK18_skl)],[f195])).
% 105.51/13.72 fof(f197,plain,(
% 105.51/13.72 ordinal(sK17_skl)),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f196])).
% 105.51/13.72 fof(f198,plain,(
% 105.51/13.72 ordinal(sK18_skl)),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f196])).
% 105.51/13.72 fof(f199,plain,(
% 105.51/13.72 in(sK17_skl,sK18_skl)|ordinal_subset(succ(sK17_skl),sK18_skl)),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f196])).
% 105.51/13.72 fof(f200,plain,(
% 105.51/13.72 ~in(sK17_skl,sK18_skl)|~ordinal_subset(succ(sK17_skl),sK18_skl)),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f196])).
% 105.51/13.72 fof(f219,plain,(
% 105.51/13.72 ![A,B,C]: ((~subset(A,B)|~subset(C,B))|subset(set_union2(A,C),B))),
% 105.51/13.72 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 105.51/13.72 fof(f220,plain,(
% 105.51/13.72 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X2,X1)|subset(set_union2(X0,X2),X1))),
% 105.51/13.72 inference(cnf_transformation,[status(thm)],[f219])).
% 105.51/13.72 fof(f221,plain,(
% 105.51/13.72 ![X0,X1]: (~in(X0,singleton(X1))|X0=X1)),
% 105.51/13.72 inference(destructive_equality_resolution,[status(thm)],[f80])).
% 105.51/13.72 fof(f266,plain,(
% 105.51/13.72 ![X0,X1,X2]: (~in(X0,X1)|in(X0,X2)|~epsilon_transitive(X2)|~in(X1,X2))),
% 105.51/13.72 inference(resolution,[status(thm)],[f95,f88])).
% 105.51/13.72 fof(f267,plain,(
% 105.51/13.72 ![X0,X1,X2]: (~in(X0,X1)|in(X0,X2)|~ordinal(X1)|~ordinal(X2)|~ordinal_subset(X1,X2))),
% 105.51/13.72 inference(resolution,[status(thm)],[f95,f181])).
% 105.51/13.72 fof(f270,plain,(
% 105.51/13.72 ![X0,X1]: (~in(X0,X1)|in(X0,sK18_skl)|~ordinal(X1)|~ordinal_subset(X1,sK18_skl))),
% 105.51/13.72 inference(resolution,[status(thm)],[f267,f198])).
% 105.51/13.72 fof(f283,plain,(
% 105.51/13.72 ![X0,X1]: (subset(singleton(X0),X1)|sK2_skl(X1,singleton(X0))=X0)),
% 105.51/13.77 inference(resolution,[status(thm)],[f96,f221])).
% 105.51/13.77 fof(f326,plain,(
% 105.51/13.77 ![X0]: (in(X0,sK18_skl)|~ordinal(succ(X0))|~ordinal_subset(succ(X0),sK18_skl))),
% 105.51/13.77 inference(resolution,[status(thm)],[f270,f188])).
% 105.51/13.77 fof(f497,plain,(
% 105.51/13.77 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X2,X1)|~ordinal(set_union2(X0,X2))|~ordinal(X1)|ordinal_subset(set_union2(X0,X2),X1))),
% 105.51/13.77 inference(resolution,[status(thm)],[f220,f182])).
% 105.51/13.77 fof(f505,plain,(
% 105.51/13.77 ![X0,X1]: (~subset(X0,X1)|~subset(singleton(X0),X1)|~ordinal(succ(X0))|~ordinal(X1)|ordinal_subset(set_union2(X0,singleton(X0)),X1))),
% 105.51/13.77 inference(paramodulation,[status(thm)],[f76,f497])).
% 105.51/13.77 fof(f510,plain,(
% 105.51/13.77 ![X0,X1]: (~subset(X0,X1)|~subset(singleton(X0),X1)|~ordinal(succ(X0))|~ordinal(X1)|ordinal_subset(succ(X0),X1))),
% 105.51/13.77 inference(forward_demodulation,[status(thm)],[f76,f505])).
% 105.51/13.77 fof(f901,plain,(
% 105.51/13.77 ![X0]: (in(X0,sK18_skl)|~ordinal_subset(succ(X0),sK18_skl)|~ordinal(X0))),
% 105.51/13.77 inference(resolution,[status(thm)],[f326,f122])).
% 105.51/13.77 fof(f921,plain,(
% 105.51/13.77 ![X0,X1]: (~subset(X0,X1)|~subset(singleton(X0),X1)|~ordinal(X1)|ordinal_subset(succ(X0),X1)|~ordinal(X0))),
% 105.51/13.77 inference(resolution,[status(thm)],[f510,f122])).
% 105.51/13.77 fof(f1327,plain,(
% 105.51/13.77 in(sK17_skl,sK18_skl)|~ordinal(sK17_skl)|in(sK17_skl,sK18_skl)),
% 105.51/13.77 inference(resolution,[status(thm)],[f901,f199])).
% 105.51/13.77 fof(f1330,plain,(
% 105.51/13.77 in(sK17_skl,sK18_skl)|~ordinal(sK17_skl)),
% 105.51/13.77 inference(duplicate_literals_removal,[status(thm)],[f1327])).
% 105.51/13.77 fof(f1331,plain,(
% 105.51/13.77 in(sK17_skl,sK18_skl)),
% 105.51/13.77 inference(forward_subsumption_resolution,[status(thm)],[f1330,f197])).
% 105.51/13.77 fof(f1346,plain,(
% 105.51/13.77 ~ordinal_subset(succ(sK17_skl),sK18_skl)),
% 105.51/13.77 inference(backward_subsumption_resolution,[status(thm)],[f200,f1331])).
% 105.51/13.77 fof(f1347,plain,(
% 105.51/13.77 ![X0]: (~in(X0,sK17_skl)|in(X0,sK18_skl)|~epsilon_transitive(sK18_skl))),
% 105.51/13.77 inference(resolution,[status(thm)],[f1331,f266])).
% 105.51/13.77 fof(f1796,plain,(
% 105.51/13.77 ![X0]: (~in(X0,sK17_skl)|in(X0,sK18_skl)|~ordinal(sK18_skl))),
% 105.51/13.77 inference(resolution,[status(thm)],[f1347,f59])).
% 105.51/13.77 fof(f1798,plain,(
% 105.51/13.77 ![X0]: (~in(X0,sK17_skl)|in(X0,sK18_skl))),
% 105.51/13.77 inference(forward_subsumption_resolution,[status(thm)],[f1796,f198])).
% 105.51/13.77 fof(f1841,plain,(
% 105.51/13.77 ![X0]: (in(sK2_skl(X0,sK17_skl),sK18_skl)|subset(sK17_skl,X0))),
% 105.51/13.77 inference(resolution,[status(thm)],[f1798,f96])).
% 105.51/13.77 fof(f2011,plain,(
% 105.51/13.77 ![X0]: (~subset(X0,sK18_skl)|~subset(singleton(X0),sK18_skl)|ordinal_subset(succ(X0),sK18_skl)|~ordinal(X0))),
% 105.51/13.77 inference(resolution,[status(thm)],[f921,f198])).
% 105.51/13.77 fof(f2857,plain,(
% 105.51/13.77 subset(sK17_skl,sK18_skl)|subset(sK17_skl,sK18_skl)),
% 105.51/13.77 inference(resolution,[status(thm)],[f1841,f97])).
% 105.51/13.77 fof(f2865,plain,(
% 105.51/13.77 subset(sK17_skl,sK18_skl)),
% 105.51/13.77 inference(duplicate_literals_removal,[status(thm)],[f2857])).
% 105.51/13.77 fof(f6707,plain,(
% 105.51/13.77 ~subset(sK17_skl,sK18_skl)|~subset(singleton(sK17_skl),sK18_skl)|ordinal_subset(succ(sK17_skl),sK18_skl)),
% 105.51/13.77 inference(resolution,[status(thm)],[f2011,f197])).
% 105.51/13.77 fof(f6712,plain,(
% 105.51/13.77 ~subset(singleton(sK17_skl),sK18_skl)|ordinal_subset(succ(sK17_skl),sK18_skl)),
% 105.51/13.77 inference(forward_subsumption_resolution,[status(thm)],[f6707,f2865])).
% 105.51/13.77 fof(f23925,plain,(
% 105.51/13.77 ~subset(singleton(sK17_skl),sK18_skl)),
% 105.51/13.77 inference(forward_subsumption_resolution,[status(thm)],[f6712,f1346])).
% 105.51/13.77 fof(f23932,plain,(
% 105.51/13.77 sK2_skl(sK18_skl,singleton(sK17_skl))=sK17_skl),
% 105.51/13.77 inference(resolution,[status(thm)],[f23925,f283])).
% 105.51/13.77 fof(f24001,plain,(
% 105.51/13.77 subset(singleton(sK17_skl),sK18_skl)|~in(sK17_skl,sK18_skl)),
% 105.51/13.77 inference(paramodulation,[status(thm)],[f23932,f97])).
% 105.51/13.77 fof(f24027,plain,(
% 105.51/13.77 ~in(sK17_skl,sK18_skl)),
% 105.51/13.77 inference(forward_subsumption_resolution,[status(thm)],[f24001,f23925])).
% 105.51/13.77 fof(f24028,plain,(
% 105.51/13.77 $false),
% 105.51/13.77 inference(forward_subsumption_resolution,[status(thm)],[f24027,f1331])).
% 105.51/13.77 % SZS output end CNFRefutation for theBenchmark.p
% 6.79/13.82 % Elapsed time: 13.422671 seconds
% 6.79/13.82 % CPU time: 106.188308 seconds
% 6.79/13.82 % Total memory used: 645.173 MB
% 6.79/13.82 % Net memory used: 562.803 MB
%------------------------------------------------------------------------------