(* -------------------------------------------------------------------------- *)
(*  Util                                                                      *)
(* -------------------------------------------------------------------------- *)

let mk_times x y = mk_binop `( *. )` x y
let mk_plus x y = mk_binop `( +. )` x y 
let mk_gt x y = mk_binop `( >. )` x y 
let _0 = `&0`
let _1 = `&1`
let m_1 = `-- &1`
let list_disj l = end_itlist (curry mk_disj) l

(* -------------------------------------------------------------------------- *)
(*  Definitions                                                               *)
(* -------------------------------------------------------------------------- *)

(* 
 * t = 1.25841
 * 2t = 2.51682
 * (2t)^2 = 6.3343829124
 *)
let dodecTrunc = kepler_def `dodecTrunc = #1.25841`
let twoDodecTrunc = kepler_def `twoDodecTrunc = #2.51682`
let twoDodecTruncSq = kepler_def `twoDodecTruncSq = #6.3343829124`
let dodecSlope = kepler_def `dodecSlope = #0.42755`

let volume_x = kepler_def(`volume_x x1 x2 x3 x4 x5 x6 =
        let del = sqrt (delta_x x1 x2 x3 x4 x5 x6) in
        let u126 = ups_x x1 x2 x6 in
        let u135 = ups_x x1 x3 x5 in
        let u234 = ups_x x2 x3 x4 in
        let vol = ((&1)/((&48)*del))*
                ((x1*(x2+x6-x1)+x2*(x1+x6-x2))*(chi_x x4 x5 x3 x1 x2 x6)/u126
               +(x2*(x3+x4-x2)+x3*(--x3+x4+x2))*(chi_x x6 x5 x1 x3 x2 x4)/u234
               +(x1*(--x1+x3+x5)+x3*(x1-x3+x5))*(chi_x x4 x6 x2 x1 x3 x5)/u135) in
          vol`)

let truncated_volume_x = kepler_def(`truncated_volume_x x1 x2 x3 x4 x5 x6 =
        let vor = vort_x x1 x2 x3 x4 x5 x6 dodecTrunc in
        let sol = sol_x x1 x2 x3 x4 x5 x6 in
          (vor - (&4 / &3) * sol) / (--(&4) * doct)`)

let omega_x = kepler_def( `omega_x x1 x2 x3 x4 x5 x6 =
    if eta_x x1 x2 x6 < sqrt2 /\ 
       eta_x x1 x3 x5 < sqrt2 /\ 
       eta_x x2 x3 x4 < sqrt2 /\
       eta_x x4 x5 x6 < sqrt2 
    then 
      volume_x x1 x2 x3 x4 x5 x6
    else
      truncated_volume_x x1 x2 x3 x4 x5 x6`)

let squander_x = kepler_def( `squander_x x1 x2 x3 x4 x5 x6 =
    omega_x x1 x2 x3 x4 x5 x6 - dodecSlope * sol_x x1 x2 x3 x4 x5 x6`)
                          
(* -------------------------------------------------------------------------- *)
(*  Tetrahedra                                                                *)
(* -------------------------------------------------------------------------- *)

let basicTet =
  let bnds = `ineq 
    [(&4, x1, twoDodecTruncSq);
     (&4, x2, twoDodecTruncSq);
     (&4, x3, twoDodecTruncSq);
     (&4, x4, twoDodecTruncSq);
     (&4, x5, twoDodecTruncSq);
     (&4, x6, twoDodecTruncSq)]` in
  let mk_p (vol,sol,dih,y1,y2,y3,y4,y5,y6,const) = 
    let vt = mk_times vol `omega_x x1 x2 x3 x4 x5 x6` in
    let st = mk_times sol `sol_x x1 x2 x3 x4 x5 x6` in
    let dt = mk_times dih `dih_x x1 x2 x3 x4 x5 x6` in
    let y1t = mk_times y1 `sqrt x1` in
    let y2t = mk_times y2 `sqrt x2` in
    let y3t = mk_times y3 `sqrt x3` in
    let y4t = mk_times y4 `sqrt x4` in
    let y5t = mk_times y5 `sqrt x5` in
    let y6t = mk_times y6 `sqrt x6` in
    let lhs = end_itlist mk_plus [vt;st;dt;y1t;y2t;y3t;y4t;y5t;y6t;const] in
      mk_gt lhs _0 in
    fun args -> all_forall (mk_comb(bnds,mk_p args))

