%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV858-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 02:53:16 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV858-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n003.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 09:30:35 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.14/5.40 % Drodi V4.1.1
% 0.14/5.48 % Refutation found
% 0.14/5.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.48 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.48 fof(f525,axiom,(
% 0.14/5.48 (![V_Q,V_x,V_P,T_a]: (( hBOOL(hAPP(V_Q,V_x))| ~ c_lessequals(V_P,V_Q,tc_fun(T_a,tc_bool))| ~ hBOOL(hAPP(V_P,V_x)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f531,axiom,(
% 0.14/5.48 (![V_A,T_a]: (c_lessequals(V_A,V_A,tc_fun(T_a,tc_bool)) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f532,axiom,(
% 0.14/5.48 (![T_a,V_t,V_B,V_A]: (( hBOOL(hAPP(hAPP(c_in(T_a),V_t),V_B))| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_t),V_A))| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f545,axiom,(
% 0.14/5.48 (![T_a,V_x,V_S]: (( hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f546,axiom,(
% 0.14/5.48 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f547,axiom,(
% 0.14/5.48 (![V_G,V_ts,T_a]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)| ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f550,negated_conjecture,(
% 0.14/5.48 c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) ),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f551,negated_conjecture,(
% 0.14/5.48 hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)) ),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f552,negated_conjecture,(
% 0.14/5.48 ~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a) ),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f553,negated_conjecture,(
% 0.14/5.48 (![V_xb]: (( c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a)| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f554,negated_conjecture,(
% 0.14/5.48 (![V_na,V_nb]: (( c_Hoare__Mirabelle_Otriple__valid(V_na,V_nb,t_a)| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nb),v_ts_H))| hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_Ga)) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f555,negated_conjecture,(
% 0.14/5.48 (![V_na,V_nc]: (( c_Hoare__Mirabelle_Otriple__valid(V_na,V_nc,t_a)| ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nc),v_ts_H))| ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a) ) ))),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f573,axiom,(
% 0.14/5.48 class_Orderings_Olinorder(tc_nat) ),
% 0.14/5.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.48 fof(f1387,plain,(
% 0.14/5.48 ![V_x,V_P]: ((![V_Q]: (hBOOL(hAPP(V_Q,V_x))|(![T_a]: ~c_lessequals(V_P,V_Q,tc_fun(T_a,tc_bool)))))|~hBOOL(hAPP(V_P,V_x)))),
% 0.14/5.48 inference(miniscoping,[status(thm)],[f525])).
% 0.14/5.48 fof(f1388,plain,(
% 0.14/5.48 ![X0,X1,X2,X3]: (hBOOL(hAPP(X0,X1))|~c_lessequals(X2,X0,tc_fun(X3,tc_bool))|~hBOOL(hAPP(X2,X1)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f1387])).
% 0.14/5.48 fof(f1399,plain,(
% 0.14/5.48 ![X0,X1]: (c_lessequals(X0,X0,tc_fun(X1,tc_bool)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f531])).
% 0.14/5.48 fof(f1400,plain,(
% 0.14/5.48 ![T_a,V_B,V_A]: ((![V_t]: (hBOOL(hAPP(hAPP(c_in(T_a),V_t),V_B))|~hBOOL(hAPP(hAPP(c_in(T_a),V_t),V_A))))|~c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)))),
% 0.14/5.48 inference(miniscoping,[status(thm)],[f532])).
% 0.14/5.48 fof(f1401,plain,(
% 0.14/5.48 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_in(X0),X1),X2))|~hBOOL(hAPP(hAPP(c_in(X0),X1),X3))|~c_lessequals(X3,X2,tc_fun(X0,tc_bool)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f1400])).
% 0.14/5.48 fof(f1420,plain,(
% 0.14/5.48 ![V_x,V_S]: ((![T_a]: hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)))|~hBOOL(hAPP(V_S,V_x)))),
% 0.14/5.48 inference(miniscoping,[status(thm)],[f545])).
% 0.14/5.48 fof(f1421,plain,(
% 0.14/5.48 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_in(X0),X1),X2))|~hBOOL(hAPP(X2,X1)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f1420])).
% 0.14/5.48 fof(f1422,plain,(
% 0.14/5.48 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))))),
% 0.14/5.48 inference(miniscoping,[status(thm)],[f546])).
% 0.14/5.48 fof(f1423,plain,(
% 0.14/5.48 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(hAPP(hAPP(c_in(X2),X1),X0)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f1422])).
% 0.14/5.48 fof(f1424,plain,(
% 0.14/5.48 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2)|~c_lessequals(X1,X0,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f547])).
% 0.14/5.48 fof(f1428,plain,(
% 0.14/5.48 c_lessequals(v_tsa,v_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f550])).
% 0.14/5.48 fof(f1429,plain,(
% 0.14/5.48 hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f551])).
% 0.14/5.48 fof(f1430,plain,(
% 0.14/5.48 ~c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a)),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f552])).
% 0.14/5.48 fof(f1431,plain,(
% 0.14/5.48 ![X0]: (c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_Ga)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f553])).
% 0.14/5.48 fof(f1432,plain,(
% 0.14/5.48 ![V_na]: ((![V_nb]: (c_Hoare__Mirabelle_Otriple__valid(V_na,V_nb,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nb),v_ts_H))))|hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_Ga)))),
% 0.14/5.48 inference(miniscoping,[status(thm)],[f554])).
% 0.14/5.48 fof(f1433,plain,(
% 0.14/5.48 ![X0,X1]: (c_Hoare__Mirabelle_Otriple__valid(X0,X1,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H))|hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X0)),v_Ga)))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f1432])).
% 0.14/5.48 fof(f1434,plain,(
% 0.14/5.48 ![V_na]: ((![V_nc]: (c_Hoare__Mirabelle_Otriple__valid(V_na,V_nc,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_nc),v_ts_H))))|~c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a))),
% 0.14/5.48 inference(miniscoping,[status(thm)],[f555])).
% 0.14/5.48 fof(f1435,plain,(
% 0.14/5.48 ![X0,X1]: (c_Hoare__Mirabelle_Otriple__valid(X0,X1,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_ts_H))|~c_Hoare__Mirabelle_Otriple__valid(X0,v_n(X0),t_a))),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f1434])).
% 0.14/5.48 fof(f1466,plain,(
% 0.14/5.48 class_Orderings_Olinorder(tc_nat)),
% 0.14/5.48 inference(cnf_transformation,[status(thm)],[f573])).
% 0.14/5.48 fof(f1490,plain,(
% 0.14/5.48 ![X0,X1]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,X0,X1))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1424,f1399])).
% 0.14/5.48 fof(f1496,plain,(
% 0.14/5.48 hBOOL(hAPP(v_tsa,v_xa))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1423,f1429])).
% 0.14/5.48 fof(f1497,plain,(
% 0.14/5.48 ![X0]: (hBOOL(hAPP(hAPP(c_in(X0),v_xa),v_tsa)))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1496,f1421])).
% 0.14/5.48 fof(f1552,definition,(
% 0.14/5.48 sQ4_spl <=> (c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a))),
% 0.14/5.48 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.48 fof(f1553,plain,(
% 0.14/5.48 c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a)|~sQ4_spl),
% 0.14/5.48 inference(component_clause,[status(thm)],[f1552])).
% 0.14/5.48 fof(f1555,definition,(
% 0.14/5.48 ![X0]: (sQ5_spl <=> (c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_tsa))))),
% 0.14/5.48 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.48 fof(f1556,plain,(
% 0.14/5.48 ![X0]: (c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_tsa))|~sQ5_spl)),
% 0.14/5.48 inference(component_clause,[status(thm)],[f1555])).
% 0.14/5.48 fof(f1561,plain,(
% 0.14/5.48 ![X0]: (hBOOL(hAPP(v_ts_H,X0))|~hBOOL(hAPP(v_tsa,X0)))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1428,f1388])).
% 0.14/5.48 fof(f1566,plain,(
% 0.14/5.48 ![X0]: (hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_ts_H))|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_tsa)))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1401,f1428])).
% 0.14/5.48 fof(f1592,plain,(
% 0.14/5.48 ![X0,X1]: (~hBOOL(hAPP(v_tsa,X0))|hBOOL(hAPP(hAPP(c_in(X1),X0),v_ts_H)))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1561,f1421])).
% 0.14/5.48 fof(f1593,plain,(
% 0.14/5.48 ![X0]: (hBOOL(hAPP(hAPP(c_in(X0),v_xa),v_ts_H)))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1592,f1496])).
% 0.14/5.48 fof(f1596,plain,(
% 0.14/5.48 ![X0]: (c_Hoare__Mirabelle_Otriple__valid(X0,v_xa,t_a)|hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X0)),v_Ga)))),
% 0.14/5.48 inference(resolution,[status(thm)],[f1593,f1433])).
% 0.14/5.49 fof(f1681,plain,(
% 0.14/5.49 c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a)|~sQ5_spl),
% 0.14/5.49 inference(resolution,[status(thm)],[f1556,f1497])).
% 0.14/5.49 fof(f1684,plain,(
% 0.14/5.49 $false|~sQ5_spl),
% 0.14/5.49 inference(forward_subsumption_resolution,[status(thm)],[f1681,f1430])).
% 0.14/5.49 fof(f1685,plain,(
% 0.14/5.49 ~sQ5_spl),
% 0.14/5.49 inference(contradiction_clause,[status(thm)],[f1684])).
% 0.14/5.49 fof(f1686,plain,(
% 0.14/5.49 $false|~sQ4_spl),
% 0.14/5.49 inference(forward_subsumption_resolution,[status(thm)],[f1553,f1430])).
% 0.14/5.49 fof(f1687,plain,(
% 0.14/5.49 ~sQ4_spl),
% 0.14/5.49 inference(contradiction_clause,[status(thm)],[f1686])).
% 0.14/5.49 fof(f1869,definition,(
% 0.14/5.49 sQ20_spl <=> (c_Hoare__Mirabelle_Ohoare__derivs(v_tsa,v_tsa,t_a))),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f1871,plain,(
% 0.14/5.49 ~c_Hoare__Mirabelle_Ohoare__derivs(v_tsa,v_tsa,t_a)|sQ20_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f1869])).
% 0.14/5.49 fof(f1876,plain,(
% 0.14/5.49 $false|sQ20_spl),
% 0.14/5.49 inference(forward_subsumption_resolution,[status(thm)],[f1871,f1490])).
% 0.14/5.49 fof(f1877,plain,(
% 0.14/5.49 sQ20_spl),
% 0.14/5.49 inference(contradiction_clause,[status(thm)],[f1876])).
% 0.14/5.49 fof(f1929,definition,(
% 0.14/5.49 ![X0]: (sQ23_spl <=> (~class_Orderings_Olinorder(X0)))),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f1930,plain,(
% 0.14/5.49 ![X0]: (~class_Orderings_Olinorder(X0)|~sQ23_spl)),
% 0.14/5.49 inference(component_clause,[status(thm)],[f1929])).
% 0.14/5.49 fof(f1986,plain,(
% 0.14/5.49 $false|~sQ23_spl),
% 0.14/5.49 inference(backward_subsumption_resolution,[status(thm)],[f1466,f1930])).
% 0.14/5.49 fof(f1987,plain,(
% 0.14/5.49 ~sQ23_spl),
% 0.14/5.49 inference(contradiction_clause,[status(thm)],[f1986])).
% 0.14/5.49 fof(f2026,definition,(
% 0.14/5.49 sQ29_spl <=> (hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_x)),v_Ga)))),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f2027,plain,(
% 0.14/5.49 hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_x)),v_Ga))|~sQ29_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f2026])).
% 0.14/5.49 fof(f2028,plain,(
% 0.14/5.49 ~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(v_x)),v_Ga))|sQ29_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f2026])).
% 0.14/5.49 fof(f2037,plain,(
% 0.14/5.49 c_Hoare__Mirabelle_Otriple__valid(v_x,v_n(v_x),t_a)|~sQ29_spl),
% 0.14/5.49 inference(resolution,[status(thm)],[f2027,f1431])).
% 0.14/5.49 fof(f2041,plain,(
% 0.14/5.49 ![X0]: (c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_ts_H))|~sQ29_spl)),
% 0.14/5.49 inference(resolution,[status(thm)],[f2037,f1435])).
% 0.14/5.49 fof(f2164,plain,(
% 0.14/5.49 ![X0]: (c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a)|~hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_tsa))|~sQ29_spl)),
% 0.14/5.49 inference(resolution,[status(thm)],[f2041,f1566])).
% 0.14/5.49 fof(f2170,plain,(
% 0.14/5.49 sQ5_spl|~sQ29_spl),
% 0.14/5.49 inference(split_clause,[status(thm)],[f2164,f1555,f2026])).
% 0.14/5.49 fof(f2465,plain,(
% 0.14/5.49 c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a)|sQ29_spl),
% 0.14/5.49 inference(resolution,[status(thm)],[f1596,f2028])).
% 0.14/5.49 fof(f2470,plain,(
% 0.14/5.49 sQ4_spl|sQ29_spl),
% 0.14/5.49 inference(split_clause,[status(thm)],[f2465,f1552,f2026])).
% 0.14/5.49 fof(f2471,plain,(
% 0.14/5.49 $false),
% 0.14/5.49 inference(sat_refutation,[status(thm)],[f1685,f1687,f1877,f1987,f2170,f2470])).
% 0.14/5.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.50 % Elapsed time: 0.119437 seconds
% 0.14/5.50 % CPU time: 0.650294 seconds
% 0.14/5.50 % Total memory used: 142.621 MB
% 0.14/5.50 % Net memory used: 141.782 MB
%------------------------------------------------------------------------------