(* examples for use with the "zero" prover *)
(* times are user/system/gc/real *)
(* original prover on left, exception optimized on right *)

(* each timing run was performed as follows:
   1) fresh copy of the HOLL prover (under SML109.32)
   2) declare exception UNCHANGED
   3) load code for rule
   4) load examples
   5) load timing functions
   6) check s1-->s13 in order

*)

val s1 = X "7 + (4 * (3 - 3))";
(* 0.100/0/0/0.115       0.140/0.010/0.020/0.151   *)

val s2 = X "(3 + 0 - 0) * 0";
(* 0.090/0/0/0.100       0.090/0/0/0.099           *)

val s3 = X "(3 + 7 + 8 * 9) * (0 - 0)";
(* 0.170/0/0/0.178       0.170/0/0/0.217           *)

val s4 = X "(8 + 0 - 0)";
(* 0.060/0/0/0.079       0.070/0/0/0.081           *)

val s5 = X "0 - 9";
(* 0.040/0/0/0.039       0.050/0.010/0/0.065       *)
 
val s6 = X "(9 + 0) - (7 * 0) + (0 + 0) + (0 + 14)";
(* 0.220/0/0/0.227       0.220/0/0/0.223           *)

val s7 = X "7 * (0 - 0 + 0 * 0 - 0 + 0)";
(* 0.170/0/0/0.172       0.200/0/0/0.208           *)

val s8 = X "(3 * 4 + 9 - 12) + (3 * 0) + (0 * 4) + (7 - 0 + 14 + 24 * 5)";
(* 0.390/0/0/0.400       0.400/0/0/0/0.406         *)

val s9 = X "x + 0";
(* 0.040/0/0/0.037       0.040/0/0/0.043           *)

val s10 = X "(f x) + 0";
(* 0.030/0/0/0.032       0.030/0/0/0.033           *)

val s11 = X "(f x) * 0";
(* 0.030/0/0/0.029       0.030/0/0/0.031           *)

val s12 = X("(3 * 4 + 9 - 12) + (3 * 0) + (0 * 4) + (7 - 0 + 14 + 24 * 5)"^
	  " + "^"(f x) * 0"^" - "^"7 * (0 - 0 + 0 * 0 - 0 + 0)");
(* 0.610/0/0/0.620       0.630/0/0/0.637           *)

val s13 = X ("1 + 1 + 1 + 0 + 1 + 1 + 1 + 1 + 1 + 1 +"^
             "0 - 0 - 0 - 0 - 0 - 0 - 0 - 0 - 0 - 0");
(* 0.530/0.010/0.010/0.559   0.540/0/0/0.550       *)



(* for what this is worth.....

consider the following four time sets:

0.540/0/0/0.550
0.500/0/0/0.550
0.520/0.010/0/0.519
0.570/0.030/0.020/0.619 

the results of four consecutive tests of the
"optimized" zero prover on s13  *)