%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM600+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 01:43:19 PM UTC 2026
% Result : Theorem 0.03s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM600+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.03/0.35 % CPULimit : 300
% 0.03/0.35 % WCLimit : 300
% 0.03/0.35 % DateTime : Mon Sep 21 02:44:17 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.38 % Drodi V4.1.1
% 0.03/0.41 % Refutation found
% 0.03/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.41 fof(f3,axiom,(
% 0.03/0.41 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.03/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.41 fof(f66,definition,(
% 0.03/0.41 (! [W0,W1] :( ( aFunction0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtlbdtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElementOf0(W3,szDzozmdt0(W0))& sdtlpdtrp0(W0,W3) = W1 ) ) )) ) )) )),
% 0.03/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.41 fof(f73,hypothesis,(
% 0.03/0.41 ( aSet0(xT)& isFinite0(xT) ) ),
% 0.03/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.41 fof(f92,hypothesis,(
% 0.03/0.41 ( aFunction0(xd)& szDzozmdt0(xd) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( ( aSet0(W1)& ( ( ( (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0))) ))| aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )& sbrdtbr0(W1) = xk )| aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) ) )=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )) )) ),
% 0.03/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.41 fof(f94,hypothesis,(
% 0.03/0.41 ( aElementOf0(szDzizrdt0(xd),xT)& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))& (! [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))<=> ( aElementOf0(W0,szDzozmdt0(xd))& sdtlpdtrp0(xd,W0) = szDzizrdt0(xd) ) ) )) ),
% 0.03/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.41 fof(f97,conjecture,(
% 0.03/0.41 (! [W0] :( ( (? [W1] :( aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))& sdtlpdtrp0(xe,W1) = W0 ))& aElementOf0(W0,xO) )=> (? [W1] :( aElementOf0(W1,szNzAzT0)& ( sdtlpdtrp0(xd,W1) = szDzizrdt0(xd)| aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )& sdtlpdtrp0(xe,W1) = W0 ) )) )),
% 0.03/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.41 fof(f98,negated_conjecture,(
% 0.03/0.41 ~((! [W0] :( ( (? [W1] :( aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))& sdtlpdtrp0(xe,W1) = W0 ))& aElementOf0(W0,xO) )=> (? [W1] :( aElementOf0(W1,szNzAzT0)& ( sdtlpdtrp0(xd,W1) = szDzizrdt0(xd)| aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )& sdtlpdtrp0(xe,W1) = W0 ) )) ))),
% 0.03/0.41 inference(negated_conjecture,[status(cth)],[f97])).
% 0.03/0.41 fof(f105,plain,(
% 0.03/0.41 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.03/0.41 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.03/0.41 fof(f106,plain,(
% 0.03/0.41 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.03/0.41 inference(cnf_transformation,[status(thm)],[f105])).
% 0.03/0.41 fof(f311,plain,(
% 0.03/0.41 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|(![W2]: (W2=sdtlbdtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))))))),
% 0.03/0.41 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 0.03/0.41 fof(f312,plain,(
% 0.03/0.41 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtlbdtrb0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1))&(aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1))))))&(W2=sdtlbdtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1))&(aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))))))))),
% 0.03/0.41 inference(NNF_transformation,[status(thm)],[f311])).
% 0.03/0.41 fof(f313,plain,(
% 0.03/0.41 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtlbdtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1)))))))&(![W2]: (W2=sdtlbdtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1))&(aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))))))))),
% 0.03/0.41 inference(miniscoping,[status(thm)],[f312])).
% 0.03/0.41 fof(f314,plain,(
% 0.03/0.41 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtlbdtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1)))))))&(![W2]: (W2=sdtlbdtrb0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK12_skl(W2,W1,W0),W2)|(~aElementOf0(sK12_skl(W2,W1,W0),szDzozmdt0(W0))|~sdtlpdtrp0(W0,sK12_skl(W2,W1,W0))=W1))&(aElementOf0(sK12_skl(W2,W1,W0),W2)|(aElementOf0(sK12_skl(W2,W1,W0),szDzozmdt0(W0))&sdtlpdtrp0(W0,sK12_skl(W2,W1,W0))=W1))))))))),
% 0.03/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(W3,sK12_skl(W2,W1,W0))],[f313])).
% 0.03/0.42 fof(f316,plain,(
% 0.03/0.42 ![X0,X1,X2,X3]: (~aFunction0(X0)|~aElement0(X1)|~X2=sdtlbdtrb0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(X3,szDzozmdt0(X0)))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f314])).
% 0.03/0.42 fof(f355,plain,(
% 0.03/0.42 aSet0(xT)),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f73])).
% 0.03/0.42 fof(f536,plain,(
% 0.03/0.42 (aFunction0(xd)&szDzozmdt0(xd)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: ((~aSet0(W1)|((((?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0)))))&~aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))))|~sbrdtbr0(W1)=xk)&~aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))))|sdtlpdtrp0(xd,W0)=sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)))))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 0.03/0.42 fof(f537,plain,(
% 0.03/0.42 (aFunction0(xd)&szDzozmdt0(xd)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: ((~aSet0(W1)|((((aElementOf0(sK32_skl(W1,W0),W1)&~aElementOf0(sK32_skl(W1,W0),sdtlpdtrp0(xN,szszuzczcdt0(W0))))&~aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))))|~sbrdtbr0(W1)=xk)&~aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))))|sdtlpdtrp0(xd,W0)=sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)))))),
% 0.03/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(W2,sK32_skl(W1,W0))],[f536])).
% 0.03/0.42 fof(f538,plain,(
% 0.03/0.42 aFunction0(xd)),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f537])).
% 0.03/0.42 fof(f539,plain,(
% 0.03/0.42 szDzozmdt0(xd)=szNzAzT0),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f537])).
% 0.03/0.42 fof(f554,plain,(
% 0.03/0.42 (aElementOf0(szDzizrdt0(xd),xT)&aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))))&(![W0]: ((~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))&(aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))))),
% 0.03/0.42 inference(NNF_transformation,[status(thm)],[f94])).
% 0.03/0.42 fof(f555,plain,(
% 0.03/0.42 (aElementOf0(szDzizrdt0(xd),xT)&aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))))&((![W0]: (~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))&(![W0]: (aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))))),
% 0.03/0.42 inference(miniscoping,[status(thm)],[f554])).
% 0.03/0.42 fof(f556,plain,(
% 0.03/0.42 aElementOf0(szDzizrdt0(xd),xT)),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f555])).
% 0.03/0.42 fof(f575,plain,(
% 0.03/0.42 (?[W0]: (((?[W1]: (aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,W1)=W0))&aElementOf0(W0,xO))&(![W1]: ((~aElementOf0(W1,szNzAzT0)|(~sdtlpdtrp0(xd,W1)=szDzizrdt0(xd)&~aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))))|~sdtlpdtrp0(xe,W1)=W0))))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f98])).
% 0.03/0.42 fof(f576,plain,(
% 0.03/0.42 (((aElementOf0(sK36_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,sK36_skl)=sK35_skl)&aElementOf0(sK35_skl,xO))&(![W1]: ((~aElementOf0(W1,szNzAzT0)|(~sdtlpdtrp0(xd,W1)=szDzizrdt0(xd)&~aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))))|~sdtlpdtrp0(xe,W1)=sK35_skl)))),
% 0.03/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl]),skolemize(W0,sK35_skl),skolemize(W1,sK36_skl)],[f575])).
% 0.03/0.42 fof(f577,plain,(
% 0.03/0.42 aElementOf0(sK36_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f576])).
% 0.03/0.42 fof(f578,plain,(
% 0.03/0.42 sdtlpdtrp0(xe,sK36_skl)=sK35_skl),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f576])).
% 0.03/0.42 fof(f581,plain,(
% 0.03/0.42 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|~sdtlpdtrp0(xe,X0)=sK35_skl)),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f576])).
% 0.03/0.42 fof(f785,plain,(
% 0.03/0.42 ![X0,X1,X2]: (~aFunction0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtlbdtrb0(X0,X1))|aElementOf0(X2,szDzozmdt0(X0)))),
% 0.03/0.42 inference(destructive_equality_resolution,[status(thm)],[f316])).
% 0.03/0.42 fof(f820,plain,(
% 0.03/0.42 ~aElementOf0(sK36_skl,szNzAzT0)|~sdtlpdtrp0(xe,sK36_skl)=sK35_skl),
% 0.03/0.42 inference(resolution,[status(thm)],[f581,f577])).
% 0.03/0.42 fof(f821,definition,(
% 0.03/0.42 sQ0_spl <=> (aElementOf0(sK36_skl,szNzAzT0))),
% 0.03/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.03/0.42 fof(f823,plain,(
% 0.03/0.42 ~aElementOf0(sK36_skl,szNzAzT0)|sQ0_spl),
% 0.03/0.42 inference(component_clause,[status(thm)],[f821])).
% 0.03/0.42 fof(f824,definition,(
% 0.03/0.42 sQ1_spl <=> (sdtlpdtrp0(xe,sK36_skl)=sK35_skl)),
% 0.03/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.03/0.42 fof(f826,plain,(
% 0.03/0.42 ~sdtlpdtrp0(xe,sK36_skl)=sK35_skl|sQ1_spl),
% 0.03/0.42 inference(component_clause,[status(thm)],[f824])).
% 0.03/0.42 fof(f827,plain,(
% 0.03/0.42 ~sQ0_spl|~sQ1_spl),
% 0.03/0.42 inference(split_clause,[status(thm)],[f820,f821,f824])).
% 0.03/0.42 fof(f829,plain,(
% 0.03/0.42 ~aFunction0(xd)|~aElement0(szDzizrdt0(xd))|aElementOf0(sK36_skl,szDzozmdt0(xd))),
% 0.03/0.42 inference(resolution,[status(thm)],[f785,f577])).
% 0.03/0.42 fof(f830,definition,(
% 0.03/0.42 sQ2_spl <=> (aFunction0(xd))),
% 0.03/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.03/0.42 fof(f832,plain,(
% 0.03/0.42 ~aFunction0(xd)|sQ2_spl),
% 0.03/0.42 inference(component_clause,[status(thm)],[f830])).
% 0.03/0.42 fof(f833,definition,(
% 0.03/0.42 sQ3_spl <=> (aElement0(szDzizrdt0(xd)))),
% 0.03/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.03/0.42 fof(f836,definition,(
% 0.03/0.42 sQ4_spl <=> (aElementOf0(sK36_skl,szDzozmdt0(xd)))),
% 0.03/0.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.03/0.42 fof(f837,plain,(
% 0.03/0.42 aElementOf0(sK36_skl,szDzozmdt0(xd))|~sQ4_spl),
% 0.03/0.42 inference(component_clause,[status(thm)],[f836])).
% 0.03/0.42 fof(f839,plain,(
% 0.03/0.42 ~sQ2_spl|~sQ3_spl|sQ4_spl),
% 0.03/0.42 inference(split_clause,[status(thm)],[f829,f830,f833,f836])).
% 0.03/0.42 fof(f840,plain,(
% 0.03/0.42 aElementOf0(sK36_skl,szNzAzT0)|~sQ4_spl),
% 0.03/0.42 inference(forward_demodulation,[status(thm)],[f539,f837])).
% 0.03/0.42 fof(f841,plain,(
% 0.03/0.42 $false|sQ0_spl|~sQ4_spl),
% 0.03/0.42 inference(forward_subsumption_resolution,[status(thm)],[f840,f823])).
% 0.03/0.42 fof(f842,plain,(
% 0.03/0.42 sQ0_spl|~sQ4_spl),
% 0.03/0.42 inference(contradiction_clause,[status(thm)],[f841])).
% 0.03/0.42 fof(f843,plain,(
% 0.03/0.42 ~sK35_skl=sK35_skl|sQ1_spl),
% 0.03/0.42 inference(forward_demodulation,[status(thm)],[f578,f826])).
% 0.03/0.42 fof(f844,plain,(
% 0.03/0.42 $false|sQ1_spl),
% 0.03/0.42 inference(trivial_equality_resolution,[status(thm)],[f843])).
% 0.03/0.42 fof(f845,plain,(
% 0.03/0.42 sQ1_spl),
% 0.03/0.42 inference(contradiction_clause,[status(thm)],[f844])).
% 0.03/0.42 fof(f856,plain,(
% 0.03/0.42 $false|sQ2_spl),
% 0.03/0.42 inference(forward_subsumption_resolution,[status(thm)],[f832,f538])).
% 0.03/0.42 fof(f857,plain,(
% 0.03/0.42 sQ2_spl),
% 0.03/0.42 inference(contradiction_clause,[status(thm)],[f856])).
% 0.03/0.42 fof(f858,plain,(
% 0.03/0.42 ~aSet0(xT)|aElement0(szDzizrdt0(xd))),
% 0.03/0.42 inference(resolution,[status(thm)],[f106,f556])).
% 0.03/0.42 fof(f861,definition,(
% 0.03/0.42 sQ6_spl <=> (aSet0(xT))),
% 0.03/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.03/0.42 fof(f863,plain,(
% 0.03/0.42 ~aSet0(xT)|sQ6_spl),
% 0.03/0.42 inference(component_clause,[status(thm)],[f861])).
% 0.03/0.42 fof(f864,plain,(
% 0.03/0.42 ~sQ6_spl|sQ3_spl),
% 0.03/0.42 inference(split_clause,[status(thm)],[f858,f861,f833])).
% 0.03/0.42 fof(f879,plain,(
% 0.03/0.42 $false|sQ6_spl),
% 0.03/0.42 inference(forward_subsumption_resolution,[status(thm)],[f863,f355])).
% 0.03/0.42 fof(f880,plain,(
% 0.03/0.42 sQ6_spl),
% 0.03/0.42 inference(contradiction_clause,[status(thm)],[f879])).
% 0.03/0.42 fof(f881,plain,(
% 0.03/0.42 $false),
% 0.03/0.42 inference(sat_refutation,[status(thm)],[f827,f839,f842,f845,f857,f864,f880])).
% 0.03/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.41/0.46 % Elapsed time: 0.090704 seconds
% 0.41/0.46 % CPU time: 0.198063 seconds
% 0.41/0.46 % Total memory used: 124.883 MB
% 0.41/0.46 % Net memory used: 124.532 MB
%------------------------------------------------------------------------------