%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM432+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 01:42:52 PM UTC 2026
% Result : Theorem 90.66s 11.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM432+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n012.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 02:28:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 90.66/11.80 % Refutation found
% 90.66/11.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 90.66/11.80 % SZS output start CNFRefutation for theBenchmark
% 90.66/11.80 fof(f5,axiom,(
% 90.66/11.80 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtpldt0(W0,W1)) ) )),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f6,axiom,(
% 90.66/11.80 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtasdt0(W0,W1)) ) )),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f18,definition,(
% 90.66/11.80 (! [W0] :( aInteger0(W0)=> (! [W1] :( aDivisorOf0(W1,W0)<=> ( aInteger0(W1)& W1 != sz00& (? [W2] :( aInteger0(W2)& sdtasdt0(W1,W2) = W0 ) )) ) )) )),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f19,definition,(
% 90.66/11.80 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2)& W2 != sz00 )=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) )),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f21,axiom,(
% 90.66/11.80 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2)& W2 != sz00 )=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)=> sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) )),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f22,hypothesis,(
% 90.66/11.80 ( aInteger0(xa)& aInteger0(xb)& aInteger0(xq)& xq != sz00& aInteger0(xc) ) ),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f24,hypothesis,(
% 90.66/11.80 ( aInteger0(xn)& sdtasdt0(xq,xn) = sdtpldt0(xa,smndt0(xb)) ) ),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f25,hypothesis,(
% 90.66/11.80 ( aInteger0(xm)& sdtasdt0(xq,xm) = sdtpldt0(xb,smndt0(xc)) ) ),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f26,hypothesis,(
% 90.66/11.80 sdtasdt0(xq,sdtpldt0(xn,xm)) = sdtpldt0(xa,smndt0(xc)) ),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f27,conjecture,(
% 90.66/11.80 sdteqdtlpzmzozddtrp0(xa,xc,xq) ),
% 90.66/11.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.66/11.80 fof(f28,negated_conjecture,(
% 90.66/11.80 ~(sdteqdtlpzmzozddtrp0(xa,xc,xq) )),
% 90.66/11.80 inference(negated_conjecture,[status(cth)],[f27])).
% 90.66/11.80 fof(f36,plain,(
% 90.66/11.80 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtpldt0(W0,W1)))),
% 90.66/11.80 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 90.66/11.80 fof(f37,plain,(
% 90.66/11.80 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtpldt0(X0,X1)))),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f36])).
% 90.66/11.80 fof(f38,plain,(
% 90.66/11.80 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtasdt0(W0,W1)))),
% 90.66/11.80 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 90.66/11.80 fof(f39,plain,(
% 90.66/11.80 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtasdt0(X0,X1)))),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f38])).
% 90.66/11.80 fof(f68,plain,(
% 90.66/11.80 ![W0]: (~aInteger0(W0)|(![W1]: (aDivisorOf0(W1,W0)<=>((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0))))))),
% 90.66/11.80 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 90.66/11.80 fof(f69,plain,(
% 90.66/11.80 ![W0]: (~aInteger0(W0)|(![W1]: ((~aDivisorOf0(W1,W0)|((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0))))&(aDivisorOf0(W1,W0)|((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))))))),
% 90.66/11.80 inference(NNF_transformation,[status(thm)],[f68])).
% 90.66/11.80 fof(f70,plain,(
% 90.66/11.80 ![W0]: (~aInteger0(W0)|((![W1]: (~aDivisorOf0(W1,W0)|((aInteger0(W1)&~W1=sz00)&(?[W2]: (aInteger0(W2)&sdtasdt0(W1,W2)=W0)))))&(![W1]: (aDivisorOf0(W1,W0)|((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))))))),
% 90.66/11.80 inference(miniscoping,[status(thm)],[f69])).
% 90.66/11.80 fof(f71,plain,(
% 90.66/11.80 ![W0]: (~aInteger0(W0)|((![W1]: (~aDivisorOf0(W1,W0)|((aInteger0(W1)&~W1=sz00)&(aInteger0(sK0_skl(W1,W0))&sdtasdt0(W1,sK0_skl(W1,W0))=W0))))&(![W1]: (aDivisorOf0(W1,W0)|((~aInteger0(W1)|W1=sz00)|(![W2]: (~aInteger0(W2)|~sdtasdt0(W1,W2)=W0)))))))),
% 90.66/11.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f70])).
% 90.66/11.80 fof(f76,plain,(
% 90.66/11.80 ![X0,X1,X2]: (~aInteger0(X0)|aDivisorOf0(X1,X0)|~aInteger0(X1)|X1=sz00|~aInteger0(X2)|~sdtasdt0(X1,X2)=X0)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f71])).
% 90.66/11.80 fof(f77,plain,(
% 90.66/11.80 ![W0,W1,W2]: ((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|(sdteqdtlpzmzozddtrp0(W0,W1,W2)<=>aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1)))))),
% 90.66/11.80 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 90.66/11.80 fof(f78,plain,(
% 90.66/11.80 ![W0,W1,W2]: ((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|((~sdteqdtlpzmzozddtrp0(W0,W1,W2)|aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))))&(sdteqdtlpzmzozddtrp0(W0,W1,W2)|~aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))))))),
% 90.66/11.80 inference(NNF_transformation,[status(thm)],[f77])).
% 90.66/11.80 fof(f80,plain,(
% 90.66/11.80 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|sdteqdtlpzmzozddtrp0(X0,X1,X2)|~aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))))),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f78])).
% 90.66/11.80 fof(f83,plain,(
% 90.66/11.80 ![W0,W1,W2]: ((((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|W2=sz00)|(~sdteqdtlpzmzozddtrp0(W0,W1,W2)|sdteqdtlpzmzozddtrp0(W1,W0,W2)))),
% 90.66/11.80 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 90.66/11.80 fof(f84,plain,(
% 90.66/11.80 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|X2=sz00|~sdteqdtlpzmzozddtrp0(X0,X1,X2)|sdteqdtlpzmzozddtrp0(X1,X0,X2))),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f83])).
% 90.66/11.80 fof(f85,plain,(
% 90.66/11.80 aInteger0(xa)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f22])).
% 90.66/11.80 fof(f87,plain,(
% 90.66/11.80 aInteger0(xq)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f22])).
% 90.66/11.80 fof(f88,plain,(
% 90.66/11.80 ~xq=sz00),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f22])).
% 90.66/11.80 fof(f89,plain,(
% 90.66/11.80 aInteger0(xc)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f22])).
% 90.66/11.80 fof(f92,plain,(
% 90.66/11.80 aInteger0(xn)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f24])).
% 90.66/11.80 fof(f94,plain,(
% 90.66/11.80 aInteger0(xm)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f25])).
% 90.66/11.80 fof(f96,plain,(
% 90.66/11.80 sdtasdt0(xq,sdtpldt0(xn,xm))=sdtpldt0(xa,smndt0(xc))),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f26])).
% 90.66/11.80 fof(f97,plain,(
% 90.66/11.80 ~sdteqdtlpzmzozddtrp0(xa,xc,xq)),
% 90.66/11.80 inference(cnf_transformation,[status(thm)],[f28])).
% 90.66/11.80 fof(f99,plain,(
% 90.66/11.80 ![X0,X1]: (~aInteger0(sdtasdt0(X0,X1))|aDivisorOf0(X0,sdtasdt0(X0,X1))|~aInteger0(X0)|X0=sz00|~aInteger0(X1))),
% 90.66/11.80 inference(destructive_equality_resolution,[status(thm)],[f76])).
% 90.66/11.80 fof(f112,definition,(
% 90.66/11.80 sQ3_spl <=> (xq=sz00)),
% 90.66/11.80 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 90.66/11.80 fof(f113,plain,(
% 90.66/11.80 xq=sz00|~sQ3_spl),
% 90.66/11.80 inference(component_clause,[status(thm)],[f112])).
% 90.66/11.80 fof(f125,definition,(
% 90.66/11.80 sQ6_spl <=> (aInteger0(xa))),
% 90.66/11.80 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 90.66/11.80 fof(f127,plain,(
% 90.66/11.80 ~aInteger0(xa)|sQ6_spl),
% 90.66/11.80 inference(component_clause,[status(thm)],[f125])).
% 90.66/11.80 fof(f131,definition,(
% 90.66/11.80 sQ8_spl <=> (aInteger0(xq))),
% 90.66/11.80 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 90.66/11.80 fof(f133,plain,(
% 90.66/11.80 ~aInteger0(xq)|sQ8_spl),
% 90.66/11.80 inference(component_clause,[status(thm)],[f131])).
% 90.66/11.80 fof(f138,plain,(
% 90.66/11.80 $false|~sQ3_spl),
% 90.66/11.80 inference(forward_subsumption_resolution,[status(thm)],[f113,f88])).
% 90.66/11.80 fof(f139,plain,(
% 90.66/11.80 ~sQ3_spl),
% 90.66/11.80 inference(contradiction_clause,[status(thm)],[f138])).
% 90.66/11.80 fof(f141,definition,(
% 90.66/11.80 sQ10_spl <=> (aInteger0(xc))),
% 90.66/11.80 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 90.66/11.80 fof(f143,plain,(
% 90.66/11.80 ~aInteger0(xc)|sQ10_spl),
% 90.66/11.80 inference(component_clause,[status(thm)],[f141])).
% 90.66/11.80 fof(f148,plain,(
% 90.66/11.80 $false|sQ8_spl),
% 90.66/11.80 inference(forward_subsumption_resolution,[status(thm)],[f133,f87])).
% 90.66/11.80 fof(f149,plain,(
% 90.66/11.80 sQ8_spl),
% 90.66/11.80 inference(contradiction_clause,[status(thm)],[f148])).
% 90.66/11.80 fof(f172,plain,(
% 90.66/11.80 $false|sQ6_spl),
% 90.66/11.80 inference(forward_subsumption_resolution,[status(thm)],[f127,f85])).
% 90.66/11.80 fof(f173,plain,(
% 90.66/11.80 sQ6_spl),
% 90.66/11.80 inference(contradiction_clause,[status(thm)],[f172])).
% 90.66/11.80 fof(f242,definition,(
% 90.66/11.80 sQ24_spl <=> (sdteqdtlpzmzozddtrp0(xc,xa,xq))),
% 90.66/11.80 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 90.66/11.80 fof(f244,plain,(
% 90.66/11.80 ~sdteqdtlpzmzozddtrp0(xc,xa,xq)|sQ24_spl),
% 90.66/11.80 inference(component_clause,[status(thm)],[f242])).
% 90.66/11.80 fof(f246,plain,(
% 90.66/11.80 $false|sQ10_spl),
% 90.66/11.80 inference(forward_subsumption_resolution,[status(thm)],[f143,f89])).
% 90.66/11.80 fof(f247,plain,(
% 90.66/11.80 sQ10_spl),
% 90.66/11.80 inference(contradiction_clause,[status(thm)],[f246])).
% 90.66/11.80 fof(f290,definition,(
% 90.66/11.80 sQ26_spl <=> (sdteqdtlpzmzozddtrp0(xa,xc,xq))),
% 90.66/11.80 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 90.66/11.84 fof(f334,plain,(
% 90.66/11.84 ~aInteger0(xc)|~aInteger0(xa)|~aInteger0(xq)|xq=sz00|~sdteqdtlpzmzozddtrp0(xc,xa,xq)),
% 90.66/11.84 inference(resolution,[status(thm)],[f97,f84])).
% 90.66/11.84 fof(f335,plain,(
% 90.66/11.84 ~sQ10_spl|~sQ6_spl|~sQ8_spl|sQ3_spl|~sQ24_spl),
% 90.66/11.84 inference(split_clause,[status(thm)],[f334,f141,f125,f131,f112,f242])).
% 90.66/11.84 fof(f391,plain,(
% 90.66/11.84 ~aInteger0(xa)|~aInteger0(xc)|~aInteger0(xq)|xq=sz00|~sdteqdtlpzmzozddtrp0(xa,xc,xq)|sQ24_spl),
% 90.66/11.84 inference(resolution,[status(thm)],[f244,f84])).
% 90.66/11.84 fof(f392,plain,(
% 90.66/11.84 ~sQ6_spl|~sQ10_spl|~sQ8_spl|sQ3_spl|~sQ26_spl|sQ24_spl),
% 90.66/11.84 inference(split_clause,[status(thm)],[f391,f125,f141,f131,f112,f290,f242])).
% 90.66/11.84 fof(f545,plain,(
% 90.66/11.84 ![X0,X1]: (aDivisorOf0(X0,sdtasdt0(X0,X1))|~aInteger0(X0)|X0=sz00|~aInteger0(X1))),
% 90.66/11.84 inference(forward_subsumption_resolution,[status(thm)],[f99,f39])).
% 90.66/11.84 fof(f688,definition,(
% 90.66/11.84 sQ38_spl <=> (aInteger0(sdtpldt0(xn,xm)))),
% 90.66/11.84 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 90.66/11.84 fof(f690,plain,(
% 90.66/11.84 ~aInteger0(sdtpldt0(xn,xm))|sQ38_spl),
% 90.66/11.84 inference(component_clause,[status(thm)],[f688])).
% 90.66/11.84 fof(f905,definition,(
% 90.66/11.84 sQ44_spl <=> (aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc))))),
% 90.66/11.84 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 90.66/11.84 fof(f906,plain,(
% 90.66/11.84 aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc)))|~sQ44_spl),
% 90.66/11.84 inference(component_clause,[status(thm)],[f905])).
% 90.66/11.84 fof(f1135,plain,(
% 90.66/11.84 aDivisorOf0(xq,sdtpldt0(xa,smndt0(xc)))|~aInteger0(xq)|xq=sz00|~aInteger0(sdtpldt0(xn,xm))),
% 90.66/11.84 inference(paramodulation,[status(thm)],[f96,f545])).
% 90.66/11.84 fof(f1151,plain,(
% 90.66/11.84 sQ44_spl|~sQ8_spl|sQ3_spl|~sQ38_spl),
% 90.66/11.84 inference(split_clause,[status(thm)],[f1135,f905,f131,f112,f688])).
% 90.66/11.84 fof(f10167,definition,(
% 90.66/11.84 sQ309_spl <=> (aInteger0(xn))),
% 90.66/11.84 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 90.66/11.84 fof(f10169,plain,(
% 90.66/11.84 ~aInteger0(xn)|sQ309_spl),
% 90.66/11.84 inference(component_clause,[status(thm)],[f10167])).
% 90.66/11.84 fof(f13474,definition,(
% 90.66/11.84 sQ366_spl <=> (aInteger0(xm))),
% 90.66/11.84 introduced(definition,[new_symbols(definition,[sQ366_spl])],[split_symbol_definition])).
% 90.66/11.84 fof(f13476,plain,(
% 90.66/11.84 ~aInteger0(xm)|sQ366_spl),
% 90.66/11.84 inference(component_clause,[status(thm)],[f13474])).
% 90.66/11.84 fof(f14129,plain,(
% 90.66/11.84 ~aInteger0(xn)|~aInteger0(xm)|sQ38_spl),
% 90.66/11.84 inference(resolution,[status(thm)],[f690,f37])).
% 90.66/11.84 fof(f14130,plain,(
% 90.66/11.84 ~sQ309_spl|~sQ366_spl|sQ38_spl),
% 90.66/11.84 inference(split_clause,[status(thm)],[f14129,f10167,f13474,f688])).
% 90.66/11.84 fof(f14131,plain,(
% 90.66/11.84 $false|sQ309_spl),
% 90.66/11.84 inference(forward_subsumption_resolution,[status(thm)],[f10169,f92])).
% 90.66/11.84 fof(f14132,plain,(
% 90.66/11.84 sQ309_spl),
% 90.66/11.84 inference(contradiction_clause,[status(thm)],[f14131])).
% 90.66/11.84 fof(f14133,plain,(
% 90.66/11.84 $false|sQ366_spl),
% 90.66/11.84 inference(forward_subsumption_resolution,[status(thm)],[f13476,f94])).
% 90.66/11.84 fof(f14134,plain,(
% 90.66/11.84 sQ366_spl),
% 90.66/11.84 inference(contradiction_clause,[status(thm)],[f14133])).
% 90.66/11.84 fof(f25237,plain,(
% 90.66/11.84 ~aInteger0(xa)|~aInteger0(xc)|~aInteger0(xq)|xq=sz00|sdteqdtlpzmzozddtrp0(xa,xc,xq)|~sQ44_spl),
% 90.66/11.84 inference(resolution,[status(thm)],[f80,f906])).
% 90.66/11.84 fof(f25241,plain,(
% 90.66/11.84 ~sQ6_spl|~sQ10_spl|~sQ8_spl|sQ3_spl|sQ26_spl|~sQ44_spl),
% 90.66/11.84 inference(split_clause,[status(thm)],[f25237,f125,f141,f131,f112,f290,f905])).
% 90.66/11.84 fof(f25244,plain,(
% 90.66/11.84 $false),
% 90.66/11.84 inference(sat_refutation,[status(thm)],[f139,f149,f173,f247,f335,f392,f1151,f14130,f14132,f14134,f25241])).
% 90.66/11.84 % SZS output end CNFRefutation for theBenchmark.p
% 90.66/11.88 % Elapsed time: 11.518856 seconds
% 90.66/11.88 % CPU time: 91.229926 seconds
% 90.66/11.88 % Total memory used: 880.624 MB
% 90.66/11.88 % Net memory used: 817.976 MB
%------------------------------------------------------------------------------