3 [ #2.0 * #1.3254 * #2.0 * #1.3254,x1, #8.0; #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
4 #4.0,x3, #8.0; #4.0, x4, #8.0; #4.0,x5, #8.0; #4.0,x6, #8.0]
5 (unit6 x1 x2 x3 x4 x5 x6 * #2.0 + rad2_x x1 x2 x3 x4 x5 x6 * -- &1 < &0)`;;
8 verify_flyspeck_ineq 3 ineq_tm;;
12 [ #2.0 * #1.3254 * #2.0 * #1.3254,x1, #8.0; #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
13 #4.0,x3, #8.0; #4.0, x4, #8.0; #4.0,x5, #8.0; #4.0,x6, #8.0]
14 (&0 < delta_x x1 x2 x3 x4 x5 x6 * &4)`;;
17 [ #2.0 * #1.3254 * #2.0 * #1.3254,x1, #8.0; #2.0 * #1.3254 * #2.0 * #1.3254, x2, #8.0;
18 #4.0,x3, #8.0; #4.0, x4, #8.0; #4.0,x5, #8.0; #4.0,x6, #8.0]
19 ((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)`;;
22 let delta_x4_pos = verify_flyspeck_ineq 3 ineq1_tm;;
24 let ineq2_th = verify_flyspeck_ineq 3 ineq2_tm;;
26 let eq_th = REWRITE_CONV[ineq; IMP_IMP] ineq_tm;;
27 let INEQ_RULE = UNDISCH_ALL o SPEC_ALL o REWRITE_RULE[ineq; IMP_IMP];;
28 let th0 = INEQ_RULE delta_x4_pos;;
29 let th1 = INEQ_RULE ineq2_th;;
30 let th2 = MATCH_MP REAL_LT_RDIV_EQ th0;;
31 let th3 = REWRITE_RULE[GSYM th2; GSYM rad2_x] th1;;
32 let th4 = ONCE_REWRITE_RULE[REAL_ARITH `a < b <=> a + b * -- &1 < &0`] th3;;
33 let result = (REWRITE_RULE[GSYM eq_th] o DISCH_ALL) th4;;
38 add_example {id = "7067938795";
40 ineq_tm = `ineq [ #4.0,x1, #6.3504; #4.0,x2, #6.3504; #4.0,x3, #6.3504; #4.0,x4, #4.0;
41 #3.01 * #3.01, x5, #3.24 * #3.24; #3.01 * #3.01,x6, #3.24 * #3.24]
42 (dih_x' x1 x2 x3 x4 x5 x6 +
43 unit6 x1 x2 x3 x4 x5 x6 * pi * --(&1 / #2.0) +
44 unit6 x1 x2 x3 x4 x5 x6 * #0.46 <
47 (* base = 200: 690s (834s total) (386s (468s) Ubuntu 9/Ocaml 3.09.3)*)
48 verify_flyspeck_ineq 4 ineq_tm;;
52 let ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
53 &2, y3, #2.52; #2.52, y4, sqrt(&8);
54 &2, y5, #2.52; &2, y6, #2.52]
55 ( ((dih_y' y1 y2 y3 y4 y5 y6) - #1.629 +
56 (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
57 (#0.763 * (y4 - #2.52)) -
58 (#0.315 * (y1 - #2.0))) * (-- &1) < &0)`;;
60 (* base = 200: 27946s (31514s total) (Ubuntu 9: 15226 (17091)) *)
61 verify_flyspeck_ineq 5 ineq_tm;;
63 let ineq_tm2 = `ineq [ #4.0,x1, #6.3504; #4.0,x2, #6.3504; #4.0,x3, #6.3504; #6.3504,x4, #8.0;
64 #4.0, x5, #6.3504; #4.0,x6, #6.3504]
65 (dih_x' x1 x2 x3 x4 x5 x6 * -- &1 +
66 unit6 x1 x2 x3 x4 x5 x6 * #1.629 +
67 sqrt_x2 x1 x2 x3 x4 x5 x6 * -- #0.414 +
68 sqrt_x3 x1 x2 x3 x4 x5 x6 * -- #0.414 +
69 sqrt_x5 x1 x2 x3 x4 x5 x6 * -- #0.414 +
70 sqrt_x6 x1 x2 x3 x4 x5 x6 * -- #0.414 +
71 unit6 x1 x2 x3 x4 x5 x6 * #0.414 * #8.0 +
72 sqrt_x4 x1 x2 x3 x4 x5 x6 * #0.763 +
73 unit6 x1 x2 x3 x4 x5 x6 * #0.763 * -- #2.52 +
74 sqrt_x1 x1 x2 x3 x4 x5 x6 * #0.315 +
75 unit6 x1 x2 x3 x4 x5 x6 * #0.315 * -- #2.0 <
78 (* Ubuntu 9: 6hr (16279s (14296s) with Sys.time()) *)
79 verify_flyspeck_ineq 5 ineq_tm2;;
82 let ineq_tm = `ineq [&2, y1, #2.52; &2, y2, #2.52;
83 &2, y3, #2.52; &2, y4, #2.52;
84 &2, y5, #2.52; &2, y6, #2.52]
85 (dih_y' y1 y2 y3 y4 y5 y6 < #1.893)`;;
87 (* base = 200: 5570s (6480s total) *)
88 verify_flyspeck_ineq 10 ineq_tm;;
90 (* base = 200 (Ubuntu 9): 3600s total (2716s (3128s) with Sys.time()) *)
91 verify_flyspeck_ineq 4 ineq_tm;;
94 [ #4.0,x1, #6.3504; #4.0,x2, #6.3504; #4.0,x3, #6.3504; #4.0,x4, #6.3504;
95 #4.0, x5, #6.3504; #4.0,x6, #6.3504]
96 (dih_x' x1 x2 x3 x4 x5 x6 + unit6 x1 x2 x3 x4 x5 x6 * -- #1.893 < &0)`;;
98 (* base = 200 (Ubuntu 9): 1593s (1450s) *)
99 verify_flyspeck_ineq 4 ineq_tm2;;