%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU025+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:19:06 PM UTC 2026
% Result : Theorem 0.13s 0.38s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 27
% Syntax : Number of formulae : 108 ( 25 unt; 16 def)
% Number of atoms : 266 ( 43 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 256 ( 98 ~; 100 |; 28 &)
% ( 16 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 17 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 39 ( 35 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( function(function_inverse(A))
& relation(function_inverse(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(relation_rng(A),relation_dom(B))
=> relation_dom(relation_composition(A,B)) = relation_dom(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(relation_dom(A),relation_rng(B))
=> relation_rng(relation_composition(B,A)) = relation_rng(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_dom(A) = relation_rng(function_inverse(A))
& relation_rng(A) = relation_dom(function_inverse(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A)
& relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A)
& relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A) ) ) ),
inference(negated_conjecture,[status(cth)],[f37]) ).
fof(f40,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f54,plain,
! [X0] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f63,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f64,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f98,plain,
( function(sK5_skl)
& empty(sK5_skl)
& relation(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f23]) ).
fof(f100,plain,
empty(sK5_skl),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
function(sK5_skl),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f102,plain,
( relation(sK6_skl)
& ~ empty(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f24]) ).
fof(f104,plain,
relation(sK6_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f110,plain,
( one_to_one(sK9_skl)
& function(sK9_skl)
& relation(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f27]) ).
fof(f111,plain,
relation(sK9_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
function(sK9_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f117,plain,
! [A] : subset(A,A),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f118,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f127,plain,
! [A] :
( ! [B] :
( relation_dom(relation_composition(A,B)) = relation_dom(A)
| ~ subset(relation_rng(A),relation_dom(B))
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f128,plain,
! [X0,X1] :
( relation_dom(relation_composition(X0,X1)) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_dom(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [A] :
( ! [B] :
( relation_rng(relation_composition(B,A)) = relation_rng(A)
| ~ subset(relation_dom(A),relation_rng(B))
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f130,plain,
! [X0,X1] :
( relation_rng(relation_composition(X1,X0)) = relation_rng(X0)
| ~ subset(relation_dom(X0),relation_rng(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f134,plain,
! [A] :
( ( relation_dom(A) = relation_rng(function_inverse(A))
& relation_rng(A) = relation_dom(function_inverse(A)) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f135,plain,
! [X0] :
( relation_rng(X0) = relation_dom(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
! [X0] :
( relation_dom(X0) = relation_rng(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
? [A] :
( ( relation_rng(relation_composition(A,function_inverse(A))) != relation_dom(A)
| relation_dom(relation_composition(A,function_inverse(A))) != relation_dom(A) )
& one_to_one(A)
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f138,plain,
( ( relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl))) != relation_dom(sK11_skl)
| relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl))) != relation_dom(sK11_skl) )
& one_to_one(sK11_skl)
& function(sK11_skl)
& relation(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f137]) ).
fof(f139,plain,
relation(sK11_skl),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
function(sK11_skl),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
one_to_one(sK11_skl),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f142,plain,
( relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl))) != relation_dom(sK11_skl)
| relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl))) != relation_dom(sK11_skl) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f146,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f147,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f154,definition,
( sQ0_spl
<=> relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl))) = relation_dom(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f157,definition,
( sQ1_spl
<=> relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl))) = relation_dom(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f160,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f142,f154,f157]) ).
fof(f166,plain,
( relation_rng(sK11_skl) = relation_dom(function_inverse(sK11_skl))
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f135,f141]) ).
fof(f168,definition,
( sQ2_spl
<=> relation(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f170,plain,
( sQ2_spl
| ~ relation(sK11_skl) ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,definition,
( sQ3_spl
<=> function(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f173,plain,
( sQ3_spl
| ~ function(sK11_skl) ),
inference(component_clause,[status(thm)],[f171]) ).
fof(f174,definition,
( sQ4_spl
<=> relation_rng(sK11_skl) = relation_dom(function_inverse(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f175,plain,
( ~ sQ4_spl
| relation_rng(sK11_skl) = relation_dom(function_inverse(sK11_skl)) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,plain,
( sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f166,f168,f171,f174]) ).
fof(f192,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f173,f140]) ).
fof(f193,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f192]) ).
fof(f194,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f170,f139]) ).
fof(f195,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f194]) ).
fof(f198,definition,
( sQ8_spl
<=> relation(function_inverse(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f200,plain,
( sQ8_spl
| ~ relation(function_inverse(sK11_skl)) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f209,plain,
( sQ8_spl
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f200,f54]) ).
fof(f211,plain,
( sQ8_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f209,f168,f171,f198]) ).
fof(f212,plain,
( relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl))
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f136,f141]) ).
fof(f214,definition,
( sQ11_spl
<=> relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f215,plain,
( ~ sQ11_spl
| relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl)) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,plain,
( sQ11_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f212,f168,f171,f214]) ).
fof(f237,definition,
( sQ14_spl
<=> relation(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f239,plain,
( sQ14_spl
| ~ relation(sK6_skl) ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f263,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f239,f104]) ).
fof(f264,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f263]) ).
fof(f337,definition,
( sQ31_spl
<=> relation(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( sQ31_spl
| ~ relation(sK9_skl) ),
inference(component_clause,[status(thm)],[f337]) ).
fof(f340,definition,
( sQ32_spl
<=> function(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( sQ32_spl
| ~ function(sK9_skl) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f351,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f342,f112]) ).
fof(f352,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f351]) ).
fof(f353,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f339,f111]) ).
fof(f354,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f353]) ).
fof(f447,plain,
sK5_skl = empty_set,
inference(resolution,[status(thm)],[f147,f100]) ).
fof(f467,plain,
! [X0] :
( ~ sQ4_spl
| relation_dom(relation_composition(X0,function_inverse(sK11_skl))) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_rng(sK11_skl))
| ~ relation(function_inverse(sK11_skl))
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f175,f128]) ).
fof(f504,definition,
! [X0] :
( sQ62_spl
<=> ( relation_dom(relation_composition(X0,function_inverse(sK11_skl))) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_rng(sK11_skl))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f505,plain,
! [X0] :
( ~ sQ62_spl
| relation_dom(relation_composition(X0,function_inverse(sK11_skl))) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_rng(sK11_skl))
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f507,plain,
( ~ sQ4_spl
| ~ sQ8_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f467,f504,f198,f174]) ).
fof(f511,plain,
! [X0] :
( ~ sQ4_spl
| relation_rng(relation_composition(X0,function_inverse(sK11_skl))) = relation_rng(function_inverse(sK11_skl))
| ~ subset(relation_rng(sK11_skl),relation_rng(X0))
| ~ relation(X0)
| ~ relation(function_inverse(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f175,f130]) ).
fof(f521,definition,
! [X0] :
( sQ64_spl
<=> ( relation_rng(relation_composition(X0,function_inverse(sK11_skl))) = relation_rng(function_inverse(sK11_skl))
| ~ subset(relation_rng(sK11_skl),relation_rng(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f522,plain,
! [X0] :
( ~ sQ64_spl
| relation_rng(relation_composition(X0,function_inverse(sK11_skl))) = relation_rng(function_inverse(sK11_skl))
| ~ subset(relation_rng(sK11_skl),relation_rng(X0))
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,plain,
( ~ sQ4_spl
| sQ64_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f511,f198,f521,f174]) ).
fof(f545,plain,
! [X0] :
( ~ sQ64_spl
| ~ sQ11_spl
| relation_rng(relation_composition(X0,function_inverse(sK11_skl))) = relation_dom(sK11_skl)
| ~ subset(relation_rng(sK11_skl),relation_rng(X0))
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f215,f522]) ).
fof(f549,plain,
( ~ sQ62_spl
| relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl))) = relation_dom(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f505,f118]) ).
fof(f555,plain,
( ~ sQ62_spl
| sQ0_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f549,f168,f154,f504]) ).
fof(f640,plain,
function(empty_set),
inference(backward_demodulation,[status(thm)],[f447,f101]) ).
fof(f884,definition,
( sQ115_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f886,plain,
( sQ115_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f884]) ).
fof(f899,definition,
( sQ118_spl
<=> subset(relation_dom(sK11_skl),relation_dom(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f901,plain,
( sQ118_spl
| ~ subset(relation_dom(sK11_skl),relation_dom(sK11_skl)) ),
inference(component_clause,[status(thm)],[f899]) ).
fof(f906,plain,
( sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f901,f118]) ).
fof(f907,plain,
sQ118_spl,
inference(contradiction_clause,[status(thm)],[f906]) ).
fof(f980,definition,
( sQ125_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( sQ125_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f980]) ).
fof(f983,definition,
( sQ126_spl
<=> function(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f985,plain,
( sQ126_spl
| ~ function(empty_set) ),
inference(component_clause,[status(thm)],[f983]) ).
fof(f987,plain,
( sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f64]) ).
fof(f988,plain,
sQ125_spl,
inference(contradiction_clause,[status(thm)],[f987]) ).
fof(f989,plain,
( sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f985,f640]) ).
fof(f990,plain,
sQ126_spl,
inference(contradiction_clause,[status(thm)],[f989]) ).
fof(f1122,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f886,f63]) ).
fof(f1123,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f1122]) ).
fof(f1299,plain,
( ~ sQ64_spl
| ~ sQ11_spl
| relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl))) = relation_dom(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f545,f118]) ).
fof(f1304,plain,
( ~ sQ64_spl
| ~ sQ11_spl
| sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1299,f168,f157,f214,f521]) ).
fof(f1333,plain,
$false,
inference(sat_refutation,[status(thm)],[f160,f177,f193,f195,f211,f217,f264,f352,f354,f507,f524,f555,f907,f988,f990,f1123,f1304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU025+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 05:42:56 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.13/0.38 % Refutation found
% 0.13/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.42 % Elapsed time: 0.052039 seconds
% 0.13/0.42 % CPU time: 0.196033 seconds
% 0.13/0.42 % Total memory used: 84.294 MB
% 0.13/0.42 % Net memory used: 84.129 MB
%------------------------------------------------------------------------------