(*
structure R = Random
val rand = R.rand(1029,4139871)
fun n () = R.randRange(100000000,999999999) rand
n()
  
 *)

let D_232427898 = basicTet(_1,_0,_0,_0,_0,_0,_0,_0,_0,`-- #0.20280`)
let D_501745932 = basicTet(_0,_1,_0,_0,_0,_0,_0,_0,_0,`-- #0.31568`)
let D_454413312 = basicTet(_0,m_1,_0,_0,_0,_0,_0,_0,_0,`#1.05124`)
let D_484548925 = basicTet(_0,_0,_1,_0,_0,_0,_0,_0,_0,`-- #0.85613`)
let D_140432082 = basicTet(_0,_0,m_1,_0,_0,_0,_0,_0,_0,`#1.88674`)
let D_211431164 = basicTet(_1,`-- #0.42755`,_0,_0,_0,_0,_0,_0,_0,_0)
let D_120383233 = basicTet(_1,`-- #0.68`,`#1.88718`,_0,_0,_0,_0,_0,_0,`-- #1.54550`)
let D_950195574 = basicTet(_1,`-- #0.68`,`#0.90746`,_0,_0,_0,_0,_0,_0,`-- #0.70671`)
let D_411439162 = basicTet(_1,`-- #0.68`,`#0.46654`,_0,_0,_0,_0,_0,_0,`-- #0.32922`)
let D_930476095 = basicTet(_1,`-- #0.55889`,_0,_0,_0,_0,_0,_0,_0,`#0.07365`)
let D_504216105 = basicTet(_1,`-- #0.63214`,_0,_0,_0,_0,_0,_0,_0,`#0.13033`)
let D_303447655 = basicTet(_1,`-- #0.73256`,_0,_0,_0,_0,_0,_0,_0,`#0.23590`)
let D_999530305 = basicTet(_1,`-- #0.89346`,_0,_0,_0,_0,_0,_0,_0,`#0.40504`)
let D_774222998 = basicTet(_1,`-- #0.3`,`-- #0.5734`,_0,_0,_0,_0,_0,_0,`#0.97823`)
let D_583790155 = basicTet(_1,`-- #0.3`,`-- #0.03668`,_0,_0,_0,_0,_0,_0,`-- #0.02475`)
let D_954638763 = basicTet(_1,`-- #0.3`,`#0.04165`,_0,_0,_0,_0,_0,_0,`-- #0.12118`)
let D_836501282 = basicTet(_1,`-- #0.3`,`#0.1234`,_0,_0,_0,_0,_0,_0,`-- #0.20926`)
let D_815857122 = basicTet(_1,`-- #0.42755`,`-- #0.11509`,_0,_0,_0,_0,_0,_0,`#0.17186`)
let D_143442051 = basicTet(_1,`-- #0.42755`,`-- #0.04078`,_0,_0,_0,_0,_0,_0,`#0.05072`)
let D_616037833 = basicTet(_1,`-- #0.42755`,`#0.11031`,_0,_0,_0,_0,_0,_0,`-- #0.13562`)
let D_943639543 = basicTet(_1,`-- #0.42755`,`#0.13091`,_0,_0,_0,_0,_0,_0,`-- #0.15735`)
let D_348573741 = basicTet(_1,`-- #0.55792`,`-- #0.21394`,_0,_0,_0,_0,_0,_0,`#0.41800`)
let D_887895540 = basicTet(_1,`-- #0.55792`,`-- #0.0068`,_0,_0,_0,_0,_0,_0,`#0.08191`)
let D_292050936 = basicTet(_1,`-- #0.55792`,`#0.0184`,_0,_0,_0,_0,_0,_0,`#0.05123`)
let D_747114280 = basicTet(_1,`-- #0.55792`,`#0.24335`,_0,_0,_0,_0,_0,_0,`-- #0.19398`)
let D_407035272 = basicTet(_1,`-- #0.68`,`-- #0.30651`,_0,_0,_0,_0,_0,_0,`#0.64850`)
let D_746762527 = basicTet(_1,`-- #0.68`,`-- #0.06965`,_0,_0,_0,_0,_0,_0,`#0.27799`)
let D_908135697 = basicTet(_1,`-- #0.68`,`#0.0172`,_0,_0,_0,_0,_0,_0,`#0.15661`)
let D_852700722 = basicTet(_1,`-- #0.68`,`#0.41812`,_0,_0,_0,_0,_0,_0,`-- #0.28776`)
let D_187794654 = basicTet(_1,`-- #0.64934`,_0,_0,_0,_0,_0,_0,_0,`#0.14841`)
let D_241250402 = basicTet(_1,`-- #0.6196`,_0,_0,_0,_0,_0,_0,_0,`#0.11763`)
let D_614375500 = basicTet(_1,`-- #0.58402`,_0,_0,_0,_0,_0,_0,_0,`#0.09029`)
let D_392850749 = basicTet(_1,`-- #0.25181`,_0,_0,_0,_0,_0,_0,_0,`-- #0.09649`)
let D_324682944 = basicTet(_1,`-- #0.00909`,_0,_0,_0,_0,_0,_0,_0,`-- #0.19954`)
let D_102919537 = basicTet(_1,`#0.93877`,_0,_0,_0,_0,_0,_0,_0,`-- #0.53788`)
let D_756454529 = basicTet(_1,`#0.93877`,`-- #0.20211`,_0,_0,_0,_0,_0,_0,`-- #0.28126`)
let D_563250599 = basicTet(_1,`#0.93877`,`#0.63517`,_0,_0,_0,_0,_0,_0,`-- #1.21407`)
let D_439521695 = basicTet(_1,`#1.93877`,_0,_0,_0,_0,_0,_0,_0,`-- #0.85479`)
let D_805633512 = basicTet(_1,`#1.93877`,`-- #0.20211`,_0,_0,_0,_0,_0,_0,`-- #0.62187`)
let D_892141600 = basicTet(_1,`#1.93877`,`#0.63517`,_0,_0,_0,_0,_0,_0,`-- #1.57647`)
let D_224306197 = basicTet(_1,`-- #0.42775`,_0,_0,_0,_0,_0,_0,_0,`#0.00012`)
let D_120210454 = basicTet(_1,`-- #0.55792`,_0,_0,_0,_0,_0,_0,_0,`#0.07304`)
let D_479875130 = basicTet(_1,_0,`-- #0.07853`,_0,_0,_0,_0,_0,_0,`-- #0.09374`)
let D_629548058 = basicTet(_1,_0,`-- #0.00339`,_0,_0,_0,_0,_0,_0,`-- #0.19868`)
let D_469668150 = basicTet(_1,_0,`#0.18199`,_0,_0,_0,_0,_0,_0,`-- #0.39666`)
let D_218128189 = basicTet(_1,`-- #0.42755`,`-- #0.2`,_0,_0,_0,_0,_0,_0,`#0.33207`)
let D_169113912 = basicTet(_1,`-- #0.3`,`-- #0.36373`,_0,_0,_0,_0,_0,_0,`#0.58263`)
let D_143105921 = basicTet(_1,`-- #0.3`,`#0.20583`,_0,_0,_0,_0,_0,_0,`-- #0.27984`)
let D_421739939 = basicTet(_1,`-- #0.3`,`#0.40035`,_0,_0,_0,_0,_0,_0,`-- #0.44637`)
let D_595203705 = basicTet(_1,`-- #0.3`,`#0.83259`,_0,_0,_0,_0,_0,_0,`-- #0.81644`)
let D_943490566 = basicTet(_1,`-- #0.42755`,`-- #0.51838`,_0,_0,_0,_0,_0,_0,`#0.93276`)
let D_797136399 = basicTet(_1,`-- #0.42755`,`#0.29344`,_0,_0,_0,_0,_0,_0,`-- #0.29650`)
let D_603733089 = basicTet(_1,`-- #0.42755`,`#0.57056`,_0,_0,_0,_0,_0,_0,`-- #0.53375`)
let D_459264712 = basicTet(_1,`-- #0.42755`,`#1.18656`,_0,_0,_0,_0,_0,_0,`-- #1.06114`)
let D_557495949 = basicTet(_1,`-- #0.55792`,`-- #0.67644`,_0,_0,_0,_0,_0,_0,`#1.29062`)
let D_171329882 = basicTet(_1,`-- #0.55792`,`#0.38278`,_0,_0,_0,_0,_0,_0,`-- #0.31335`)
let D_720788076 = basicTet(_1,`-- #0.55792`,`#0.74454`,_0,_0,_0,_0,_0,_0,`-- #0.62307`)
let D_554235027 = basicTet(_1,`-- #0.55792`,`#1.54837`,_0,_0,_0,_0,_0,_0,`-- #1.31127`)
let D_569393441 = basicTet(_1,`-- #0.68`,`-- #0.82445`,_0,_0,_0,_0,_0,_0,`#1.62571`)

