%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD061-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 12:22:28 PM UTC 2026
% Result : Unsatisfiable 0.18s 10.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : FLD061-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/10.42 % Computer : n002.cluster.edu
% 0.15/10.42 % Model : x86_64 x86_64
% 0.15/10.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.42 % Memory : 8046.5625MB
% 0.15/10.42 % OS : Linux 6.8.0-71-generic
% 0.15/10.42 % CPULimit : 300
% 0.15/10.42 % WCLimit : 300
% 0.15/10.42 % DateTime : Mon Sep 21 15:46:30 UTC 2026
% 0.15/10.42 % CPUTime :
% 0.15/10.43 % Drodi V4.1.1
% 0.18/10.90 % Refutation found
% 0.18/10.90 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.18/10.90 % SZS output start CNFRefutation for theBenchmark
% 0.18/10.90 fof(f4,axiom,(
% 0.18/10.90 (![X,Y]: (( equalish(add(X,Y),add(Y,X))| ~ defined(X)| ~ defined(Y) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f11,axiom,(
% 0.18/10.90 defined(additive_identity) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f14,axiom,(
% 0.18/10.90 defined(multiplicative_identity) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f16,axiom,(
% 0.18/10.90 (![X,Y]: (( equalish(X,Y)| ~ less_or_equal(X,Y)| ~ less_or_equal(Y,X) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f17,axiom,(
% 0.18/10.90 (![X,Z,Y]: (( less_or_equal(X,Z)| ~ less_or_equal(X,Y)| ~ less_or_equal(Y,Z) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f18,axiom,(
% 0.18/10.90 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f19,axiom,(
% 0.18/10.90 (![X,Z,Y]: (( less_or_equal(add(X,Z),add(Y,Z))| ~ defined(Z)| ~ less_or_equal(X,Y) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f21,axiom,(
% 0.18/10.90 (![X]: (( equalish(X,X)| ~ defined(X) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f22,axiom,(
% 0.18/10.90 (![X,Y]: (( equalish(X,Y)| ~ equalish(Y,X) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f26,axiom,(
% 0.18/10.90 (![Y,Z,X]: (( less_or_equal(Y,Z)| ~ less_or_equal(X,Z)| ~ equalish(X,Y) ) ))),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f27,axiom,(
% 0.18/10.90 ~ equalish(additive_identity,multiplicative_identity) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f28,hypothesis,(
% 0.18/10.90 defined(a) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f29,hypothesis,(
% 0.18/10.90 defined(b) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f30,hypothesis,(
% 0.18/10.90 defined(c) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f31,hypothesis,(
% 0.18/10.90 defined(d) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f32,negated_conjecture,(
% 0.18/10.90 less_or_equal(a,b) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f33,negated_conjecture,(
% 0.18/10.90 less_or_equal(c,d) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f34,negated_conjecture,(
% 0.18/10.90 ~ less_or_equal(add(a,c),add(d,b)) ),
% 0.18/10.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/10.90 fof(f39,plain,(
% 0.18/10.90 ![Y]: ((![X]: (equalish(add(X,Y),add(Y,X))|~defined(X)))|~defined(Y))),
% 0.18/10.90 inference(miniscoping,[status(thm)],[f4])).
% 0.18/10.90 fof(f40,plain,(
% 0.18/10.90 ![X0,X1]: (equalish(add(X0,X1),add(X1,X0))|~defined(X0)|~defined(X1))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f39])).
% 0.18/10.90 fof(f51,plain,(
% 0.18/10.90 defined(additive_identity)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f11])).
% 0.18/10.90 fof(f55,plain,(
% 0.18/10.90 defined(multiplicative_identity)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f14])).
% 0.18/10.90 fof(f57,plain,(
% 0.18/10.90 ![X0,X1]: (equalish(X0,X1)|~less_or_equal(X0,X1)|~less_or_equal(X1,X0))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f16])).
% 0.18/10.90 fof(f58,plain,(
% 0.18/10.90 ![Z,Y]: ((![X]: (less_or_equal(X,Z)|~less_or_equal(X,Y)))|~less_or_equal(Y,Z))),
% 0.18/10.90 inference(miniscoping,[status(thm)],[f17])).
% 0.18/10.90 fof(f59,plain,(
% 0.18/10.90 ![X0,X1,X2]: (less_or_equal(X0,X1)|~less_or_equal(X0,X2)|~less_or_equal(X2,X1))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/10.90 fof(f60,plain,(
% 0.18/10.90 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 0.18/10.90 inference(miniscoping,[status(thm)],[f18])).
% 0.18/10.90 fof(f61,plain,(
% 0.18/10.90 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f60])).
% 0.18/10.90 fof(f62,plain,(
% 0.18/10.90 ![X,Y]: ((![Z]: (less_or_equal(add(X,Z),add(Y,Z))|~defined(Z)))|~less_or_equal(X,Y))),
% 0.18/10.90 inference(miniscoping,[status(thm)],[f19])).
% 0.18/10.90 fof(f63,plain,(
% 0.18/10.90 ![X0,X1,X2]: (less_or_equal(add(X0,X1),add(X2,X1))|~defined(X1)|~less_or_equal(X0,X2))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f62])).
% 0.18/10.90 fof(f66,plain,(
% 0.18/10.90 ![X0]: (equalish(X0,X0)|~defined(X0))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f21])).
% 0.18/10.90 fof(f67,plain,(
% 0.18/10.90 ![X0,X1]: (equalish(X0,X1)|~equalish(X1,X0))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f22])).
% 0.18/10.90 fof(f74,plain,(
% 0.18/10.90 ![Y,X]: ((![Z]: (less_or_equal(Y,Z)|~less_or_equal(X,Z)))|~equalish(X,Y))),
% 0.18/10.90 inference(miniscoping,[status(thm)],[f26])).
% 0.18/10.90 fof(f75,plain,(
% 0.18/10.90 ![X0,X1,X2]: (less_or_equal(X0,X1)|~less_or_equal(X2,X1)|~equalish(X2,X0))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f74])).
% 0.18/10.90 fof(f76,plain,(
% 0.18/10.90 ~equalish(additive_identity,multiplicative_identity)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f27])).
% 0.18/10.90 fof(f77,plain,(
% 0.18/10.90 defined(a)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f28])).
% 0.18/10.90 fof(f78,plain,(
% 0.18/10.90 defined(b)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f29])).
% 0.18/10.90 fof(f79,plain,(
% 0.18/10.90 defined(c)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f30])).
% 0.18/10.90 fof(f80,plain,(
% 0.18/10.90 defined(d)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f31])).
% 0.18/10.90 fof(f81,plain,(
% 0.18/10.90 less_or_equal(a,b)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f32])).
% 0.18/10.90 fof(f82,plain,(
% 0.18/10.90 less_or_equal(c,d)),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f33])).
% 0.18/10.90 fof(f83,plain,(
% 0.18/10.90 ~less_or_equal(add(a,c),add(d,b))),
% 0.18/10.90 inference(cnf_transformation,[status(thm)],[f34])).
% 0.18/10.90 fof(f84,plain,(
% 0.18/10.90 ![X0]: (~less_or_equal(add(a,c),X0)|~less_or_equal(X0,add(d,b)))),
% 0.18/10.90 inference(resolution,[status(thm)],[f59,f83])).
% 0.18/10.90 fof(f91,plain,(
% 0.18/10.90 ![X0]: (less_or_equal(X0,a)|less_or_equal(a,X0)|~defined(X0))),
% 0.18/10.90 inference(resolution,[status(thm)],[f61,f77])).
% 0.18/10.90 fof(f104,plain,(
% 0.18/10.90 ![X0]: (less_or_equal(X0,d)|~equalish(c,X0))),
% 0.18/10.90 inference(resolution,[status(thm)],[f75,f82])).
% 0.18/10.90 fof(f105,plain,(
% 0.18/10.90 ![X0]: (less_or_equal(X0,b)|~equalish(a,X0))),
% 0.18/10.90 inference(resolution,[status(thm)],[f75,f81])).
% 0.18/10.90 fof(f108,plain,(
% 0.18/10.90 ![X0]: (~defined(c)|~less_or_equal(a,X0)|~less_or_equal(add(X0,c),add(d,b)))),
% 0.18/10.90 inference(resolution,[status(thm)],[f63,f84])).
% 0.18/10.90 fof(f109,plain,(
% 0.18/10.90 ![X0,X1,X2,X3]: (~defined(X0)|~less_or_equal(X1,X2)|less_or_equal(X3,add(X2,X0))|~equalish(add(X1,X0),X3))),
% 0.18/10.90 inference(resolution,[status(thm)],[f63,f75])).
% 0.18/10.90 fof(f110,definition,(
% 0.18/10.90 sQ2_spl <=> (defined(c))),
% 0.18/10.90 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.18/10.90 fof(f112,plain,(
% 0.18/10.90 ~defined(c)|sQ2_spl),
% 0.18/10.90 inference(component_clause,[status(thm)],[f110])).
% 0.18/10.90 fof(f117,definition,(
% 0.18/10.90 ![X0]: (sQ4_spl <=> (~less_or_equal(a,X0)|~less_or_equal(add(X0,c),add(d,b))))),
% 0.18/10.90 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.18/10.90 fof(f118,plain,(
% 0.18/10.90 ![X0]: (~less_or_equal(a,X0)|~less_or_equal(add(X0,c),add(d,b))|~sQ4_spl)),
% 0.18/10.90 inference(component_clause,[status(thm)],[f117])).
% 0.18/10.90 fof(f120,plain,(
% 0.18/10.90 ~sQ2_spl|sQ4_spl),
% 0.18/10.90 inference(split_clause,[status(thm)],[f108,f110,f117])).
% 0.18/10.90 fof(f121,plain,(
% 0.18/10.90 $false|sQ2_spl),
% 0.18/10.90 inference(forward_subsumption_resolution,[status(thm)],[f112,f79])).
% 0.18/10.90 fof(f122,plain,(
% 0.18/10.90 sQ2_spl),
% 0.18/10.90 inference(contradiction_clause,[status(thm)],[f121])).
% 0.18/10.90 fof(f124,plain,(
% 0.18/10.90 ~equalish(multiplicative_identity,additive_identity)),
% 0.18/10.90 inference(resolution,[status(thm)],[f67,f76])).
% 0.18/10.90 fof(f131,plain,(
% 0.18/10.90 less_or_equal(c,d)|~defined(c)),
% 0.18/10.90 inference(resolution,[status(thm)],[f104,f66])).
% 0.18/10.90 fof(f133,definition,(
% 0.18/10.90 sQ5_spl <=> (less_or_equal(c,d))),
% 0.18/10.90 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.18/10.90 fof(f136,plain,(
% 0.18/10.90 sQ5_spl|~sQ2_spl),
% 0.18/10.90 inference(split_clause,[status(thm)],[f131,f133,f110])).
% 0.18/10.90 fof(f139,plain,(
% 0.18/10.90 ![X0]: (less_or_equal(X0,b)|~less_or_equal(a,X0)|~less_or_equal(X0,a))),
% 0.18/10.90 inference(resolution,[status(thm)],[f105,f57])).
% 0.18/10.90 fof(f140,definition,(
% 0.18/10.90 sQ6_spl <=> (less_or_equal(a,b))),
% 0.18/10.90 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.18/10.90 fof(f408,plain,(
% 0.18/10.90 less_or_equal(a,a)|less_or_equal(a,a)),
% 0.18/10.90 inference(resolution,[status(thm)],[f91,f77])).
% 0.18/10.90 fof(f414,definition,(
% 0.18/10.90 sQ43_spl <=> (less_or_equal(a,a))),
% 0.18/10.90 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.18/10.90 fof(f415,plain,(
% 0.18/10.90 less_or_equal(a,a)|~sQ43_spl),
% 0.18/10.90 inference(component_clause,[status(thm)],[f414])).
% 0.18/10.90 fof(f417,plain,(
% 0.18/10.90 sQ43_spl),
% 0.18/10.90 inference(split_clause,[status(thm)],[f408,f414])).
% 0.18/10.92 fof(f439,plain,(
% 0.18/10.92 ![X0,X1]: (~defined(b)|~less_or_equal(X0,d)|~equalish(add(X0,b),add(X1,c))|~less_or_equal(a,X1)|~sQ4_spl)),
% 0.18/10.92 inference(resolution,[status(thm)],[f109,f118])).
% 0.18/10.92 fof(f441,definition,(
% 0.18/10.92 sQ44_spl <=> (defined(b))),
% 0.18/10.92 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.18/10.92 fof(f443,plain,(
% 0.18/10.92 ~defined(b)|sQ44_spl),
% 0.18/10.92 inference(component_clause,[status(thm)],[f441])).
% 0.18/10.92 fof(f448,definition,(
% 0.18/10.92 ![X0,X1]: (sQ46_spl <=> (~less_or_equal(X0,d)|~equalish(add(X0,b),add(X1,c))|~less_or_equal(a,X1)))),
% 0.18/10.92 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.18/10.92 fof(f449,plain,(
% 0.18/10.92 ![X0,X1]: (~less_or_equal(X0,d)|~equalish(add(X0,b),add(X1,c))|~less_or_equal(a,X1)|~sQ46_spl)),
% 0.18/10.92 inference(component_clause,[status(thm)],[f448])).
% 0.18/10.92 fof(f451,plain,(
% 0.18/10.92 ~sQ44_spl|sQ46_spl|~sQ4_spl),
% 0.18/10.92 inference(split_clause,[status(thm)],[f439,f441,f448,f117])).
% 0.18/10.92 fof(f452,plain,(
% 0.18/10.92 $false|sQ44_spl),
% 0.18/10.92 inference(forward_subsumption_resolution,[status(thm)],[f443,f78])).
% 0.18/10.92 fof(f453,plain,(
% 0.18/10.92 sQ44_spl),
% 0.18/10.92 inference(contradiction_clause,[status(thm)],[f452])).
% 0.18/10.92 fof(f528,definition,(
% 0.18/10.92 sQ48_spl <=> (defined(additive_identity))),
% 0.18/10.92 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.18/10.92 fof(f530,plain,(
% 0.18/10.92 ~defined(additive_identity)|sQ48_spl),
% 0.18/10.92 inference(component_clause,[status(thm)],[f528])).
% 0.18/10.92 fof(f544,plain,(
% 0.18/10.92 less_or_equal(a,b)|~less_or_equal(a,a)|~sQ43_spl),
% 0.18/10.92 inference(resolution,[status(thm)],[f415,f139])).
% 0.18/10.92 fof(f546,plain,(
% 0.18/10.92 sQ6_spl|~sQ43_spl),
% 0.18/10.92 inference(split_clause,[status(thm)],[f544,f140,f414])).
% 0.18/10.92 fof(f566,definition,(
% 0.18/10.92 sQ53_spl <=> (defined(d))),
% 0.18/10.92 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.18/10.92 fof(f568,plain,(
% 0.18/10.92 ~defined(d)|sQ53_spl),
% 0.18/10.92 inference(component_clause,[status(thm)],[f566])).
% 0.18/10.92 fof(f607,definition,(
% 0.18/10.92 sQ59_spl <=> (equalish(multiplicative_identity,additive_identity))),
% 0.18/10.92 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.18/10.92 fof(f608,plain,(
% 0.18/10.92 equalish(multiplicative_identity,additive_identity)|~sQ59_spl),
% 0.18/10.92 inference(component_clause,[status(thm)],[f607])).
% 0.18/10.92 fof(f710,plain,(
% 0.18/10.92 $false|~sQ59_spl),
% 0.18/10.92 inference(forward_subsumption_resolution,[status(thm)],[f608,f124])).
% 0.18/10.92 fof(f711,plain,(
% 0.18/10.92 ~sQ59_spl),
% 0.18/10.92 inference(contradiction_clause,[status(thm)],[f710])).
% 0.18/10.92 fof(f935,definition,(
% 0.18/10.92 sQ93_spl <=> (defined(multiplicative_identity))),
% 0.18/10.92 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.18/10.92 fof(f937,plain,(
% 0.18/10.92 ~defined(multiplicative_identity)|sQ93_spl),
% 0.18/10.92 inference(component_clause,[status(thm)],[f935])).
% 0.18/10.92 fof(f1156,plain,(
% 0.18/10.92 $false|sQ48_spl),
% 0.18/10.92 inference(forward_subsumption_resolution,[status(thm)],[f530,f51])).
% 0.18/10.92 fof(f1157,plain,(
% 0.18/10.92 sQ48_spl),
% 0.18/10.92 inference(contradiction_clause,[status(thm)],[f1156])).
% 0.18/10.92 fof(f1824,plain,(
% 0.18/10.92 $false|sQ93_spl),
% 0.18/10.92 inference(forward_subsumption_resolution,[status(thm)],[f937,f55])).
% 0.18/10.92 fof(f1825,plain,(
% 0.18/10.92 sQ93_spl),
% 0.18/10.92 inference(contradiction_clause,[status(thm)],[f1824])).
% 0.18/10.92 fof(f1869,plain,(
% 0.18/10.92 $false|sQ53_spl),
% 0.18/10.92 inference(forward_subsumption_resolution,[status(thm)],[f568,f80])).
% 0.18/10.92 fof(f1870,plain,(
% 0.18/10.92 sQ53_spl),
% 0.18/10.92 inference(contradiction_clause,[status(thm)],[f1869])).
% 0.18/10.92 fof(f2692,plain,(
% 0.18/10.92 ~less_or_equal(c,d)|~less_or_equal(a,b)|~defined(c)|~defined(b)|~sQ46_spl),
% 0.18/10.92 inference(resolution,[status(thm)],[f449,f40])).
% 0.18/10.92 fof(f2696,plain,(
% 0.18/10.92 ~sQ5_spl|~sQ6_spl|~sQ2_spl|~sQ44_spl|~sQ46_spl),
% 0.18/10.92 inference(split_clause,[status(thm)],[f2692,f133,f140,f110,f441,f448])).
% 0.18/10.92 fof(f2697,plain,(
% 0.18/10.92 $false),
% 0.18/10.92 inference(sat_refutation,[status(thm)],[f120,f122,f136,f417,f451,f453,f546,f711,f1157,f1825,f1870,f2696])).
% 0.18/10.92 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/10.94 % Elapsed time: 0.501494 seconds
% 0.18/10.94 % CPU time: 3.785713 seconds
% 0.18/10.94 % Total memory used: 90.077 MB
% 0.18/10.94 % Net memory used: 86.167 MB
%------------------------------------------------------------------------------