%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW285+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 03:08:54 PM UTC 2026
% Result : Theorem 10.46s 1.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW285+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n002.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 09:47:47 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.21/0.46 % Drodi V4.1.1
% 10.46/1.88 % Refutation found
% 10.46/1.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.46/1.88 % SZS output start CNFRefutation for theBenchmark
% 10.46/1.88 fof(f2,axiom,(
% 10.46/1.88 v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f11,axiom,(
% 10.46/1.88 (! [V_x,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x) = c_Groups_Ozero__class_Ozero(T_a) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f67,axiom,(
% 10.46/1.88 (! [T_a] :( class_Groups_Ozero(T_a)=> c_Polynomial_Odegree(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f75,axiom,(
% 10.46/1.88 (! [V_q,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(T_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_q) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f95,axiom,(
% 10.46/1.88 ~ (! [B_r] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),B_r) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f230,axiom,(
% 10.46/1.88 (! [V_x,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> hAPP(c_Polynomial_Opoly(T_a,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(T_a))),V_x) = c_Groups_Oone__class_Oone(T_a) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f235,axiom,(
% 10.46/1.88 (! [T_a] :( class_Rings_Ozero__neq__one(T_a)=> c_Groups_Ozero__class_Ozero(T_a) != c_Groups_Oone__class_Oone(T_a) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f278,axiom,(
% 10.46/1.88 (! [V_x,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(T_a) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f1101,axiom,(
% 10.46/1.88 class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f1102,axiom,(
% 10.46/1.88 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f1107,axiom,(
% 10.46/1.88 class_Rings_Ozero__neq__one(tc_Complex_Ocomplex) ),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f1120,axiom,(
% 10.46/1.88 class_Groups_Ozero(tc_Complex_Ocomplex) ),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f1151,axiom,(
% 10.46/1.88 (! [T_1] :( class_Rings_Ocomm__semiring__1(T_1)=> class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(T_1)) ) )),
% 10.46/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.46/1.88 fof(f1185,plain,(
% 10.46/1.88 v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f2])).
% 10.46/1.88 fof(f1221,plain,(
% 10.46/1.88 ![V_x,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x)=c_Groups_Ozero__class_Ozero(T_a))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 10.46/1.88 fof(f1222,plain,(
% 10.46/1.88 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x]: hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x)=c_Groups_Ozero__class_Ozero(T_a)))),
% 10.46/1.88 inference(miniscoping,[status(thm)],[f1221])).
% 10.46/1.88 fof(f1223,plain,(
% 10.46/1.88 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X1)=c_Groups_Ozero__class_Ozero(X0))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1222])).
% 10.46/1.88 fof(f1422,plain,(
% 10.46/1.88 ![T_a]: (~class_Groups_Ozero(T_a)|c_Polynomial_Odegree(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 10.46/1.88 fof(f1423,plain,(
% 10.46/1.88 ![X0]: (~class_Groups_Ozero(X0)|c_Polynomial_Odegree(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1422])).
% 10.46/1.88 fof(f1445,plain,(
% 10.46/1.88 ![V_q,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(T_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_q)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 10.46/1.88 fof(f1446,plain,(
% 10.46/1.88 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_q]: hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(T_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_q)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 10.46/1.88 inference(miniscoping,[status(thm)],[f1445])).
% 10.46/1.88 fof(f1447,plain,(
% 10.46/1.88 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X0)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1446])).
% 10.46/1.88 fof(f1510,plain,(
% 10.46/1.88 (?[B_r]: hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),B_r))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 10.46/1.88 fof(f1511,plain,(
% 10.46/1.88 hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),sK6_skl)),
% 10.46/1.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B_r,sK6_skl)],[f1510])).
% 10.46/1.88 fof(f1512,plain,(
% 10.46/1.88 hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),sK6_skl)),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1511])).
% 10.46/1.88 fof(f1935,plain,(
% 10.46/1.88 ![V_x,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|hAPP(c_Polynomial_Opoly(T_a,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(T_a))),V_x)=c_Groups_Oone__class_Oone(T_a))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f230])).
% 10.46/1.88 fof(f1936,plain,(
% 10.46/1.88 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_x]: hAPP(c_Polynomial_Opoly(T_a,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(T_a))),V_x)=c_Groups_Oone__class_Oone(T_a)))),
% 10.46/1.88 inference(miniscoping,[status(thm)],[f1935])).
% 10.46/1.88 fof(f1937,plain,(
% 10.46/1.88 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|hAPP(c_Polynomial_Opoly(X0,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X0))),X1)=c_Groups_Oone__class_Oone(X0))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1936])).
% 10.46/1.88 fof(f1947,plain,(
% 10.46/1.88 ![T_a]: (~class_Rings_Ozero__neq__one(T_a)|~c_Groups_Ozero__class_Ozero(T_a)=c_Groups_Oone__class_Oone(T_a))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f235])).
% 10.46/1.88 fof(f1948,plain,(
% 10.46/1.88 ![X0]: (~class_Rings_Ozero__neq__one(X0)|~c_Groups_Ozero__class_Ozero(X0)=c_Groups_Oone__class_Oone(X0))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1947])).
% 10.46/1.88 fof(f2071,plain,(
% 10.46/1.88 ![V_x,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Groups_Oone__class_Oone(T_a))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f278])).
% 10.46/1.88 fof(f2072,plain,(
% 10.46/1.88 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_x]: hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_x),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Groups_Oone__class_Oone(T_a)))),
% 10.46/1.88 inference(miniscoping,[status(thm)],[f2071])).
% 10.46/1.88 fof(f2073,plain,(
% 10.46/1.88 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Groups_Oone__class_Oone(X0))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f2072])).
% 10.46/1.88 fof(f4516,plain,(
% 10.46/1.88 class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1101])).
% 10.46/1.88 fof(f4517,plain,(
% 10.46/1.88 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1102])).
% 10.46/1.88 fof(f4522,plain,(
% 10.46/1.88 class_Rings_Ozero__neq__one(tc_Complex_Ocomplex)),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1107])).
% 10.46/1.88 fof(f4535,plain,(
% 10.46/1.88 class_Groups_Ozero(tc_Complex_Ocomplex)),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f1120])).
% 10.46/1.88 fof(f4592,plain,(
% 10.46/1.88 ![T_1]: (~class_Rings_Ocomm__semiring__1(T_1)|class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(T_1)))),
% 10.46/1.88 inference(pre_NNF_transformation,[status(thm)],[f1151])).
% 10.46/1.88 fof(f4593,plain,(
% 10.46/1.88 ![X0]: (~class_Rings_Ocomm__semiring__1(X0)|class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(X0)))),
% 10.46/1.88 inference(cnf_transformation,[status(thm)],[f4592])).
% 10.46/1.88 fof(f5222,plain,(
% 10.46/1.88 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 10.46/1.88 inference(resolution,[status(thm)],[f4517,f1447])).
% 10.46/1.88 fof(f5242,plain,(
% 10.46/1.88 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 10.46/1.88 inference(resolution,[status(thm)],[f4517,f1223])).
% 10.46/1.88 fof(f5250,plain,(
% 10.46/1.88 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f1185,f5222])).
% 10.46/1.88 fof(f5251,plain,(
% 10.46/1.88 hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))=v_p),
% 10.46/1.88 inference(backward_demodulation,[status(thm)],[f5255,f1512])).
% 10.46/1.88 fof(f5255,plain,(
% 10.46/1.88 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),X0)=v_p)),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f1185,f5250])).
% 10.46/1.88 fof(f5270,plain,(
% 10.46/1.88 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f1185,f5242])).
% 10.46/1.88 fof(f5503,plain,(
% 10.46/1.88 c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 10.46/1.88 inference(resolution,[status(thm)],[f4535,f1423])).
% 10.46/1.88 fof(f5529,plain,(
% 10.46/1.88 c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f1185,f5503])).
% 10.46/1.88 fof(f6568,plain,(
% 10.46/1.88 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex))),
% 10.46/1.88 inference(resolution,[status(thm)],[f1937,f4516])).
% 10.46/1.88 fof(f6650,plain,(
% 10.46/1.88 ~c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),
% 10.46/1.88 inference(resolution,[status(thm)],[f1948,f4522])).
% 10.46/1.88 fof(f7045,plain,(
% 10.46/1.88 class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 10.46/1.88 inference(resolution,[status(thm)],[f4593,f4516])).
% 10.46/1.88 fof(f7457,plain,(
% 10.46/1.88 ![X0]: (hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 10.46/1.88 inference(resolution,[status(thm)],[f2073,f7045])).
% 10.46/1.88 fof(f7491,plain,(
% 10.46/1.88 hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=v_p),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f5529,f5251])).
% 10.46/1.88 fof(f7492,plain,(
% 10.46/1.88 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex))),
% 10.46/1.88 inference(backward_demodulation,[status(thm)],[f7509,f6568])).
% 10.46/1.88 fof(f7509,plain,(
% 10.46/1.88 c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex))=v_p),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f7457,f7491])).
% 10.46/1.88 fof(f7511,plain,(
% 10.46/1.88 c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),
% 10.46/1.88 inference(forward_demodulation,[status(thm)],[f5270,f7492])).
% 7.14/1.92 fof(f7512,plain,(
% 7.14/1.92 $false),
% 7.14/1.92 inference(forward_subsumption_resolution,[status(thm)],[f7511,f6650])).
% 7.14/1.92 % SZS output end CNFRefutation for theBenchmark.p
% 7.14/1.93 % Elapsed time: 1.559547 seconds
% 7.14/1.93 % CPU time: 11.473034 seconds
% 7.14/1.93 % Total memory used: 360.139 MB
% 7.14/1.93 % Net memory used: 350.499 MB
%------------------------------------------------------------------------------