let D_992963254 = basicTet
  (_0,_1,_0,`#0.245`,`#0.245`,`#0.245`,
   `-- #0.063`,`-- #0.063`,`-- #0.063`,`-- #1.64327`)

let D_157321192 = basicTet
  (_0,_1,_0,`#0.3798`,`#0.3798`,`#0.3798`,
   `-- #0.198`,`-- #0.198`,`-- #0.198`,`-- #1.64207`)

(* Error: changed from 0.480715*)
let D_954705068 = basicTet
  (_0,m_1,_0,`-- #0.151`,`-- #0.151`,`-- #0.151`,
   `#0.323`,`#0.323`,`#0.323`,`-- #0.48070`)

let D_607292193 = basicTet
  (_1,`-- #0.42755`,_0,`-- #0.0392`,`-- #0.0392`,`-- #0.0392`,
   `-- #0.0101`,`-- #0.0101`,`-- #0.0101`,`#0.29580`)

let D_852636576 = basicTet
  (_1,_0,_0,`#0.107`,`#0.107`,`#0.107`,
   `-- #0.116`,`-- #0.116`,`-- #0.116`,`-- #0.18169`)

let D_981457443 = basicTet
  (_1,_0,_0,`#0.0623`,`#0.0623`,`#0.0623`,
   `-- #0.0722`,`-- #0.0722`,`-- #0.0722`,`-- #0.17629`)

