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