%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG036+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 11:49:30 AM UTC 2026
% Result : Theorem 0.08s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG036+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n026.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 12:56:22 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.38 % Refutation found
% 0.08/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.38 fof(f7,conjecture,(
% 0.08/0.38 ( ( op(e0,e0) = e0& op(e1,e1) = e0& op(e2,e2) = e0& op(e3,e3) = e0 )| ( op(e0,e0) = e1& op(e1,e1) = e1& op(e2,e2) = e1& op(e3,e3) = e1 )| ( op(e0,e0) = e2& op(e1,e1) = e2& op(e2,e2) = e2& op(e3,e3) = e2 )| ( op(e0,e0) = e3& op(e1,e1) = e3& op(e2,e2) = e3& op(e3,e3) = e3 )| ~ ( ( op(e0,e0) = e0& op(e1,e1) = e0& op(e2,e2) = e0& op(e3,e3) = e0 )| ( op(e0,e0) = e1& op(e1,e1) = e1& op(e2,e2) = e1& op(e3,e3) = e1 )| ( op(e0,e0) = e2& op(e1,e1) = e2& op(e2,e2) = e2& op(e3,e3) = e2 )| ( op(e0,e0) = e3& op(e1,e1) = e3& op(e2,e2) = e3& op(e3,e3) = e3 ) ) ) ),
% 0.08/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.38 fof(f8,negated_conjecture,(
% 0.08/0.38 ~(( ( op(e0,e0) = e0& op(e1,e1) = e0& op(e2,e2) = e0& op(e3,e3) = e0 )| ( op(e0,e0) = e1& op(e1,e1) = e1& op(e2,e2) = e1& op(e3,e3) = e1 )| ( op(e0,e0) = e2& op(e1,e1) = e2& op(e2,e2) = e2& op(e3,e3) = e2 )| ( op(e0,e0) = e3& op(e1,e1) = e3& op(e2,e2) = e3& op(e3,e3) = e3 )| ~ ( ( op(e0,e0) = e0& op(e1,e1) = e0& op(e2,e2) = e0& op(e3,e3) = e0 )| ( op(e0,e0) = e1& op(e1,e1) = e1& op(e2,e2) = e1& op(e3,e3) = e1 )| ( op(e0,e0) = e2& op(e1,e1) = e2& op(e2,e2) = e2& op(e3,e3) = e2 )| ( op(e0,e0) = e3& op(e1,e1) = e3& op(e2,e2) = e3& op(e3,e3) = e3 ) ) ) )),
% 0.08/0.38 inference(negated_conjecture,[status(cth)],[f7])).
% 0.08/0.38 fof(f121,plain,(
% 0.08/0.38 (((((((~op(e0,e0)=e0|~op(e1,e1)=e0)|~op(e2,e2)=e0)|~op(e3,e3)=e0)&(((~op(e0,e0)=e1|~op(e1,e1)=e1)|~op(e2,e2)=e1)|~op(e3,e3)=e1))&(((~op(e0,e0)=e2|~op(e1,e1)=e2)|~op(e2,e2)=e2)|~op(e3,e3)=e2))&(((~op(e0,e0)=e3|~op(e1,e1)=e3)|~op(e2,e2)=e3)|~op(e3,e3)=e3))&((((((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2))|(((op(e0,e0)=e3&op(e1,e1)=e3)&op(e2,e2)=e3)&op(e3,e3)=e3)))),
% 0.08/0.38 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.08/0.38 fof(f122,definition,(
% 0.08/0.38 sP0_prd<=>(((((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.08/0.38 fof(f123,plain,(
% 0.08/0.38 ((((((~op(e0,e0)=e0|~op(e1,e1)=e0)|~op(e2,e2)=e0)|~op(e3,e3)=e0)&(((~op(e0,e0)=e1|~op(e1,e1)=e1)|~op(e2,e2)=e1)|~op(e3,e3)=e1))&(((~op(e0,e0)=e2|~op(e1,e1)=e2)|~op(e2,e2)=e2)|~op(e3,e3)=e2))&(((~op(e0,e0)=e3|~op(e1,e1)=e3)|~op(e2,e2)=e3)|~op(e3,e3)=e3))&(sP0_prd|(((op(e0,e0)=e3&op(e1,e1)=e3)&op(e2,e2)=e3)&op(e3,e3)=e3))),
% 0.08/0.38 inference(formula_renaming,[status(thm)],[f121,f122])).
% 0.08/0.38 fof(f124,plain,(
% 0.08/0.38 ~op(e0,e0)=e0|~op(e1,e1)=e0|~op(e2,e2)=e0|~op(e3,e3)=e0),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f125,plain,(
% 0.08/0.38 ~op(e0,e0)=e1|~op(e1,e1)=e1|~op(e2,e2)=e1|~op(e3,e3)=e1),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f126,plain,(
% 0.08/0.38 ~op(e0,e0)=e2|~op(e1,e1)=e2|~op(e2,e2)=e2|~op(e3,e3)=e2),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f127,plain,(
% 0.08/0.38 ~op(e0,e0)=e3|~op(e1,e1)=e3|~op(e2,e2)=e3|~op(e3,e3)=e3),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f128,plain,(
% 0.08/0.38 sP0_prd|op(e0,e0)=e3),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f129,plain,(
% 0.08/0.38 sP0_prd|op(e1,e1)=e3),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f130,plain,(
% 0.08/0.38 sP0_prd|op(e2,e2)=e3),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f131,plain,(
% 0.08/0.38 sP0_prd|op(e3,e3)=e3),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.38 fof(f132,definition,(
% 0.08/0.38 sP1_prd<=>((((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.08/0.38 fof(f133,plain,(
% 0.08/0.38 sP0_prd<=>(sP1_prd|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2))),
% 0.08/0.38 inference(formula_renaming,[status(thm)],[f122,f132])).
% 0.08/0.38 fof(f134,plain,(
% 0.08/0.38 (~sP0_prd|(sP1_prd|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2)))&(sP0_prd|(~sP1_prd&(((~op(e0,e0)=e2|~op(e1,e1)=e2)|~op(e2,e2)=e2)|~op(e3,e3)=e2)))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f133])).
% 0.08/0.38 fof(f135,plain,(
% 0.08/0.38 ~sP0_prd|sP1_prd|op(e0,e0)=e2),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f134])).
% 0.08/0.38 fof(f136,plain,(
% 0.08/0.38 ~sP0_prd|sP1_prd|op(e1,e1)=e2),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f134])).
% 0.08/0.38 fof(f137,plain,(
% 0.08/0.38 ~sP0_prd|sP1_prd|op(e2,e2)=e2),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f134])).
% 0.08/0.38 fof(f138,plain,(
% 0.08/0.38 ~sP0_prd|sP1_prd|op(e3,e3)=e2),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f134])).
% 0.08/0.38 fof(f141,definition,(
% 0.08/0.38 sP2_prd<=>(((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.08/0.38 fof(f142,plain,(
% 0.08/0.38 sP1_prd<=>(sP2_prd|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))),
% 0.08/0.38 inference(formula_renaming,[status(thm)],[f132,f141])).
% 0.08/0.38 fof(f143,plain,(
% 0.08/0.38 (~sP1_prd|(sP2_prd|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1)))&(sP1_prd|(~sP2_prd&(((~op(e0,e0)=e1|~op(e1,e1)=e1)|~op(e2,e2)=e1)|~op(e3,e3)=e1)))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f142])).
% 0.08/0.38 fof(f144,plain,(
% 0.08/0.38 ~sP1_prd|sP2_prd|op(e0,e0)=e1),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f143])).
% 0.08/0.38 fof(f145,plain,(
% 0.08/0.38 ~sP1_prd|sP2_prd|op(e1,e1)=e1),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f143])).
% 0.08/0.38 fof(f146,plain,(
% 0.08/0.38 ~sP1_prd|sP2_prd|op(e2,e2)=e1),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f143])).
% 0.08/0.38 fof(f147,plain,(
% 0.08/0.38 ~sP1_prd|sP2_prd|op(e3,e3)=e1),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f143])).
% 0.08/0.38 fof(f150,plain,(
% 0.08/0.38 (~sP2_prd|(((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0))&(sP2_prd|(((~op(e0,e0)=e0|~op(e1,e1)=e0)|~op(e2,e2)=e0)|~op(e3,e3)=e0))),
% 0.08/0.38 inference(NNF_transformation,[status(thm)],[f141])).
% 0.08/0.38 fof(f151,plain,(
% 0.08/0.38 ~sP2_prd|op(e0,e0)=e0),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f150])).
% 0.08/0.38 fof(f152,plain,(
% 0.08/0.38 ~sP2_prd|op(e1,e1)=e0),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f150])).
% 0.08/0.38 fof(f153,plain,(
% 0.08/0.38 ~sP2_prd|op(e2,e2)=e0),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f150])).
% 0.08/0.38 fof(f154,plain,(
% 0.08/0.38 ~sP2_prd|op(e3,e3)=e0),
% 0.08/0.38 inference(cnf_transformation,[status(thm)],[f150])).
% 0.08/0.38 fof(f156,definition,(
% 0.08/0.38 sQ0_spl <=> (op(e0,e0)=e0)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f159,definition,(
% 0.08/0.38 sQ1_spl <=> (op(e0,e0)=e1)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f162,definition,(
% 0.08/0.38 sQ2_spl <=> (op(e0,e0)=e2)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f165,definition,(
% 0.08/0.38 sQ3_spl <=> (op(e0,e0)=e3)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f221,definition,(
% 0.08/0.38 sQ20_spl <=> (op(e1,e1)=e0)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f224,definition,(
% 0.08/0.38 sQ21_spl <=> (op(e1,e1)=e1)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f227,definition,(
% 0.08/0.38 sQ22_spl <=> (op(e1,e1)=e2)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f230,definition,(
% 0.08/0.38 sQ23_spl <=> (op(e1,e1)=e3)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f286,definition,(
% 0.08/0.38 sQ40_spl <=> (op(e2,e2)=e0)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f289,definition,(
% 0.08/0.38 sQ41_spl <=> (op(e2,e2)=e1)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f292,definition,(
% 0.08/0.38 sQ42_spl <=> (op(e2,e2)=e2)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f295,definition,(
% 0.08/0.38 sQ43_spl <=> (op(e2,e2)=e3)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f351,definition,(
% 0.08/0.38 sQ60_spl <=> (op(e3,e3)=e0)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f354,definition,(
% 0.08/0.38 sQ61_spl <=> (op(e3,e3)=e1)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f357,definition,(
% 0.08/0.38 sQ62_spl <=> (op(e3,e3)=e2)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f360,definition,(
% 0.08/0.38 sQ63_spl <=> (op(e3,e3)=e3)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f409,plain,(
% 0.08/0.38 ~sQ0_spl|~sQ20_spl|~sQ40_spl|~sQ60_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f124,f156,f221,f286,f351])).
% 0.08/0.38 fof(f410,plain,(
% 0.08/0.38 ~sQ1_spl|~sQ21_spl|~sQ41_spl|~sQ61_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f125,f159,f224,f289,f354])).
% 0.08/0.38 fof(f411,plain,(
% 0.08/0.38 ~sQ2_spl|~sQ22_spl|~sQ42_spl|~sQ62_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f126,f162,f227,f292,f357])).
% 0.08/0.38 fof(f412,plain,(
% 0.08/0.38 ~sQ3_spl|~sQ23_spl|~sQ43_spl|~sQ63_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f127,f165,f230,f295,f360])).
% 0.08/0.38 fof(f413,definition,(
% 0.08/0.38 sQ68_spl <=> (sP0_prd)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f416,plain,(
% 0.08/0.38 sQ68_spl|sQ3_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f128,f413,f165])).
% 0.08/0.38 fof(f417,plain,(
% 0.08/0.38 sQ68_spl|sQ23_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f129,f413,f230])).
% 0.08/0.38 fof(f418,plain,(
% 0.08/0.38 sQ68_spl|sQ43_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f130,f413,f295])).
% 0.08/0.38 fof(f419,plain,(
% 0.08/0.38 sQ68_spl|sQ63_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f131,f413,f360])).
% 0.08/0.38 fof(f420,definition,(
% 0.08/0.38 sQ69_spl <=> (sP1_prd)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f423,plain,(
% 0.08/0.38 ~sQ68_spl|sQ69_spl|sQ2_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f135,f413,f420,f162])).
% 0.08/0.38 fof(f424,plain,(
% 0.08/0.38 ~sQ68_spl|sQ69_spl|sQ22_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f136,f413,f420,f227])).
% 0.08/0.38 fof(f425,plain,(
% 0.08/0.38 ~sQ68_spl|sQ69_spl|sQ42_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f137,f413,f420,f292])).
% 0.08/0.38 fof(f426,plain,(
% 0.08/0.38 ~sQ68_spl|sQ69_spl|sQ62_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f138,f413,f420,f357])).
% 0.08/0.38 fof(f429,definition,(
% 0.08/0.38 sQ70_spl <=> (sP2_prd)),
% 0.08/0.38 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.08/0.38 fof(f432,plain,(
% 0.08/0.38 ~sQ69_spl|sQ70_spl|sQ1_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f144,f420,f429,f159])).
% 0.08/0.38 fof(f433,plain,(
% 0.08/0.38 ~sQ69_spl|sQ70_spl|sQ21_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f145,f420,f429,f224])).
% 0.08/0.38 fof(f434,plain,(
% 0.08/0.38 ~sQ69_spl|sQ70_spl|sQ41_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f146,f420,f429,f289])).
% 0.08/0.38 fof(f435,plain,(
% 0.08/0.38 ~sQ69_spl|sQ70_spl|sQ61_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f147,f420,f429,f354])).
% 0.08/0.38 fof(f438,plain,(
% 0.08/0.38 ~sQ70_spl|sQ0_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f151,f429,f156])).
% 0.08/0.38 fof(f439,plain,(
% 0.08/0.38 ~sQ70_spl|sQ20_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f152,f429,f221])).
% 0.08/0.38 fof(f440,plain,(
% 0.08/0.38 ~sQ70_spl|sQ40_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f153,f429,f286])).
% 0.08/0.38 fof(f441,plain,(
% 0.08/0.38 ~sQ70_spl|sQ60_spl),
% 0.08/0.38 inference(split_clause,[status(thm)],[f154,f429,f351])).
% 0.08/0.38 fof(f443,plain,(
% 0.08/0.38 $false),
% 0.08/0.38 inference(sat_refutation,[status(thm)],[f409,f410,f411,f412,f416,f417,f418,f419,f423,f424,f425,f426,f432,f433,f434,f435,f438,f439,f440,f441])).
% 0.08/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.43 % Elapsed time: 0.063254 seconds
% 0.14/0.43 % CPU time: 0.165351 seconds
% 0.14/0.43 % Total memory used: 108.135 MB
% 0.14/0.43 % Net memory used: 108.083 MB
%------------------------------------------------------------------------------