%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU236+1 : TPTP v9.3.1. Released v3.3.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 02:22:05 PM UTC 2026
% Result : Theorem 91.32s 17.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU236+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.45 % Computer : n003.cluster.edu
% 0.16/5.45 % Model : x86_64 x86_64
% 0.16/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.45 % Memory : 8046.5625MB
% 0.16/5.45 % OS : Linux 6.8.0-71-generic
% 0.16/5.45 % CPULimit : 300
% 0.16/5.45 % WCLimit : 300
% 0.16/5.45 % DateTime : Mon Sep 21 06:03:35 UTC 2026
% 0.16/5.45 % CPUTime :
% 0.16/5.46 % Drodi V4.1.1
% 91.32/17.10 % Refutation found
% 91.32/17.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 91.32/17.10 % SZS output start CNFRefutation for theBenchmark
% 91.32/17.10 fof(f3,axiom,(
% 91.32/17.10 (! [A] :( ordinal(A)=> ( epsilon_transitive(A)& epsilon_connected(A) ) ) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f10,axiom,(
% 91.32/17.10 (! [A] : succ(A) = set_union2(A,singleton(A)) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f11,axiom,(
% 91.32/17.10 (! [A,B] :( B = singleton(A)<=> (! [C] :( in(C,B)<=> C = A ) )) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f12,axiom,(
% 91.32/17.10 (! [A] :( epsilon_transitive(A)<=> (! [B] :( in(B,A)=> subset(B,A) ) )) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f13,axiom,(
% 91.32/17.10 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f27,axiom,(
% 91.32/17.10 (! [A] :( ordinal(A)=> ( ~ empty(succ(A))& epsilon_transitive(succ(A))& epsilon_connected(succ(A))& ordinal(succ(A)) ) ) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f43,axiom,(
% 91.32/17.10 (! [A,B] :( ( ordinal(A)& ordinal(B) )=> ( ordinal_subset(A,B)<=> subset(A,B) ) ) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f46,axiom,(
% 91.32/17.10 (! [A] : in(A,succ(A)) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f50,conjecture,(
% 91.32/17.10 (! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ( in(A,B)<=> ordinal_subset(succ(A),B) ) ) )) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f51,negated_conjecture,(
% 91.32/17.10 ~((! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ( in(A,B)<=> ordinal_subset(succ(A),B) ) ) )) ))),
% 91.32/17.10 inference(negated_conjecture,[status(cth)],[f50])).
% 91.32/17.10 fof(f58,axiom,(
% 91.32/17.10 (! [A,B,C] :( ( subset(A,B)& subset(C,B) )=> subset(set_union2(A,C),B) ) )),
% 91.32/17.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.32/17.10 fof(f63,plain,(
% 91.32/17.10 ![A]: (~ordinal(A)|(epsilon_transitive(A)&epsilon_connected(A)))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 91.32/17.10 fof(f64,plain,(
% 91.32/17.10 ![X0]: (~ordinal(X0)|epsilon_transitive(X0))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f63])).
% 91.32/17.10 fof(f81,plain,(
% 91.32/17.10 ![X0]: (succ(X0)=set_union2(X0,singleton(X0)))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f10])).
% 91.32/17.10 fof(f82,plain,(
% 91.32/17.10 ![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)))))),
% 91.32/17.10 inference(NNF_transformation,[status(thm)],[f11])).
% 91.32/17.10 fof(f83,plain,(
% 91.32/17.10 (![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)))))),
% 91.32/17.10 inference(miniscoping,[status(thm)],[f82])).
% 91.32/17.10 fof(f84,plain,(
% 91.32/17.10 (![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))))),
% 91.32/17.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f83])).
% 91.32/17.10 fof(f85,plain,(
% 91.32/17.10 ![X0,X1,X2]: (~X0=singleton(X1)|~in(X2,X0)|X2=X1)),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f84])).
% 91.32/17.10 fof(f89,plain,(
% 91.32/17.10 ![A]: (epsilon_transitive(A)<=>(![B]: (~in(B,A)|subset(B,A))))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 91.32/17.10 fof(f90,plain,(
% 91.32/17.10 ![A]: ((~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A))))&(epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 91.32/17.10 inference(NNF_transformation,[status(thm)],[f89])).
% 91.32/17.10 fof(f91,plain,(
% 91.32/17.10 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 91.32/17.10 inference(miniscoping,[status(thm)],[f90])).
% 91.32/17.10 fof(f92,plain,(
% 91.32/17.10 (![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))))),
% 91.32/17.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f91])).
% 91.32/17.10 fof(f93,plain,(
% 91.32/17.10 ![X0,X1]: (~epsilon_transitive(X0)|~in(X1,X0)|subset(X1,X0))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f92])).
% 91.32/17.10 fof(f96,plain,(
% 91.32/17.10 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 91.32/17.10 fof(f97,plain,(
% 91.32/17.10 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 91.32/17.10 inference(NNF_transformation,[status(thm)],[f96])).
% 91.32/17.10 fof(f98,plain,(
% 91.32/17.10 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 91.32/17.10 inference(miniscoping,[status(thm)],[f97])).
% 91.32/17.10 fof(f99,plain,(
% 91.32/17.10 (![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))))),
% 91.32/17.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f98])).
% 91.32/17.10 fof(f100,plain,(
% 91.32/17.10 ![X0,X1,X2]: (~subset(X0,X1)|~in(X2,X0)|in(X2,X1))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f99])).
% 91.32/17.10 fof(f101,plain,(
% 91.32/17.10 ![X0,X1]: (subset(X0,X1)|in(sK2_skl(X1,X0),X0))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f99])).
% 91.32/17.10 fof(f102,plain,(
% 91.32/17.10 ![X0,X1]: (subset(X0,X1)|~in(sK2_skl(X1,X0),X1))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f99])).
% 91.32/17.10 fof(f123,plain,(
% 91.32/17.10 ![A]: (~ordinal(A)|(((~empty(succ(A))&epsilon_transitive(succ(A)))&epsilon_connected(succ(A)))&ordinal(succ(A))))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 91.32/17.10 fof(f127,plain,(
% 91.32/17.10 ![X0]: (~ordinal(X0)|ordinal(succ(X0)))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f123])).
% 91.32/17.10 fof(f180,plain,(
% 91.32/17.10 ![A,B]: ((~ordinal(A)|~ordinal(B))|(ordinal_subset(A,B)<=>subset(A,B)))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 91.32/17.10 fof(f181,plain,(
% 91.32/17.10 ![A,B]: ((~ordinal(A)|~ordinal(B))|((~ordinal_subset(A,B)|subset(A,B))&(ordinal_subset(A,B)|~subset(A,B))))),
% 91.32/17.10 inference(NNF_transformation,[status(thm)],[f180])).
% 91.32/17.10 fof(f182,plain,(
% 91.32/17.10 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|~ordinal_subset(X0,X1)|subset(X0,X1))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f181])).
% 91.32/17.10 fof(f183,plain,(
% 91.32/17.10 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|ordinal_subset(X0,X1)|~subset(X0,X1))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f181])).
% 91.32/17.10 fof(f189,plain,(
% 91.32/17.10 ![X0]: (in(X0,succ(X0)))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f46])).
% 91.32/17.10 fof(f195,plain,(
% 91.32/17.10 (?[A]: (ordinal(A)&(?[B]: (ordinal(B)&(in(A,B)<~>ordinal_subset(succ(A),B))))))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 91.32/17.10 fof(f196,plain,(
% 91.32/17.10 ?[A]: (ordinal(A)&(?[B]: (ordinal(B)&((in(A,B)|ordinal_subset(succ(A),B))&(~in(A,B)|~ordinal_subset(succ(A),B))))))),
% 91.32/17.10 inference(NNF_transformation,[status(thm)],[f195])).
% 91.32/17.10 fof(f197,plain,(
% 91.32/17.10 (ordinal(sK16_skl)&(ordinal(sK17_skl)&((in(sK16_skl,sK17_skl)|ordinal_subset(succ(sK16_skl),sK17_skl))&(~in(sK16_skl,sK17_skl)|~ordinal_subset(succ(sK16_skl),sK17_skl)))))),
% 91.32/17.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(A,sK16_skl),skolemize(B,sK17_skl)],[f196])).
% 91.32/17.10 fof(f198,plain,(
% 91.32/17.10 ordinal(sK16_skl)),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f197])).
% 91.32/17.10 fof(f199,plain,(
% 91.32/17.10 ordinal(sK17_skl)),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f197])).
% 91.32/17.10 fof(f200,plain,(
% 91.32/17.10 in(sK16_skl,sK17_skl)|ordinal_subset(succ(sK16_skl),sK17_skl)),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f197])).
% 91.32/17.10 fof(f201,plain,(
% 91.32/17.10 ~in(sK16_skl,sK17_skl)|~ordinal_subset(succ(sK16_skl),sK17_skl)),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f197])).
% 91.32/17.10 fof(f220,plain,(
% 91.32/17.10 ![A,B,C]: ((~subset(A,B)|~subset(C,B))|subset(set_union2(A,C),B))),
% 91.32/17.10 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 91.32/17.10 fof(f221,plain,(
% 91.32/17.10 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X2,X1)|subset(set_union2(X0,X2),X1))),
% 91.32/17.10 inference(cnf_transformation,[status(thm)],[f220])).
% 91.32/17.10 fof(f222,plain,(
% 91.32/17.10 ![X0,X1]: (~in(X0,singleton(X1))|X0=X1)),
% 91.32/17.10 inference(destructive_equality_resolution,[status(thm)],[f85])).
% 91.32/17.10 fof(f267,plain,(
% 91.32/17.10 ![X0,X1,X2]: (~in(X0,X1)|in(X0,X2)|~epsilon_transitive(X2)|~in(X1,X2))),
% 91.32/17.10 inference(resolution,[status(thm)],[f100,f93])).
% 91.32/17.10 fof(f268,plain,(
% 91.32/17.10 ![X0,X1,X2]: (~in(X0,X1)|in(X0,X2)|~ordinal(X1)|~ordinal(X2)|~ordinal_subset(X1,X2))),
% 91.32/17.10 inference(resolution,[status(thm)],[f100,f182])).
% 91.32/17.10 fof(f271,plain,(
% 91.32/17.10 ![X0,X1]: (~in(X0,X1)|in(X0,sK17_skl)|~ordinal(X1)|~ordinal_subset(X1,sK17_skl))),
% 91.32/17.10 inference(resolution,[status(thm)],[f268,f199])).
% 91.32/17.10 fof(f284,plain,(
% 91.32/17.10 ![X0,X1]: (subset(singleton(X0),X1)|sK2_skl(X1,singleton(X0))=X0)),
% 86.65/17.15 inference(resolution,[status(thm)],[f101,f222])).
% 86.65/17.15 fof(f327,plain,(
% 86.65/17.15 ![X0]: (in(X0,sK17_skl)|~ordinal(succ(X0))|~ordinal_subset(succ(X0),sK17_skl))),
% 86.65/17.15 inference(resolution,[status(thm)],[f271,f189])).
% 86.65/17.15 fof(f497,plain,(
% 86.65/17.15 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X2,X1)|~ordinal(set_union2(X0,X2))|~ordinal(X1)|ordinal_subset(set_union2(X0,X2),X1))),
% 86.65/17.15 inference(resolution,[status(thm)],[f221,f183])).
% 86.65/17.15 fof(f513,plain,(
% 86.65/17.15 ![X0,X1]: (~subset(X0,X1)|~subset(singleton(X0),X1)|~ordinal(succ(X0))|~ordinal(X1)|ordinal_subset(set_union2(X0,singleton(X0)),X1))),
% 86.65/17.15 inference(paramodulation,[status(thm)],[f81,f497])).
% 86.65/17.15 fof(f518,plain,(
% 86.65/17.15 ![X0,X1]: (~subset(X0,X1)|~subset(singleton(X0),X1)|~ordinal(succ(X0))|~ordinal(X1)|ordinal_subset(succ(X0),X1))),
% 86.65/17.15 inference(forward_demodulation,[status(thm)],[f81,f513])).
% 86.65/17.15 fof(f909,plain,(
% 86.65/17.15 ![X0]: (in(X0,sK17_skl)|~ordinal_subset(succ(X0),sK17_skl)|~ordinal(X0))),
% 86.65/17.15 inference(resolution,[status(thm)],[f327,f127])).
% 86.65/17.15 fof(f979,plain,(
% 86.65/17.15 ![X0,X1]: (~subset(X0,X1)|~subset(singleton(X0),X1)|~ordinal(X1)|ordinal_subset(succ(X0),X1)|~ordinal(X0))),
% 86.65/17.15 inference(resolution,[status(thm)],[f518,f127])).
% 86.65/17.15 fof(f1174,plain,(
% 86.65/17.15 in(sK16_skl,sK17_skl)|~ordinal(sK16_skl)|in(sK16_skl,sK17_skl)),
% 86.65/17.15 inference(resolution,[status(thm)],[f909,f200])).
% 86.65/17.15 fof(f1177,plain,(
% 86.65/17.15 in(sK16_skl,sK17_skl)|~ordinal(sK16_skl)),
% 86.65/17.15 inference(duplicate_literals_removal,[status(thm)],[f1174])).
% 86.65/17.15 fof(f1178,plain,(
% 86.65/17.15 in(sK16_skl,sK17_skl)),
% 86.65/17.15 inference(forward_subsumption_resolution,[status(thm)],[f1177,f198])).
% 86.65/17.15 fof(f1199,plain,(
% 86.65/17.15 ~ordinal_subset(succ(sK16_skl),sK17_skl)),
% 86.65/17.15 inference(backward_subsumption_resolution,[status(thm)],[f201,f1178])).
% 86.65/17.15 fof(f1202,plain,(
% 86.65/17.15 ![X0]: (~in(X0,sK16_skl)|in(X0,sK17_skl)|~epsilon_transitive(sK17_skl))),
% 86.65/17.15 inference(resolution,[status(thm)],[f1178,f267])).
% 86.65/17.15 fof(f2079,plain,(
% 86.65/17.15 ![X0]: (~in(X0,sK16_skl)|in(X0,sK17_skl)|~ordinal(sK17_skl))),
% 86.65/17.15 inference(resolution,[status(thm)],[f1202,f64])).
% 86.65/17.15 fof(f2081,plain,(
% 86.65/17.15 ![X0]: (~in(X0,sK16_skl)|in(X0,sK17_skl))),
% 86.65/17.15 inference(forward_subsumption_resolution,[status(thm)],[f2079,f199])).
% 86.65/17.15 fof(f2088,plain,(
% 86.65/17.15 ![X0]: (in(sK2_skl(X0,sK16_skl),sK17_skl)|subset(sK16_skl,X0))),
% 86.65/17.15 inference(resolution,[status(thm)],[f2081,f101])).
% 86.65/17.15 fof(f2128,plain,(
% 86.65/17.15 ![X0]: (~subset(X0,sK17_skl)|~subset(singleton(X0),sK17_skl)|ordinal_subset(succ(X0),sK17_skl)|~ordinal(X0))),
% 86.65/17.15 inference(resolution,[status(thm)],[f979,f199])).
% 86.65/17.15 fof(f3647,plain,(
% 86.65/17.15 subset(sK16_skl,sK17_skl)|subset(sK16_skl,sK17_skl)),
% 86.65/17.15 inference(resolution,[status(thm)],[f2088,f102])).
% 86.65/17.15 fof(f3660,plain,(
% 86.65/17.15 subset(sK16_skl,sK17_skl)),
% 86.65/17.15 inference(duplicate_literals_removal,[status(thm)],[f3647])).
% 86.65/17.15 fof(f7017,plain,(
% 86.65/17.15 ~subset(sK16_skl,sK17_skl)|~subset(singleton(sK16_skl),sK17_skl)|ordinal_subset(succ(sK16_skl),sK17_skl)),
% 86.65/17.15 inference(resolution,[status(thm)],[f2128,f198])).
% 86.65/17.15 fof(f7022,plain,(
% 86.65/17.15 ~subset(singleton(sK16_skl),sK17_skl)|ordinal_subset(succ(sK16_skl),sK17_skl)),
% 86.65/17.15 inference(forward_subsumption_resolution,[status(thm)],[f7017,f3660])).
% 86.65/17.15 fof(f19129,plain,(
% 86.65/17.15 ~subset(singleton(sK16_skl),sK17_skl)),
% 86.65/17.15 inference(forward_subsumption_resolution,[status(thm)],[f7022,f1199])).
% 86.65/17.15 fof(f19136,plain,(
% 86.65/17.15 sK2_skl(sK17_skl,singleton(sK16_skl))=sK16_skl),
% 86.65/17.15 inference(resolution,[status(thm)],[f19129,f284])).
% 86.65/17.15 fof(f19187,plain,(
% 86.65/17.15 subset(singleton(sK16_skl),sK17_skl)|~in(sK16_skl,sK17_skl)),
% 86.65/17.15 inference(paramodulation,[status(thm)],[f19136,f102])).
% 86.65/17.15 fof(f19206,plain,(
% 86.65/17.15 ~in(sK16_skl,sK17_skl)),
% 86.65/17.15 inference(forward_subsumption_resolution,[status(thm)],[f19187,f19129])).
% 86.65/17.15 fof(f19207,plain,(
% 86.65/17.15 $false),
% 86.65/17.15 inference(forward_subsumption_resolution,[status(thm)],[f19206,f1178])).
% 86.65/17.15 % SZS output end CNFRefutation for theBenchmark.p
% 86.65/17.19 % Elapsed time: 11.718453 seconds
% 86.65/17.19 % CPU time: 92.590279 seconds
% 86.65/17.19 % Total memory used: 507.842 MB
% 86.65/17.19 % Net memory used: 442.865 MB
%------------------------------------------------------------------------------