%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD037-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:22 PM UTC 2026
% Result : Unsatisfiable 0.15s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : FLD037-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n014.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 15:39:34 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.42 % Drodi V4.1.1
% 0.15/0.45 % Refutation found
% 0.15/0.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.45 fof(f7,axiom,(
% 0.15/0.45 (![X]: (( equalish(multiply(X,multiplicative_inverse(X)),multiplicative_identity)| ~ defined(X)| equalish(X,additive_identity) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f11,axiom,(
% 0.15/0.45 defined(additive_identity) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f14,axiom,(
% 0.15/0.45 defined(multiplicative_identity) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f15,axiom,(
% 0.15/0.45 (![X]: (( defined(multiplicative_inverse(X))| ~ defined(X)| equalish(X,additive_identity) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f16,axiom,(
% 0.15/0.45 (![X,Y]: (( equalish(X,Y)| ~ less_or_equal(X,Y)| ~ less_or_equal(Y,X) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f18,axiom,(
% 0.15/0.45 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f21,axiom,(
% 0.15/0.45 (![X]: (( equalish(X,X)| ~ defined(X) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f22,axiom,(
% 0.15/0.45 (![X,Y]: (( equalish(X,Y)| ~ equalish(Y,X) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f23,axiom,(
% 0.15/0.45 (![X,Z,Y]: (( equalish(X,Z)| ~ equalish(X,Y)| ~ equalish(Y,Z) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f25,axiom,(
% 0.15/0.45 (![X,Z,Y]: (( equalish(multiply(X,Z),multiply(Y,Z))| ~ defined(Z)| ~ equalish(X,Y) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f26,axiom,(
% 0.15/0.45 (![Y,Z,X]: (( less_or_equal(Y,Z)| ~ less_or_equal(X,Z)| ~ equalish(X,Y) ) ))),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f28,hypothesis,(
% 0.15/0.45 defined(a) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f29,hypothesis,(
% 0.15/0.45 defined(b) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f30,negated_conjecture,(
% 0.15/0.45 ~ equalish(a,additive_identity) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f31,negated_conjecture,(
% 0.15/0.45 equalish(a,b) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f32,negated_conjecture,(
% 0.15/0.45 ~ equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) ),
% 0.15/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f42,plain,(
% 0.15/0.45 ![X0]: (equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity)|~defined(X0)|equalish(X0,additive_identity))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f7])).
% 0.15/0.45 fof(f49,plain,(
% 0.15/0.45 defined(additive_identity)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f11])).
% 0.15/0.45 fof(f53,plain,(
% 0.15/0.45 defined(multiplicative_identity)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f14])).
% 0.15/0.45 fof(f54,plain,(
% 0.15/0.45 ![X0]: (defined(multiplicative_inverse(X0))|~defined(X0)|equalish(X0,additive_identity))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f15])).
% 0.15/0.45 fof(f55,plain,(
% 0.15/0.45 ![X0,X1]: (equalish(X0,X1)|~less_or_equal(X0,X1)|~less_or_equal(X1,X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.45 fof(f58,plain,(
% 0.15/0.45 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f18])).
% 0.15/0.45 fof(f59,plain,(
% 0.15/0.45 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f58])).
% 0.15/0.45 fof(f64,plain,(
% 0.15/0.45 ![X0]: (equalish(X0,X0)|~defined(X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f21])).
% 0.15/0.45 fof(f65,plain,(
% 0.15/0.45 ![X0,X1]: (equalish(X0,X1)|~equalish(X1,X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f22])).
% 0.15/0.45 fof(f66,plain,(
% 0.15/0.45 ![Z,Y]: ((![X]: (equalish(X,Z)|~equalish(X,Y)))|~equalish(Y,Z))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f23])).
% 0.15/0.45 fof(f67,plain,(
% 0.15/0.45 ![X0,X1,X2]: (equalish(X0,X1)|~equalish(X0,X2)|~equalish(X2,X1))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f66])).
% 0.15/0.45 fof(f70,plain,(
% 0.15/0.45 ![X,Y]: ((![Z]: (equalish(multiply(X,Z),multiply(Y,Z))|~defined(Z)))|~equalish(X,Y))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f25])).
% 0.15/0.45 fof(f71,plain,(
% 0.15/0.45 ![X0,X1,X2]: (equalish(multiply(X0,X1),multiply(X2,X1))|~defined(X1)|~equalish(X0,X2))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f70])).
% 0.15/0.45 fof(f72,plain,(
% 0.15/0.45 ![Y,X]: ((![Z]: (less_or_equal(Y,Z)|~less_or_equal(X,Z)))|~equalish(X,Y))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f26])).
% 0.15/0.45 fof(f73,plain,(
% 0.15/0.45 ![X0,X1,X2]: (less_or_equal(X0,X1)|~less_or_equal(X2,X1)|~equalish(X2,X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.15/0.45 fof(f75,plain,(
% 0.15/0.45 defined(a)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f28])).
% 0.15/0.45 fof(f76,plain,(
% 0.15/0.45 defined(b)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f29])).
% 0.15/0.45 fof(f77,plain,(
% 0.15/0.45 ~equalish(a,additive_identity)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f30])).
% 0.15/0.45 fof(f78,plain,(
% 0.15/0.45 equalish(a,b)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/0.45 fof(f79,plain,(
% 0.15/0.45 ~equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f32])).
% 0.15/0.45 fof(f86,plain,(
% 0.15/0.45 ~equalish(multiply(b,multiplicative_inverse(a)),multiplicative_identity)),
% 0.15/0.45 inference(resolution,[status(thm)],[f65,f79])).
% 0.15/0.45 fof(f93,plain,(
% 0.15/0.45 ![X0]: (~equalish(multiply(b,multiplicative_inverse(a)),X0)|~equalish(X0,multiplicative_identity))),
% 0.15/0.45 inference(resolution,[status(thm)],[f67,f86])).
% 0.15/0.45 fof(f98,plain,(
% 0.15/0.45 ![X0]: (~equalish(a,X0)|~equalish(X0,additive_identity))),
% 0.15/0.45 inference(resolution,[status(thm)],[f67,f77])).
% 0.15/0.45 fof(f140,plain,(
% 0.15/0.45 ~equalish(a,additive_identity)|~defined(a)),
% 0.15/0.45 inference(resolution,[status(thm)],[f98,f64])).
% 0.15/0.45 fof(f141,definition,(
% 0.15/0.45 sQ6_spl <=> (equalish(a,additive_identity))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f144,definition,(
% 0.15/0.45 sQ7_spl <=> (defined(a))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f146,plain,(
% 0.15/0.45 ~defined(a)|sQ7_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f144])).
% 0.15/0.45 fof(f147,plain,(
% 0.15/0.45 ~sQ6_spl|~sQ7_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f140,f141,f144])).
% 0.15/0.45 fof(f162,plain,(
% 0.15/0.45 $false|sQ7_spl),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f146,f75])).
% 0.15/0.45 fof(f163,plain,(
% 0.15/0.45 sQ7_spl),
% 0.15/0.45 inference(contradiction_clause,[status(thm)],[f162])).
% 0.15/0.45 fof(f221,definition,(
% 0.15/0.45 sQ15_spl <=> (defined(multiplicative_inverse(a)))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f223,plain,(
% 0.15/0.45 ~defined(multiplicative_inverse(a))|sQ15_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f221])).
% 0.15/0.45 fof(f244,plain,(
% 0.15/0.45 ![X0]: (~defined(multiplicative_inverse(a))|~equalish(b,X0)|~equalish(multiply(X0,multiplicative_inverse(a)),multiplicative_identity))),
% 0.15/0.45 inference(resolution,[status(thm)],[f71,f93])).
% 0.15/0.45 fof(f245,definition,(
% 0.15/0.45 ![X0]: (sQ18_spl <=> (~equalish(b,X0)|~equalish(multiply(X0,multiplicative_inverse(a)),multiplicative_identity)))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f246,plain,(
% 0.15/0.45 ![X0]: (~equalish(b,X0)|~equalish(multiply(X0,multiplicative_inverse(a)),multiplicative_identity)|~sQ18_spl)),
% 0.15/0.45 inference(component_clause,[status(thm)],[f245])).
% 0.15/0.45 fof(f248,plain,(
% 0.15/0.45 ~sQ15_spl|sQ18_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f244,f221,f245])).
% 0.15/0.45 fof(f249,plain,(
% 0.15/0.45 ~defined(a)|equalish(a,additive_identity)|sQ15_spl),
% 0.15/0.45 inference(resolution,[status(thm)],[f223,f54])).
% 0.15/0.45 fof(f250,plain,(
% 0.15/0.45 ~sQ7_spl|sQ6_spl|sQ15_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f249,f144,f141,f221])).
% 0.15/0.45 fof(f265,plain,(
% 0.15/0.45 ![X0]: (less_or_equal(X0,b)|less_or_equal(b,X0)|~defined(X0))),
% 0.15/0.45 inference(resolution,[status(thm)],[f59,f76])).
% 0.15/0.45 fof(f266,plain,(
% 0.15/0.45 ![X0]: (less_or_equal(X0,a)|less_or_equal(a,X0)|~defined(X0))),
% 0.15/0.45 inference(resolution,[status(thm)],[f59,f75])).
% 0.15/0.45 fof(f267,plain,(
% 0.15/0.45 ![X0]: (less_or_equal(X0,multiplicative_identity)|less_or_equal(multiplicative_identity,X0)|~defined(X0))),
% 0.15/0.45 inference(resolution,[status(thm)],[f59,f53])).
% 0.15/0.45 fof(f268,plain,(
% 0.15/0.45 ![X0]: (less_or_equal(X0,additive_identity)|less_or_equal(additive_identity,X0)|~defined(X0))),
% 0.15/0.45 inference(resolution,[status(thm)],[f59,f49])).
% 0.15/0.45 fof(f309,plain,(
% 0.15/0.45 less_or_equal(b,b)|less_or_equal(b,b)),
% 0.15/0.45 inference(resolution,[status(thm)],[f265,f76])).
% 0.15/0.45 fof(f320,definition,(
% 0.15/0.45 sQ26_spl <=> (less_or_equal(b,b))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f321,plain,(
% 0.15/0.45 less_or_equal(b,b)|~sQ26_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f320])).
% 0.15/0.45 fof(f323,plain,(
% 0.15/0.45 sQ26_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f309,f320])).
% 0.15/0.45 fof(f324,definition,(
% 0.15/0.45 sQ27_spl <=> (less_or_equal(a,b))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f325,plain,(
% 0.15/0.45 less_or_equal(a,b)|~sQ27_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f324])).
% 0.15/0.45 fof(f326,plain,(
% 0.15/0.45 ~less_or_equal(a,b)|sQ27_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f324])).
% 0.15/0.45 fof(f327,definition,(
% 0.15/0.45 sQ28_spl <=> (less_or_equal(b,a))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f329,plain,(
% 0.15/0.45 ~less_or_equal(b,a)|sQ28_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f327])).
% 0.15/0.45 fof(f346,plain,(
% 0.15/0.45 ![X0]: (less_or_equal(X0,b)|~equalish(b,X0)|~sQ26_spl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f321,f73])).
% 0.15/0.45 fof(f370,plain,(
% 0.15/0.45 equalish(b,a)|~less_or_equal(b,a)|~sQ27_spl),
% 0.15/0.45 inference(resolution,[status(thm)],[f325,f55])).
% 0.15/0.45 fof(f371,definition,(
% 0.15/0.45 sQ35_spl <=> (equalish(b,a))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f374,plain,(
% 0.15/0.45 sQ35_spl|~sQ28_spl|~sQ27_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f370,f371,f327,f324])).
% 0.15/0.45 fof(f512,plain,(
% 0.15/0.45 less_or_equal(a,a)|less_or_equal(a,a)),
% 0.15/0.45 inference(resolution,[status(thm)],[f266,f75])).
% 0.15/0.45 fof(f523,definition,(
% 0.15/0.45 sQ48_spl <=> (less_or_equal(a,a))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f524,plain,(
% 0.15/0.45 less_or_equal(a,a)|~sQ48_spl),
% 0.15/0.45 inference(component_clause,[status(thm)],[f523])).
% 0.15/0.45 fof(f526,plain,(
% 0.15/0.45 sQ48_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f512,f523])).
% 0.15/0.45 fof(f548,plain,(
% 0.15/0.45 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 0.15/0.45 inference(resolution,[status(thm)],[f267,f53])).
% 0.15/0.45 fof(f559,definition,(
% 0.15/0.45 sQ55_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f562,plain,(
% 0.15/0.45 sQ55_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f548,f559])).
% 0.15/0.45 fof(f578,plain,(
% 0.15/0.45 ![X0]: (less_or_equal(X0,a)|~equalish(a,X0)|~sQ48_spl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f524,f73])).
% 0.15/0.45 fof(f667,plain,(
% 0.15/0.45 less_or_equal(additive_identity,additive_identity)|less_or_equal(additive_identity,additive_identity)),
% 0.15/0.45 inference(resolution,[status(thm)],[f268,f49])).
% 0.15/0.45 fof(f678,definition,(
% 0.15/0.45 sQ63_spl <=> (less_or_equal(additive_identity,additive_identity))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.15/0.45 fof(f681,plain,(
% 0.15/0.45 sQ63_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f667,f678])).
% 0.15/0.45 fof(f880,plain,(
% 0.15/0.45 ~equalish(b,a)|sQ27_spl|~sQ26_spl),
% 0.15/0.45 inference(resolution,[status(thm)],[f326,f346])).
% 0.15/0.45 fof(f1021,plain,(
% 0.15/0.45 ~equalish(a,b)|sQ27_spl|~sQ26_spl),
% 0.15/0.45 inference(resolution,[status(thm)],[f880,f65])).
% 0.15/0.45 fof(f1022,plain,(
% 0.15/0.45 $false|sQ27_spl|~sQ26_spl),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1021,f78])).
% 0.15/0.45 fof(f1023,plain,(
% 0.15/0.45 sQ27_spl|~sQ26_spl),
% 0.15/0.45 inference(contradiction_clause,[status(thm)],[f1022])).
% 0.15/0.45 fof(f1040,plain,(
% 0.15/0.45 ~equalish(a,b)|sQ28_spl|~sQ48_spl),
% 0.15/0.45 inference(resolution,[status(thm)],[f329,f578])).
% 0.15/0.45 fof(f1041,plain,(
% 0.15/0.45 $false|sQ28_spl|~sQ48_spl),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1040,f78])).
% 0.15/0.45 fof(f1042,plain,(
% 0.15/0.45 sQ28_spl|~sQ48_spl),
% 0.15/0.45 inference(contradiction_clause,[status(thm)],[f1041])).
% 0.15/0.45 fof(f1232,plain,(
% 0.15/0.45 ~equalish(b,a)|~defined(a)|equalish(a,additive_identity)|~sQ18_spl),
% 0.15/0.45 inference(resolution,[status(thm)],[f246,f42])).
% 0.15/0.45 fof(f1235,plain,(
% 0.15/0.45 ~sQ35_spl|~sQ7_spl|sQ6_spl|~sQ18_spl),
% 0.15/0.45 inference(split_clause,[status(thm)],[f1232,f371,f144,f141,f245])).
% 0.15/0.45 fof(f1236,plain,(
% 0.15/0.45 $false),
% 0.15/0.45 inference(sat_refutation,[status(thm)],[f147,f163,f248,f250,f323,f374,f526,f562,f681,f1023,f1042,f1235])).
% 0.15/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.48 % Elapsed time: 0.058657 seconds
% 0.15/0.48 % CPU time: 0.239168 seconds
% 0.15/0.48 % Total memory used: 13.834 MB
% 0.15/0.48 % Net memory used: 13.620 MB
%------------------------------------------------------------------------------