%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP644+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:34:57 PM UTC 2026
% Result : Theorem 81.86s 16.89s
% Output : CNFRefutation 88.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 18
% Syntax : Number of formulae : 79 ( 22 unt; 12 def)
% Number of atoms : 277 ( 0 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 325 ( 127 ~; 128 |; 40 &)
% ( 14 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 13 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 46 ( 42 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f71,axiom,
! [A] : r1_tarski(k1_xboole_0,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1265,axiom,
? [A] :
( v3_ordinal1(A)
& v2_ordinal1(A)
& v1_ordinal1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18994,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k3_group_1(A,B),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21871,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_group_2(C,A)
=> ( r1_rlvect_1(C,B)
=> r1_rlvect_1(C,k3_group_1(A,B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36508,axiom,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
<=> r1_rlvect_1(B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36512,conjecture,
! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
=> r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36513,negated_conjecture,
~ ! [A] :
( ( l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_group_2(B,A)
& v1_group_1(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
=> r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f36512]) ).
fof(f36742,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f39463,plain,
( v3_ordinal1(sK244_skl)
& v2_ordinal1(sK244_skl)
& v1_ordinal1(sK244_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK244_skl]),skolemize(A,sK244_skl)],[f1265]) ).
fof(f39466,plain,
v3_ordinal1(sK244_skl),
inference(cnf_transformation,[status(thm)],[f39463]) ).
fof(f97882,plain,
! [A,B] :
( m1_subset_1(k3_group_1(A,B),u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18994]) ).
fof(f97883,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f97882]) ).
fof(f108064,plain,
! [A] :
( ! [B] :
( ! [C] :
( r1_rlvect_1(C,k3_group_1(A,B))
| ~ r1_rlvect_1(C,B)
| ~ m1_group_2(C,A) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21871]) ).
fof(f108065,plain,
! [X0,X1,X2] :
( r1_rlvect_1(X2,k3_group_1(X0,X1))
| ~ r1_rlvect_1(X2,X1)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f108064]) ).
fof(f162770,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
<=> r1_rlvect_1(B,C) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_group_2(B,A)
| ~ v1_group_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36508]) ).
fof(f162771,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ r1_rlvect_1(B,C)
| r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) )
& ( r1_rlvect_1(B,C)
| ~ r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) ) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_group_2(B,A)
| ~ v1_group_1(B) )
| ~ l1_group_1(A)
| ~ v4_group_1(A)
| ~ v3_group_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f162770]) ).
fof(f162772,plain,
! [X0,X1,X2] :
( r1_rlvect_1(X1,X2)
| ~ r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f162771]) ).
fof(f162773,plain,
! [X0,X1,X2] :
( ~ r1_rlvect_1(X1,X2)
| r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f162771]) ).
fof(f162780,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B))
& r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))
& m1_subset_1(C,u1_struct_0(A)) )
& m1_group_2(B,A)
& v1_group_1(B) )
& l1_group_1(A)
& v4_group_1(A)
& v3_group_1(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36513]) ).
fof(f162781,plain,
( ~ r2_hidden(k3_group_1(sK12737_skl,sK12739_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl))
& r2_hidden(sK12739_skl,k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl))
& m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl))
& m1_group_2(sK12738_skl,sK12737_skl)
& v1_group_1(sK12738_skl)
& l1_group_1(sK12737_skl)
& v4_group_1(sK12737_skl)
& v3_group_1(sK12737_skl)
& ~ v3_struct_0(sK12737_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12737_skl,sK12738_skl,sK12739_skl]),skolemize(A,sK12737_skl),skolemize(B,sK12738_skl),skolemize(C,sK12739_skl)],[f162780]) ).
fof(f162782,plain,
~ v3_struct_0(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162783,plain,
v3_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162784,plain,
v4_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162785,plain,
l1_group_1(sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162786,plain,
v1_group_1(sK12738_skl),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162787,plain,
m1_group_2(sK12738_skl,sK12737_skl),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162788,plain,
m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl)),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162789,plain,
r2_hidden(sK12739_skl,k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f162790,plain,
~ r2_hidden(k3_group_1(sK12737_skl,sK12739_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)),
inference(cnf_transformation,[status(thm)],[f162781]) ).
fof(f181738,definition,
! [X1] :
( sQ57_spl
<=> ~ v3_ordinal1(X1) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f181739,plain,
! [X0] :
( ~ sQ57_spl
| ~ v3_ordinal1(X0) ),
inference(component_clause,[status(thm)],[f181738]) ).
fof(f196593,definition,
( sQ3079_spl
<=> v3_struct_0(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3079_spl])],[split_symbol_definition]) ).
fof(f196594,plain,
( ~ sQ3079_spl
| v3_struct_0(sK12737_skl) ),
inference(component_clause,[status(thm)],[f196593]) ).
fof(f196596,definition,
( sQ3080_spl
<=> v3_group_1(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3080_spl])],[split_symbol_definition]) ).
fof(f196598,plain,
( sQ3080_spl
| ~ v3_group_1(sK12737_skl) ),
inference(component_clause,[status(thm)],[f196596]) ).
fof(f196599,definition,
( sQ3081_spl
<=> v4_group_1(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3081_spl])],[split_symbol_definition]) ).
fof(f196601,plain,
( sQ3081_spl
| ~ v4_group_1(sK12737_skl) ),
inference(component_clause,[status(thm)],[f196599]) ).
fof(f196602,definition,
( sQ3082_spl
<=> l1_group_1(sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3082_spl])],[split_symbol_definition]) ).
fof(f196604,plain,
( sQ3082_spl
| ~ l1_group_1(sK12737_skl) ),
inference(component_clause,[status(thm)],[f196602]) ).
fof(f196609,plain,
( sQ3082_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f196604,f162785]) ).
fof(f196610,plain,
sQ3082_spl,
inference(contradiction_clause,[status(thm)],[f196609]) ).
fof(f196611,plain,
( sQ3081_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f196601,f162784]) ).
fof(f196612,plain,
sQ3081_spl,
inference(contradiction_clause,[status(thm)],[f196611]) ).
fof(f196613,plain,
( sQ3080_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f196598,f162783]) ).
fof(f196614,plain,
sQ3080_spl,
inference(contradiction_clause,[status(thm)],[f196613]) ).
fof(f196615,plain,
( ~ sQ3079_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f196594,f162782]) ).
fof(f196616,plain,
~ sQ3079_spl,
inference(contradiction_clause,[status(thm)],[f196615]) ).
fof(f197682,definition,
( sQ3091_spl
<=> v1_group_1(sK12738_skl) ),
introduced(definition,[new_symbols(definition,[sQ3091_spl])],[split_symbol_definition]) ).
fof(f197684,plain,
( sQ3091_spl
| ~ v1_group_1(sK12738_skl) ),
inference(component_clause,[status(thm)],[f197682]) ).
fof(f197685,definition,
( sQ3092_spl
<=> m1_group_2(sK12738_skl,sK12737_skl) ),
introduced(definition,[new_symbols(definition,[sQ3092_spl])],[split_symbol_definition]) ).
fof(f197687,plain,
( sQ3092_spl
| ~ m1_group_2(sK12738_skl,sK12737_skl) ),
inference(component_clause,[status(thm)],[f197685]) ).
fof(f197695,plain,
( sQ3092_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f197687,f162787]) ).
fof(f197696,plain,
sQ3092_spl,
inference(contradiction_clause,[status(thm)],[f197695]) ).
fof(f197697,plain,
( sQ3091_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f197684,f162786]) ).
fof(f197698,plain,
sQ3091_spl,
inference(contradiction_clause,[status(thm)],[f197697]) ).
fof(f201132,plain,
( r1_rlvect_1(sK12738_skl,sK12739_skl)
| ~ m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl))
| ~ m1_group_2(sK12738_skl,sK12737_skl)
| ~ v1_group_1(sK12738_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f162789,f162772]) ).
fof(f201181,definition,
( sQ3156_spl
<=> m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3156_spl])],[split_symbol_definition]) ).
fof(f201183,plain,
( sQ3156_spl
| ~ m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl)) ),
inference(component_clause,[status(thm)],[f201181]) ).
fof(f201184,definition,
( sQ3157_spl
<=> r1_rlvect_1(sK12738_skl,sK12739_skl) ),
introduced(definition,[new_symbols(definition,[sQ3157_spl])],[split_symbol_definition]) ).
fof(f201187,plain,
( sQ3157_spl
| ~ sQ3156_spl
| ~ sQ3092_spl
| ~ sQ3091_spl
| ~ sQ3082_spl
| ~ sQ3081_spl
| ~ sQ3080_spl
| sQ3079_spl ),
inference(split_clause,[status(thm)],[f201132,f196593,f196596,f196599,f196602,f197682,f197685,f201181,f201184]) ).
fof(f201215,plain,
( ~ r1_rlvect_1(sK12738_skl,k3_group_1(sK12737_skl,sK12739_skl))
| ~ m1_subset_1(k3_group_1(sK12737_skl,sK12739_skl),u1_struct_0(sK12737_skl))
| ~ m1_group_2(sK12738_skl,sK12737_skl)
| ~ v1_group_1(sK12738_skl)
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f162790,f162773]) ).
fof(f201218,definition,
( sQ3161_spl
<=> m1_subset_1(k3_group_1(sK12737_skl,sK12739_skl),u1_struct_0(sK12737_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3161_spl])],[split_symbol_definition]) ).
fof(f201220,plain,
( sQ3161_spl
| ~ m1_subset_1(k3_group_1(sK12737_skl,sK12739_skl),u1_struct_0(sK12737_skl)) ),
inference(component_clause,[status(thm)],[f201218]) ).
fof(f201221,definition,
( sQ3162_spl
<=> r1_rlvect_1(sK12738_skl,k3_group_1(sK12737_skl,sK12739_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3162_spl])],[split_symbol_definition]) ).
fof(f201223,plain,
( sQ3162_spl
| ~ r1_rlvect_1(sK12738_skl,k3_group_1(sK12737_skl,sK12739_skl)) ),
inference(component_clause,[status(thm)],[f201221]) ).
fof(f201224,plain,
( ~ sQ3162_spl
| ~ sQ3161_spl
| ~ sQ3092_spl
| ~ sQ3091_spl
| ~ sQ3082_spl
| ~ sQ3081_spl
| ~ sQ3080_spl
| sQ3079_spl ),
inference(split_clause,[status(thm)],[f201215,f196593,f196596,f196599,f196602,f197682,f197685,f201218,f201221]) ).
fof(f201257,plain,
( sQ3156_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f201183,f162788]) ).
fof(f201258,plain,
sQ3156_spl,
inference(contradiction_clause,[status(thm)],[f201257]) ).
fof(f201267,definition,
! [X0] :
( sQ3165_spl
<=> ~ r1_tarski(k1_xboole_0,X0) ),
introduced(definition,[new_symbols(definition,[sQ3165_spl])],[split_symbol_definition]) ).
fof(f201268,plain,
! [X0] :
( ~ sQ3165_spl
| ~ r1_tarski(k1_xboole_0,X0) ),
inference(component_clause,[status(thm)],[f201267]) ).
fof(f201279,plain,
( ~ sQ3165_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f201268,f36742]) ).
fof(f201280,plain,
~ sQ3165_spl,
inference(contradiction_clause,[status(thm)],[f201279]) ).
fof(f201337,plain,
( sQ3162_spl
| ~ r1_rlvect_1(sK12738_skl,sK12739_skl)
| ~ m1_group_2(sK12738_skl,sK12737_skl)
| ~ m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl))
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f201223,f108065]) ).
fof(f201338,plain,
( sQ3162_spl
| ~ sQ3157_spl
| ~ sQ3092_spl
| ~ sQ3156_spl
| ~ sQ3082_spl
| ~ sQ3081_spl
| ~ sQ3080_spl
| sQ3079_spl ),
inference(split_clause,[status(thm)],[f201337,f196593,f196596,f196599,f196602,f201181,f197685,f201184,f201221]) ).
fof(f201921,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f39466,f181739]) ).
fof(f201922,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f201921]) ).
fof(f203201,plain,
( sQ3161_spl
| ~ m1_subset_1(sK12739_skl,u1_struct_0(sK12737_skl))
| ~ l1_group_1(sK12737_skl)
| ~ v4_group_1(sK12737_skl)
| ~ v3_group_1(sK12737_skl)
| v3_struct_0(sK12737_skl) ),
inference(resolution,[status(thm)],[f201220,f97883]) ).
fof(f203203,plain,
( sQ3161_spl
| ~ sQ3156_spl
| ~ sQ3082_spl
| ~ sQ3081_spl
| ~ sQ3080_spl
| sQ3079_spl ),
inference(split_clause,[status(thm)],[f203201,f196593,f196596,f196599,f196602,f201181,f201218]) ).
fof(f203204,plain,
$false,
inference(sat_refutation,[status(thm)],[f196610,f196612,f196614,f196616,f197696,f197698,f201187,f201224,f201258,f201280,f201338,f201922,f203203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP644+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n005.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.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:25:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 6.78/7.08 % Drodi V4.1.1
% 81.86/16.89 % Refutation found
% 81.86/16.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 81.86/16.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.40/18.39 % Elapsed time: 17.930330 seconds
% 14.40/18.39 % CPU time: 86.215126 seconds
% 14.40/18.39 % Total memory used: 11.596 GB
% 14.40/18.39 % Net memory used: 11.500 GB
%------------------------------------------------------------------------------