%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP410-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:35 PM UTC 2026
% Result : Unsatisfiable 3.69s 0.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP410-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n007.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 : Sun Sep 20 20:10:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 3.69/0.95 % Refutation found
% 3.69/0.95 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.69/0.95 % SZS output start CNFRefutation for theBenchmark
% 3.69/0.95 fof(f1,axiom,(
% 3.69/0.95 (![A,B,C]: (multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(inverse(C),C))) = B ))),
% 3.69/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.69/0.95 fof(f2,negated_conjecture,(
% 3.69/0.95 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 3.69/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.69/0.95 fof(f3,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2)))=X1)),
% 3.69/0.95 inference(cnf_transformation,[status(thm)],[f1])).
% 3.69/0.95 fof(f4,plain,(
% 3.69/0.95 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 3.69/0.95 inference(cnf_transformation,[status(thm)],[f2])).
% 3.69/0.95 fof(f5,definition,(
% 3.69/0.95 sF2_fnc=inverse(b2)),
% 3.69/0.95 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 3.69/0.95 fof(f6,definition,(
% 3.69/0.95 sF1_fnc=multiply(sF2_fnc,b2)),
% 3.69/0.95 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.69/0.95 fof(f7,definition,(
% 3.69/0.95 sF0_fnc=multiply(sF1_fnc,a2)),
% 3.69/0.95 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.69/0.95 fof(f8,plain,(
% 3.69/0.95 ~sF0_fnc=a2),
% 3.69/0.95 inference(definition_folding,[],[f4,f7,f6,f5])).
% 3.69/0.95 fof(f10,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3,f3])).
% 3.69/0.95 fof(f13,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(X3,multiply(inverse(X2),X2))))),X1),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))=X3)),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3,f3])).
% 3.69/0.95 fof(f14,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF2_fnc)),inverse(multiply(inverse(b2),b2)))=X1)),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f5,f3])).
% 3.69/0.95 fof(f19,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF2_fnc)),inverse(multiply(sF2_fnc,b2)))=X1)),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f5,f14])).
% 3.69/0.95 fof(f20,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF2_fnc)),inverse(sF1_fnc))=X1)),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f6,f19])).
% 3.69/0.95 fof(f104,plain,(
% 3.69/0.95 ![X0,X1,X2]: (X0=multiply(inverse(multiply(X1,inverse(multiply(multiply(X0,inverse(multiply(inverse(X2),X2))),X2)))),multiply(X1,inverse(X2))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3,f10])).
% 3.69/0.95 fof(f191,plain,(
% 3.69/0.95 ![X0,X1]: (X0=multiply(inverse(multiply(X1,inverse(multiply(multiply(X0,inverse(multiply(sF2_fnc,b2))),b2)))),multiply(X1,inverse(b2))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f5,f104])).
% 3.69/0.95 fof(f195,plain,(
% 3.69/0.95 ![X0,X1,X2]: (X0=multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,b2)))),multiply(X1,sF2_fnc)),inverse(multiply(multiply(X0,inverse(multiply(inverse(sF1_fnc),sF1_fnc))),sF1_fnc)))),X2))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f20,f104])).
% 3.69/0.95 fof(f210,plain,(
% 3.69/0.95 ![X0,X1]: (X0=multiply(inverse(multiply(X1,inverse(multiply(multiply(X0,inverse(sF1_fnc)),b2)))),multiply(X1,inverse(b2))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f6,f191])).
% 3.69/0.95 fof(f211,plain,(
% 3.69/0.95 ![X0,X1]: (X0=multiply(inverse(multiply(X1,inverse(multiply(multiply(X0,inverse(sF1_fnc)),b2)))),multiply(X1,sF2_fnc)))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f5,f210])).
% 3.69/0.95 fof(f216,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X2,inverse(multiply(X1,b2)))),multiply(X2,sF2_fnc)))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f20,f211])).
% 3.69/0.95 fof(f1802,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(b2,b2)))),multiply(X1,sF2_fnc)),inverse(multiply(multiply(X2,inverse(multiply(inverse(sF1_fnc),sF1_fnc))),sF1_fnc)))),b2)))),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,sF2_fnc)))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f195,f216])).
% 3.69/0.95 fof(f1934,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,sF2_fnc)))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f195,f1802])).
% 3.69/0.95 fof(f1992,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X1,inverse(b2))),multiply(X1,sF2_fnc)))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f5,f1934])).
% 3.69/0.95 fof(f2090,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc)))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f5,f1992])).
% 3.69/0.95 fof(f2096,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,b2)))),multiply(X1,sF2_fnc)),inverse(multiply(multiply(X0,inverse(multiply(inverse(sF1_fnc),sF1_fnc))),sF1_fnc)))),sF2_fnc))=multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc)))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f195,f2090])).
% 3.69/0.95 fof(f2166,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(inverse(X0),X0)=multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc)))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f195,f2096])).
% 3.69/0.95 fof(f2231,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(inverse(X0),X0)=multiply(inverse(X1),X1))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f2166,f2166])).
% 3.69/0.95 fof(f2348,plain,(
% 3.69/0.95 ![X0]: (multiply(sF2_fnc,b2)=multiply(inverse(X0),X0))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f5,f2231])).
% 3.69/0.95 fof(f2634,plain,(
% 3.69/0.95 ![X0]: (sF1_fnc=multiply(inverse(X0),X0))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f6,f2348])).
% 3.69/0.95 fof(f2661,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(X3,multiply(inverse(X2),X2))))),X1),inverse(sF1_fnc))=X3)),
% 3.69/0.95 inference(backward_demodulation,[status(thm)],[f2634,f13])).
% 3.69/0.95 fof(f2668,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(sF1_fnc))=X1)),
% 3.69/0.95 inference(backward_demodulation,[status(thm)],[f2634,f3])).
% 3.69/0.95 fof(f2718,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(X3,sF1_fnc)))),X1),inverse(sF1_fnc))=X3)),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f2634,f2661])).
% 3.69/0.95 fof(f2746,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc)))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f2668,f2668])).
% 3.69/0.95 fof(f3056,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(sF1_fnc))),X1),inverse(sF1_fnc))=inverse(sF1_fnc))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f2634,f2718])).
% 3.69/0.95 fof(f3076,plain,(
% 3.69/0.95 ![X0]: (multiply(multiply(inverse(X0),X0),inverse(sF1_fnc))=inverse(sF1_fnc))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f2668,f3056])).
% 3.69/0.95 fof(f3077,plain,(
% 3.69/0.95 multiply(sF1_fnc,inverse(sF1_fnc))=inverse(sF1_fnc)),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f2634,f3076])).
% 3.69/0.95 fof(f3092,plain,(
% 3.69/0.95 ![X0]: (multiply(multiply(inverse(multiply(X0,inverse(inverse(sF1_fnc)))),multiply(X0,inverse(inverse(sF1_fnc)))),inverse(sF1_fnc))=sF1_fnc)),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3077,f2668])).
% 3.69/0.95 fof(f3095,plain,(
% 3.69/0.95 multiply(sF1_fnc,inverse(sF1_fnc))=sF1_fnc),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f2634,f3092])).
% 3.69/0.95 fof(f3096,plain,(
% 3.69/0.95 sF1_fnc=inverse(sF1_fnc)),
% 3.69/0.95 inference(backward_demodulation,[status(thm)],[f3095,f3077])).
% 3.69/0.95 fof(f3112,plain,(
% 3.69/0.95 multiply(sF1_fnc,sF1_fnc)=sF1_fnc),
% 3.69/0.95 inference(backward_demodulation,[status(thm)],[f3096,f3095])).
% 3.69/0.95 fof(f3124,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),sF1_fnc)=X1)),
% 3.69/0.95 inference(backward_demodulation,[status(thm)],[f3096,f2668])).
% 3.69/0.95 fof(f3167,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,inverse(X1))),sF1_fnc)=inverse(X1))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f2634,f3124])).
% 3.69/0.95 fof(f3177,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(X1))),sF1_fnc)=inverse(X1))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3096,f3167])).
% 3.69/0.95 fof(f3331,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(sF1_fnc))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3096,f2746])).
% 3.69/0.95 fof(f3332,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF1_fnc)),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3096,f3331])).
% 3.69/0.95 fof(f3333,plain,(
% 3.69/0.95 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF1_fnc)),sF1_fnc)=multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3096,f3332])).
% 3.69/0.95 fof(f3338,plain,(
% 3.69/0.95 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,sF1_fnc)),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(sF1_fnc,X2)))),multiply(X1,inverse(X2))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3096,f3333])).
% 3.69/0.95 fof(f3379,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF1_fnc)),sF1_fnc),sF1_fnc)=X1)),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3333,f3124])).
% 3.69/0.95 fof(f3385,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(sF1_fnc,sF1_fnc)=multiply(inverse(multiply(X0,inverse(multiply(sF1_fnc,X1)))),multiply(X0,inverse(X1))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f2634,f3338])).
% 3.69/0.95 fof(f3386,plain,(
% 3.69/0.95 ![X0,X1]: (sF1_fnc=multiply(inverse(multiply(X0,inverse(multiply(sF1_fnc,X1)))),multiply(X0,inverse(X1))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3112,f3385])).
% 3.69/0.95 fof(f3545,plain,(
% 3.69/0.95 ![X0]: (multiply(multiply(inverse(multiply(inverse(inverse(X0)),sF1_fnc)),sF1_fnc),sF1_fnc)=inverse(X0))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f2634,f3177])).
% 3.69/0.95 fof(f3756,plain,(
% 3.69/0.95 ![X0]: (sF1_fnc=multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(sF1_fnc,X0))),inverse(X0))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f2634,f3386])).
% 3.69/0.95 fof(f3781,plain,(
% 3.69/0.95 ![X0]: (sF1_fnc=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,X0))),inverse(X0))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3096,f3756])).
% 3.69/0.95 fof(f3818,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,inverse(multiply(inverse(inverse(multiply(sF1_fnc,X1))),inverse(X1))))),sF1_fnc)=sF1_fnc)),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3781,f3124])).
% 3.69/0.95 fof(f3851,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(multiply(inverse(inverse(multiply(sF1_fnc,X1))),inverse(X1))))),sF1_fnc)=sF1_fnc)),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3096,f3818])).
% 3.69/0.95 fof(f3852,plain,(
% 3.69/0.95 ![X0]: (inverse(multiply(inverse(inverse(multiply(sF1_fnc,X0))),inverse(X0)))=sF1_fnc)),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3177,f3851])).
% 3.69/0.95 fof(f3879,plain,(
% 3.69/0.95 ![X0,X1]: (multiply(multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(inverse(X1)))),sF1_fnc)=inverse(inverse(multiply(sF1_fnc,X1))))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f3852,f3124])).
% 3.69/0.95 fof(f3924,plain,(
% 3.69/0.95 ![X0]: (inverse(inverse(X0))=inverse(inverse(multiply(sF1_fnc,X0))))),
% 3.69/0.95 inference(forward_demodulation,[status(thm)],[f3177,f3879])).
% 3.69/0.95 fof(f3955,plain,(
% 3.69/0.95 inverse(inverse(a2))=inverse(inverse(sF0_fnc))),
% 3.69/0.95 inference(paramodulation,[status(thm)],[f7,f3924])).
% 3.69/0.97 fof(f3994,plain,(
% 3.69/0.97 multiply(multiply(inverse(multiply(inverse(inverse(a2)),sF1_fnc)),sF1_fnc),sF1_fnc)=inverse(sF0_fnc)),
% 3.69/0.97 inference(paramodulation,[status(thm)],[f3955,f3545])).
% 3.69/0.97 fof(f4010,plain,(
% 3.69/0.97 inverse(a2)=inverse(sF0_fnc)),
% 3.69/0.97 inference(forward_demodulation,[status(thm)],[f3545,f3994])).
% 3.69/0.97 fof(f5422,plain,(
% 3.69/0.97 ![X0]: (multiply(multiply(multiply(inverse(multiply(X0,inverse(a2))),multiply(X0,sF1_fnc)),sF1_fnc),sF1_fnc)=sF0_fnc)),
% 3.69/0.97 inference(paramodulation,[status(thm)],[f4010,f3379])).
% 3.69/0.97 fof(f5470,plain,(
% 3.69/0.97 a2=sF0_fnc),
% 3.69/0.97 inference(forward_demodulation,[status(thm)],[f3379,f5422])).
% 3.69/0.97 fof(f5471,plain,(
% 3.69/0.97 $false),
% 3.69/0.97 inference(forward_subsumption_resolution,[status(thm)],[f5470,f8])).
% 3.69/0.97 % SZS output end CNFRefutation for theBenchmark.p
% 3.69/1.01 % Elapsed time: 0.628351 seconds
% 3.69/1.01 % CPU time: 4.435333 seconds
% 3.69/1.01 % Total memory used: 198.440 MB
% 3.69/1.01 % Net memory used: 196.854 MB
%------------------------------------------------------------------------------