legacy/inequalities/inequality_spec.ml

   1 (* inequalities used in the text part of the kepler conjecture *)
   2
   3 (* They are not ALL listed here.
   4
   5 The following are in kep_inequalities2.ml
   6 996268658 P2
   7 824762926 P2
   8 675785884 P2
   9 657406669 P2
  10 551665569 P2
  11 325738864 P2
  12 314974315 P2
  13 277330628 P2
  14 193592217 P2
  15
  16 The following need to be moved here, but they are composites
  17 of several inequalites.
  18
  19 984628285 C
  20 971555266 C
  21 940884472 C
  22 934150983 C
  23 874876755 C
  24 855294746 C
  25 852270725 C
  26 83777706 C
  27 830854305 C
  28 815492935 C
  29 764978100 C
  30 73974037 C
  31 729988292 C
  32 692155251 C
  33 636208429 C
  34 628964355 C
  35 618205535 C
  36 531888597 C
  37 485049042 C
  38 311189443 C
  39 209361863 C
  40 193836552 C
  41 187932932 C
  42 163548682 C
  43 148776243 C
  44 129662166 C
  45 128523606 C
  46 *)
  47
  48 parse_as_infix("+.",(16,"right"));
  49 parse_as_infix("-.",(18,"left"));
  50 parse_as_infix("*.",(20,"right"));
  51 parse_as_infix("**.",(24,"left"));
  52 parse_as_infix("<.",(12,"right"));
  53 parse_as_infix("<=.",(12,"right"));
  54 parse_as_infix(">.",(12,"right"));
  55 parse_as_infix(">=.",(12,"right"));
  56 override_interface("+.",`real_add:real->real->real`);
  57 override_interface("-.",`real_sub:real->real->real`);
  58 override_interface("*.",`real_mul:real->real->real`);
  59 override_interface("**.",`real_pow:real->num->real`);
  60 (* boolean *)
  61 override_interface("<.",`real_lt:real->real->bool`);
  62 override_interface("<=.",`real_le:real->real->bool`);
  63 override_interface(">.",`real_gt:real->real->bool`);
  64 override_interface(">=.",`real_ge:real->real->bool`);
  65 (* unary *)
  66 override_interface("--.",`real_neg:real->real`);
  67 override_interface("&.",`real_of_num:num->real`);
  68 override_interface("||.",`real_abs:real->real`);;
  69
  70
  71 let I_115383627=
  72    all_forall `ineq
  73     [((#4.0), x1, square_2t0);
  74      ((#4.0), x2, (square (#2.168)));
  75      ((#4.0), x3, (square (#2.168)));
  76      ((#4.0), x4, square_2t0);
  77      (square_2t0, x5, square_2t0);
  78      (square_2t0, x6, square_4t0)
  79     ]
  80     ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.51) \/
  81       (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0)) `;;
  82
  83
  84 let I_115756648=
  85    all_forall `ineq
  86     [((#4.0), x1, square_2t0);
  87      ((#4.0), x2, square_2t0)
  88     ]
  89     ( (overlap_f (sqrt x1) (sqrt x2)) >.  (#0.887))`;;
  90
  91 let I_122081309=
  92    all_forall `ineq
  93     [((#4.0), x1, square_2t0);
  94      ((#4.0), x2, (square (#2.168)));
  95      ((#4.0), x3, (square (#2.168)));
  96      ((#8.0), x4, (#8.0));
  97      (square_2t0, x5, square_2t0);
  98      (square_2t0, x6, square_4t0)
  99     ]
 100     ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.77) \/
 101       (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 102
 103
 104 let I_135427691=
 105    all_forall `ineq
 106     [((#4.0), x1, square_2t0);
 107      ((#4.0), x2, (square (#2.168)));
 108      ((#4.0), x3, (square (#2.168)));
 109      (square_2t0, x4, (#8.0));
 110      (square_2t0, x5, square_2t0);
 111      (square_2t0, x6, square_4t0)
 112     ]
 113     (
 114          (
 115             ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (--. (#0.12))) \/
 116            ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.2)) \/
 117            (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 118
 119
 120
 121 let J_175514843=
 122    all_forall `ineq
 123     [(square_2t0, x1, (#8.0));
 124      ((#4.0), x2, square_2t0);
 125      ((#4.0), x3, square_2t0);
 126      ((#4.0), x4, square_2t0);
 127      ((#4.0), x5, square_2t0);
 128      ((#4.0), x6, square_2t0)
 129     ]
 130     ( ( (mu_upright_x x1 x2 x3 x4 x5 x6) +.
 131            (  (--. (#0.1378)) *.  ( (#1.0) +.  (  (( --. ) (dih_x x1 x2 x3 x4 x5 x6)) /  (  (#2.0) *.  pi)))) +.
 132            (  (#2.0) *.  (#0.0263))) <.
 133            (vor_0_x x1 x2 x3 x4 x5 x6))`;;
 134
 135
 136 let J_208809199=
 137    all_forall `ineq
 138     [((#4.0), x1, square_2t0);
 139      ((#4.0), x2, square_2t0);
 140      ((#4.0), x3, square_2t0);
 141
 142         ((#4.0), x4, square_2t0);
 143      ((#4.0), x5, square_2t0);
 144      ((#4.0), x6, square_2t0)
 145     ]
 146     ( (dih_x x1 x2 x3 x4 x5 x6) >.  (#0.8638))`;;
 147
 148
 149 let I_2298281931=
 150 all_forall `ineq
 151    [
 152    ((#4.0),x1,square_2t0);
 153    ((#4.0),x2,square_2t0);
 154    ((#4.0),x3,square_2t0);
 155    ((#4.0),x4,(#8.0));
 156    ((#4.0),x5,square_2t0);
 157    ((#4.0),x6,(#8.0))
 158    ]
 159    (((x1 pow 5)*x4 - (&2)*(x1 pow 4)*x2*x4 + (x1 pow 3)*(x2 pow 2)*x4 - (&2)*(x1 pow 4)*x3*x4 +
 160    (&4)*(x1 pow 3)*x2*x3*x4 - (&2)*(x1 pow 2)*(x2 pow 2)*x3*x4 + (x1 pow 3)*(x3 pow 2)*x4 -
 161    (&2)*(x1 pow 2)*x2*(x3 pow 2)*x4 + x1*(x2 pow 2)*(x3 pow 2)*x4 - (x1 pow 4)*x2*x5 +
 162    (&2)*(x1 pow 3)*(x2 pow 2)*x5 - (x1 pow 2)*(x2 pow 3)*x5 + (x1 pow 4)*x3*x5 -
 163    (x1 pow 3)*x2*x3*x5 - (x1 pow 2)*(x2 pow 2)*x3*x5 + x1*(x2 pow 3)*x3*x5 -
 164    (x1 pow 3)*(x3 pow 2)*x5 + (&2)*(x1 pow 2)*x2*(x3 pow 2)*x5 -
 165    x1*(x2 pow 2)*(x3 pow 2)*x5 - (&2)*(x1 pow 4)*x4*x5 + (&4)*(x1 pow 3)*x2*x4*x5 -
 166    (&2)*(x1 pow 2)*(x2 pow 2)*x4*x5 + (&2)*(x1 pow 3)*x2*(x5 pow 2) -
 167    (&4)*(x1 pow 2)*(x2 pow 2)*(x5 pow 2) + (&2)*x1*(x2 pow 3)*(x5 pow 2) -
 168    (x1 pow 3)*x3*(x5 pow 2) + (&3)*(x1 pow 2)*x2*x3*(x5 pow 2) -
 169    (&3)*x1*(x2 pow 2)*x3*(x5 pow 2) + (x2 pow 3)*x3*(x5 pow 2) + (x1 pow 3)*x4*(x5 pow 2) -
 170    (&2)*(x1 pow 2)*x2*x4*(x5 pow 2) + x1*(x2 pow 2)*x4*(x5 pow 2) -
 171    (x1 pow 2)*x2*(x5 pow 3) + (&2)*x1*(x2 pow 2)*(x5 pow 3) - (x2 pow 3)*(x5 pow 3) +
 172    (x1 pow 4)*x2*x6 - (x1 pow 3)*(x2 pow 2)*x6 - (x1 pow 4)*x3*x6 - (x1 pow 3)*x2*x3*x6 +
 173    (&2)*(x1 pow 2)*(x2 pow 2)*x3*x6 + (&2)*(x1 pow 3)*(x3 pow 2)*x6 -
 174    (x1 pow 2)*x2*(x3 pow 2)*x6 - x1*(x2 pow 2)*(x3 pow 2)*x6 - (x1 pow 2)*(x3 pow 3)*x6 +
 175    x1*x2*(x3 pow 3)*x6 - (&2)*(x1 pow 4)*x4*x6 + (&4)*(x1 pow 3)*x3*x4*x6 -
 176    (&2)*(x1 pow 2)*(x3 pow 2)*x4*x6 - (x1 pow 3)*x2*x5*x6 + (&3)*(x1 pow 2)*(x2 pow 2)*x5*x6 -
 177    (x1 pow 3)*x3*x5*x6 - (&4)*(x1 pow 2)*x2*x3*x5*x6 + x1*(x2 pow 2)*x3*x5*x6 +
 178    (&3)*(x1 pow 2)*(x3 pow 2)*x5*x6 + x1*x2*(x3 pow 2)*x5*x6 -
 179    (&2)*(x2 pow 2)*(x3 pow 2)*x5*x6 + (&4)*(x1 pow 3)*x4*x5*x6 - (&4)*x1*x2*x3*x4*x5*x6 -
 180    (x1 pow 2)*x2*(x5 pow 2)*x6 - (&3)*x1*(x2 pow 2)*(x5 pow 2)*x6 +
 181    (&2)*(x1 pow 2)*x3*(x5 pow 2)*x6 + x1*x2*x3*(x5 pow 2)*x6 + (x2 pow 2)*x3*(x5 pow 2)*x6 -
 182    (&2)*(x1 pow 2)*x4*(x5 pow 2)*x6 + x1*x2*(x5 pow 3)*x6 + (x2 pow 2)*(x5 pow 3)*x6 -
 183    (x1 pow 3)*x2*(x6 pow 2) + (&2)*(x1 pow 3)*x3*(x6 pow 2) +
 184    (&3)*(x1 pow 2)*x2*x3*(x6 pow 2) - (&4)*(x1 pow 2)*(x3 pow 2)*(x6 pow 2) -
 185    (&3)*x1*x2*(x3 pow 2)*(x6 pow 2) + (&2)*x1*(x3 pow 3)*(x6 pow 2) +
 186    x2*(x3 pow 3)*(x6 pow 2) + (x1 pow 3)*x4*(x6 pow 2) - (&2)*(x1 pow 2)*x3*x4*(x6 pow 2) +
 187    x1*(x3 pow 2)*x4*(x6 pow 2) + (&2)*(x1 pow 2)*x2*x5*(x6 pow 2) -
 188    (x1 pow 2)*x3*x5*(x6 pow 2) + x1*x2*x3*x5*(x6 pow 2) - (&3)*x1*(x3 pow 2)*x5*(x6 pow 2) +
 189    x2*(x3 pow 2)*x5*(x6 pow 2) - (&2)*(x1 pow 2)*x4*x5*(x6 pow 2) -
 190    x1*x2*(x5 pow 2)*(x6 pow 2) - x1*x3*(x5 pow 2)*(x6 pow 2) -
 191    (&2)*x2*x3*(x5 pow 2)*(x6 pow 2) + x1*x4*(x5 pow 2)*(x6 pow 2) -
 192    (x1 pow 2)*x3*(x6 pow 3) + (&2)*x1*(x3 pow 2)*(x6 pow 3) - (x3 pow 3)*(x6 pow 3) +
 193    x1*x3*x5*(x6 pow 3) + (x3 pow 2)*x5*(x6 pow 3)) < (#0.0))`;;
 194
 195
 196 let J_241241504_1=
 197    all_forall `ineq
 198     [((#4.0), x1, square_2t0);
 199      ((#4.0), x2, square_2t0);
 200      ((#4.0), x3, square_2t0);
 201      ((square (#2.177303)), x4, square_2t0);
 202      ((#4.0), x5, square_2t0);
 203      ((#4.0), x6, square_2t0)
 204     ]
 205     ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <.  (  #0.028794285 ))`;;
 206
 207
 208 let I_312132053=
 209    all_forall `ineq
 210     [((#4.0), x1, square_2t0);
 211      ((#4.0), x2, (square (#2.168)));
 212      ((#4.0), x3, (square (#2.168)));
 213      ((#4.0), x4, square_2t0);
 214      (square_2t0, x5, (square (#3.488)));
 215      (square_2t0, x6, square_2t0)
 216     ]
 217     (
 218       ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (--. (#0.1453)))`;;
 219
 220 let J_346093004=
 221    all_forall `ineq
 222     [((#4.0), x1, square_2t0);
 223      ((#4.0), x2, square_2t0);
 224      ((#4.0), x3, square_2t0);
 225
 226          (square_2t0, x4, (#8.0));
 227      ((#4.0), x5, square_2t0);
 228      ((#4.0), x6, square_2t0)
 229     ]
 230     (
 231             ( (gamma_x x1 x2 x3 x4 x5 x6) <=.  (#0.0)) \/
 232             ( (eta_x x1 x2 x6) >.  (#2.0)) \/
 233             ( (eta_x x2 x3 x4) >.  (#2.0)) \/
 234             ( (eta_x x1 x3 x5) >.  (#2.0)) \/
 235             ( (eta_x x4 x5 x6) >.  (#2.0)))`;;
 236
 237 let J_40003553=
 238    all_forall `ineq
 239     [(square_2t0, x1, (#8.0));
 240      ((#4.0), x2, square_2t0);
 241      ((#4.0), x3, square_2t0);
 242
 243         ((#4.0), x4, square_2t0);
 244      ((#4.0), x5, square_2t0);
 245      ((#4.0), x6, square_2t0)
 246     ]
 247     ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <=.  (#0.0))`;;
 248
 249 let I_467530297=
 250    all_forall `ineq
 251     [((#4.0), x1, square_2t0);
 252      ((#4.0), x2, (square (#2.168)));
 253      ((#4.0), x3, (square (#2.168)));
 254      ((#4.0), x4, square_2t0);
 255      (square_2t0, x5, square_2t0);
 256      (square_2t0, x6, square_4t0)
 257     ]
 258     (
 259          (
 260            ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (--. (#0.1376))) \/
 261            ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.2)) \/
 262            (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 263
 264
 265 let J_522528841=
 266    all_forall `ineq
 267     [(square_2t0, x1, (#8.0));
 268      ((#4.0), x2, square_2t0);
 269      ((#4.0), x3, square_2t0);
 270
 271         ((#4.0), x4, square_2t0);
 272      ((#4.0), x5, square_2t0);
 273      ((#4.0), x6, square_2t0)
 274     ]
 275     ( ( (  (#2.0) *.  (gamma_x x1 x2 x3 x4 x5 x6)) +.
 276        (vor_0_x x1 x2 x3 x4 x5 x6) +.
 277      (( --. ) (vor_0_x_flipped x1 x2 x3 x4 x5 x6))) <=.  (#0.0))`;;
 278
 279
 280 let J_53415898=
 281    all_forall `ineq
 282     [((#4.0), x1, square_2t0);
 283      ((#4.0), x2, square_2t0);
 284      ((#4.0), x3, square_2t0);
 285      ((#4.0), x4, square_2t0);
 286      ((#4.0), x5, square_2t0);
 287      ((#4.0), x6, square_2t0)
 288     ]
 289     ( (sigma1_qrtet_x x1 x2 x3 x4 x5 x6) <=.  (#0.0))`;;
 290
 291 let I_535502975=
 292    all_forall `ineq
 293     [((square (#2.3)), x1, square_2t0);
 294      ((#4.0), x2, square_2t0);
 295      ((#4.0), x3, square_2t0);
 296      ((#4.0), x4, square_2t0);
 297      (square_2t0, x5, (square (#3.02)));
 298      (square_2t0, x6, (square (#3.02)))
 299     ]
 300     (
 301             (
 302                 ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.
 303                 (--. (#0.1371))) \/
 304             ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.14)) \/
 305             ( (dih_x x1 x2 x3 x4 x5 x6) >.  (#1.51)))`;;
 306
 307 let J_554253147=
 308    all_forall `ineq
 309     [
 310      (square_2t0, x1, (#8.0));
 311      ((#4.0), x2, square_2t0);
 312      ((#4.0), x3, square_2t0);
 313      ((#4.0), x4,square_2t0);
 314      ((#4.0), x5, square_2t0);
 315      ((#4.0), x6, square_2t0)
 316     ]
 317     ( ( (mu_upright_x x1 x2 x3 x4 x5 x6) +.  (mu_flipped_x x1 x2 x3 x4 x5 x6) +.
 318            (  (crown (  (sqrt x1) /  (#2.0))) *.  ( (#1.0) +.  (  (( --. ) (dih_x x1 x2 x3 x4 x5 x6)) /  pi))) +.
 319            (  (#2.0) *.  (anc (sqrt x1) (sqrt x2) (sqrt x6)))) <.
 320            ( (vor_0_x x1 x2 x3 x4 x5 x6) +.  (vor_0_x_flipped x1 x2 x3 x4 x5 x6)))`;;
 321
 322 let I_560470084=
 323    all_forall `ineq
 324     [((#4.0), x1, square_2t0);
 325      ((square (#2.3)), x2, square_2t0);
 326      ((#4.0), x3, square_2t0);
 327      (square_2t0, x4, (#8.0));
 328      ((#4.0), x5, square_2t0);
 329      ((#4.0), x6, square_2t0)
 330     ]
 331     (
 332                 ( (tauhat_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih2_x x1 x2 x3 x4 x5 x6))) >.
 333                 (--. (#0.2137)))`;;
 334
 335 let I_572068135=
 336    all_forall `ineq
 337     [((square (#2.3)), x1, (#6.3001));
 338      ((#4.0), x2, (#6.3001));
 339      ((#4.0), x3, (#6.3001));
 340      ((#4.0), x4, (#6.3001));
 341      ((#4.0), x5, (#6.3001));
 342      ((#4.0), x6, (#6.3001))
 343     ]
 344     (
 345             (
 346                 ( (tau_sigma_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.
 347                 (--. (#0.3442))) \/
 348             ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.51)))`;;
 349
 350 let I_576221766=
 351    all_forall `ineq
 352     [((#4.0), x1, square_2t0);
 353      ((#4.0), x2, (square (#2.168)));
 354      ((#4.0), x3, (square (#2.168)));
 355      ((#8.0), x4, (#8.0));
 356      ((#4.0), x5, square_2t0);
 357      (square_2t0, x6, square_4t0)
 358     ]
 359     ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.93) \/
 360       (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 361
 362 let J_586468779=
 363    all_forall `ineq
 364     [((#4.0), x1, square_2t0);
 365      ((#4.0), x2, square_2t0);
 366      ((#4.0), x3, square_2t0);
 367
 368         ((#4.0), x4, square_2t0);
 369      ((#4.0), x5, square_2t0);
 370      ((#4.0), x6, square_2t0)
 371     ]
 372     ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <=.  pt)`;;
 373
 374 let J_587618947=
 375    all_forall `ineq
 376     [((#4.0), x1, square_2t0);
 377      ((#4.0), x2, square_2t0);
 378      ((#4.0), x3, square_2t0);
 379
 380          (square_2t0, x4, (#8.0));
 381      (square_2t0, x5, (#8.0));
 382      (square_2t0, x6, (#8.0))
 383     ]
 384     (
 385             ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.  (#0.0)) \/
 386             ( (eta_x x1 x2 x6) >.  (sqrt (#2.0))) \/
 387             ( (eta_x x2 x3 x4) >.  (sqrt (#2.0))) \/
 388             ( (eta_x x1 x3 x5) >.  (sqrt (#2.0))) \/
 389             ( (eta_x x4 x5 x6) >.  (sqrt (#2.0))))`;;
 390
 391 let J_5901405=
 392    all_forall `ineq
 393     [((#4.0), x2, square_2t0);
 394      ((#4.0), x3, square_2t0);
 395      ((#4.0), x4, square_2t0);
 396      (square_2t0, x1, (#8.0));
 397      ((#4.0), x5, square_2t0);
 398      ((#4.0), x6, square_2t0)
 399     ]
 400     (( (vor_analytic_x x1 x2 x3 x4 x5 x6) <=.  (#0.0)) \/
 401     (chi_x x5 x6 x1  x2 x3 x4 >. (#0.0)   ))`;;
 402
 403 let I_60314528=
 404    all_forall `ineq
 405     [((#4.0), x1, square_2t0);
 406      ((#4.0), x2, (square (#2.168)));
 407      ((#4.0), x3, (square (#2.168)));
 408      ((#4.0), x4, (#4.0));
 409      (square_2t0, x5, square_2t0);
 410      (square_2t0, x6, square_4t0)
 411     ]
 412     ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.16) \/
 413         (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 414
 415
 416
 417 let I_603910880=
 418    all_forall `ineq
 419     [((#4.0), x1, square_2t0);
 420      ((#4.0), x2, (square (#2.168)));
 421      ((#4.0), x3, (square (#2.168)));
 422      (square_2t0, x4, (#8.0));
 423      ((#4.0), x5, square_2t0);
 424      (square_2t0, x6, square_4t0)
 425     ]
 426     (
 427          (
 428             ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (--. (#0.266))) \/
 429            ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.2)) \/
 430            (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 431
 432
 433 let J_629256313=
 434    all_forall `ineq
 435     [(square_2t0, x1, (#8.0));
 436      ((#4.0), x2, square_2t0);
 437      ((#4.0), x3, square_2t0);
 438      ((#4.0), x4, square_2t0);
 439
 440          (square_2t0, x5, (#8.0));
 441      ((#4.0), x6, square_2t0)
 442     ]
 443     (
 444             ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.  (#0.0)) \/
 445             ( (eta_x x1 x2 x6) >. (sqrt (#2.0))) \/
 446             ( (eta_x x2 x3 x4) >. (sqrt (#2.0))) \/
 447             ( (eta_x x1 x3 x5) >. (sqrt (#2.0))) \/
 448             ( (eta_x x4 x5 x6) >. (sqrt (#2.0))))`;;
 449
 450
 451 let I_644534985=
 452    all_forall `ineq
 453     [((#4.0), x1, square_2t0);
 454      ((#4.0), x2, (square (#2.168)));
 455      ((#4.0), x3, (square (#2.168)));
 456      ((#4.0), x4, square_2t0);
 457      ((#4.0), x5, square_2t0);
 458      (square_2t0, x6, square_4t0)
 459     ]
 460     (
 461          (
 462            ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (--. (#0.2391))) \/
 463            ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.2)) \/
 464            (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 465
 466 let I_690646028=
 467    all_forall `ineq
 468     [((#4.0), x1, square_2t0);
 469      ((#4.0), x2, (square (#2.168)));
 470      ((#4.0), x3, (square (#2.168)));
 471      ((#4.0), x4, square_2t0);
 472      (square_2t0, x5, square_4t0);
 473      ((#4.0), x6, square_2t0)
 474     ]
 475     ( ( (dih_x x1 x2 x3 x4 x5 x6) +.  (  (#0.5) *.  ( (#2.402) -.  (sqrt x4)))) <.  (  pi /  (#2.0)) \/
 476      (delta_x x1 x2 x3 x4 x5 x6 < (#0.0)))`;;
 477
 478 let I_69064028=I_690646028;; (* because of a typo *)
 479
 480
 481 let J_703457064=
 482    all_forall `ineq
 483     [(square_2t0, x1, (#8.0));
 484      ((#4.0), x2, square_2t0);
 485      ((#4.0), x6, square_2t0)
 486     ]
 487     ( (anc (sqrt x1) (sqrt x2) (sqrt x6)) <.  (#0.0263))`;;
 488
 489 let I_723700608=
 490    all_forall `ineq
 491     [((square (#2.3)), x1, (#6.3001));
 492      ((#4.0), x2, (#6.3001));
 493      ((#4.0), x3, (#6.3001));
 494      ((#4.0), x4, (#6.3001));
 495      ((#4.0), x5, (#6.3001));
 496      ((#8.0), x6, (square (#3.02)))
 497     ]
 498     (
 499             (
 500                 ( (tau_0_x x1 x2 x3 x4 x5 x6) -.  (  (#0.2529) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.
 501                 (--. (#0.1787))) \/
 502             ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.26)) \/
 503             ( (dih_x x1 x2 x3 x4 x5 x6) >.  (#1.63)))`;;
 504
 505
 506
 507
 508 let I_735258244=
 509    all_forall `ineq
 510     [((#4.0), x1, square_2t0);
 511      ((#4.0), x2, square_2t0);
 512      ((#4.0), x3, square_2t0);
 513      ((square (#3.2)), x4, (square (#3.2)));
 514
 515         (square_2t0, x5, square_2t0);
 516      ((#4.0), x6, (#4.0))
 517     ]
 518     (
 519             (beta (acs (  (sqrt x1) /  (#2.51))) (arclength (sqrt x1) (sqrt x3) (sqrt x5))) <.
 520             (dih3_x x1 x2 x3 x4 x5 x6))`;;
 521
 522 let J_738318844=
 523    all_forall `ineq
 524     [((#4.0), x1, square_2t0);
 525      ((#4.0), x2, square_2t0);
 526      ((#4.0), x3, square_2t0);
 527
 528          (square_2t0, x4, (#8.0));
 529      (square_2t0, x5, (#8.0));
 530      ((#4.0), x6, square_2t0)
 531     ]
 532     (
 533             ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.  (#0.0)) \/
 534             ( (eta_x x1 x2 x6) >.  (sqrt (#2.0))) \/
 535             ( (eta_x x2 x3 x4) >.  (sqrt (#2.0))) \/
 536             ( (eta_x x1 x3 x5) >.  (sqrt (#2.0))) \/
 537             ( (eta_x x4 x5 x6) >.  (sqrt (#2.0))))`;;
 538
 539
 540 let I_751442360=
 541    all_forall `ineq
 542     [(square_2t0, x1, (square (#2.696)));
 543      ((#4.0), x2, (square (#2.168)));
 544      ((#4.0), x3, (square (#2.168)));
 545      ((#4.0), x4, square_2t0);
 546      ((#4.0), x5, square_2t0);
 547      ((#4.0), x6, square_2t0)
 548     ]
 549     ( (dih2_x x1 x2 x3 x4 x5 x6) >.  (#0.74))`;;
 550
 551 let I_757995764=
 552    all_forall `ineq
 553     [((#4.0), x1, square_2t0);
 554      ((#4.0), x2, (square (#2.23)));
 555      ((#4.0), x3, (square (#2.23)));
 556      ((square (#2.77)), x4, (#8.0));
 557
 558      ((#4.0), x5, square_2t0);
 559      ((#4.0), x6, (#4.0))
 560     ]
 561     (
 562             (beta (acs (  (sqrt x1) /  (#2.77))) (arclength (sqrt x1) (sqrt x3) (sqrt x5))) <.
 563             (dih3_x x1 x2 x3 x4 x5 x6))`;;
 564
 565
 566 let I_821707685=
 567    all_forall `ineq
 568     [((#4.0), x1, (#6.3001));
 569      ((#4.0), x2, (square (#2.168)));
 570      ((#4.0), x3, (square (#2.168)));
 571      ((#4.0), x4, (#6.3001));
 572      ((#4.0), x5, (#6.3001));
 573      (square_2t0, x6, square_4t0)
 574     ]
 575     ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.63) \/
 576       (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
 577
 578 let J_82950290=
 579    all_forall `ineq
 580     [((#4.0), x1, square_2t0);
 581      ((#4.0), x2, square_2t0);
 582      ((#4.0), x3, square_2t0);
 583
 584         ((#4.0), x4, (square (#2.177303)));
 585      ((#4.0), x5, square_2t0);
 586      ((#4.0), x6, square_2t0)
 587     ]
 588     ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <.
 589                 ( (#0.31023815) +.  (  (--. (#0.207045)) *.  (dih_x x1 x2 x3 x4 x5 x6))))`;;
 590
 591
 592 let J_855677395=
 593    all_forall `ineq
 594     [((square (#2.69)), x1, (#8.0));
 595      ((#4.0), x2, square_2t0);
 596      ((#4.0), x3, square_2t0);
 597      ((#4.0), x4, square_2t0);
 598      ((#4.0), x5, square_2t0);
 599      ((#4.0), x6, square_2t0)
 600     ]
 601     ( ( (mu_upright_x x1 x2 x3 x4 x5 x6) +.  (mu_flipped_x x1 x2 x3 x4 x5 x6)) <.
 602            ( (vor_0_x x1 x2 x3 x4 x5 x6) +.  (vor_0_x_flipped x1 x2 x3 x4 x5 x6) +.
 603               (  (#0.02) *.  ( (  pi /  (#2.0)) +.  (( --. ) (dih_x x1 x2 x3 x4 x5 x6))))))`;;
 604
 605 let J_892806084=
 606    all_forall `ineq
 607     [(square_2t0, x1, (#8.0));
 608      ((#4.0), x2, square_2t0);
 609      ((#4.0), x3, square_2t0);
 610      ((#4.0), x4, square_2t0);
 611      ((#4.0), x5, square_2t0);
 612      ((#4.0), x6, square_2t0)
 613     ]
 614     ( ( (vor_analytic_x x1 x2 x3 x4 x5 x6) +.
 615      (vor_analytic_x_flipped x1 x2 x3 x4 x5 x6) +.
 616                (vor_0_x x1 x2 x3 x4 x5 x6) +.
 617       (( --. ) (vor_0_x_flipped x1 x2 x3 x4 x5 x6))) <=.  (#0.0))`;;
 618
 619 let J_906566422=
 620    all_forall `ineq
 621     [((square (#1.255)), x, (#2.0))
 622     ]
 623     ( (crown (sqrt x)) <.  (--. (#0.1378)))`;;
 624
 625 let J_917032944=
 626    all_forall `ineq
 627     [(square_2t0, x1, (#8.0));
 628      ((#4.0), x2, square_2t0);
 629      ((#4.0), x3, square_2t0);
 630      ((#4.0), x4, square_2t0);
 631
 632          (square_2t0, x5, (#8.0));
 633      (square_2t0, x6, (#8.0))
 634     ]
 635     (
 636             ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <.  (#0.0)) \/
 637             ( (eta_x x1 x2 x6) >.  (sqrt (#2.0))) \/
 638             ( (eta_x x2 x3 x4) >.  (sqrt (#2.0))) \/
 639             ( (eta_x x1 x3 x5) >.  (sqrt (#2.0))) \/
 640             ( (eta_x x4 x5 x6) >.  (sqrt (#2.0))))`;;
 641
 642 let J_984463800=
 643    all_forall `ineq
 644     [((#4.0), x1, square_2t0);
 645      ((#4.0), x2, square_2t0);
 646      ((#4.0), x3, square_2t0);
 647
 648         ((#4.0), x4, square_2t0);
 649      ((#4.0), x5, square_2t0);
 650      ((#4.0), x6, square_2t0)
 651     ]
 652     ( (dih_x x1 x2 x3 x4 x5 x6) <.  (#1.874445))`;;
 653