%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP149+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:32:48 PM UTC 2026
% Result : Theorem 0.03s 0.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NLP149+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 01:43:06 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.03/0.31 % Refutation found
% 0.03/0.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.31 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.31 fof(f1,axiom,(
% 0.03/0.31 (! [U,V] :( furniture(U,V)=> instrumentality(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f2,axiom,(
% 0.03/0.31 (! [U,V] :( seat(U,V)=> furniture(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f3,axiom,(
% 0.03/0.31 (! [U,V] :( frontseat(U,V)=> seat(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f18,axiom,(
% 0.03/0.31 (! [U,V] :( object(U,V)=> nonliving(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f20,axiom,(
% 0.03/0.31 (! [U,V] :( artifact(U,V)=> object(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f21,axiom,(
% 0.03/0.31 (! [U,V] :( instrumentality(U,V)=> artifact(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f38,axiom,(
% 0.03/0.31 (! [U,V] :( human_person(U,V)=> animate(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f48,axiom,(
% 0.03/0.31 (! [U,V] :( man(U,V)=> human_person(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f49,axiom,(
% 0.03/0.31 (! [U,V] :( fellow(U,V)=> man(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f50,axiom,(
% 0.03/0.31 (! [U,V] :( animate(U,V)=> ~ nonliving(U,V) ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f59,axiom,(
% 0.03/0.31 (! [U,V,W,X] :( be(U,V,W,X)=> W = X ) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f60,axiom,(
% 0.03/0.31 (! [U,V] :( two(U,V)<=> (? [W] :( member(U,W,V)& (? [X] :( member(U,X,V)& X != W& (! [Y] :( member(U,Y,V)=> ( Y = X| Y = W ) ) )) )) )) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f62,conjecture,(
% 0.03/0.31 ~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z] :( of(U,V,W)& city(U,W)& hollywood_placename(U,V)& placename(U,V)& street(U,W)& lonely(U,W)& chevy(U,X)& white(U,X)& dirty(U,X)& old(U,X)& event(U,Y)& agent(U,Y,X)& present(U,Y)& barrel(U,Y)& down(U,Y,W)& in(U,Y,W)& (! [X1] :( member(U,X1,Z)=> (? [X2,X3] :( frontseat(U,X3)& state(U,X2)& be(U,X2,X1,X3)& in(U,X3,X3) ) )))& two(U,Z)& group(U,Z)& (! [X4] :( member(U,X4,Z)=> ( fellow(U,X4)& young(U,X4) ) ) )) )) )),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f63,negated_conjecture,(
% 0.03/0.31 ~(~ (? [U] :( actual_world(U)& (? [V,W,X,Y,Z] :( of(U,V,W)& city(U,W)& hollywood_placename(U,V)& placename(U,V)& street(U,W)& lonely(U,W)& chevy(U,X)& white(U,X)& dirty(U,X)& old(U,X)& event(U,Y)& agent(U,Y,X)& present(U,Y)& barrel(U,Y)& down(U,Y,W)& in(U,Y,W)& (! [X1] :( member(U,X1,Z)=> (? [X2,X3] :( frontseat(U,X3)& state(U,X2)& be(U,X2,X1,X3)& in(U,X3,X3) ) )))& two(U,Z)& group(U,Z)& (! [X4] :( member(U,X4,Z)=> ( fellow(U,X4)& young(U,X4) ) ) )) )) ))),
% 0.03/0.31 inference(negated_conjecture,[status(cth)],[f62])).
% 0.03/0.31 fof(f64,plain,(
% 0.03/0.31 ![U,V]: (~furniture(U,V)|instrumentality(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.03/0.31 fof(f65,plain,(
% 0.03/0.31 ![X0,X1]: (~furniture(X0,X1)|instrumentality(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f64])).
% 0.03/0.31 fof(f66,plain,(
% 0.03/0.31 ![U,V]: (~seat(U,V)|furniture(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.03/0.31 fof(f67,plain,(
% 0.03/0.31 ![X0,X1]: (~seat(X0,X1)|furniture(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f66])).
% 0.03/0.31 fof(f68,plain,(
% 0.03/0.31 ![U,V]: (~frontseat(U,V)|seat(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.03/0.31 fof(f69,plain,(
% 0.03/0.31 ![X0,X1]: (~frontseat(X0,X1)|seat(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f68])).
% 0.03/0.31 fof(f98,plain,(
% 0.03/0.31 ![U,V]: (~object(U,V)|nonliving(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.03/0.31 fof(f99,plain,(
% 0.03/0.31 ![X0,X1]: (~object(X0,X1)|nonliving(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f98])).
% 0.03/0.31 fof(f102,plain,(
% 0.03/0.31 ![U,V]: (~artifact(U,V)|object(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.03/0.31 fof(f103,plain,(
% 0.03/0.31 ![X0,X1]: (~artifact(X0,X1)|object(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f102])).
% 0.03/0.31 fof(f104,plain,(
% 0.03/0.31 ![U,V]: (~instrumentality(U,V)|artifact(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.03/0.31 fof(f105,plain,(
% 0.03/0.31 ![X0,X1]: (~instrumentality(X0,X1)|artifact(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f104])).
% 0.03/0.31 fof(f138,plain,(
% 0.03/0.31 ![U,V]: (~human_person(U,V)|animate(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.03/0.31 fof(f139,plain,(
% 0.03/0.31 ![X0,X1]: (~human_person(X0,X1)|animate(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f138])).
% 0.03/0.31 fof(f158,plain,(
% 0.03/0.31 ![U,V]: (~man(U,V)|human_person(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.03/0.31 fof(f159,plain,(
% 0.03/0.31 ![X0,X1]: (~man(X0,X1)|human_person(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f158])).
% 0.03/0.31 fof(f160,plain,(
% 0.03/0.31 ![U,V]: (~fellow(U,V)|man(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.03/0.31 fof(f161,plain,(
% 0.03/0.31 ![X0,X1]: (~fellow(X0,X1)|man(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f160])).
% 0.03/0.31 fof(f162,plain,(
% 0.03/0.31 ![U,V]: (~animate(U,V)|~nonliving(U,V))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.03/0.31 fof(f163,plain,(
% 0.03/0.31 ![X0,X1]: (~animate(X0,X1)|~nonliving(X0,X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f162])).
% 0.03/0.31 fof(f180,plain,(
% 0.03/0.31 ![U,V,W,X]: (~be(U,V,W,X)|W=X)),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.03/0.31 fof(f181,plain,(
% 0.03/0.31 ![W,X]: ((![U,V]: ~be(U,V,W,X))|W=X)),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f180])).
% 0.03/0.31 fof(f182,plain,(
% 0.03/0.31 ![X0,X1,X2,X3]: (~be(X0,X1,X2,X3)|X2=X3)),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f181])).
% 0.03/0.31 fof(f183,plain,(
% 0.03/0.31 ![U,V]: (two(U,V)<=>(?[W]: (member(U,W,V)&(?[X]: ((member(U,X,V)&~X=W)&(![Y]: (~member(U,Y,V)|(Y=X|Y=W))))))))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.03/0.31 fof(f184,plain,(
% 0.03/0.31 ![U,V]: ((~two(U,V)|(?[W]: (member(U,W,V)&(?[X]: ((member(U,X,V)&~X=W)&(![Y]: (~member(U,Y,V)|(Y=X|Y=W))))))))&(two(U,V)|(![W]: (~member(U,W,V)|(![X]: ((~member(U,X,V)|X=W)|(?[Y]: (member(U,Y,V)&(~Y=X&~Y=W)))))))))),
% 0.03/0.31 inference(NNF_transformation,[status(thm)],[f183])).
% 0.03/0.31 fof(f185,plain,(
% 0.03/0.31 (![U,V]: (~two(U,V)|(?[W]: (member(U,W,V)&(?[X]: ((member(U,X,V)&~X=W)&(![Y]: (~member(U,Y,V)|(Y=X|Y=W)))))))))&(![U,V]: (two(U,V)|(![W]: (~member(U,W,V)|(![X]: ((~member(U,X,V)|X=W)|(?[Y]: (member(U,Y,V)&(~Y=X&~Y=W)))))))))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f184])).
% 0.03/0.31 fof(f186,plain,(
% 0.03/0.31 (![U,V]: (~two(U,V)|(member(U,sK0_skl(V,U),V)&((member(U,sK1_skl(V,U),V)&~sK1_skl(V,U)=sK0_skl(V,U))&(![Y]: (~member(U,Y,V)|(Y=sK1_skl(V,U)|Y=sK0_skl(V,U))))))))&(![U,V]: (two(U,V)|(![W]: (~member(U,W,V)|(![X]: ((~member(U,X,V)|X=W)|(member(U,sK2_skl(X,W,V,U),V)&(~sK2_skl(X,W,V,U)=X&~sK2_skl(X,W,V,U)=W))))))))),
% 0.03/0.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(W,sK0_skl(V,U)),skolemize(X,sK1_skl(V,U)),skolemize(Y,sK2_skl(X,W,V,U))],[f185])).
% 0.03/0.31 fof(f187,plain,(
% 0.03/0.31 ![X0,X1]: (~two(X0,X1)|member(X0,sK0_skl(X1,X0),X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f186])).
% 0.03/0.31 fof(f196,plain,(
% 0.03/0.31 ?[U]: (actual_world(U)&(?[V,W,X,Y,Z]: (((((((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W))&(![X1]: (~member(U,X1,Z)|(?[X2,X3]: (((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3))&in(U,X3,X3))))))&two(U,Z))&group(U,Z))&(![X4]: (~member(U,X4,Z)|(fellow(U,X4)&young(U,X4)))))))),
% 0.03/0.31 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.03/0.31 fof(f197,plain,(
% 0.03/0.31 ?[U]: (actual_world(U)&(?[Z]: (((((?[W,Y]: (((((?[X]: (((((((((?[V]: (((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V)))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X)))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W)))&(![X1]: (~member(U,X1,Z)|(?[X3]: ((?[X2]: ((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3)))&in(U,X3,X3))))))&two(U,Z))&group(U,Z))&(![X4]: (~member(U,X4,Z)|(fellow(U,X4)&young(U,X4)))))))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f196])).
% 0.03/0.31 fof(f198,plain,(
% 0.03/0.31 (actual_world(sK3_skl)&(((((((((((((((((((of(sK3_skl,sK8_skl,sK5_skl)&city(sK3_skl,sK5_skl))&hollywood_placename(sK3_skl,sK8_skl))&placename(sK3_skl,sK8_skl))&street(sK3_skl,sK5_skl))&lonely(sK3_skl,sK5_skl))&chevy(sK3_skl,sK7_skl))&white(sK3_skl,sK7_skl))&dirty(sK3_skl,sK7_skl))&old(sK3_skl,sK7_skl))&event(sK3_skl,sK6_skl))&agent(sK3_skl,sK6_skl,sK7_skl))&present(sK3_skl,sK6_skl))&barrel(sK3_skl,sK6_skl))&down(sK3_skl,sK6_skl,sK5_skl))&in(sK3_skl,sK6_skl,sK5_skl))&(![X1]: (~member(sK3_skl,X1,sK4_skl)|(((frontseat(sK3_skl,sK9_skl(X1))&state(sK3_skl,sK10_skl(X1)))&be(sK3_skl,sK10_skl(X1),X1,sK9_skl(X1)))&in(sK3_skl,sK9_skl(X1),sK9_skl(X1))))))&two(sK3_skl,sK4_skl))&group(sK3_skl,sK4_skl))&(![X4]: (~member(sK3_skl,X4,sK4_skl)|(fellow(sK3_skl,X4)&young(sK3_skl,X4))))))),
% 0.03/0.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(U,sK3_skl),skolemize(Z,sK4_skl),skolemize(W,sK5_skl),skolemize(Y,sK6_skl),skolemize(X,sK7_skl),skolemize(V,sK8_skl),skolemize(X3,sK9_skl(X1)),skolemize(X2,sK10_skl(X1))],[f197])).
% 0.03/0.32 fof(f216,plain,(
% 0.03/0.32 ![X0]: (~member(sK3_skl,X0,sK4_skl)|frontseat(sK3_skl,sK9_skl(X0)))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.32 fof(f218,plain,(
% 0.03/0.32 ![X0]: (~member(sK3_skl,X0,sK4_skl)|be(sK3_skl,sK10_skl(X0),X0,sK9_skl(X0)))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.32 fof(f220,plain,(
% 0.03/0.32 two(sK3_skl,sK4_skl)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.32 fof(f222,plain,(
% 0.03/0.32 ![X0]: (~member(sK3_skl,X0,sK4_skl)|fellow(sK3_skl,X0))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f198])).
% 0.03/0.32 fof(f298,plain,(
% 0.03/0.32 member(sK3_skl,sK0_skl(sK4_skl,sK3_skl),sK4_skl)),
% 0.03/0.32 inference(resolution,[status(thm)],[f187,f220])).
% 0.03/0.32 fof(f300,plain,(
% 0.03/0.32 fellow(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f298,f222])).
% 0.03/0.32 fof(f302,plain,(
% 0.03/0.32 be(sK3_skl,sK10_skl(sK0_skl(sK4_skl,sK3_skl)),sK0_skl(sK4_skl,sK3_skl),sK9_skl(sK0_skl(sK4_skl,sK3_skl)))),
% 0.03/0.32 inference(resolution,[status(thm)],[f298,f218])).
% 0.03/0.32 fof(f304,plain,(
% 0.03/0.32 frontseat(sK3_skl,sK9_skl(sK0_skl(sK4_skl,sK3_skl)))),
% 0.03/0.32 inference(resolution,[status(thm)],[f298,f216])).
% 0.03/0.32 fof(f326,plain,(
% 0.03/0.32 man(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f300,f161])).
% 0.03/0.32 fof(f327,plain,(
% 0.03/0.32 human_person(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f326,f159])).
% 0.03/0.32 fof(f331,plain,(
% 0.03/0.32 animate(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f327,f139])).
% 0.03/0.32 fof(f332,plain,(
% 0.03/0.32 sK0_skl(sK4_skl,sK3_skl)=sK9_skl(sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f302,f182])).
% 0.03/0.32 fof(f335,plain,(
% 0.03/0.32 frontseat(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(backward_demodulation,[status(thm)],[f332,f304])).
% 0.03/0.32 fof(f340,plain,(
% 0.03/0.32 seat(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f335,f69])).
% 0.03/0.32 fof(f350,plain,(
% 0.03/0.32 ~nonliving(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f331,f163])).
% 0.03/0.32 fof(f351,plain,(
% 0.03/0.32 furniture(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f340,f67])).
% 0.03/0.32 fof(f356,plain,(
% 0.03/0.32 instrumentality(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f351,f65])).
% 0.03/0.32 fof(f359,plain,(
% 0.03/0.32 artifact(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f356,f105])).
% 0.03/0.32 fof(f361,plain,(
% 0.03/0.32 object(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f359,f103])).
% 0.03/0.32 fof(f365,plain,(
% 0.03/0.32 nonliving(sK3_skl,sK0_skl(sK4_skl,sK3_skl))),
% 0.03/0.32 inference(resolution,[status(thm)],[f361,f99])).
% 0.03/0.32 fof(f368,plain,(
% 0.03/0.32 $false),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f365,f350])).
% 0.03/0.32 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.33 % Elapsed time: 0.032681 seconds
% 0.03/0.33 % CPU time: 0.094417 seconds
% 0.03/0.33 % Total memory used: 83.961 MB
% 0.03/0.33 % Net memory used: 83.912 MB
%------------------------------------------------------------------------------