let rec_seq = ` !x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
  x3 = abs(x2) - x1 /\ x4 = abs(x3) - x2 /\ x5 = abs(x4) - x3 /\
  x6 = abs(x5) - x4 /\ x7 = abs(x6) - x5 /\
  x8 = abs(x7) - x6 /\ x9 = abs(x8) - x7 /\ x10 = abs(x9) - x8 /\
  x11 = abs(x10) - x9 ==> x1 = x10 /\ x2 = x11`;;

let test_std =  `!a b c d.
  ((&0 + &1 * a + &0 * b + &0 * c + &0 * d >= &0)
   /\
   (&0 + &0 * a + &1 * b + &0 * c + &0 * d >= &0)
   /\
   (&0 + &0 * a + &0 * b + &1 * c + &0 * d >= &0)
   /\
   (&0 + &0 * a + &0 * b + &0 * c + &1 * d >= &0)
   /\
   (&0 + &3008 * a + &20980 * b + (-- &97775) * c + (-- &101225) * d >= &0)
   /\
   (&0 + &3985 * a + &25643 * b + (-- &135871) * c + (-- &130580) * d >= &0)
   /\
   (&0 + &4324 * a + &26978 * b + (-- &133655) * c + (-- &168473) * d >= &0)
   /\
   (&0 + &3534 * a + &25361 * b + (-- &46243) * c + (-- &100407) * d >= &0)
   /\
(&0 + &8836 * a + &40796 * b + (-- &176661) * c + (-- &215616) * d >= &0)
   /\
   (&0 + &5376 * a + &37562 * b + (-- &182576) * c + (-- &217615) * d >= &0)
   /\
   (&0 + &4982 * a + &33088 * b + (-- &98880) * c + (-- &167278) * d >= &0)
   /\
   (&0 + &4775 * a + &39122 * b + (-- &136701) * c + (-- &193393) * d >= &0)
   /\
   (&0 + &8046 * a + &42958 * b + (-- &225138) * c + (-- &256575) * d >= &0)
   /\
   (&0 + &8554 * a + &48955 * b + (-- &257370) * c + (-- &312877) * d >= &0)
   /\
   (&0 + &6147 * a + &45514 * b + (-- &165274) * c + (-- &227099) * d >= &0)
   /\
   (&0 + &8366 * a + &55140 * b + (-- &203989) * c + (-- &321623) * d >= &0)
   /\
   (&0 + &13479 * a + &68037 * b + (-- &174270) * c + (-- &341743) * d >= &0)
   /\
   (&0 + &21808 * a + &78302 * b + (-- &322990) * c + (-- &487539) * d >= &0)
   /\
   (&1 + (-- &8554 / &10000) * a + (-- &48955 / &10000) * b + &0 * c + &0 * d >= &0)
   /\
   (&1 + &0 * a + &0 * b + (-- &257370 / &10000) * c + (-- &312877 / &10000) * d >= &0)) ==>
  &1 * a + &1 / &2 * b + &1 / &3 * c + &1 / &4 * d <= &2057990000 / &1743360801`;;

let gale = `~(?T14 T24 T25 T35 T46 T47 T57 T58.
                T14 < &20 /\
                T24 + T25 < &20 /\
                T35 < &20 /\
                T14 + T24 - T46 - T47 = &0 /\
    T25 + T35 - T57 - T58 = &0 /\
    T46 > &10 /\
    T47 + T57 > &20 /\
    T58 > &30 /\
    T14 < &30 /\
    T24 < &20 /\
    T25 < &10 /\
    T35 < &10 /\
    T46 < &10 /\
    T47 < &2 /\
    T57 < &20 /\
    T58 < &30)`;;