]> matita.cs.unibo.it Git - helm.git/blobdiff - benchmarks/mostri20060328
moved benchmnarks/ dir outside of components/
[helm.git] / benchmarks / mostri20060328
diff --git a/benchmarks/mostri20060328 b/benchmarks/mostri20060328
new file mode 100644 (file)
index 0000000..dbc94d4
--- /dev/null
@@ -0,0 +1,43 @@
+cic:/Coq/Reals/Ranalysis1/cond_D2.con \e[0;32mOK\e[0m 83.58
+cic:/Coq/Reals/Rcomplete/R_complete.con \e[0;32mOK\e[0m 32.06
+cic:/Coq/Reals/Cos_plus/Majxy_cv_R0.con \e[0;32mOK\e[0m 62.82
+cic:/Coq/Reals/RiemannInt/cont1.con \e[0;32mOK\e[0m 83.09
+cic:/Coq/Reals/Exp_prop/maj_Reste_cv_R0.con \e[0;32mOK\e[0m 32.46
+cic:/Coq/Reals/Alembert/AlembertC3_step1.con \e[0;32mOK\e[0m 12.76
+cic:/Coq/Reals/Alembert/Alembert_C6.con \e[0;32mOK\e[0m 32.20
+cic:/Coq/Reals/Rtrigo_def/exist_exp.con \e[0;32mOK\e[0m 13.75
+cic:/Coq/Reals/NewtonInt/NewtonInt_P7.con \e[0;32mOK\e[0m 12.77
+cic:/Coq/Reals/AltSeries/PI_ineq.con \e[0;32mOK\e[0m 27.98
+cic:/Coq/Reals/Rtrigo_def/cos_0.con \e[0;32mOK\e[0m 40.67
+cic:/Coq/Reals/Rtrigo_def/cos_sym.con \e[0;32mOK\e[0m 16.38
+cic:/Coq/Reals/Rtrigo_def/cosh.con \e[0;32mOK\e[0m 12.47
+cic:/Coq/Reals/Rtrigo_def/exp_0.con \e[0;32mOK\e[0m 43.30
+cic:/Coq/Reals/Rtrigo_def/sin_0.con \e[0;32mOK\e[0m 17.23
+cic:/Coq/Reals/Rtrigo_def/sin_antisym.con \e[0;32mOK\e[0m 11.80
+cic:/Coq/Reals/Rtrigo_def/sinh.con \e[0;32mOK\e[0m 13.72
+cic:/Coq/Reals/Rtrigo_calc/cosd.con \e[0;32mOK\e[0m 12.97
+cic:/Coq/Reals/Rtrigo_calc/sind.con \e[0;32mOK\e[0m 11.28
+cic:/Coq/Reals/Rtrigo_alt/PI_4.con \e[0;32mOK\e[0m 16.22
+cic:/Coq/Reals/Rtrigo/sin_PI2.con \e[0;32mOK\e[0m 15.47
+cic:/Coq/Reals/Rtrigo/tan.con \e[0;32mOK\e[0m 20.95
+cic:/Coq/Reals/RiemannInt/RiemannInt_P10.con \e[0;32mOK\e[0m 31.47
+cic:/Coq/Reals/RiemannInt/SubEqui_P8.con \e[0;32mOK\e[0m 13.01
+cic:/Coq/Reals/Ranalysis4/Rcontinuity_abs.con \e[0;32mOK\e[0m 31.19
+cic:/Coq/Reals/Ranalysis4/continuity_finite_sum.con \e[0;32mOK\e[0m 50.57
+cic:/Coq/Reals/Ranalysis4/derivable_pt_lim_finite_sum.con \e[0;32mOK\e[0m 63.33
+cic:/Coq/Reals/Ranalysis1/derivable_continuous.con \e[0;32mOK\e[0m 16.94
+cic:/Coq/Reals/Ranalysis1/derivable_pow.con \e[0;32mOK\e[0m 20.21
+cic:/Coq/Reals/Ranalysis1/derive_pt_pow.con \e[0;32mOK\e[0m 17.64
+cic:/Coq/Reals/Rtopology/prolongement_C0.con \e[0;32mOK\e[0m 43.05
+cic:/Coq/Reals/RiemannInt/RiemannInt_P11.con \e[0;32mOK\e[0m 17.29
+cic:/Coq/Reals/RiemannInt/RiemannInt_P22.con \e[0;32mOK\e[0m 49.30
+cic:/Coq/Reals/RiemannInt/RiemannInt_P23.con \e[0;32mOK\e[0m 31.02
+cic:/Coq/Reals/RiemannInt/RiemannInt_P4.con \e[0;32mOK\e[0m 18.70
+cic:/Coq/Reals/RiemannInt/RiemannInt_P6.con \e[0;32mOK\e[0m 10.47
+cic:/Coq/Reals/RiemannInt/RiemannInt_exists.con \e[0;32mOK\e[0m 84.98
+cic:/Lyon/FIRING-SQUAD/reflection/C_Vg.con OK 10.75 5.77%
+cic:/CoRN/model/setoids/Nsetoid/on.con OK 43.24 -0.29%
+cic:/CoRN/devel/loeb/IDA/Ch6/on.con OK 43.29 -1.75%
+cic:/Marseille/GC/liveness/until_zero/always_eventually_grey_until_zero_trace.con OK 0.22 -99.67%
+cic:/Marseille/GC/liveness/until_zero/always_eventually_white_until_zero_trace.con OK 0.15 -99.76%
+cic:/Coq/Reals/Ranalysis1/cond_D2.con OK 82.51 -1.27%