moved benchmnarks/ dir outside of components/

[helm.git] / benchmarks / mostri20060329_subst_avoids_beta_redexes

diff --git a/benchmarks/mostri20060329_subst_avoids_beta_redexes b/benchmarks/mostri20060329_subst_avoids_beta_redexes
new file mode 100644 (file)
index 0000000..be462ef
--- /dev/null
+++ b/benchmarks/mostri20060329_subst_avoids_beta_redexes
@@ -0,0 +1,46 @@
+cic:/Coq/Reals/Ranalysis1/cond_D2.con \e[0;32mOK\e[0m 86.94 4.03%
+cic:/Coq/Reals/Rcomplete/R_complete.con \e[0;32mOK\e[0m 19.53 -39.07%
+cic:/Coq/Reals/Cos_plus/Majxy_cv_R0.con \e[0;32mOK\e[0m 65.01 3.48%
+cic:/Coq/Reals/RiemannInt/cont1.con \e[0;32mOK\e[0m 83.87 0.93%
+cic:/Coq/Reals/Exp_prop/maj_Reste_cv_R0.con \e[0;32mOK\e[0m 32.64 0.54%
+cic:/Coq/Reals/Alembert/AlembertC3_step1.con \e[0;32mOK\e[0m 11.53 -9.65%
+cic:/Coq/Reals/Alembert/Alembert_C6.con \e[0;32mOK\e[0m 3.86 -88.00%
+cic:/Coq/Reals/Rtrigo_def/exist_exp.con \e[0;32mOK\e[0m 11.03 -19.79%
+cic:/Coq/Reals/NewtonInt/NewtonInt_P7.con \e[0;32mOK\e[0m 12.94 1.31%
+cic:/Coq/Reals/AltSeries/PI_ineq.con \e[0;32mOK\e[0m 28.26 1.00%
+cic:/Coq/Reals/Rtrigo_def/cos_0.con \e[0;32mOK\e[0m 1.24 -96.96%
+cic:/Coq/Reals/Rtrigo_def/cos_sym.con \e[0;32mOK\e[0m 0.02 -99.89%
+cic:/Coq/Reals/Rtrigo_def/cosh.con \e[0;32mOK\e[0m 0.01 -99.95%
+cic:/Coq/Reals/Rtrigo_def/exp_0.con \e[0;32mOK\e[0m 0.37 -99.14%
+cic:/Coq/Reals/Rtrigo_def/sin_0.con \e[0;32mOK\e[0m 0.13 -99.22%
+cic:/Coq/Reals/Rtrigo_def/sin_antisym.con \e[0;32mOK\e[0m 0.04 -99.64%
+cic:/Coq/Reals/Rtrigo_def/sinh.con \e[0;32mOK\e[0m 0.00 -99.98%
+cic:/Coq/Reals/Rtrigo_calc/cosd.con \e[0;32mOK\e[0m 0.01 -99.95%
+cic:/Coq/Reals/Rtrigo_calc/sind.con \e[0;32mOK\e[0m 0.00 -99.97%
+cic:/Coq/Reals/Rtrigo_alt/PI_4.con \e[0;32mOK\e[0m 0.05 -99.72%
+cic:/Coq/Reals/Rtrigo/sin_PI2.con \e[0;32mOK\e[0m 0.00 -99.99%
+cic:/Coq/Reals/Rtrigo/tan.con \e[0;32mOK\e[0m 0.00 -99.98%
+cic:/Coq/Reals/RiemannInt/RiemannInt_P10.con \e[0;32mOK\e[0m 9.02 -71.33%
+cic:/Coq/Reals/RiemannInt/SubEqui_P8.con \e[0;32mOK\e[0m 2.99 -77.05%
+cic:/Coq/Reals/Ranalysis4/Rcontinuity_abs.con \e[0;32mOK\e[0m 0.49 -98.42%
+cic:/Coq/Reals/Ranalysis4/continuity_finite_sum.con \e[0;32mOK\e[0m 0.20 -99.61%
+cic:/Coq/Reals/Ranalysis4/derivable_pt_lim_finite_sum.con \e[0;32mOK\e[0m 0.78 -98.77%
+cic:/Coq/Reals/Ranalysis1/derivable_continuous.con \e[0;32mOK\e[0m 0.00 -99.98%
+cic:/Coq/Reals/Ranalysis1/derivable_pow.con \e[0;32mOK\e[0m 0.00 -99.98%
+cic:/Coq/Reals/Ranalysis1/derive_pt_pow.con \e[0;32mOK\e[0m 0.01 -99.92%
+cic:/Coq/Reals/Rtopology/prolongement_C0.con \e[0;32mOK\e[0m 44.93 4.37%
+cic:/Coq/Reals/RiemannInt/RiemannInt_P11.con \e[0;32mOK\e[0m 17.57 1.61%
+cic:/Coq/Reals/RiemannInt/RiemannInt_P22.con \e[0;32mOK\e[0m 51.30 4.05%
+cic:/Coq/Reals/RiemannInt/RiemannInt_P23.con \e[0;32mOK\e[0m 32.16 3.67%
+cic:/Coq/Reals/RiemannInt/RiemannInt_P4.con \e[0;32mOK\e[0m 19.58 4.73%
+cic:/Coq/Reals/RiemannInt/RiemannInt_P6.con \e[0;32mOK\e[0m 8.26 -21.09%
+cic:/Coq/Reals/RiemannInt/RiemannInt_exists.con \e[0;32mOK\e[0m 0.10 -99.88%
+cic:/Lyon/FIRING-SQUAD/reflection/C_Vg.con \e[0;32mOK\e[0m 11.24 4.52%
+cic:/CoRN/model/setoids/Nsetoid/on.con \e[0;32mOK\e[0m 45.40 4.99%
+cic:/CoRN/devel/loeb/IDA/Ch6/on.con \e[0;32mOK\e[0m 45.23 4.48%
+cic:/Marseille/GC/liveness/until_zero/always_eventually_grey_until_zero_trace.con \e[0;32mOK\e[0m 0.25 14.49%
+cic:/Marseille/GC/liveness/until_zero/always_eventually_white_until_zero_trace.con \e[0;32mOK\e[0m 0.17 10.43%
+cic:/Coq/Reals/Ranalysis1/cond_D2.con \e[0;32mOK\e[0m 0.00 -100.00%
+=============
+Total: 647.16
+Old: 1305.26 (-50.42%)