(* TSKAJXY-TADIAMB *)
let ineq_tm = `ineq
 [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;  
	#4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
 (unit6 x1 x2 x3 x4 x5 x6 *  #2.0 + rad2_x x1 x2 x3 x4 x5 x6 * -- &1 < &0)`;;

(* Too difficult:
verify_flyspeck_ineq 3 ineq_tm;;
*)

let ineq1_tm = `ineq
 [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;  
	#4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
 (&0 < delta_x x1 x2 x3 x4 x5 x6 * &4)`;;

let ineq2_tm = `ineq
 [ #2.0 *  #1.3254 *  #2.0 *  #1.3254,x1, #8.0;  #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;  
	#4.0,x3, #8.0; #4.0, x4, #8.0;  #4.0,x5, #8.0;  #4.0,x6, #8.0]
 ((unit6 x1 x2 x3 x4 x5 x6 * #2.0) * (delta_x x1 x2 x3 x4 x5 x6 * &4) < rho_x x1 x2 x3 x4 x5 x6)`;;

(* easy *)
let delta_x4_pos = verify_flyspeck_ineq 3 ineq1_tm;;
(* easy *)
let ineq2_th = verify_flyspeck_ineq 3 ineq2_tm;;

let eq_th = REWRITE_CONV[ineq; IMP_IMP] ineq_tm;;
let INEQ_RULE = UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[ineq; IMP_IMP];;
let th0 = INEQ_RULE delta_x4_pos;;
let th1 = INEQ_RULE ineq2_th;;
let th2 = MATCH_MP REAL_LT_RDIV_EQ th0;;
let th3 = REWRITE_RULE[GSYM th2; GSYM rad2_x] th1;;
let th4 = ONCE_REWRITE_RULE[REAL_ARITH `a < b <=> a + b * -- &1 < &0`] th3;;
let result = (REWRITE_RULE[GSYM eq_th] o DISCH_ALL) th4;;



(* 7067938795 *)
add_example {id = "7067938795";
	     difficulty = Medium;
	     ineq_tm = `ineq [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #4.0; 
			       #3.01 *  #3.01, x5, #3.24 *  #3.24;  #3.01 *  #3.01,x6, #3.24 *  #3.24]
    (dih_x' x1 x2 x3 x4 x5 x6 +
       unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 /  #2.0) +
       unit6 x1 x2 x3 x4 x5 x6 *  #0.46 <
     &0)`;;

(* base = 200: 690s (834s total) (386s (468s) Ubuntu 9/Ocaml 3.09.3)*)
verify_flyspeck_ineq 4 ineq_tm;;


(* 3318775219 *)
let ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
		   &2, y3, #2.52; #2.52, y4, sqrt(&8);
		   &2, y5, #2.52; &2, y6, #2.52]
    ( ((dih_y' y1 y2 y3 y4 y5 y6) - #1.629 +  
	(#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
	(#0.763 * (y4 - #2.52)) - 
	(#0.315 * (y1 - #2.0))) * (-- &1)  < &0)`;;

(* base = 200: 27946s (31514s total) (Ubuntu 9: 15226 (17091)) *)
verify_flyspeck_ineq 5 ineq_tm;;

let ineq_tm2 = `ineq [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #6.3504,x4, #8.0; 
  #4.0, x5, #6.3504;  #4.0,x6, #6.3504]
 (dih_x' x1 x2 x3 x4 x5 x6 * -- &1 +
  unit6 x1 x2 x3 x4 x5 x6 *  #1.629 +
  sqrt_x2 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  sqrt_x3 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  sqrt_x5 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  sqrt_x6 x1 x2 x3 x4 x5 x6 * -- #0.414 +
  unit6 x1 x2 x3 x4 x5 x6 *  #0.414 *  #8.0 +
  sqrt_x4 x1 x2 x3 x4 x5 x6 *  #0.763 +
  unit6 x1 x2 x3 x4 x5 x6 *  #0.763 * -- #2.52 +
  sqrt_x1 x1 x2 x3 x4 x5 x6 *  #0.315 +
  unit6 x1 x2 x3 x4 x5 x6 *  #0.315 * -- #2.0 <
  &0)`;;

(* Ubuntu 9: 6hr (16279s (14296s) with Sys.time()) *)
verify_flyspeck_ineq 5 ineq_tm2;;

(* 5490182221 *)
let ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
		     &2, y3, #2.52; &2, y4, #2.52;
		     &2, y5, #2.52; &2, y6, #2.52]
  (dih_y' y1 y2 y3 y4 y5 y6 < #1.893)`;;

(* base = 200: 5570s (6480s total) *)
verify_flyspeck_ineq 10 ineq_tm;;

(* base = 200 (Ubuntu 9): 3600s total (2716s (3128s) with Sys.time()) *)
verify_flyspeck_ineq 4 ineq_tm;;

let ineq_tm2 = `ineq
 [ #4.0,x1, #6.3504;  #4.0,x2, #6.3504;  #4.0,x3, #6.3504;  #4.0,x4, #6.3504; 
  #4.0, x5, #6.3504;  #4.0,x6, #6.3504]
 (dih_x' x1 x2 x3 x4 x5 x6 + unit6 x1 x2 x3 x4 x5 x6 * -- #1.893 < &0)`;;

(* base = 200 (Ubuntu 9): 1593s (1450s) *)
verify_flyspeck_ineq 4 ineq_tm2;;