let D_400655725 = basicTet
  (_0,_0,_1,`-- #0.237`,`#0.372`,`#0.372`,
   `-- #0.708`,`#0.372`,`#0.372`,`-- #2.31694`)

let D_552790530 = basicTet
  (_0,_0,_1,`-- #0.237`,`#0.363`,`#0.363`,
   `-- #0.688`,`#0.363`,`#0.363`,`-- #2.28494`)

(* Error: changed from 0.9505*)
let D_339650543 = basicTet
  (_0,_0,m_1,`#0.505`,`-- #0.152`,`-- #0.152`,
   `#0.766`,`-- #0.152`,`-- #0.152`,`-- #0.09503`)

(* -------------------------------------------------------------------------- *)
(*  Quadrilaterals                                                            *)
(* -------------------------------------------------------------------------- *)

let basicQuad =
  let bnds = `ineq 
    [(&4, x1, twoDodecTruncSq);
     (&4, x2, twoDodecTruncSq);
     (&4, x3, twoDodecTruncSq);
     (twoDodecTruncSq, x4, #26.0));
     (&4, x5, twoDodecTruncSq);
     (&4, x6, twoDodecTruncSq);
     (&4, x7, twoDodecTruncSq);
     (&4, x8, twoDodecTruncSq);
     (&4, x9, twoDodecTruncSq)]` in
  let mk_times x y = mk_binop `( *. )` x y in
  let mk_plus x y = mk_binop `( +. )` x y in
  let mk_gt x y = mk_binop `( >. )` x y in
  let constr1 = `delta_x x1 x2 x3 x4 x5 x6 < &0` in
  let constr2 = `delta_x x7 x2 x3 x4 x8 x9 < &0` in
  let constr3 = `cross_diag_x x1 x2 x3 x4 x5 x6 x7 x8 x9 < twoDodecTrunc` in
  let mk_p (vol,sol,dih,const) = 
    let vt = mk_times vol `omega_x x1 x2 x3 x4 x5 x6 + omega_x x7 x2 x3 x4 x8 x9` in
    let st = mk_times sol `sol_x x1 x2 x3 x4 x5 x6 + sol_x x7 x2 x3 x4 x8 x9` in
    let dt = mk_times dih `dih_x x1 x2 x3 x4 x5 x6` in
    let rhs = end_itlist  mk_plus [vt;st;dt;const] in
      mk_gt rhs _0 in
    fun args -> 
      all_forall (mk_comb(bnds,list_disj [mk_p args;constr1;constr2;constr3]))

