%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG039+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 : 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 11:49:30 AM UTC 2026
% Result : Theorem 0.02s 0.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG039+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Mon Sep 21 12:53:54 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.30 % Drodi V4.1.1
% 0.02/0.32 % Refutation found
% 0.02/0.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/0.32 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.32 fof(f7,conjecture,(
% 0.02/0.32 ~ ( ( ( 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.02/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.32 fof(f8,negated_conjecture,(
% 0.02/0.32 ~(~ ( ( ( 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.02/0.32 inference(negated_conjecture,[status(cth)],[f7])).
% 0.02/0.32 fof(f122,plain,(
% 0.02/0.32 ((((((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.02/0.32 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.02/0.32 fof(f123,definition,(
% 0.02/0.32 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.02/0.32 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.02/0.32 fof(f124,plain,(
% 0.02/0.32 (sP0_prd|(((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.02/0.32 inference(formula_renaming,[status(thm)],[f122,f123])).
% 0.02/0.32 fof(f125,plain,(
% 0.02/0.32 sP0_prd|op(e0,e0)=e3),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f126,plain,(
% 0.02/0.32 sP0_prd|op(e1,e1)=e3),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f127,plain,(
% 0.02/0.32 sP0_prd|op(e2,e2)=e3),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f128,plain,(
% 0.02/0.32 sP0_prd|op(e3,e3)=e3),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f129,plain,(
% 0.02/0.32 ~op(e0,e0)=e0|~op(e1,e1)=e0|~op(e2,e2)=e0|~op(e3,e3)=e0),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f130,plain,(
% 0.02/0.32 ~op(e0,e0)=e1|~op(e1,e1)=e1|~op(e2,e2)=e1|~op(e3,e3)=e1),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f131,plain,(
% 0.02/0.32 ~op(e0,e0)=e2|~op(e1,e1)=e2|~op(e2,e2)=e2|~op(e3,e3)=e2),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f132,plain,(
% 0.02/0.32 ~op(e0,e0)=e3|~op(e1,e1)=e3|~op(e2,e2)=e3|~op(e3,e3)=e3),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f124])).
% 0.02/0.32 fof(f133,definition,(
% 0.02/0.32 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.02/0.32 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.02/0.32 fof(f134,plain,(
% 0.02/0.32 sP0_prd<=>(sP1_prd|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2))),
% 0.02/0.32 inference(formula_renaming,[status(thm)],[f123,f133])).
% 0.02/0.32 fof(f135,plain,(
% 0.02/0.32 (~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.02/0.32 inference(NNF_transformation,[status(thm)],[f134])).
% 0.02/0.32 fof(f136,plain,(
% 0.02/0.32 ~sP0_prd|sP1_prd|op(e0,e0)=e2),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f135])).
% 0.02/0.32 fof(f137,plain,(
% 0.02/0.32 ~sP0_prd|sP1_prd|op(e1,e1)=e2),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f135])).
% 0.02/0.32 fof(f138,plain,(
% 0.02/0.32 ~sP0_prd|sP1_prd|op(e2,e2)=e2),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f135])).
% 0.02/0.32 fof(f139,plain,(
% 0.02/0.32 ~sP0_prd|sP1_prd|op(e3,e3)=e2),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f135])).
% 0.02/0.32 fof(f142,definition,(
% 0.02/0.32 sP2_prd<=>(((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.02/0.32 fof(f143,plain,(
% 0.02/0.32 sP1_prd<=>(sP2_prd|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))),
% 0.02/0.32 inference(formula_renaming,[status(thm)],[f133,f142])).
% 0.02/0.32 fof(f144,plain,(
% 0.02/0.32 (~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.02/0.32 inference(NNF_transformation,[status(thm)],[f143])).
% 0.02/0.32 fof(f145,plain,(
% 0.02/0.32 ~sP1_prd|sP2_prd|op(e0,e0)=e1),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f144])).
% 0.02/0.32 fof(f146,plain,(
% 0.02/0.32 ~sP1_prd|sP2_prd|op(e1,e1)=e1),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f144])).
% 0.02/0.32 fof(f147,plain,(
% 0.02/0.32 ~sP1_prd|sP2_prd|op(e2,e2)=e1),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f144])).
% 0.02/0.32 fof(f148,plain,(
% 0.02/0.32 ~sP1_prd|sP2_prd|op(e3,e3)=e1),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f144])).
% 0.02/0.32 fof(f151,plain,(
% 0.02/0.32 (~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.02/0.32 inference(NNF_transformation,[status(thm)],[f142])).
% 0.02/0.32 fof(f152,plain,(
% 0.02/0.32 ~sP2_prd|op(e0,e0)=e0),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f151])).
% 0.02/0.32 fof(f153,plain,(
% 0.02/0.32 ~sP2_prd|op(e1,e1)=e0),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f151])).
% 0.02/0.32 fof(f154,plain,(
% 0.02/0.32 ~sP2_prd|op(e2,e2)=e0),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f151])).
% 0.02/0.32 fof(f155,plain,(
% 0.02/0.32 ~sP2_prd|op(e3,e3)=e0),
% 0.02/0.32 inference(cnf_transformation,[status(thm)],[f151])).
% 0.02/0.32 fof(f157,definition,(
% 0.02/0.32 sQ0_spl <=> (op(e0,e0)=e0)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f160,definition,(
% 0.02/0.32 sQ1_spl <=> (op(e0,e0)=e1)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f163,definition,(
% 0.02/0.32 sQ2_spl <=> (op(e0,e0)=e2)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f166,definition,(
% 0.02/0.32 sQ3_spl <=> (op(e0,e0)=e3)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f222,definition,(
% 0.02/0.32 sQ20_spl <=> (op(e1,e1)=e0)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f225,definition,(
% 0.02/0.32 sQ21_spl <=> (op(e1,e1)=e1)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f228,definition,(
% 0.02/0.32 sQ22_spl <=> (op(e1,e1)=e2)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f231,definition,(
% 0.02/0.32 sQ23_spl <=> (op(e1,e1)=e3)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f287,definition,(
% 0.02/0.32 sQ40_spl <=> (op(e2,e2)=e0)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f290,definition,(
% 0.02/0.32 sQ41_spl <=> (op(e2,e2)=e1)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f293,definition,(
% 0.02/0.32 sQ42_spl <=> (op(e2,e2)=e2)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f296,definition,(
% 0.02/0.32 sQ43_spl <=> (op(e2,e2)=e3)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f352,definition,(
% 0.02/0.32 sQ60_spl <=> (op(e3,e3)=e0)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f355,definition,(
% 0.02/0.32 sQ61_spl <=> (op(e3,e3)=e1)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f358,definition,(
% 0.02/0.32 sQ62_spl <=> (op(e3,e3)=e2)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f361,definition,(
% 0.02/0.32 sQ63_spl <=> (op(e3,e3)=e3)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f410,definition,(
% 0.02/0.32 sQ68_spl <=> (sP0_prd)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f413,plain,(
% 0.02/0.32 sQ68_spl|sQ3_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f125,f410,f166])).
% 0.02/0.32 fof(f414,plain,(
% 0.02/0.32 sQ68_spl|sQ23_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f126,f410,f231])).
% 0.02/0.32 fof(f415,plain,(
% 0.02/0.32 sQ68_spl|sQ43_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f127,f410,f296])).
% 0.02/0.32 fof(f416,plain,(
% 0.02/0.32 sQ68_spl|sQ63_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f128,f410,f361])).
% 0.02/0.32 fof(f417,plain,(
% 0.02/0.32 ~sQ0_spl|~sQ20_spl|~sQ40_spl|~sQ60_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f129,f157,f222,f287,f352])).
% 0.02/0.32 fof(f418,plain,(
% 0.02/0.32 ~sQ1_spl|~sQ21_spl|~sQ41_spl|~sQ61_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f130,f160,f225,f290,f355])).
% 0.02/0.32 fof(f419,plain,(
% 0.02/0.32 ~sQ2_spl|~sQ22_spl|~sQ42_spl|~sQ62_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f131,f163,f228,f293,f358])).
% 0.02/0.32 fof(f420,plain,(
% 0.02/0.32 ~sQ3_spl|~sQ23_spl|~sQ43_spl|~sQ63_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f132,f166,f231,f296,f361])).
% 0.02/0.32 fof(f421,definition,(
% 0.02/0.32 sQ69_spl <=> (sP1_prd)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f424,plain,(
% 0.02/0.32 ~sQ68_spl|sQ69_spl|sQ2_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f136,f410,f421,f163])).
% 0.02/0.32 fof(f425,plain,(
% 0.02/0.32 ~sQ68_spl|sQ69_spl|sQ22_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f137,f410,f421,f228])).
% 0.02/0.32 fof(f426,plain,(
% 0.02/0.32 ~sQ68_spl|sQ69_spl|sQ42_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f138,f410,f421,f293])).
% 0.02/0.32 fof(f427,plain,(
% 0.02/0.32 ~sQ68_spl|sQ69_spl|sQ62_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f139,f410,f421,f358])).
% 0.02/0.32 fof(f430,definition,(
% 0.02/0.32 sQ70_spl <=> (sP2_prd)),
% 0.02/0.32 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.02/0.32 fof(f433,plain,(
% 0.02/0.32 ~sQ69_spl|sQ70_spl|sQ1_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f145,f421,f430,f160])).
% 0.02/0.32 fof(f434,plain,(
% 0.02/0.32 ~sQ69_spl|sQ70_spl|sQ21_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f146,f421,f430,f225])).
% 0.02/0.32 fof(f435,plain,(
% 0.02/0.32 ~sQ69_spl|sQ70_spl|sQ41_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f147,f421,f430,f290])).
% 0.02/0.32 fof(f436,plain,(
% 0.02/0.32 ~sQ69_spl|sQ70_spl|sQ61_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f148,f421,f430,f355])).
% 0.02/0.32 fof(f439,plain,(
% 0.02/0.32 ~sQ70_spl|sQ0_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f152,f430,f157])).
% 0.02/0.32 fof(f440,plain,(
% 0.02/0.32 ~sQ70_spl|sQ20_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f153,f430,f222])).
% 0.02/0.32 fof(f441,plain,(
% 0.02/0.32 ~sQ70_spl|sQ40_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f154,f430,f287])).
% 0.02/0.32 fof(f442,plain,(
% 0.02/0.32 ~sQ70_spl|sQ60_spl),
% 0.02/0.32 inference(split_clause,[status(thm)],[f155,f430,f352])).
% 0.02/0.32 fof(f444,plain,(
% 0.02/0.32 $false),
% 0.02/0.32 inference(sat_refutation,[status(thm)],[f413,f414,f415,f416,f417,f418,f419,f420,f424,f425,f426,f427,f433,f434,f435,f436,f439,f440,f441,f442])).
% 0.02/0.32 % SZS output end CNFRefutation for theBenchmark.p
% 0.07/0.35 % Elapsed time: 0.039475 seconds
% 0.07/0.35 % CPU time: 0.093477 seconds
% 0.07/0.35 % Total memory used: 108.170 MB
% 0.07/0.35 % Net memory used: 108.119 MB
%------------------------------------------------------------------------------