%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU026+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 02:21:35 PM UTC 2026
% Result : Theorem 0.11s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU026+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 05:47:34 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.51 % Refutation found
% 0.11/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.51 fof(f5,axiom,(
% 0.11/0.51 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f23,axiom,(
% 0.11/0.51 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f27,axiom,(
% 0.11/0.51 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f29,axiom,(
% 0.11/0.51 (! [A,B] : subset(A,A) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f33,axiom,(
% 0.11/0.51 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(relation_rng(A),relation_dom(B))=> relation_dom(relation_composition(A,B)) = relation_dom(A) ) ) )) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f34,axiom,(
% 0.11/0.51 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(relation_dom(A),relation_rng(B))=> relation_rng(relation_composition(B,A)) = relation_rng(A) ) ) )) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f36,axiom,(
% 0.11/0.51 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_rng(A) = relation_dom(function_inverse(A))& relation_dom(A) = relation_rng(function_inverse(A)) ) ) ) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f37,conjecture,(
% 0.11/0.51 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_dom(relation_composition(function_inverse(A),A)) = relation_rng(A)& relation_rng(relation_composition(function_inverse(A),A)) = relation_rng(A) ) ) ) )),
% 0.11/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.51 fof(f38,negated_conjecture,(
% 0.11/0.51 ~((! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_dom(relation_composition(function_inverse(A),A)) = relation_rng(A)& relation_rng(relation_composition(function_inverse(A),A)) = relation_rng(A) ) ) ) ))),
% 0.11/0.51 inference(negated_conjecture,[status(cth)],[f37])).
% 0.11/0.51 fof(f53,plain,(
% 0.11/0.51 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.11/0.51 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.11/0.51 fof(f54,plain,(
% 0.11/0.51 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f53])).
% 0.11/0.51 fof(f98,plain,(
% 0.11/0.51 ((relation(sK5_skl)&empty(sK5_skl))&function(sK5_skl))),
% 0.11/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f23])).
% 0.11/0.51 fof(f100,plain,(
% 0.11/0.51 empty(sK5_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f98])).
% 0.11/0.51 fof(f110,plain,(
% 0.11/0.51 ((relation(sK9_skl)&function(sK9_skl))&one_to_one(sK9_skl))),
% 0.11/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f27])).
% 0.11/0.51 fof(f111,plain,(
% 0.11/0.51 relation(sK9_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.51 fof(f112,plain,(
% 0.11/0.51 function(sK9_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.51 fof(f117,plain,(
% 0.11/0.51 ![A]: subset(A,A)),
% 0.11/0.51 inference(miniscoping,[status(thm)],[f29])).
% 0.11/0.51 fof(f118,plain,(
% 0.11/0.51 ![X0]: (subset(X0,X0))),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f117])).
% 0.11/0.51 fof(f127,plain,(
% 0.11/0.51 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(relation_rng(A),relation_dom(B))|relation_dom(relation_composition(A,B))=relation_dom(A)))))),
% 0.11/0.51 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.11/0.51 fof(f128,plain,(
% 0.11/0.51 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(relation_rng(X0),relation_dom(X1))|relation_dom(relation_composition(X0,X1))=relation_dom(X0))),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f127])).
% 0.11/0.51 fof(f129,plain,(
% 0.11/0.51 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(relation_dom(A),relation_rng(B))|relation_rng(relation_composition(B,A))=relation_rng(A)))))),
% 0.11/0.51 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.11/0.51 fof(f130,plain,(
% 0.11/0.51 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(relation_dom(X0),relation_rng(X1))|relation_rng(relation_composition(X1,X0))=relation_rng(X0))),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f129])).
% 0.11/0.51 fof(f134,plain,(
% 0.11/0.51 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_rng(A)=relation_dom(function_inverse(A))&relation_dom(A)=relation_rng(function_inverse(A)))))),
% 0.11/0.51 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.11/0.51 fof(f135,plain,(
% 0.11/0.51 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(X0)=relation_dom(function_inverse(X0)))),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f134])).
% 0.11/0.51 fof(f136,plain,(
% 0.11/0.51 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(X0)=relation_rng(function_inverse(X0)))),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f134])).
% 0.11/0.51 fof(f137,plain,(
% 0.11/0.51 (?[A]: ((relation(A)&function(A))&(one_to_one(A)&(~relation_dom(relation_composition(function_inverse(A),A))=relation_rng(A)|~relation_rng(relation_composition(function_inverse(A),A))=relation_rng(A)))))),
% 0.11/0.51 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.11/0.51 fof(f138,plain,(
% 0.11/0.51 ((relation(sK11_skl)&function(sK11_skl))&(one_to_one(sK11_skl)&(~relation_dom(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl)|~relation_rng(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl))))),
% 0.11/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f137])).
% 0.11/0.51 fof(f139,plain,(
% 0.11/0.51 relation(sK11_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f138])).
% 0.11/0.51 fof(f140,plain,(
% 0.11/0.51 function(sK11_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f138])).
% 0.11/0.51 fof(f141,plain,(
% 0.11/0.51 one_to_one(sK11_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f138])).
% 0.11/0.51 fof(f142,plain,(
% 0.11/0.51 ~relation_dom(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl)|~relation_rng(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl)),
% 0.11/0.51 inference(cnf_transformation,[status(thm)],[f138])).
% 0.11/0.51 fof(f154,definition,(
% 0.11/0.51 sQ0_spl <=> (relation_dom(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f157,definition,(
% 0.11/0.51 sQ1_spl <=> (relation_rng(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f160,plain,(
% 0.11/0.51 ~sQ0_spl|~sQ1_spl),
% 0.11/0.51 inference(split_clause,[status(thm)],[f142,f154,f157])).
% 0.11/0.51 fof(f170,plain,(
% 0.11/0.51 ~relation(sK11_skl)|~function(sK11_skl)|relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))),
% 0.11/0.51 inference(resolution,[status(thm)],[f135,f141])).
% 0.11/0.51 fof(f172,definition,(
% 0.11/0.51 sQ2_spl <=> (relation(sK11_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f174,plain,(
% 0.11/0.51 ~relation(sK11_skl)|sQ2_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f172])).
% 0.11/0.51 fof(f175,definition,(
% 0.11/0.51 sQ3_spl <=> (function(sK11_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f177,plain,(
% 0.11/0.51 ~function(sK11_skl)|sQ3_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f175])).
% 0.11/0.51 fof(f178,definition,(
% 0.11/0.51 sQ4_spl <=> (relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl)))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f179,plain,(
% 0.11/0.51 relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))|~sQ4_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f178])).
% 0.11/0.51 fof(f181,plain,(
% 0.11/0.51 ~sQ2_spl|~sQ3_spl|sQ4_spl),
% 0.11/0.51 inference(split_clause,[status(thm)],[f170,f172,f175,f178])).
% 0.11/0.51 fof(f194,definition,(
% 0.11/0.51 sQ7_spl <=> (relation(function_inverse(sK11_skl)))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f196,plain,(
% 0.11/0.51 ~relation(function_inverse(sK11_skl))|sQ7_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f194])).
% 0.11/0.51 fof(f202,plain,(
% 0.11/0.51 $false|sQ3_spl),
% 0.11/0.51 inference(forward_subsumption_resolution,[status(thm)],[f177,f140])).
% 0.11/0.51 fof(f203,plain,(
% 0.11/0.51 sQ3_spl),
% 0.11/0.51 inference(contradiction_clause,[status(thm)],[f202])).
% 0.11/0.51 fof(f210,plain,(
% 0.11/0.51 ~relation(sK11_skl)|~function(sK11_skl)|sQ7_spl),
% 0.11/0.51 inference(resolution,[status(thm)],[f196,f54])).
% 0.11/0.51 fof(f211,plain,(
% 0.11/0.51 ~sQ2_spl|~sQ3_spl|sQ7_spl),
% 0.11/0.51 inference(split_clause,[status(thm)],[f210,f172,f175,f194])).
% 0.11/0.51 fof(f212,plain,(
% 0.11/0.51 $false|sQ2_spl),
% 0.11/0.51 inference(forward_subsumption_resolution,[status(thm)],[f174,f139])).
% 0.11/0.51 fof(f213,plain,(
% 0.11/0.51 sQ2_spl),
% 0.11/0.51 inference(contradiction_clause,[status(thm)],[f212])).
% 0.11/0.51 fof(f214,plain,(
% 0.11/0.51 ~relation(sK11_skl)|~function(sK11_skl)|relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))),
% 0.11/0.51 inference(resolution,[status(thm)],[f136,f141])).
% 0.11/0.51 fof(f216,definition,(
% 0.11/0.51 sQ9_spl <=> (relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl)))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f217,plain,(
% 0.11/0.51 relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))|~sQ9_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f216])).
% 0.11/0.51 fof(f219,plain,(
% 0.11/0.51 ~sQ2_spl|~sQ3_spl|sQ9_spl),
% 0.11/0.51 inference(split_clause,[status(thm)],[f214,f172,f175,f216])).
% 0.11/0.51 fof(f231,definition,(
% 0.11/0.51 sQ11_spl <=> (empty(sK5_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f233,plain,(
% 0.11/0.51 ~empty(sK5_skl)|sQ11_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f231])).
% 0.11/0.51 fof(f269,plain,(
% 0.11/0.51 $false|sQ11_spl),
% 0.11/0.51 inference(forward_subsumption_resolution,[status(thm)],[f233,f100])).
% 0.11/0.51 fof(f270,plain,(
% 0.11/0.51 sQ11_spl),
% 0.11/0.51 inference(contradiction_clause,[status(thm)],[f269])).
% 0.11/0.51 fof(f273,definition,(
% 0.11/0.51 sQ17_spl <=> (relation(sK9_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f275,plain,(
% 0.11/0.51 ~relation(sK9_skl)|sQ17_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f273])).
% 0.11/0.51 fof(f276,definition,(
% 0.11/0.51 sQ18_spl <=> (function(sK9_skl))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f278,plain,(
% 0.11/0.51 ~function(sK9_skl)|sQ18_spl),
% 0.11/0.51 inference(component_clause,[status(thm)],[f276])).
% 0.11/0.51 fof(f287,plain,(
% 0.11/0.51 $false|sQ18_spl),
% 0.11/0.51 inference(forward_subsumption_resolution,[status(thm)],[f278,f112])).
% 0.11/0.51 fof(f288,plain,(
% 0.11/0.51 sQ18_spl),
% 0.11/0.51 inference(contradiction_clause,[status(thm)],[f287])).
% 0.11/0.51 fof(f289,plain,(
% 0.11/0.51 $false|sQ17_spl),
% 0.11/0.51 inference(forward_subsumption_resolution,[status(thm)],[f275,f111])).
% 0.11/0.51 fof(f290,plain,(
% 0.11/0.51 sQ17_spl),
% 0.11/0.51 inference(contradiction_clause,[status(thm)],[f289])).
% 0.11/0.51 fof(f362,plain,(
% 0.11/0.51 ![X0]: (~relation(function_inverse(sK11_skl))|~relation(X0)|~subset(relation_dom(sK11_skl),relation_dom(X0))|relation_dom(relation_composition(function_inverse(sK11_skl),X0))=relation_dom(function_inverse(sK11_skl))|~sQ9_spl)),
% 0.11/0.51 inference(paramodulation,[status(thm)],[f217,f128])).
% 0.11/0.51 fof(f369,definition,(
% 0.11/0.51 ![X0]: (sQ30_spl <=> (~relation(X0)|~subset(relation_dom(sK11_skl),relation_dom(X0))|relation_dom(relation_composition(function_inverse(sK11_skl),X0))=relation_dom(function_inverse(sK11_skl))))),
% 0.11/0.51 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.11/0.51 fof(f370,plain,(
% 0.11/0.51 ![X0]: (~relation(X0)|~subset(relation_dom(sK11_skl),relation_dom(X0))|relation_dom(relation_composition(function_inverse(sK11_skl),X0))=relation_dom(function_inverse(sK11_skl))|~sQ30_spl)),
% 0.11/0.51 inference(component_clause,[status(thm)],[f369])).
% 0.11/0.51 fof(f372,plain,(
% 0.11/0.51 ~sQ7_spl|sQ30_spl|~sQ9_spl),
% 0.11/0.51 inference(split_clause,[status(thm)],[f362,f194,f369,f216])).
% 0.11/0.51 fof(f381,plain,(
% 0.11/0.51 ![X0]: (~relation(X0)|~subset(relation_dom(sK11_skl),relation_dom(X0))|relation_dom(relation_composition(function_inverse(sK11_skl),X0))=relation_rng(sK11_skl)|~sQ4_spl|~sQ30_spl)),
% 0.11/0.51 inference(forward_demodulation,[status(thm)],[f179,f370])).
% 0.11/0.51 fof(f404,plain,(
% 0.11/0.51 ~relation(sK11_skl)|relation_dom(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl)|~sQ4_spl|~sQ30_spl),
% 0.11/0.51 inference(resolution,[status(thm)],[f381,f118])).
% 0.11/0.51 fof(f407,plain,(
% 0.11/0.51 ~sQ2_spl|sQ0_spl|~sQ4_spl|~sQ30_spl),
% 0.11/0.51 inference(split_clause,[status(thm)],[f404,f172,f154,f178,f369])).
% 0.11/0.51 fof(f481,plain,(
% 0.11/0.51 ![X0]: (~relation(X0)|~relation(function_inverse(sK11_skl))|~subset(relation_dom(X0),relation_dom(sK11_skl))|relation_rng(relation_composition(function_inverse(sK11_skl),X0))=relation_rng(X0)|~sQ9_spl)),
% 0.11/0.51 inference(paramodulation,[status(thm)],[f217,f130])).
% 0.11/0.51 fof(f502,definition,(
% 0.11/0.52 ![X0]: (sQ57_spl <=> (~relation(X0)|~subset(relation_dom(X0),relation_dom(sK11_skl))|relation_rng(relation_composition(function_inverse(sK11_skl),X0))=relation_rng(X0)))),
% 0.11/0.52 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.11/0.52 fof(f503,plain,(
% 0.11/0.52 ![X0]: (~relation(X0)|~subset(relation_dom(X0),relation_dom(sK11_skl))|relation_rng(relation_composition(function_inverse(sK11_skl),X0))=relation_rng(X0)|~sQ57_spl)),
% 0.11/0.52 inference(component_clause,[status(thm)],[f502])).
% 0.11/0.52 fof(f505,plain,(
% 0.11/0.52 sQ57_spl|~sQ7_spl|~sQ9_spl),
% 0.11/0.52 inference(split_clause,[status(thm)],[f481,f502,f194,f216])).
% 0.11/0.52 fof(f574,plain,(
% 0.11/0.52 ~relation(sK11_skl)|relation_rng(relation_composition(function_inverse(sK11_skl),sK11_skl))=relation_rng(sK11_skl)|~sQ57_spl),
% 0.11/0.52 inference(resolution,[status(thm)],[f503,f118])).
% 0.11/0.52 fof(f578,plain,(
% 0.11/0.52 ~sQ2_spl|sQ1_spl|~sQ57_spl),
% 0.11/0.52 inference(split_clause,[status(thm)],[f574,f172,f157,f502])).
% 0.11/0.52 fof(f594,plain,(
% 0.11/0.52 $false),
% 0.11/0.52 inference(sat_refutation,[status(thm)],[f160,f181,f203,f211,f213,f219,f270,f288,f290,f372,f407,f505,f578])).
% 0.11/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.54 % Elapsed time: 0.153006 seconds
% 0.11/0.54 % CPU time: 0.922828 seconds
% 0.11/0.54 % Total memory used: 99.549 MB
% 0.11/0.54 % Net memory used: 98.757 MB
%------------------------------------------------------------------------------