]> matita.cs.unibo.it Git - helm.git/blob - helm/software/benchmarks/mostri20060329_ripristinata_convertibilita_aggressiva
Preparing for 0.5.9 release.
[helm.git] / helm / software / benchmarks / mostri20060329_ripristinata_convertibilita_aggressiva
1 cic:/Coq/Reals/Ranalysis1/cond_D2.con \e[0;32mOK\e[0m 0.03 -99.96%
2 cic:/Coq/Reals/Rcomplete/R_complete.con \e[0;32mOK\e[0m 2.17 -88.89%
3 cic:/Coq/Reals/Cos_plus/Majxy_cv_R0.con \e[0;32mOK\e[0m 1.52 -97.66%
4 cic:/Coq/Reals/RiemannInt/cont1.con \e[0;32mOK\e[0m 0.02 -99.98%
5 cic:/Coq/Reals/Exp_prop/maj_Reste_cv_R0.con \e[0;32mOK\e[0m 1.50 -95.41%
6 cic:/Coq/Reals/Alembert/AlembertC3_step1.con \e[0;32mOK\e[0m 0.42 -96.38%
7 cic:/Coq/Reals/Alembert/Alembert_C6.con \e[0;32mOK\e[0m 0.48 -87.50%
8 cic:/Coq/Reals/Rtrigo_def/exist_exp.con \e[0;32mOK\e[0m 0.07 -99.39%
9 cic:/Coq/Reals/NewtonInt/NewtonInt_P7.con \e[0;32mOK\e[0m 0.13 -99.02%
10 cic:/Coq/Reals/AltSeries/PI_ineq.con \e[0;32mOK\e[0m 0.14 -99.49%
11 cic:/Coq/Reals/Rtrigo_def/cos_0.con \e[0;32mOK\e[0m 0.14 -88.48%
12 cic:/Coq/Reals/Rtrigo_def/cos_sym.con \e[0;32mOK\e[0m 0.01 -42.27%
13 cic:/Coq/Reals/Rtrigo_def/cosh.con \e[0;32mOK\e[0m 0.01 -33.83%
14 cic:/Coq/Reals/Rtrigo_def/exp_0.con \e[0;32mOK\e[0m 0.03 -93.08%
15 cic:/Coq/Reals/Rtrigo_def/sin_0.con \e[0;32mOK\e[0m 0.13 -3.27%
16 cic:/Coq/Reals/Rtrigo_def/sin_antisym.con \e[0;32mOK\e[0m 0.03 -31.63%
17 cic:/Coq/Reals/Rtrigo_def/sinh.con \e[0;32mOK\e[0m 0.00 inf%
18 cic:/Coq/Reals/Rtrigo_calc/cosd.con \e[0;32mOK\e[0m 0.01 -39.88%
19 cic:/Coq/Reals/Rtrigo_calc/sind.con \e[0;32mOK\e[0m 0.00 inf%
20 cic:/Coq/Reals/Rtrigo_alt/PI_4.con \e[0;32mOK\e[0m 0.03 -33.35%
21 cic:/Coq/Reals/Rtrigo/sin_PI2.con \e[0;32mOK\e[0m 0.00 inf%
22 cic:/Coq/Reals/Rtrigo/tan.con \e[0;32mOK\e[0m 0.00 inf%
23 cic:/Coq/Reals/RiemannInt/RiemannInt_P10.con \e[0;32mOK\e[0m 0.84 -90.66%
24 cic:/Coq/Reals/RiemannInt/SubEqui_P8.con \e[0;32mOK\e[0m 0.42 -85.91%
25 cic:/Coq/Reals/Ranalysis4/Rcontinuity_abs.con \e[0;32mOK\e[0m 0.12 -76.11%
26 cic:/Coq/Reals/Ranalysis4/continuity_finite_sum.con \e[0;32mOK\e[0m 0.04 -79.14%
27 cic:/Coq/Reals/Ranalysis4/derivable_pt_lim_finite_sum.con \e[0;32mOK\e[0m 0.06 -92.79%
28 cic:/Coq/Reals/Ranalysis1/derivable_continuous.con \e[0;32mOK\e[0m 0.00 inf%
29 cic:/Coq/Reals/Ranalysis1/derivable_pow.con \e[0;32mOK\e[0m 0.00 inf%
30 cic:/Coq/Reals/Ranalysis1/derive_pt_pow.con \e[0;32mOK\e[0m 0.01 34.17%
31 cic:/Coq/Reals/Rtopology/prolongement_C0.con \e[0;32mOK\e[0m 0.53 -98.83%
32 cic:/Coq/Reals/RiemannInt/RiemannInt_P11.con \e[0;32mOK\e[0m 1.10 -93.72%
33 cic:/Coq/Reals/RiemannInt/RiemannInt_P22.con \e[0;32mOK\e[0m 0.94 -98.16%
34 cic:/Coq/Reals/RiemannInt/RiemannInt_P23.con \e[0;32mOK\e[0m 0.45 -98.60%
35 cic:/Coq/Reals/RiemannInt/RiemannInt_P4.con \e[0;32mOK\e[0m 1.06 -94.57%
36 cic:/Coq/Reals/RiemannInt/RiemannInt_P6.con \e[0;32mOK\e[0m 5.33 -35.46%
37 cic:/Coq/Reals/RiemannInt/RiemannInt_exists.con \e[0;32mOK\e[0m 0.09 -12.22%
38 cic:/Lyon/FIRING-SQUAD/reflection/C_Vg.con \e[0;32mOK\e[0m 0.15 -98.67%
39 cic:/CoRN/model/setoids/Nsetoid/on.con \e[0;32mOK\e[0m 0.12 -99.74%
40 cic:/CoRN/devel/loeb/IDA/Ch6/on.con \e[0;32mOK\e[0m 0.06 -99.87%
41 cic:/Marseille/GC/liveness/until_zero/always_eventually_grey_until_zero_trace.con \e[0;32mOK\e[0m 0.23 -7.27%
42 cic:/Marseille/GC/liveness/until_zero/always_eventually_white_until_zero_trace.con \e[0;32mOK\e[0m 0.16 -8.43%
43 cic:/Coq/Reals/Ranalysis1/cond_D2.con \e[0;32mOK\e[0m 0.00 inf%
44 =============
45 Total: 18.59
46 Old: 647.16 (-97.13%)