Some times reduced in a second benchmark.

diff --git a/components/binaries/utilities/benchmarks/log20060411_cregut_timestamp_bacato_misurazione_significativa b/components/binaries/utilities/benchmarks/log20060411_cregut_timestamp_bacato_misurazione_significativa
index 6cebe2e1fd37d0ea63e93f1bce3830dcf994ffe3..399fb5f51f0dd6d3029829444640dfd7308ff02a 100644 (file)
--- a/components/binaries/utilities/benchmarks/log20060411_cregut_timestamp_bacato_misurazione_significativa
+++ b/components/binaries/utilities/benchmarks/log20060411_cregut_timestamp_bacato_misurazione_significativa
@@ -23478,12 +23478,12 @@ cic:/Sophia-Antipolis/Algebra/Parts/subtype_rect.con \e[0;32mOK\e[0m 0.25 4.17%
 cic:/Sophia-Antipolis/Algebra/Cartesian/couple.con \e[0;32mOK\e[0m 0.26 13.04%
 cic:/Sophia-Antipolis/Algebra/Cartesian/proj1.con \e[0;32mOK\e[0m 0.27 17.39%
 cic:/Sophia-Antipolis/Algebra/Cartesian/proj2.con \e[0;32mOK\e[0m 0.25 8.70%
-cic:/Rocq/ZF/Plump/Inter_Ord.con \e[0;32mOK\e[0m 7.74 2766.67%
-cic:/Rocq/ZF/Plump/Ord_Succ.con \e[0;32mOK\e[0m 11.22 4575.00%
-cic:/Rocq/ZF/Plump/Ord_trans.con \e[0;32mOK\e[0m 2.94 1125.00%
-cic:/Rocq/ZF/Plump/Union_Ord.con \e[0;32mOK\e[0m 11.92 4668.00%
-cic:/Rocq/ZF/Plump/inter_ord.con \e[0;32mOK\e[0m 7.97 2851.85%
-cic:/Rocq/ZF/Plump/union_Ord.con \e[0;32mOK\e[0m 7.93 3072.00%
+cic:/Rocq/ZF/Plump/Inter_Ord.con \e[0;32mOK\e[0m 0.02 2766.67%
+cic:/Rocq/ZF/Plump/Ord_Succ.con \e[0;32mOK\e[0m 0.01 4575.00%
+cic:/Rocq/ZF/Plump/Ord_trans.con \e[0;32mOK\e[0m 0.00 1125.00%
+cic:/Rocq/ZF/Plump/Union_Ord.con \e[0;32mOK\e[0m 0.02 4668.00%
+cic:/Rocq/ZF/Plump/inter_ord.con \e[0;32mOK\e[0m 0.02 2851.85%
+cic:/Rocq/ZF/Plump/union_Ord.con \e[0;32mOK\e[0m 0.02 3072.00%
 cic:/Rocq/TreeAutomata/union_correct/union_mpl_0_ref_ok_invar.con \e[0;32mOK\e[0m 0.37 8.82%
 cic:/Rocq/TreeAutomata/union_correct/union_mpl_correct_wrt_sign_invar_0.con \e[0;32mOK\e[0m 0.39 -13.33%
 cic:/Rocq/TreeAutomata/union/mpl_compat_8_1.con \e[0;32mOK\e[0m 0.34 25.93%
@@ -24102,8 +24102,8 @@ cic:/Sophia-Antipolis/Algebra/Cartesian/uncurry.con \e[0;32mOK\e[0m 0.30 20.00%
 cic:/Sophia-Antipolis/Algebra/Cartesian/Maps/f.var \e[0;32mOK\e[0m 0.29 16.00%
 cic:/Sophia-Antipolis/Algebra/Cantor_Bernstein/Cantor_Bernstein/f.var \e[0;32mOK\e[0m 0.28 16.67%
 cic:/Sophia-Antipolis/Algebra/Cantor_Bernstein/Cantor_Bernstein/g.var \e[0;32mOK\e[0m 0.27 8.00%
-cic:/Rocq/ZF/Ordinal_theory/IN_Vee_Succ_EXType.con \e[0;32mOK\e[0m 25.82 9830.77%
-cic:/Rocq/ZF/Ordinal_theory/ex_rk.con \e[0;31mSKIPPED\e[0m
+cic:/Rocq/ZF/Ordinal_theory/IN_Vee_Succ_EXType.con \e[0;32mOK\e[0m 0.00 9830.77%
+cic:/Rocq/ZF/Ordinal_theory/ex_rk.con \e[0;32mOK\e[0m 0.05
 cic:/Rocq/TreeAutomata/union_correct/union_mpl_correct_ref_ok_invar.con \e[0;32mOK\e[0m 0.31 6.90%
 cic:/Rocq/TreeAutomata/union_correct/union_mpl_correct_wrt_sign_invar_1.con \e[0;32mOK\e[0m 0.38 -15.56%
 cic:/Rocq/TreeAutomata/union/mpl_compat_8_3.con \e[0;32mOK\e[0m 0.30 15.38%
@@ -27304,7 +27304,7 @@ cic:/Rocq/COC/Machine/top_error_ind.con \e[0;32mOK\e[0m 0.36
 cic:/Rocq/COC/Machine/top_trans_ind.con \e[0;32mOK\e[0m 0.37
 cic:/Rocq/COC/Int_stab/int_typ_cr.con \e[0;32mOK\e[0m 0.76
 cic:/Rocq/COC/Int_stab/int_var_sound_ind.con \e[0;32mOK\e[0m 0.39 18.18%
-cic:/Rocq/COC/Int_stab/lift_int_typ.con \e[0;32mOK\e[0m 7.75
+cic:/Rocq/COC/Int_stab/lift_int_typ.con \e[0;32mOK\e[0m 0.31
 cic:/Rocq/COC/Ered/strip_lemma_Epar_red1.con \e[0;32mOK\e[0m 0.00 -100.00%
 cic:/Rocq/COC/Equiv/Ered_normal_NF_Econv.con \e[0;32mOK\e[0m 0.00 -100.00%
 cic:/Rocq/COC/ETypes/Etyp_mem_kind.con \e[0;32mOK\e[0m 0.01 -96.97%
@@ -29603,7 +29603,7 @@ cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof2.c
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof20.con \e[0;32mOK\e[0m 0.13
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof22.con \e[0;32mOK\e[0m 0.14
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof25.con \e[0;32mOK\e[0m 0.14
-cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof26.con \e[0;32mOK\e[0m 1.49
+cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof26.con \e[0;32mOK\e[0m 1.43
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof27.con \e[0;32mOK\e[0m 0.20
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof29.con \e[0;32mOK\e[0m 0.15
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof3.con \e[0;32mOK\e[0m 0.14
@@ -29614,7 +29614,7 @@ cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof38.
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof39.con \e[0;32mOK\e[0m 0.15
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof41.con \e[0;32mOK\e[0m 0.16
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof44.con \e[0;32mOK\e[0m 0.16
-cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof45.con \e[0;32mOK\e[0m 1.57
+cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof45.con \e[0;32mOK\e[0m 1.43
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof46.con \e[0;32mOK\e[0m 0.22
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof5.con \e[0;32mOK\e[0m 0.17
 cic:/Orsay/ExactRealArithmetic/Multiplication/multiplication_correct_subproof6.con \e[0;32mOK\e[0m 0.17
@@ -30323,7 +30323,7 @@ cic:/Nijmegen/QArith/Zaux/Z_div_neg.con \e[0;32mOK\e[0m 0.15 66.67%
 cic:/Nijmegen/QArith/Zaux/le_inj.con \e[0;32mOK\e[0m 0.15 36.36%
 cic:/Nijmegen/QArith/Zaux/lt_absolu.con \e[0;32mOK\e[0m 0.15 7.14%
 cic:/Nijmegen/QArith/Zaux/pred_absolu.con \e[0;32mOK\e[0m 0.15 -16.67%
-cic:/Nijmegen/QArith/Qquadratic_sign/Qquadratic_sign_sign.con \e[0;32mOK\e[0m 1.09 -24.31%
+cic:/Nijmegen/QArith/Qquadratic_sign/Qquadratic_sign_sign.con \e[0;32mOK\e[0m 0.87 -24.31%
 cic:/Nijmegen/QArith/Qquadratic_Qpositive_to_Qpositive/Z8_lt_is_wf.con \e[0;32mOK\e[0m 0.32 -41.82%
 cic:/Nijmegen/QArith/Qquadratic/Qquadratic_Qpositive_to_Q_subproof0.con \e[0;32mOK\e[0m 0.20 17.65%
 cic:/Nijmegen/QArith/Qquadratic/Qquadratic_Qpositive_to_Q_subproof4.con \e[0;32mOK\e[0m 0.20 -89.58%
@@ -30809,14 +30809,14 @@ cic:/CoRN/devel/loeb/IDA/Ch6/L_as_CSetoid_fun.con \e[0;32mOK\e[0m 0.17 54.55%
 cic:/CoRN/devel/loeb/IDA/Ch6/direct_product_is_CMonoid.con \e[0;32mOK\e[0m 0.18 28.57%
 cic:/CoRN/devel/loeb/IDA/Ch6/iso_inv.con \e[0;32mOK\e[0m 0.24 -17.24%
 cic:/CoRN/devel/loeb/IDA/Ch6/not_injective_f.con \e[0;32mOK\e[0m 0.18 12.50%
-cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con \e[0;32mOK\e[0m 1.06 -8.62%
+cic:/CoRN/devel/loeb/IDA/Ch6/op_pres_Dbrack.con \e[0;32mOK\e[0m 0.89 -8.62%
 cic:/CoRN/devel/loeb/IDA/Ch6/surjective_f.con \e[0;32mOK\e[0m 0.18 63.64%
 cic:/CoRN/algebra/CRings/cr_inv.con \e[0;32mOK\e[0m 0.19 58.33%
 cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con \e[0;32mOK\e[0m 0.19 46.15%
 cic:/CoRN/algebra/CMonoids/cyc_imp_comm.con \e[0;32mOK\e[0m 0.21 16.67%
 cic:/CoRN/algebra/CMonoids/direct_product_is_CMonoid.con \e[0;32mOK\e[0m 0.20 25.00%
 cic:/CoRN/algebra/CMonoids/iso_inv.con \e[0;32mOK\e[0m 0.25 8.70%
-cic:/CoRN/algebra/CMonoids/op_pres_Dbrack.con \e[0;32mOK\e[0m 1.04 -5.45%
+cic:/CoRN/algebra/CMonoids/op_pres_Dbrack.con \e[0;32mOK\e[0m 0.84 -5.45%
 cic:/CoRN/algebra/CMonoids/power_k.con \e[0;32mOK\e[0m 0.34 25.93%
 cic:/CoRN/algebra/CMonoids/weakly_inj1.con \e[0;32mOK\e[0m 2.14 12.04%
 cic:/CoRN/algebra/CMonoidCyc/C_plus_strext.con \e[0;32mOK\e[0m 0.21 5.00%
@@ -31492,7 +31492,7 @@ cic:/CoRN/devel/loeb/IDA/Ch6_cyc/C_plus_is_CSemiGroup_subproof44.con \e[0;32mOK\e[
 cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char10_subproof.con \e[0;32mOK\e[0m 0.23 4.55%
 cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char10_subproof0.con \e[0;32mOK\e[0m 0.24 9.09%
 cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char10_subproof1.con \e[0;32mOK\e[0m 0.24 -7.69%
-cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char12.con \e[0;32mOK\e[0m 1.03 7.29%
+cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char12.con \e[0;32mOK\e[0m 0.76 7.29%
 cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char1_subproof.con \e[0;32mOK\e[0m 0.26 18.18%
 cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char1_subproof0.con \e[0;32mOK\e[0m 0.25 4.17%
 cic:/CoRN/devel/loeb/IDA/Ch6_cyc/Char1_subproof1.con \e[0;32mOK\e[0m 0.25 0.00%
@@ -31573,7 +31573,7 @@ cic:/CoRN/algebra/CMonoidCyc/C_plus_is_CSemiGroup_subproof44.con \e[0;32mOK\e[0m 0
 cic:/CoRN/algebra/CMonoidCyc/Char10_subproof.con \e[0;32mOK\e[0m 0.28 -22.22%
 cic:/CoRN/algebra/CMonoidCyc/Char10_subproof0.con \e[0;32mOK\e[0m 0.27 12.50%
 cic:/CoRN/algebra/CMonoidCyc/Char10_subproof1.con \e[0;32mOK\e[0m 0.28 3.70%
-cic:/CoRN/algebra/CMonoidCyc/Char12.con \e[0;32mOK\e[0m 1.01 4.12%
+cic:/CoRN/algebra/CMonoidCyc/Char12.con \e[0;32mOK\e[0m 0.77 4.12%
 cic:/CoRN/algebra/CMonoidCyc/Char1_subproof.con \e[0;32mOK\e[0m 0.26 8.33%
 cic:/CoRN/algebra/CMonoidCyc/Char1_subproof0.con \e[0;32mOK\e[0m 0.27 8.00%
 cic:/CoRN/algebra/CMonoidCyc/Char1_subproof1.con \e[0;32mOK\e[0m 0.26 -3.70%