%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP488-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:36:42 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP488-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:17:52 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.39 % Refutation found
% 0.10/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.39 fof(f1,axiom,(
% 0.10/0.39 (![A,B,C]: (double_divide(A,double_divide(double_divide(double_divide(identity,double_divide(double_divide(A,identity),double_divide(B,C))),B),identity)) = C ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f2,axiom,(
% 0.10/0.39 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f3,axiom,(
% 0.10/0.39 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f4,axiom,(
% 0.10/0.39 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f5,negated_conjecture,(
% 0.10/0.39 multiply(identity,a2) != a2 ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f6,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X0,identity),double_divide(X1,X2))),X1),identity))=X2)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.39 fof(f7,plain,(
% 0.10/0.39 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.39 fof(f8,plain,(
% 0.10/0.39 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.39 fof(f9,plain,(
% 0.10/0.39 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.39 fof(f10,plain,(
% 0.10/0.39 ~multiply(identity,a2)=a2),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.39 fof(f11,definition,(
% 0.10/0.39 sF0_fnc=multiply(identity,a2)),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.10/0.39 fof(f12,plain,(
% 0.10/0.39 ~sF0_fnc=a2),
% 0.10/0.39 inference(definition_folding,[],[f10,f11])).
% 0.10/0.39 fof(f13,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(double_divide(X0,identity),double_divide(X1,X2)))))=X2)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f7,f6])).
% 0.10/0.39 fof(f14,plain,(
% 0.10/0.39 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.10/0.39 fof(f15,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),double_divide(X1,X2)))))=X2)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f8,f13])).
% 0.10/0.39 fof(f16,plain,(
% 0.10/0.39 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f9,f14])).
% 0.10/0.39 fof(f17,plain,(
% 0.10/0.39 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f8,f14])).
% 0.10/0.39 fof(f20,plain,(
% 0.10/0.39 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),multiply(X2,double_divide(identity,double_divide(multiply(X1,X0),double_divide(X2,X3)))))=X3)),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f14,f15])).
% 0.10/0.39 fof(f21,plain,(
% 0.10/0.39 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),X2))))=multiply(X3,double_divide(identity,double_divide(inverse(X1),double_divide(X3,X2)))))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f15,f15])).
% 0.10/0.39 fof(f22,plain,(
% 0.10/0.39 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),identity))))=inverse(X1))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f9,f15])).
% 0.10/0.39 fof(f25,plain,(
% 0.10/0.39 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(inverse(X0)))))=inverse(X1))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f8,f22])).
% 0.10/0.39 fof(f26,plain,(
% 0.10/0.39 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,multiply(identity,X0))))=inverse(X1))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f17,f25])).
% 0.10/0.39 fof(f27,plain,(
% 0.10/0.39 ![X0]: (multiply(identity,inverse(X0))=inverse(multiply(identity,X0)))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f17,f17])).
% 0.10/0.39 fof(f28,plain,(
% 0.10/0.39 ![X0,X1]: (multiply(identity,double_divide(X0,X1))=inverse(multiply(X1,X0)))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f14,f17])).
% 0.10/0.39 fof(f30,plain,(
% 0.10/0.39 ![X0]: (multiply(multiply(identity,X0),inverse(X0))=inverse(identity))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f17,f16])).
% 0.10/0.39 fof(f70,plain,(
% 0.10/0.39 ![X0]: (multiply(multiply(identity,inverse(X0)),multiply(identity,X0))=inverse(identity))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f17,f30])).
% 0.10/0.39 fof(f90,plain,(
% 0.10/0.39 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(X0,X1),multiply(X2,double_divide(identity,double_divide(multiply(X1,X0),X3))))=multiply(X4,double_divide(identity,double_divide(inverse(X2),double_divide(X4,X3)))))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f15,f20])).
% 0.10/0.39 fof(f92,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),multiply(X2,double_divide(identity,double_divide(multiply(X1,X0),inverse(X2)))))=identity)),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f8,f20])).
% 0.10/0.39 fof(f258,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(inverse(X0)))))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,identity)))))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f8,f21])).
% 0.10/0.39 fof(f262,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),X2))))=inverse(multiply(double_divide(inverse(X1),double_divide(identity,X2)),identity)))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f28,f21])).
% 0.10/0.39 fof(f274,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X2)))))=multiply(X2,double_divide(identity,double_divide(inverse(X1),identity))))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f9,f21])).
% 0.10/0.39 fof(f275,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),identity))))=multiply(X2,double_divide(identity,double_divide(inverse(X1),inverse(X2)))))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f8,f21])).
% 0.10/0.39 fof(f302,plain,(
% 0.10/0.39 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,multiply(identity,X0))))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,identity)))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f17,f258])).
% 0.10/0.39 fof(f303,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(X0)=multiply(X1,double_divide(identity,double_divide(inverse(X0),double_divide(X1,identity)))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f26,f302])).
% 0.10/0.39 fof(f305,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(X0)=multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X1)))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f8,f303])).
% 0.10/0.39 fof(f306,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,double_divide(X0,X1))),identity))=X1)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f262,f15])).
% 0.10/0.39 fof(f307,plain,(
% 0.10/0.39 ![X0,X1,X2]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,X1)),identity))=multiply(X2,double_divide(identity,double_divide(inverse(X0),double_divide(X2,X1)))))),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f262,f21])).
% 0.10/0.39 fof(f345,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,inverse(X1))),identity))=multiply(X1,double_divide(identity,double_divide(inverse(X0),identity))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f262,f274])).
% 0.10/0.39 fof(f346,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,inverse(X1))),identity))=multiply(X1,double_divide(identity,inverse(inverse(X0)))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f8,f345])).
% 0.10/0.39 fof(f348,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,inverse(X1))),identity))=multiply(X1,double_divide(identity,multiply(identity,X0))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f17,f346])).
% 0.10/0.39 fof(f349,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,identity)),identity))=multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X1)))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f262,f275])).
% 0.10/0.39 fof(f350,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(inverse(X0),inverse(identity)),identity))=multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X1)))))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f8,f349])).
% 0.10/0.39 fof(f351,plain,(
% 0.10/0.39 ![X0]: (inverse(multiply(double_divide(inverse(X0),inverse(identity)),identity))=inverse(X0))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f305,f350])).
% 0.10/0.39 fof(f386,plain,(
% 0.10/0.39 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),multiply(X2,double_divide(identity,double_divide(multiply(X1,X0),X3))))=inverse(multiply(double_divide(inverse(X2),double_divide(identity,X3)),identity)))),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f307,f90])).
% 0.10/0.39 fof(f404,plain,(
% 0.10/0.39 ![X0]: (inverse(multiply(double_divide(inverse(X0),double_divide(identity,inverse(X0))),identity))=identity)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f386,f92])).
% 0.10/0.39 fof(f406,plain,(
% 0.10/0.39 ![X0]: (multiply(X0,double_divide(identity,multiply(identity,X0)))=identity)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f348,f404])).
% 0.10/0.39 fof(f407,plain,(
% 0.10/0.39 inverse(multiply(multiply(identity,identity),identity))=identity),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f28,f406])).
% 0.10/0.39 fof(f415,plain,(
% 0.10/0.39 multiply(identity,inverse(double_divide(identity,multiply(identity,identity))))=inverse(identity)),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f406,f27])).
% 0.10/0.39 fof(f425,plain,(
% 0.10/0.39 multiply(identity,multiply(multiply(identity,identity),identity))=inverse(identity)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f14,f415])).
% 0.10/0.39 fof(f460,plain,(
% 0.10/0.39 multiply(multiply(multiply(identity,identity),identity),double_divide(identity,inverse(identity)))=identity),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f425,f406])).
% 0.10/0.39 fof(f468,plain,(
% 0.10/0.39 multiply(multiply(multiply(identity,identity),identity),identity)=identity),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f9,f460])).
% 0.10/0.39 fof(f479,plain,(
% 0.10/0.39 ![X0]: (inverse(multiply(double_divide(identity,double_divide(identity,double_divide(multiply(multiply(identity,identity),identity),X0))),identity))=X0)),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f407,f306])).
% 0.10/0.39 fof(f541,plain,(
% 0.10/0.39 ![X0,X1]: (inverse(multiply(double_divide(X0,inverse(identity)),identity))=inverse(multiply(double_divide(inverse(X1),double_divide(identity,double_divide(X1,X0))),identity)))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f306,f351])).
% 0.10/0.39 fof(f557,plain,(
% 0.10/0.39 ![X0]: (inverse(multiply(double_divide(X0,inverse(identity)),identity))=X0)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f306,f541])).
% 0.10/0.39 fof(f567,plain,(
% 0.10/0.39 inverse(multiply(identity,identity))=identity),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f9,f557])).
% 0.10/0.39 fof(f576,plain,(
% 0.10/0.39 multiply(identity,inverse(identity))=identity),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f27,f567])).
% 0.10/0.39 fof(f589,plain,(
% 0.10/0.39 multiply(identity,multiply(identity,identity))=inverse(identity)),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f576,f70])).
% 0.10/0.39 fof(f620,plain,(
% 0.10/0.39 ![X0]: (double_divide(multiply(multiply(identity,identity),identity),multiply(X0,double_divide(identity,inverse(identity))))=inverse(X0))),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f425,f26])).
% 0.10/0.39 fof(f636,plain,(
% 0.10/0.39 ![X0]: (double_divide(multiply(multiply(identity,identity),identity),multiply(X0,identity))=inverse(X0))),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f9,f620])).
% 0.10/0.39 fof(f664,plain,(
% 0.10/0.39 multiply(multiply(identity,identity),double_divide(identity,inverse(identity)))=identity),
% 0.10/0.39 inference(paramodulation,[status(thm)],[f589,f406])).
% 0.10/0.39 fof(f673,plain,(
% 0.10/0.39 multiply(identity,identity)=identity),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f677,f468])).
% 0.10/0.39 fof(f674,plain,(
% 0.10/0.39 multiply(identity,identity)=inverse(identity)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f677,f425])).
% 0.10/0.39 fof(f675,plain,(
% 0.10/0.39 ![X0]: (double_divide(identity,multiply(X0,identity))=inverse(X0))),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f677,f636])).
% 0.10/0.39 fof(f676,plain,(
% 0.10/0.39 ![X0]: (inverse(multiply(double_divide(identity,double_divide(identity,double_divide(identity,X0))),identity))=X0)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f677,f479])).
% 0.10/0.39 fof(f677,plain,(
% 0.10/0.39 multiply(multiply(identity,identity),identity)=identity),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f9,f664])).
% 0.10/0.39 fof(f703,plain,(
% 0.10/0.39 ![X0]: (inverse(multiply(double_divide(X0,identity),identity))=X0)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f723,f557])).
% 0.10/0.40 fof(f723,plain,(
% 0.10/0.40 identity=inverse(identity)),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f673,f674])).
% 0.10/0.40 fof(f736,plain,(
% 0.10/0.40 ![X0]: (inverse(multiply(inverse(X0),identity))=X0)),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f8,f703])).
% 0.10/0.40 fof(f846,plain,(
% 0.10/0.40 ![X0]: (inverse(multiply(X0,identity))=multiply(inverse(X0),identity))),
% 0.10/0.40 inference(paramodulation,[status(thm)],[f736,f736])).
% 0.10/0.40 fof(f863,plain,(
% 0.10/0.40 ![X0]: (multiply(inverse(double_divide(identity,double_divide(identity,double_divide(identity,X0)))),identity)=X0)),
% 0.10/0.40 inference(backward_demodulation,[status(thm)],[f846,f676])).
% 0.10/0.40 fof(f905,plain,(
% 0.10/0.40 ![X0]: (multiply(multiply(double_divide(identity,double_divide(identity,X0)),identity),identity)=X0)),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f14,f863])).
% 0.10/0.40 fof(f956,plain,(
% 0.10/0.40 ![X0]: (multiply(multiply(X0,identity),identity)=inverse(inverse(X0)))),
% 0.10/0.40 inference(paramodulation,[status(thm)],[f675,f14])).
% 0.10/0.40 fof(f975,plain,(
% 0.10/0.40 ![X0]: (multiply(identity,double_divide(identity,double_divide(identity,X0)))=X0)),
% 0.10/0.40 inference(backward_demodulation,[status(thm)],[f978,f905])).
% 0.10/0.40 fof(f978,plain,(
% 0.10/0.40 ![X0]: (multiply(multiply(X0,identity),identity)=multiply(identity,X0))),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f17,f956])).
% 0.10/0.40 fof(f983,plain,(
% 0.10/0.40 ![X0]: (inverse(multiply(double_divide(identity,X0),identity))=X0)),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f28,f975])).
% 0.10/0.40 fof(f984,plain,(
% 0.10/0.40 ![X0]: (multiply(inverse(double_divide(identity,X0)),identity)=X0)),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f846,f983])).
% 0.10/0.40 fof(f985,plain,(
% 0.10/0.40 ![X0]: (X0=multiply(identity,X0))),
% 0.10/0.40 inference(backward_demodulation,[status(thm)],[f986,f978])).
% 0.10/0.40 fof(f986,plain,(
% 0.10/0.40 ![X0]: (multiply(multiply(X0,identity),identity)=X0)),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f14,f984])).
% 0.10/0.40 fof(f991,plain,(
% 0.10/0.40 sF0_fnc=a2),
% 0.10/0.40 inference(backward_demodulation,[status(thm)],[f985,f11])).
% 0.10/0.40 fof(f1030,plain,(
% 0.10/0.40 $false),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f991,f12])).
% 0.10/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.41 % Elapsed time: 0.040482 seconds
% 0.10/0.41 % CPU time: 0.192002 seconds
% 0.10/0.41 % Total memory used: 9.800 MB
% 0.10/0.41 % Net memory used: 9.338 MB
%------------------------------------------------------------------------------