%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG049+2 : 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 : n005.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:05:13 PM UTC 2026
% Result : Theorem 214.48s 32.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG049+2 : 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.11/5.37 % Computer : n005.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 04:15:23 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 214.48/32.76 % Refutation found
% 214.48/32.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 214.48/32.76 % SZS output start CNFRefutation for theBenchmark
% 214.48/32.76 fof(f7,axiom,(
% 214.48/32.76 (! [W0] :( aNaturalNumber0(W0)=> iLess0(W0,szszuzczcdt0(W0)) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f11,axiom,(
% 214.48/32.76 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f26,axiom,(
% 214.48/32.76 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> ( ( sdtlseqdt0(sz0z00,W0)& sdtlseqdt0(sz0z00,W1) )=> ( sdtlseqdt0(sz0z00,sdtpldt0(W0,W1))& sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)) ) ) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f30,axiom,(
% 214.48/32.76 (! [W0] :( aVector0(W0)=> aNaturalNumber0(aDimensionOf0(W0)) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f31,axiom,(
% 214.48/32.76 (! [W0,W1] :( ( aVector0(W0)& aNaturalNumber0(W1) )=> aScalar0(sdtlbdtrb0(W0,W1)) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f34,axiom,(
% 214.48/32.76 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( aDimensionOf0(W0) = aDimensionOf0(W1)=> aScalar0(sdtasasdt0(W0,W1)) ) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f36,axiom,(
% 214.48/32.76 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( ( aDimensionOf0(W0) = aDimensionOf0(W1)& aDimensionOf0(W1) != sz00 )=> sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f37,hypothesis,(
% 214.48/32.76 aVector0(xs) ),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f38,hypothesis,(
% 214.48/32.76 (! [W0] :( aVector0(W0)=> ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs))=> sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ) )),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f39,hypothesis,(
% 214.48/32.76 aDimensionOf0(xs) != sz00 ),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f40,hypothesis,(
% 214.48/32.76 ( aVector0(sziznziztdt0(xs))& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ))& aVector0(sziznziztdt0(xs))& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ) )) ),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f41,hypothesis,(
% 214.48/32.76 ( aVector0(sziznziztdt0(xs))& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ))& aVector0(sziznziztdt0(xs))& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)& (! [W0] :( aNaturalNumber0(W0)=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) ))& sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ) ),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f42,conjecture,(
% 214.48/32.76 sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
% 214.48/32.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 214.48/32.76 fof(f43,negated_conjecture,(
% 214.48/32.76 ~(sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )),
% 214.48/32.76 inference(negated_conjecture,[status(cth)],[f42])).
% 214.48/32.76 fof(f59,plain,(
% 214.48/32.76 ![W0]: (~aNaturalNumber0(W0)|iLess0(W0,szszuzczcdt0(W0)))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 214.48/32.76 fof(f60,plain,(
% 214.48/32.76 ![X0]: (~aNaturalNumber0(X0)|iLess0(X0,szszuzczcdt0(X0)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f59])).
% 214.48/32.76 fof(f67,plain,(
% 214.48/32.76 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 214.48/32.76 fof(f68,plain,(
% 214.48/32.76 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f67])).
% 214.48/32.76 fof(f109,plain,(
% 214.48/32.76 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|((~sdtlseqdt0(sz0z00,W0)|~sdtlseqdt0(sz0z00,W1))|(sdtlseqdt0(sz0z00,sdtpldt0(W0,W1))&sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)))))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 214.48/32.76 fof(f110,plain,(
% 214.48/32.76 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(sz0z00,X0)|~sdtlseqdt0(sz0z00,X1)|sdtlseqdt0(sz0z00,sdtpldt0(X0,X1)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f109])).
% 214.48/32.76 fof(f119,plain,(
% 214.48/32.76 ![W0]: (~aVector0(W0)|aNaturalNumber0(aDimensionOf0(W0)))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 214.48/32.76 fof(f120,plain,(
% 214.48/32.76 ![X0]: (~aVector0(X0)|aNaturalNumber0(aDimensionOf0(X0)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f119])).
% 214.48/32.76 fof(f121,plain,(
% 214.48/32.76 ![W0,W1]: ((~aVector0(W0)|~aNaturalNumber0(W1))|aScalar0(sdtlbdtrb0(W0,W1)))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 214.48/32.76 fof(f122,plain,(
% 214.48/32.76 ![X0,X1]: (~aVector0(X0)|~aNaturalNumber0(X1)|aScalar0(sdtlbdtrb0(X0,X1)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f121])).
% 214.48/32.76 fof(f134,plain,(
% 214.48/32.76 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|(~aDimensionOf0(W0)=aDimensionOf0(W1)|aScalar0(sdtasasdt0(W0,W1))))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 214.48/32.76 fof(f135,plain,(
% 214.48/32.76 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aScalar0(sdtasasdt0(X0,X1)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f134])).
% 214.48/32.76 fof(f138,plain,(
% 214.48/32.76 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|((~aDimensionOf0(W0)=aDimensionOf0(W1)|aDimensionOf0(W1)=sz00)|sdtasasdt0(W0,W1)=sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1))))))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 214.48/32.76 fof(f139,plain,(
% 214.48/32.76 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aDimensionOf0(X1)=sz00|sdtasasdt0(X0,X1)=sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1)))))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f138])).
% 214.48/32.76 fof(f140,plain,(
% 214.48/32.76 aVector0(xs)),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f37])).
% 214.48/32.76 fof(f141,plain,(
% 214.48/32.76 ![W0]: (~aVector0(W0)|(~iLess0(aDimensionOf0(W0),aDimensionOf0(xs))|sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0))))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 214.48/32.76 fof(f142,plain,(
% 214.48/32.76 ![X0]: (~aVector0(X0)|~iLess0(aDimensionOf0(X0),aDimensionOf0(xs))|sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f141])).
% 214.48/32.76 fof(f143,plain,(
% 214.48/32.76 ~aDimensionOf0(xs)=sz00),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f39])).
% 214.48/32.76 fof(f144,plain,(
% 214.48/32.76 ((((aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(sziznziztdt0(xs),W0)=sdtlbdtrb0(xs,W0))))&aVector0(sziznziztdt0(xs)))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(sziznziztdt0(xs),W0)=sdtlbdtrb0(xs,W0)))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 214.48/32.76 fof(f145,plain,(
% 214.48/32.76 aVector0(sziznziztdt0(xs))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f144])).
% 214.48/32.76 fof(f146,plain,(
% 214.48/32.76 szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs)),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f144])).
% 214.48/32.76 fof(f151,plain,(
% 214.48/32.76 (((((aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(sziznziztdt0(xs),W0)=sdtlbdtrb0(xs,W0))))&aVector0(sziznziztdt0(xs)))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&(![W0]: (~aNaturalNumber0(W0)|sdtlbdtrb0(sziznziztdt0(xs),W0)=sdtlbdtrb0(xs,W0))))&sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 214.48/32.76 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 214.48/32.76 fof(f158,plain,(
% 214.48/32.76 sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f151])).
% 214.48/32.76 fof(f159,plain,(
% 214.48/32.76 ~sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))),
% 214.48/32.76 inference(cnf_transformation,[status(thm)],[f43])).
% 214.48/32.76 fof(f199,plain,(
% 214.48/32.76 ~aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xs))|aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))),
% 214.48/32.76 inference(resolution,[status(thm)],[f145,f135])).
% 214.48/32.76 fof(f203,plain,(
% 214.48/32.76 aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))),
% 214.48/32.76 inference(trivial_equality_resolution,[status(thm)],[f199])).
% 19.73/32.92 fof(f339,plain,(
% 19.73/32.92 aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs)))),
% 19.73/32.92 inference(resolution,[status(thm)],[f120,f145])).
% 19.73/32.92 fof(f340,plain,(
% 19.73/32.92 aNaturalNumber0(aDimensionOf0(xs))),
% 19.73/32.92 inference(resolution,[status(thm)],[f120,f140])).
% 19.73/32.92 fof(f395,plain,(
% 19.73/32.92 iLess0(aDimensionOf0(sziznziztdt0(xs)),szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))))),
% 19.73/32.92 inference(resolution,[status(thm)],[f60,f339])).
% 19.73/32.92 fof(f533,plain,(
% 19.73/32.92 ~aDimensionOf0(xs)=aDimensionOf0(xs)|aDimensionOf0(xs)=sz00|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 19.73/32.92 inference(resolution,[status(thm)],[f139,f140])).
% 19.73/32.92 fof(f538,plain,(
% 19.73/32.92 aDimensionOf0(xs)=sz00|sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 19.73/32.92 inference(trivial_equality_resolution,[status(thm)],[f533])).
% 19.73/32.92 fof(f539,plain,(
% 19.73/32.92 sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 19.73/32.92 inference(forward_subsumption_resolution,[status(thm)],[f538,f143])).
% 19.73/32.92 fof(f712,plain,(
% 19.73/32.92 ![X0]: (~aNaturalNumber0(X0)|aScalar0(sdtlbdtrb0(xs,X0)))),
% 19.73/32.92 inference(resolution,[status(thm)],[f122,f140])).
% 19.73/32.92 fof(f731,plain,(
% 19.73/32.92 aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs)))),
% 19.73/32.92 inference(resolution,[status(thm)],[f712,f340])).
% 19.73/32.92 fof(f792,plain,(
% 19.73/32.92 aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 19.73/32.92 inference(resolution,[status(thm)],[f731,f68])).
% 19.73/32.92 fof(f6056,plain,(
% 19.73/32.92 ![X0]: (~aScalar0(X0)|~aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))|~sdtlseqdt0(sz0z00,X0)|sdtlseqdt0(sz0z00,sdtpldt0(X0,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))))),
% 19.73/32.92 inference(resolution,[status(thm)],[f158,f110])).
% 19.73/32.92 fof(f15836,plain,(
% 19.73/32.92 iLess0(aDimensionOf0(sziznziztdt0(xs)),aDimensionOf0(xs))),
% 19.73/32.92 inference(forward_demodulation,[status(thm)],[f146,f395])).
% 19.73/32.92 fof(f15837,plain,(
% 19.73/32.92 ~aVector0(sziznziztdt0(xs))|sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))),
% 19.73/32.92 inference(resolution,[status(thm)],[f15836,f142])).
% 19.73/32.92 fof(f15838,plain,(
% 19.73/32.92 sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))),
% 19.73/32.92 inference(forward_subsumption_resolution,[status(thm)],[f15837,f145])).
% 19.73/32.92 fof(f140385,plain,(
% 19.73/32.92 ![X0]: (~aScalar0(X0)|~sdtlseqdt0(sz0z00,X0)|sdtlseqdt0(sz0z00,sdtpldt0(X0,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))))),
% 19.73/32.92 inference(backward_subsumption_resolution,[status(thm)],[f6056,f792])).
% 19.73/32.92 fof(f145875,plain,(
% 19.73/32.92 ~aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))|sdtlseqdt0(sz0z00,sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))),
% 19.73/32.92 inference(resolution,[status(thm)],[f140385,f15838])).
% 19.73/32.92 fof(f145891,plain,(
% 19.73/32.92 ~aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))|sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))),
% 19.73/32.92 inference(forward_demodulation,[status(thm)],[f539,f145875])).
% 19.73/32.92 fof(f145892,plain,(
% 19.73/32.92 sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))),
% 19.73/32.92 inference(forward_subsumption_resolution,[status(thm)],[f145891,f203])).
% 19.73/32.92 fof(f146141,plain,(
% 19.73/32.92 $false),
% 19.73/32.92 inference(forward_subsumption_resolution,[status(thm)],[f145892,f159])).
% 19.73/32.92 % SZS output end CNFRefutation for theBenchmark.p
% 19.73/32.98 % Elapsed time: 27.559903 seconds
% 19.73/32.98 % CPU time: 217.932125 seconds
% 19.73/32.98 % Total memory used: 1.419 GB
% 19.73/32.98 % Net memory used: 1.354 GB
%------------------------------------------------------------------------------