let D_195763418 = basicQuad (_1,_0,_0,`-- #0.45513`)
let D_346647038 = basicQuad (_0,_1,_0,`-- #0.73192`)
let D_542422328 = basicQuad (_0,m_1,_0,`#2.85860`)
let D_958501031 = basicQuad (_0,_0,_1,`-- #1.15242`)
let D_977882706 = basicQuad (_0,_0,m_1,`#3.25887`)
let D_817699709 = basicQuad (_1,`-- #0.42755`,_0,`-- #0.031350`)

(* false *)
(* let D_221335081 = basicQuad (_1,`-- #0.42775`,`-- #0.15098`,`-- #0.3670`) *)

(* false *)
(* let D_380511524 = basicQuad (_1,`-- #0.42775`,`-- #0.09098`,`-- #0.1737`) *)

let D_534704091 = basicQuad (_1,`-- #0.42775`,`-- #0.00000`,`#0.0310`)

(* too true *)
(* let D_510654661 = basicQuad (_1,`-- #0.42775`,`#0.18519`,`#0.3183`) *)


let D_296038926 = basicQuad (_1,`-- #0.42775`,`#0.20622`,`#0.3438`)

(* false *)
(* let D_725284239 = basicQuad (_1,`-- #0.55792`,`-- #0.30124`,`-- #1.0173`) *)

(* false *)
(* let D_508592316 = basicQuad (_1,`-- #0.55792`,`-- #0.02921`,`-- #0.2101`) *)

(* false *)
(* let D_780228595 = basicQuad (_1,`-- #0.55792`,`-- #0.00000`,`-- #0.1393`) *)

(* false *)
(* let D_129176394 = basicQuad (_1,`-- #0.55792`,`#0.05947`,`-- #0.0470`) *)

let D_794503453 = basicQuad (_1,`-- #0.55792`,`#0.39938`,`#0.4305`)
let D_820371697 = basicQuad (_1,`-- #0.55792`,`#2.50210`,`#2.8976`)

(* false *)
(* let D_993947481 = basicQuad (_1,`-- #0.68000`,`-- #0.44194`,`-- #1.6264`) *)

(* false *)
(* let D_888634003 = basicQuad (_1,`-- #0.68000`,`-- #0.10957`,`-- #0.6753`) *)

(* false *)
(* let D_985594975 = basicQuad (_1,`-- #0.68000`,`-- #0.00000`,`-- #0.4029`) *)

let D_278856582 = basicQuad (_1,`-- #0.68000`,`#0.86096`,`#0.8262`)
let D_309781213 = basicQuad (_1,`-- #0.68000`,`#2.44439`,`#2.7002`)

(* false *)
(* let D_546070702 = basicQuad (_1,`-- #0.30000`,`-- #0.12596`,`-- #0.1279`) *)

let D_273299220 = basicQuad (_1,`-- #0.30000`,`-- #0.02576`,`#0.1320`)
let D_420356876 = basicQuad (_1,`-- #0.30000`,`#0.00000`,`#0.1945`)
let D_168730298 = basicQuad (_1,`-- #0.30000`,`#0.03700`,`#0.2480`)

let D_563211815 = basicQuad (_1,`-- #0.30000`,`#0.22476`,`#0.5111`)
let D_923665644 = basicQuad (_1,`-- #0.30000`,`#2.31852`,`#2.9625`)

(* false *)
(* let D_131907821 = basicQuad (_1,_0,`-- #0.23227`,`-- #0.1042`) *)

let D_632783039 = basicQuad (_1,_0,`#0.07448`,`#0.5591`)
let D_997560269 = basicQuad (_1,_0,`#0.22019`,`#0.7627`)
let D_849090707 = basicQuad (_1,_0,`#0.80927`,`#1.5048`)
let D_741613981 = basicQuad (_1,_0,`#5.84380`,`#7.3468`)