/bat0/stac/Code/icra/WALi-OpenNWA/../icra -cra_newton_basic -cra-split-loops

Passing command-line option -cra-split-loops to duet.
<Unique State Name, 22> -> <Unique State Name, 27>	Base relation: 
{j := 0
 when i:64 < n:65}	
<Unique State Name, 22> -> <Unique State Name, 85>	Base relation: 
{when n:65 <= i:64}	
<Unique State Name, 40> -> <Unique State Name, 27>	Base relation: 
{j := (j:66 + 1)
 when j:66 <= k:67}	
<Unique State Name, 40> -> <Unique State Name, 45>	Base relation: 
{l := 0
 when k:67 < j:66}	
<Unique State Name, 58> -> <Unique State Name, 45>	Base relation: 
{l := (l:68 + 1)
 when l:68 <= m:69}	
<Unique State Name, 58> -> <Unique State Name, 54>	Base relation: 
{__cost := (__cost:70 + 1)
 m := (m:69 + 1)
 when (m:69 < l:68 /\ 0 <= __cost:70 /\ 0 <= (__cost:70 + 1))}	
<Unique State Name, 96> -> <Unique State Name, 101 95>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 9> -> <Unique State Name, 92>	Base relation: 
{param0 := tmp___0:8
 param0@pos := type_err:37
 param0@width := type_err:38}	
<Unique State Name, 101> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 36> -> <Unique State Name, 104>	Base relation: 
{when (0 <= k:67 /\ 0 <= j:66 /\ j:66 < i:64)}	
<Unique State Name, 8> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := 0
 when (0 <= tr:7 /\ tr:6 <= 0)}	
<Unique State Name, 8> -> <Unique State Name, 96>	Base relation: 
{param0 := tr:39
 param0@pos := type_err:40
 param0@width := type_err:41
 when (tr:5 < 0 \/ 0 < tr:4)}	
<Unique State Name, 97> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 argv := param1:30
 argv@pos := param1@pos:29
 argv@width := param1@width:28}	
<Unique State Name, 54> -> <Unique State Name, 102>	Base relation: 
{when (0 <= m:69 /\ 0 <= l:68 /\ l:68 < k:67)}	
<Unique State Name, 45> -> <Unique State Name, 103>	Base relation: 
{when (0 <= l:68 /\ 0 <= k:67 /\ k:67 < j:66)}	
<Unique State Name, 104> -> <Unique State Name, 40>	Base relation: 
{}	
<Unique State Name, 49> -> <Unique State Name, 36>	Base relation: 
{k := (k:67 + 1)
 when k:67 <= l:68}	
<Unique State Name, 49> -> <Unique State Name, 54>	Base relation: 
{m := 0
 when l:68 < k:67}	
<Unique State Name, 100> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 91> -> <Unique State Name, 100>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36}	
<Unique State Name, 103> -> <Unique State Name, 49>	Base relation: 
{}	
<Unique State Name, 105> -> <Unique State Name, 31>	Base relation: 
{}	
<Unique State Name, 99> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 31> -> <Unique State Name, 18>	Base relation: 
{i := (i:64 + 1)
 when i:64 <= j:66}	
<Unique State Name, 31> -> <Unique State Name, 36>	Base relation: 
{k := 0
 when j:66 < i:64}	
<Unique State Name, 85> -> <Unique State Name, 99>	Base relation: 
{return := havoc:71
 return@pos := type_err:74
 return@width := type_err:75}	
<Unique State Name, 18> -> <Unique State Name, 106>	Base relation: 
{when 0 <= i:64}	
<Unique State Name, 95> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := havoc:19}	
<Unique State Name, 102> -> <Unique State Name, 58>	Base relation: 
{}	
<Unique State Name, 106> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 89> -> <Unique State Name, 18>	Base relation: 
{i := 0
 n := param0:27}	
<Unique State Name, 27> -> <Unique State Name, 105>	Base relation: 
{when (0 <= j:66 /\ 0 <= i:64 /\ i:64 < n:65)}	
<Unique State Name, 92> -> <Unique State Name, 89 91>	Base relation: 
{}	MergeFn[Base relation: 
{}]
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:70 + 1)
 m := (m:69 + 1)
 when (0 <= m:69 /\ 0 <= l:68 /\ l:68 < k:67 /\ m:69 < l:68 /\ 0 <= __cost:70
         /\ 0 <= (__cost:70 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':2990) = (1)*(__cost:70) + 1
           (m':2991) = (1)*(m:69) + 1
           }
          pre:
            [|-l:68+k:67-1>=0; __cost:70>=0; m:69>=0; l:68-m:69-1>=0|]
          post:
            [|-l:68+k:67-1>=0; m':2991-1>=0; __cost':2990-1>=0;
              l:68-m':2991>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':2990
   m := m':2991
   when ((!(0 <= K:3001) \/ mid___cost:3004 = (__cost:70 + K:3001))
           /\ (!(0 <= K:3001) \/ mid_m:3003 = (m:69 + K:3001))
           /\ ((K:3001 = 0 /\ m:69 = mid_m:3003
                  /\ __cost:70 = mid___cost:3004)
                 \/ (1 <= K:3001 /\ 0 <= (-1 + -l:68 + k:67)
                       /\ 0 <= __cost:70 /\ 0 <= m:69
                       /\ 0 <= (-1 + l:68 + -m:69)
                       /\ 0 <= (-1 + -l:68 + k:67) /\ 0 <= (-1 + mid_m:3003)
                       /\ 0 <= (-1 + mid___cost:3004)
                       /\ 0 <= (l:68 + -mid_m:3003))) /\ K:3002 = 0
           /\ mid_m:3003 = m':2991 /\ mid___cost:3004 = __cost':2990
           /\ 0 = K:3002 /\ (K:3001 + K:3002) = K:3000 /\ 0 <= K:3000)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':3017
 l := (l:68 + 1)
 m := m':3016
 when (0 <= l:68 /\ 0 <= k:67 /\ k:67 < j:66 /\ l:68 < k:67
         /\ (!(0 <= K:3012) \/ mid___cost:3013 = (__cost:70 + K:3012))
         /\ (!(0 <= K:3012) \/ mid_m:3014 = K:3012)
         /\ ((K:3012 = 0 /\ 0 = mid_m:3014 /\ __cost:70 = mid___cost:3013)
               \/ (1 <= K:3012 /\ 0 <= (-1 + -l:68 + k:67) /\ 0 <= __cost:70
                     /\ 0 <= (-1 + l:68) /\ 0 <= (-1 + -l:68 + k:67)
                     /\ 0 <= (-1 + mid_m:3014) /\ 0 <= (-1 + mid___cost:3013)
                     /\ 0 <= (l:68 + -mid_m:3014))) /\ K:3015 = 0
         /\ mid_m:3014 = m':3016 /\ mid___cost:3013 = __cost':3017
         /\ 0 = K:3015 /\ (K:3012 + K:3015) = K:3018 /\ 0 <= K:3018
         /\ 0 <= m':3016 /\ 0 <= l:68 /\ l:68 < k:67 /\ l:68 <= m':3016)}
**** alpha hat: 
  {<Split [!(-__cost:70 <= 0)
            (l':3019) = 1
           (__cost':2990) = (1)*(__cost:70) + 0
           (m':2991) = 0
           }
          pre:
            [|l:68=0; -__cost:70-1>=0; -k:67+j:66-1>=0; k:67-1>=0|]
          post:
            [|l':3019-1=0; m':2991=0; -k:67+j:66-1>=0; -__cost':2990-1>=0;
              k:67-1>=0|]
           ((-__cost':2990 + l':3019)) = (-1)*(__cost:70) + 1
          (__cost':2990) = (1)*((-__cost:70 + l:68)) + (2)*(__cost:70) + 0
          ((-__cost':2990 + m':2991)) = (-1)*(__cost:70) + 0
          (__cost':2990) <= (1)*(__cost:70) + (-1)*1 + k:67
          (-__cost':2990) <= (1)*(-__cost:70) + (-1)*(-__cost:70 + l:68)
          (-__cost':2990) <= (1)*(-__cost:70) + 0
          }
  pre:
    [|-l:68+k:67-1>=0; -k:67+j:66-1>=0; l:68>=0; __cost:70>=0|]
  post:
    [|-l':3019+m':2991+1=0; -l':3019+k:67>=0; -k:67+j:66-1>=0; l':3019-1>=0;
      __cost':2990-l':3019+1>=0|]],
[!((1 + -l:68) <= 0)
  (l':3019) = 1
 (m':2991) = 0
 (__cost':2990) = (1)*(__cost:70) + 0
 } pre:   [|l:68=0; -k:67+j:66-1>=0; k:67-1>=0|] post:
  [|l':3019-1=0; m':2991=0; -k:67+j:66-1>=0; k:67-1>=0|]
 (l':3019) = (1)*(l:68) + 1 (m':2991) = (1)*(l:68) + 0
(__cost':2990) = (1)*(l:68) + (1)*(__cost:70) + 0
(__cost':2990) <= (1)*(__cost:70) + (-1)*1 + k:67
(-__cost':2990) <= (1)*(-__cost:70) + (-1)*1 } pre:
  [|-k:67+j:66-1>=0; __cost:70>=0; l:68-1>=0; k:67-l:68-1>=0|] post:
  [|-m':2991+l':3019-1=0; -k:67+j:66-1>=0; m':2991-1>=0;
    __cost':2990-m':2991>=0; k:67-m':2991-1>=0|]]>}
**** star transition: 
  {__cost := __cost':2990
   l := l':3019
   m := m':2991
   when ((!((0 <= K:3053 /\ K:3053 <= 0)) \/ mid_l:3056 = l:68)
           /\ (!(1 <= K:3053) \/ mid_l:3056 = 1)
           /\ (!(0 <= K:3053) \/ mid___cost:3057 = __cost:70)
           /\ (!((0 <= K:3053 /\ K:3053 <= 0)) \/ mid_m:3055 = m:69)
           /\ (!(1 <= K:3053) \/ mid_m:3055 = 0)
           /\ ((K:3053 = 0 /\ m:69 = mid_m:3055 /\ l:68 = mid_l:3056
                  /\ __cost:70 = mid___cost:3057)
                 \/ (1 <= K:3053 /\ l:68 = 0 /\ 0 <= (-1 + -__cost:70)
                       /\ 0 <= (-1 + -k:67 + j:66) /\ 0 <= (-1 + k:67)
                       /\ (-1 + mid_l:3056) = 0 /\ mid_m:3055 = 0
                       /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= (-1 + -mid___cost:3057) /\ 0 <= (-1 + k:67)))
           /\ (0 = K:3053 \/ !(-__cost:70 <= 0))
           /\ (!(0 <= K:3054)
                 \/ (-__cost':2990 + l':3019) = ((-mid___cost:3057
                                                    + mid_l:3056)
                                                   + (3/2 * K:3054)
                                                   + -(((-mid___cost:3057
                                                           + mid_l:3056)
                                                          * K:3054))
                                                   + -((mid___cost:3057
                                                          * K:3054))
                                                   + (-1/2
                                                        * (K:3054 * K:3054))))
           /\ (!(0 <= K:3054)
                 \/ __cost':2990 = (mid___cost:3057 + (-1/2 * K:3054)
                                      + ((-mid___cost:3057 + mid_l:3056)
                                           * K:3054)
                                      + (mid___cost:3057 * K:3054)
                                      + (1/2 * (K:3054 * K:3054))))
           /\ (!((0 <= K:3054 /\ K:3054 <= 0))
                 \/ (-__cost':2990 + m':2991) = ((-mid___cost:3057
                                                    + mid_m:3055)
                                                   + (3/2 * K:3054)
                                                   + -(((-mid___cost:3057
                                                           + mid_l:3056)
                                                          * K:3054))
                                                   + -((mid___cost:3057
                                                          * K:3054))
                                                   + (-1/2
                                                        * (K:3054 * K:3054))))
           /\ (!(1 <= K:3054)
                 \/ (-__cost':2990 + m':2991) = (-1
                                                   + (-mid___cost:3057
                                                        + mid_l:3056)
                                                   + (3/2 * K:3054)
                                                   + -(((-mid___cost:3057
                                                           + mid_l:3056)
                                                          * K:3054))
                                                   + -((mid___cost:3057
                                                          * K:3054))
                                                   + (-1/2
                                                        * (K:3054 * K:3054))))
           /\ (!(0 <= K:3054)
                 \/ __cost':2990 <= (mid___cost:3057 + -K:3054
                                       + (k:67 * K:3054)))
           /\ (!(0 <= K:3054)
                 \/ -__cost':2990 <= (-mid___cost:3057 + (5/6 * K:3054)
                                        + (-3/2
                                             * (-mid___cost:3057 + mid_l:3056)
                                             * K:3054)
                                        + (-1/2 * mid___cost:3057 * K:3054)
                                        + -((K:3054 * K:3054))
                                        + (1/2
                                             * (-mid___cost:3057 + mid_l:3056)
                                             * (K:3054 * K:3054))
                                        + (1/2 * mid___cost:3057
                                             * (K:3054 * K:3054))
                                        + (1/6 * (K:3054 * (K:3054 * K:3054)))))
           /\ (!(0 <= K:3054) \/ -__cost':2990 <= -mid___cost:3057)
           /\ ((K:3054 = 0 /\ mid_m:3055 = m':2991 /\ mid_l:3056 = l':3019
                  /\ mid___cost:3057 = __cost':2990)
                 \/ (1 <= K:3054 /\ 0 <= (-1 + -mid_l:3056 + k:67)
                       /\ 0 <= (-1 + -k:67 + j:66) /\ 0 <= mid_l:3056
                       /\ 0 <= mid___cost:3057
                       /\ (1 + -l':3019 + m':2991) = 0
                       /\ 0 <= (-l':3019 + k:67) /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= (-1 + l':3019)
                       /\ 0 <= (1 + __cost':2990 + -l':3019)))
           /\ (0 = K:3054 \/ -mid___cost:3057 <= 0)
           /\ (K:3053 + K:3054) = K:3052
           /\ (!((0 <= K:3058 /\ K:3058 <= 0)) \/ mid_l:3061 = l:68)
           /\ (!(1 <= K:3058) \/ mid_l:3061 = 1)
           /\ (!((0 <= K:3058 /\ K:3058 <= 0)) \/ mid_m:3060 = m:69)
           /\ (!(1 <= K:3058) \/ mid_m:3060 = 0)
           /\ (!(0 <= K:3058) \/ mid___cost:3062 = __cost:70)
           /\ ((K:3058 = 0 /\ m:69 = mid_m:3060 /\ l:68 = mid_l:3061
                  /\ __cost:70 = mid___cost:3062)
                 \/ (1 <= K:3058 /\ l:68 = 0 /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= (-1 + k:67) /\ (-1 + mid_l:3061) = 0
                       /\ mid_m:3060 = 0 /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= (-1 + k:67)))
           /\ (0 = K:3058 \/ !((1 + -l:68) <= 0))
           /\ (!(0 <= K:3059) \/ l':3019 = (mid_l:3061 + K:3059))
           /\ (!((0 <= K:3059 /\ K:3059 <= 0))
                 \/ m':2991 = (mid_m:3060 + K:3059))
           /\ (!(1 <= K:3059) \/ m':2991 = (-1 + mid_l:3061 + K:3059))
           /\ (!(0 <= K:3059)
                 \/ __cost':2990 = (mid___cost:3062 + (-1/2 * K:3059)
                                      + (mid_l:3061 * K:3059)
                                      + (1/2 * (K:3059 * K:3059))))
           /\ (!(0 <= K:3059)
                 \/ __cost':2990 <= (mid___cost:3062 + -K:3059
                                       + (k:67 * K:3059)))
           /\ (!(0 <= K:3059)
                 \/ -__cost':2990 <= (-mid___cost:3062 + -K:3059))
           /\ ((K:3059 = 0 /\ mid_m:3060 = m':2991 /\ mid_l:3061 = l':3019
                  /\ mid___cost:3062 = __cost':2990)
                 \/ (1 <= K:3059 /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= mid___cost:3062 /\ 0 <= (-1 + mid_l:3061)
                       /\ 0 <= (-1 + k:67 + -mid_l:3061)
                       /\ (-1 + -m':2991 + l':3019) = 0
                       /\ 0 <= (-1 + -k:67 + j:66) /\ 0 <= (-1 + m':2991)
                       /\ 0 <= (__cost':2990 + -m':2991)
                       /\ 0 <= (-1 + k:67 + -m':2991)))
           /\ (0 = K:3059 \/ (1 + -mid_l:3061) <= 0)
           /\ (K:3058 + K:3059) = K:3052 /\ 0 <= K:3052)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':3082
 k := (k:67 + 1)
 l := l':3083
 m := m':3084
 when (0 <= k:67 /\ 0 <= j:66 /\ j:66 < i:64 /\ k:67 < j:66
         /\ (!((0 <= K:3077 /\ K:3077 <= 0)) \/ mid_l:3078 = 0)
         /\ (!(1 <= K:3077) \/ mid_l:3078 = 1)
         /\ (!(0 <= K:3077) \/ mid___cost:3079 = __cost:70)
         /\ (!((0 <= K:3077 /\ K:3077 <= 0)) \/ mid_m:3080 = m:69)
         /\ (!(1 <= K:3077) \/ mid_m:3080 = 0)
         /\ ((K:3077 = 0 /\ m:69 = mid_m:3080 /\ 0 = mid_l:3078
                /\ __cost:70 = mid___cost:3079)
               \/ (1 <= K:3077 /\ 0 <= (-1 + -__cost:70)
                     /\ 0 <= (-1 + -k:67 + j:66) /\ 0 <= (-1 + k:67)
                     /\ (-1 + mid_l:3078) = 0 /\ mid_m:3080 = 0
                     /\ 0 <= (-1 + -k:67 + j:66)
                     /\ 0 <= (-1 + -mid___cost:3079) /\ 0 <= (-1 + k:67)))
         /\ (0 = K:3077 \/ !(-__cost:70 <= 0))
         /\ (!(0 <= K:3081)
               \/ (-__cost':3082 + l':3083) = ((-mid___cost:3079 + mid_l:3078)
                                                 + (3/2 * K:3081)
                                                 + -(((-mid___cost:3079
                                                         + mid_l:3078)
                                                        * K:3081))
                                                 + -((mid___cost:3079
                                                        * K:3081))
                                                 + (-1/2 * (K:3081 * K:3081))))
         /\ (!(0 <= K:3081)
               \/ __cost':3082 = (mid___cost:3079 + (-1/2 * K:3081)
                                    + ((-mid___cost:3079 + mid_l:3078)
                                         * K:3081)
                                    + (mid___cost:3079 * K:3081)
                                    + (1/2 * (K:3081 * K:3081))))
         /\ (!((0 <= K:3081 /\ K:3081 <= 0))
               \/ (-__cost':3082 + m':3084) = ((-mid___cost:3079 + mid_m:3080)
                                                 + (3/2 * K:3081)
                                                 + -(((-mid___cost:3079
                                                         + mid_l:3078)
                                                        * K:3081))
                                                 + -((mid___cost:3079
                                                        * K:3081))
                                                 + (-1/2 * (K:3081 * K:3081))))
         /\ (!(1 <= K:3081)
               \/ (-__cost':3082 + m':3084) = (-1
                                                 + (-mid___cost:3079
                                                      + mid_l:3078)
                                                 + (3/2 * K:3081)
                                                 + -(((-mid___cost:3079
                                                         + mid_l:3078)
                                                        * K:3081))
                                                 + -((mid___cost:3079
                                                        * K:3081))
                                                 + (-1/2 * (K:3081 * K:3081))))
         /\ (!(0 <= K:3081)
               \/ __cost':3082 <= (mid___cost:3079 + -K:3081
                                     + (k:67 * K:3081)))
         /\ (!(0 <= K:3081)
               \/ -__cost':3082 <= (-mid___cost:3079 + (5/6 * K:3081)
                                      + (-3/2
                                           * (-mid___cost:3079 + mid_l:3078)
                                           * K:3081)
                                      + (-1/2 * mid___cost:3079 * K:3081)
                                      + -((K:3081 * K:3081))
                                      + (1/2
                                           * (-mid___cost:3079 + mid_l:3078)
                                           * (K:3081 * K:3081))
                                      + (1/2 * mid___cost:3079
                                           * (K:3081 * K:3081))
                                      + (1/6 * (K:3081 * (K:3081 * K:3081)))))
         /\ (!(0 <= K:3081) \/ -__cost':3082 <= -mid___cost:3079)
         /\ ((K:3081 = 0 /\ mid_m:3080 = m':3084 /\ mid_l:3078 = l':3083
                /\ mid___cost:3079 = __cost':3082)
               \/ (1 <= K:3081 /\ 0 <= (-1 + -mid_l:3078 + k:67)
                     /\ 0 <= (-1 + -k:67 + j:66) /\ 0 <= mid_l:3078
                     /\ 0 <= mid___cost:3079 /\ (1 + -l':3083 + m':3084) = 0
                     /\ 0 <= (-l':3083 + k:67) /\ 0 <= (-1 + -k:67 + j:66)
                     /\ 0 <= (-1 + l':3083)
                     /\ 0 <= (1 + __cost':3082 + -l':3083)))
         /\ (0 = K:3081 \/ -mid___cost:3079 <= 0)
         /\ (K:3077 + K:3081) = K:3085
         /\ (!((0 <= K:3086 /\ K:3086 <= 0)) \/ mid_l:3087 = 0)
         /\ (!(1 <= K:3086) \/ mid_l:3087 = 1)
         /\ (!((0 <= K:3086 /\ K:3086 <= 0)) \/ mid_m:3088 = m:69)
         /\ (!(1 <= K:3086) \/ mid_m:3088 = 0)
         /\ (!(0 <= K:3086) \/ mid___cost:3089 = __cost:70)
         /\ ((K:3086 = 0 /\ m:69 = mid_m:3088 /\ 0 = mid_l:3087
                /\ __cost:70 = mid___cost:3089)
               \/ (1 <= K:3086 /\ 0 <= (-1 + -k:67 + j:66)
                     /\ 0 <= (-1 + k:67) /\ (-1 + mid_l:3087) = 0
                     /\ mid_m:3088 = 0 /\ 0 <= (-1 + -k:67 + j:66)
                     /\ 0 <= (-1 + k:67)))
         /\ (!(0 <= K:3090) \/ l':3083 = (mid_l:3087 + K:3090))
         /\ (!((0 <= K:3090 /\ K:3090 <= 0))
               \/ m':3084 = (mid_m:3088 + K:3090))
         /\ (!(1 <= K:3090) \/ m':3084 = (-1 + mid_l:3087 + K:3090))
         /\ (!(0 <= K:3090)
               \/ __cost':3082 = (mid___cost:3089 + (-1/2 * K:3090)
                                    + (mid_l:3087 * K:3090)
                                    + (1/2 * (K:3090 * K:3090))))
         /\ (!(0 <= K:3090)
               \/ __cost':3082 <= (mid___cost:3089 + -K:3090
                                     + (k:67 * K:3090)))
         /\ (!(0 <= K:3090) \/ -__cost':3082 <= (-mid___cost:3089 + -K:3090))
         /\ ((K:3090 = 0 /\ mid_m:3088 = m':3084 /\ mid_l:3087 = l':3083
                /\ mid___cost:3089 = __cost':3082)
               \/ (1 <= K:3090 /\ 0 <= (-1 + -k:67 + j:66)
                     /\ 0 <= mid___cost:3089 /\ 0 <= (-1 + mid_l:3087)
                     /\ 0 <= (-1 + k:67 + -mid_l:3087)
                     /\ (-1 + -m':3084 + l':3083) = 0
                     /\ 0 <= (-1 + -k:67 + j:66) /\ 0 <= (-1 + m':3084)
                     /\ 0 <= (__cost':3082 + -m':3084)
                     /\ 0 <= (-1 + k:67 + -m':3084)))
         /\ (0 = K:3090 \/ (1 + -mid_l:3087) <= 0)
         /\ (K:3086 + K:3090) = K:3085 /\ 0 <= K:3085 /\ 0 <= l':3083
         /\ 0 <= k:67 /\ k:67 < j:66 /\ k:67 <= l':3083)}
**** alpha hat: 
  {<Split [!(-__cost:70 <= 0)
            (k':3091) = (1)*(k:67) + 1
           (__cost':2990) = (1)*(__cost:70) + 0
           ((-k':3091 + l':3019)) = (-1)*1
           }
          pre:
            [|-__cost:70-1>=0; -k:67+1>=0; -k:67+j:66-1>=0; -j:66+i:64-1>=0;
              k:67>=0|]
          post:
            [|-k':3091+l':3019+1=0; -__cost':2990-1>=0; -k':3091+2>=0;
              -k':3091+j:66>=0; -j:66+i:64-1>=0; k':3091-1>=0|]
           (l':3019) = (1)*(k:67) + 0
          (k':3091) = (1)*(k:67) + 1
          (__cost':2990) = (1)*(__cost:70) + (-1/2)*k:67 + 1/2*k:67^2
          (((6 * __cost':2990) + l':3019)) <= (1)*(((6 * __cost:70) + l:68))
                                               + (-1)*l:68 + k:67^3
          (l':3019) <= (1)*(l:68) + (-1)*1 + j:66 + (-1)*l:68
          ((-__cost':2990 + l':3019)) <= (1)*((-__cost:70 + l:68)) + 
                                          1 + (-1)*l:68
          (-__cost':2990) <= (1)*(-__cost:70) + 0
          (-l':3019) <= (1)*(-l:68) + l:68
          (((10 * __cost':2990) + (-3 * l':3019))) <= (1)*(((10 * __cost:70)
                                                              + (-3 * l:68)))
                                                       + 3*l:68 + k:67^3
          }
  pre:
    [|-2k:67-((-1 + k:67) * (-1 + k:67))+(k:67 * k:67)+1=0;
      -k:67-((-1 + k:67) * (-1 + k:67))+((-1 + k:67) * k:67)+1=0;
      -4k:67-3((-1 + k:67) * (-1 + k:67))+((k:67 * k:67) * k:67)+3>=0;
      -2k:67-5((-1 + k:67) * (-1 + k:67))+((k:67 * k:67) * k:67)+5>=0;
      -k:67+j:66-1>=0; -k:67+((-1 + k:67) * (-1 + k:67))+1>=0;
      -j:66+i:64-1>=0; (k:67 * __cost:70)>=0; __cost:70>=0; k:67>=0;
      k:67+((-1 + k:67) * (-1 + k:67))-1>=0|]
  post:
    [|-2l':3019-((-1 + l':3019) * (-1 + l':3019))+(l':3019 * l':3019)+1=0;
      -l':3019-((-1 + l':3019) * (-1 + l':3019))+((-1 + l':3019) * l':3019)+1=0;
      -l':3019+k':3091-1=0;
      -4l':3019-3((-1 + l':3019) * (-1 + l':3019))
      +((l':3019 * l':3019) * l':3019)+3>=0;
      -2l':3019-5((-1 + l':3019) * (-1 + l':3019))
      +((l':3019 * l':3019) * l':3019)+5>=0;
      -l':3019-((-1 + l':3019) * (-1 + l':3019))+2__cost':2990+1>=0;
      -l':3019+j:66-1>=0; -l':3019+((-1 + l':3019) * (-1 + l':3019))+1>=0;
      -j:66+i:64-1>=0;
      (l':3019 * ((1/2 * l':3019) + (-1/2 * (l':3019 * l':3019)) + __cost':2990))>=0;
      l':3019>=0; l':3019+((-1 + l':3019) * (-1 + l':3019))-1>=0|]],
[!((1 + __cost:70) <= 0)
  (l':3019) = (1)*(k:67) + 0
 (k':3091) = (1)*(k:67) + 1
 (__cost':2990) = (1)*(__cost:70) + (-1/2)*k:67 + 1/2*k:67^2
 (((6 * __cost':2990) + l':3019)) <= (1)*(((6 * __cost:70) + l:68))
                                      + (-1)*l:68 + k:67^3
 (l':3019) <= (1)*(l:68) + (-1)*1 + j:66 + (-1)*l:68
 ((-__cost':2990 + l':3019)) <= (1)*((-__cost:70 + l:68)) + 1 + (-1)*l:68
 (-__cost':2990) <= (1)*(-__cost:70) + 0
 (-l':3019) <= (1)*(-l:68) + l:68
 (((10 * __cost':2990) + (-3 * l':3019))) <= (1)*(((10 * __cost:70)
                                                     + (-3 * l:68))) + 
                                              3*l:68 + k:67^3
 } pre:
  [|-2k:67-((-1 + k:67) * (-1 + k:67))+(k:67 * k:67)+1=0;
    -k:67-((-1 + k:67) * (-1 + k:67))+((-1 + k:67) * k:67)+1=0;
    -4k:67-3((-1 + k:67) * (-1 + k:67))+((k:67 * k:67) * k:67)+3>=0;
    -2k:67-5((-1 + k:67) * (-1 + k:67))+((k:67 * k:67) * k:67)+5>=0;
    -k:67+j:66-1>=0; -k:67+((-1 + k:67) * (-1 + k:67))+1>=0; -j:66+i:64-1>=0;
    (k:67 * __cost:70)>=0; __cost:70>=0; k:67>=0;
    k:67+((-1 + k:67) * (-1 + k:67))-1>=0|] post:
  [|-2l':3019-((-1 + l':3019) * (-1 + l':3019))+(l':3019 * l':3019)+1=0;
    -l':3019-((-1 + l':3019) * (-1 + l':3019))+((-1 + l':3019) * l':3019)+1=0;
    -l':3019+k':3091-1=0;
    -4l':3019-3((-1 + l':3019) * (-1 + l':3019))
    +((l':3019 * l':3019) * l':3019)+3>=0;
    -2l':3019-5((-1 + l':3019) * (-1 + l':3019))
    +((l':3019 * l':3019) * l':3019)+5>=0;
    -l':3019-((-1 + l':3019) * (-1 + l':3019))+2__cost':2990+1>=0;
    -l':3019+j:66-1>=0; -l':3019+((-1 + l':3019) * (-1 + l':3019))+1>=0;
    -j:66+i:64-1>=0;
    (l':3019 * ((1/2 * l':3019) + (-1/2 * (l':3019 * l':3019)) + __cost':2990))>=0;
    l':3019>=0; l':3019+((-1 + l':3019) * (-1 + l':3019))-1>=0|]
 (k':3091) = (1)*(k:67) + 1 (__cost':2990) = (1)*(__cost:70) + 0
((-k':3091 + l':3019)) = (-1)*1 } pre:
  [|-__cost:70-1>=0; -k:67+1>=0; -k:67+j:66-1>=0; -j:66+i:64-1>=0; k:67>=0|]
post:
  [|-k':3091+l':3019+1=0; -__cost':2990-1>=0; -k':3091+2>=0;
    -k':3091+j:66>=0; -j:66+i:64-1>=0; k':3091-1>=0|]],
[!((1 + -k:67) <= 0)
  (__cost':2990) = (1)*(__cost:70) + 0
 (m':2991) = (1)*(m:69) + 0
 (k':3091) = 1
 (l':3019) = 0
 } pre:   [|k:67=0; -j:66+i:64-1>=0; j:66-1>=0|] post:
  [|k':3091-1=0; l':3019=0; -j:66+i:64-1>=0; j:66-1>=0|]
 (l':3019) = (1)*(k:67) + 0 (m':2991) = (1)*(k:67) + (-1)*1
(k':3091) = (1)*(k:67) + 1
(__cost':2990) = (1)*(__cost:70) + (-1/2)*k:67 + 1/2*k:67^2
(l':3019) <= (1)*(l:68) + (-1)*1 + j:66 + (-1)*l:68
((-__cost':2990 + l':3019)) <= (1)*((-__cost:70 + l:68)) + 1 + (-1)*l:68
(-l':3019) <= (1)*(-l:68) + (-1)*1 + l:68
(((10 * __cost':2990) + (-3 * l':3019))) <= (1)*(((10 * __cost:70)
                                                    + (-3 * l:68))) + 
                                             (-4)*1 + 3*l:68 + k:67^3 } pre:
  [|-2k:67-((-1 + k:67) * (-1 + k:67))+(k:67 * k:67)+1=0;
    -k:67-((-1 + k:67) * (-1 + k:67))+((-1 + k:67) * k:67)+1=0;
    -2k:67-5((-1 + k:67) * (-1 + k:67))+((k:67 * k:67) * k:67)+1>=0;
    -k:67+j:66-1>=0; -k:67+((-1 + k:67) * (-1 + k:67))+1>=0;
    -__cost:70+(k:67 * __cost:70)>=0; -j:66+i:64-1>=0; k:67-1>=0|] post:
  [|-2m':2991-(m':2991 * m':2991)+((1 + m':2991) * (1 + m':2991))-1=0;
    -m':2991-(m':2991 * m':2991)+(m':2991 * (1 + m':2991))=0;
    -m':2991+k':3091-2=0; -m':2991+l':3019-1=0;
    -2m':2991-5(m':2991 * m':2991)
    +((1 + (2 * m':2991) + (m':2991 * m':2991)) * (1 + m':2991))-1>=0;
    -m':2991+j:66-2>=0; -m':2991+(m':2991 * m':2991)>=0; -j:66+i:64-1>=0;
    m':2991>=0;
    m':2991+(m':2991 * m':2991)-2__cost':2990
    +2((1 + m':2991)
   * ((-1/2 * m':2991) + (-1/2 * (m':2991 * m':2991)) + __cost':2990))>=0|]]>}
**** star transition: 
  {__cost := __cost':2990
   k := k':3091
   l := l':3019
   m := m':2991
   when ((!(0 <= K:3203) \/ mid_k:3207 = (k:67 + K:3203))
           /\ (!(0 <= K:3203) \/ mid___cost:3208 = __cost:70)
           /\ (!((0 <= K:3203 /\ K:3203 <= 0))
                 \/ (-mid_k:3207 + mid_l:3206) = (-k:67 + l:68))
           /\ (!(1 <= K:3203) \/ (-mid_k:3207 + mid_l:3206) = -1)
           /\ ((K:3203 = 0 /\ m:69 = mid_m:3205 /\ l:68 = mid_l:3206
                  /\ k:67 = mid_k:3207 /\ __cost:70 = mid___cost:3208)
                 \/ (1 <= K:3203 /\ 0 <= (-1 + -__cost:70)
                       /\ 0 <= (1 + -k:67) /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= k:67
                       /\ (1 + -mid_k:3207 + mid_l:3206) = 0
                       /\ 0 <= (-1 + -mid___cost:3208)
                       /\ 0 <= (2 + -mid_k:3207) /\ 0 <= (-mid_k:3207 + j:66)
                       /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= (-1 + mid_k:3207)))
           /\ (0 = K:3203 \/ !(-__cost:70 <= 0))
           /\ (!((0 <= K:3204 /\ K:3204 <= 0))
                 \/ l':3019 = (mid_l:3206 + K:3204))
           /\ (!(1 <= K:3204)
                 \/ l':3019 = (-1 + mid_l:3206 + mid_k:3207 + -mid_l:3206
                                 + K:3204))
           /\ (!(0 <= K:3204) \/ k':3091 = (mid_k:3207 + K:3204))
           /\ (!(0 <= K:3204)
                 \/ __cost':2990 = (mid___cost:3208 + (1/3 * K:3204)
                                      + -((mid_k:3207 * K:3204))
                                      + (1/2 * (mid_k:3207 * mid_k:3207)
                                           * K:3204)
                                      + (-1/2 * (K:3204 * K:3204))
                                      + (1/2 * mid_k:3207 * (K:3204 * K:3204))
                                      + (1/6 * (K:3204 * (K:3204 * K:3204)))))
           /\ (!((0 <= K:3204 /\ K:3204 <= 0))
                 \/ ((6 * __cost':2990) + l':3019) <= (((6 * mid___cost:3208)
                                                          + mid_l:3206)
                                                         + (3/2 * K:3204)
                                                         + (-1/2 * mid_k:3207
                                                              * K:3204)
                                                         + (-3/2
                                                              * (mid_k:3207
                                                                   * mid_k:3207)
                                                              * K:3204)
                                                         + ((mid_k:3207
                                                               * (mid_k:3207
                                                                    * mid_k:3207))
                                                              * K:3204)
                                                         + (-1/4
                                                              * (K:3204
                                                                   * K:3204))
                                                         + (-3/2 * mid_k:3207
                                                              * (K:3204
                                                                   * K:3204))
                                                         + (3/2
                                                              * (mid_k:3207
                                                                   * mid_k:3207)
                                                              * (K:3204
                                                                   * K:3204))
                                                         + (-1/2
                                                              * (K:3204
                                                                   * (
                                                                   K:3204
                                                                    * K:3204)))
                                                         + (mid_k:3207
                                                              * (K:3204
                                                                   * (
                                                                   K:3204
                                                                    * K:3204)))
                                                         + (1/4
                                                              * ((K:3204
                                                                    * K:3204)
                                                                   * (
                                                                   K:3204
                                                                    * K:3204)))))
           /\ (!(1 <= K:3204)
                 \/ ((6 * __cost':2990) + l':3019) <= (-1 + mid_k:3207
                                                         + ((6
                                                               * mid___cost:3208)
                                                              + mid_l:3206)
                                                         + -mid_l:3206
                                                         + (3/2 * K:3204)
                                                         + (-1/2 * mid_k:3207
                                                              * K:3204)
                                                         + (-3/2
                                                              * (mid_k:3207
                                                                   * mid_k:3207)
                                                              * K:3204)
                                                         + ((mid_k:3207
                                                               * (mid_k:3207
                                                                    * mid_k:3207))
                                                              * K:3204)
                                                         + (-1/4
                                                              * (K:3204
                                                                   * K:3204))
                                                         + (-3/2 * mid_k:3207
                                                              * (K:3204
                                                                   * K:3204))
                                                         + (3/2
                                                              * (mid_k:3207
                                                                   * mid_k:3207)
                                                              * (K:3204
                                                                   * K:3204))
                                                         + (-1/2
                                                              * (K:3204
                                                                   * (
                                                                   K:3204
                                                                    * K:3204)))
                                                         + (mid_k:3207
                                                              * (K:3204
                                                                   * (
                                                                   K:3204
                                                                    * K:3204)))
                                                         + (1/4
                                                              * ((K:3204
                                                                    * K:3204)
                                                                   * (
                                                                   K:3204
                                                                    * K:3204)))))
           /\ (!((0 <= K:3204 /\ K:3204 <= 0))
                 \/ l':3019 <= (mid_l:3206 + (1/2 * K:3204) + (j:66 * K:3204)
                                  + -((mid_k:3207 * K:3204))
                                  + (-1/2 * (K:3204 * K:3204))))
           /\ (!(1 <= K:3204)
                 \/ l':3019 <= (-1 + mid_k:3207 + mid_l:3206 + -mid_l:3206
                                  + (1/2 * K:3204) + (j:66 * K:3204)
                                  + -((mid_k:3207 * K:3204))
                                  + (-1/2 * (K:3204 * K:3204))))
           /\ (!((0 <= K:3204 /\ K:3204 <= 0))
                 \/ (-__cost':2990 + l':3019) <= ((-mid___cost:3208
                                                     + mid_l:3206)
                                                    + (5/2 * K:3204)
                                                    + -((mid_k:3207 * K:3204))
                                                    + (-1/2
                                                         * (K:3204 * K:3204))))
           /\ (!(1 <= K:3204)
                 \/ (-__cost':2990 + l':3019) <= (-1 + mid_k:3207
                                                    + (-mid___cost:3208
                                                         + mid_l:3206)
                                                    + -mid_l:3206
                                                    + (5/2 * K:3204)
                                                    + -((mid_k:3207 * K:3204))
                                                    + (-1/2
                                                         * (K:3204 * K:3204))))
           /\ (!(0 <= K:3204) \/ -__cost':2990 <= -mid___cost:3208)
           /\ (!((0 <= K:3204 /\ K:3204 <= 0))
                 \/ -l':3019 <= (-mid_l:3206 + (-3/2 * K:3204)
                                   + (mid_k:3207 * K:3204)
                                   + (1/2 * (K:3204 * K:3204))))
           /\ (!(1 <= K:3204)
                 \/ -l':3019 <= (1 + mid_l:3206 + -mid_l:3206 + -mid_k:3207
                                   + (-3/2 * K:3204) + (mid_k:3207 * K:3204)
                                   + (1/2 * (K:3204 * K:3204))))
           /\ (!((0 <= K:3204 /\ K:3204 <= 0))
                 \/ ((10 * __cost':2990) + (-3 * l':3019)) <= (((10
                                                                   * mid___cost:3208)
                                                                  + (
                                                                  -3
                                                                    * mid_l:3206))
                                                                 + (-9/2
                                                                    * K:3204)
                                                                 + (7/2
                                                                    * mid_k:3207
                                                                    * K:3204)
                                                                 + (-3/2
                                                                    * (
                                                                    mid_k:3207
                                                                    * mid_k:3207)
                                                                    * K:3204)
                                                                 + ((mid_k:3207
                                                                    * (mid_k:3207
                                                                    * mid_k:3207))
                                                                    * K:3204)
                                                                 + (7/4
                                                                    * (
                                                                    K:3204
                                                                    * K:3204))
                                                                 + (-3/2
                                                                    * mid_k:3207
                                                                    * (
                                                                    K:3204
                                                                    * K:3204))
                                                                 + (3/2
                                                                    * (
                                                                    mid_k:3207
                                                                    * mid_k:3207)
                                                                    * (
                                                                    K:3204
                                                                    * K:3204))
                                                                 + (-1/2
                                                                    * (
                                                                    K:3204
                                                                    * (
                                                                    K:3204
                                                                    * K:3204)))
                                                                 + (mid_k:3207
                                                                    * (
                                                                    K:3204
                                                                    * (
                                                                    K:3204
                                                                    * K:3204)))
                                                                 + (1/4
                                                                    * (
                                                                    (K:3204
                                                                    * K:3204)
                                                                    * (
                                                                    K:3204
                                                                    * K:3204)))))
           /\ (!(1 <= K:3204)
                 \/ ((10 * __cost':2990) + (-3 * l':3019)) <= (3
                                                                 + ((10
                                                                    * mid___cost:3208)
                                                                    + (
                                                                    -3
                                                                    * mid_l:3206))
                                                                 + (3
                                                                    * mid_l:3206)
                                                                 + (-3
                                                                    * mid_k:3207)
                                                                 + (-9/2
                                                                    * K:3204)
                                                                 + (7/2
                                                                    * mid_k:3207
                                                                    * K:3204)
                                                                 + (-3/2
                                                                    * (
                                                                    mid_k:3207
                                                                    * mid_k:3207)
                                                                    * K:3204)
                                                                 + ((mid_k:3207
                                                                    * (mid_k:3207
                                                                    * mid_k:3207))
                                                                    * K:3204)
                                                                 + (7/4
                                                                    * (
                                                                    K:3204
                                                                    * K:3204))
                                                                 + (-3/2
                                                                    * mid_k:3207
                                                                    * (
                                                                    K:3204
                                                                    * K:3204))
                                                                 + (3/2
                                                                    * (
                                                                    mid_k:3207
                                                                    * mid_k:3207)
                                                                    * (
                                                                    K:3204
                                                                    * K:3204))
                                                                 + (-1/2
                                                                    * (
                                                                    K:3204
                                                                    * (
                                                                    K:3204
                                                                    * K:3204)))
                                                                 + (mid_k:3207
                                                                    * (
                                                                    K:3204
                                                                    * (
                                                                    K:3204
                                                                    * K:3204)))
                                                                 + (1/4
                                                                    * (
                                                                    (K:3204
                                                                    * K:3204)
                                                                    * (
                                                                    K:3204
                                                                    * K:3204)))))
           /\ ((K:3204 = 0 /\ mid_m:3205 = m':2991 /\ mid_l:3206 = l':3019
                  /\ mid_k:3207 = k':3091 /\ mid___cost:3208 = __cost':2990)
                 \/ (1 <= K:3204
                       /\ (1 + (-2 * mid_k:3207)
                             + -(((-1 + mid_k:3207) * (-1 + mid_k:3207)))
                             + (mid_k:3207 * mid_k:3207)) = 0
                       /\ (1 + -mid_k:3207
                             + -(((-1 + mid_k:3207) * (-1 + mid_k:3207)))
                             + ((-1 + mid_k:3207) * mid_k:3207)) = 0
                       /\ 0 <= (3 + (-4 * mid_k:3207)
                                  + (-3
                                       * ((-1 + mid_k:3207)
                                            * (-1 + mid_k:3207)))
                                  + ((mid_k:3207 * mid_k:3207) * mid_k:3207))
                       /\ 0 <= (5 + (-2 * mid_k:3207)
                                  + (-5
                                       * ((-1 + mid_k:3207)
                                            * (-1 + mid_k:3207)))
                                  + ((mid_k:3207 * mid_k:3207) * mid_k:3207))
                       /\ 0 <= (-1 + -mid_k:3207 + j:66)
                       /\ 0 <= (1 + -mid_k:3207
                                  + ((-1 + mid_k:3207) * (-1 + mid_k:3207)))
                       /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (mid_k:3207 * mid___cost:3208)
                       /\ 0 <= mid___cost:3208 /\ 0 <= mid_k:3207
                       /\ 0 <= (-1 + mid_k:3207
                                  + ((-1 + mid_k:3207) * (-1 + mid_k:3207)))
                       /\ (1 + (-2 * l':3019)
                             + -(((-1 + l':3019) * (-1 + l':3019)))
                             + (l':3019 * l':3019)) = 0
                       /\ (1 + -l':3019
                             + -(((-1 + l':3019) * (-1 + l':3019)))
                             + ((-1 + l':3019) * l':3019)) = 0
                       /\ (-1 + -l':3019 + k':3091) = 0
                       /\ 0 <= (3 + (-4 * l':3019)
                                  + (-3 * ((-1 + l':3019) * (-1 + l':3019)))
                                  + ((l':3019 * l':3019) * l':3019))
                       /\ 0 <= (5 + (-2 * l':3019)
                                  + (-5 * ((-1 + l':3019) * (-1 + l':3019)))
                                  + ((l':3019 * l':3019) * l':3019))
                       /\ 0 <= (1 + -l':3019
                                  + -(((-1 + l':3019) * (-1 + l':3019)))
                                  + (2 * __cost':2990))
                       /\ 0 <= (-1 + -l':3019 + j:66)
                       /\ 0 <= (1 + -l':3019
                                  + ((-1 + l':3019) * (-1 + l':3019)))
                       /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (l':3019
                                  * ((1/2 * l':3019)
                                       + (-1/2 * (l':3019 * l':3019))
                                       + __cost':2990)) /\ 0 <= l':3019
                       /\ 0 <= (-1 + l':3019
                                  + ((-1 + l':3019) * (-1 + l':3019)))))
           /\ (0 = K:3204 \/ -mid___cost:3208 <= 0)
           /\ (K:3203 + K:3204) = K:3202
           /\ (!((0 <= K:3209 /\ K:3209 <= 0))
                 \/ mid_l:3212 = (l:68 + K:3209))
           /\ (!(1 <= K:3209)
                 \/ mid_l:3212 = (-1 + l:68 + k:67 + -l:68 + K:3209))
           /\ (!(0 <= K:3209) \/ mid_k:3213 = (k:67 + K:3209))
           /\ (!(0 <= K:3209)
                 \/ mid___cost:3214 = (__cost:70 + (1/3 * K:3209)
                                         + -((k:67 * K:3209))
                                         + (1/2 * (k:67 * k:67) * K:3209)
                                         + (-1/2 * (K:3209 * K:3209))
                                         + (1/2 * k:67 * (K:3209 * K:3209))
                                         + (1/6
                                              * (K:3209 * (K:3209 * K:3209)))))
           /\ (!((0 <= K:3209 /\ K:3209 <= 0))
                 \/ ((6 * mid___cost:3214) + mid_l:3212) <= (((6 * __cost:70)
                                                                + l:68)
                                                               + (3/2
                                                                    * K:3209)
                                                               + (-1/2 * k:67
                                                                    * K:3209)
                                                               + (-3/2
                                                                    * (
                                                                    k:67
                                                                    * k:67)
                                                                    * K:3209)
                                                               + ((k:67
                                                                    * (
                                                                    k:67
                                                                    * k:67))
                                                                    * K:3209)
                                                               + (-1/4
                                                                    * (
                                                                    K:3209
                                                                    * K:3209))
                                                               + (-3/2 * k:67
                                                                    * (
                                                                    K:3209
                                                                    * K:3209))
                                                               + (3/2
                                                                    * (
                                                                    k:67
                                                                    * k:67)
                                                                    * (
                                                                    K:3209
                                                                    * K:3209))
                                                               + (-1/2
                                                                    * (
                                                                    K:3209
                                                                    * (
                                                                    K:3209
                                                                    * K:3209)))
                                                               + (k:67
                                                                    * (
                                                                    K:3209
                                                                    * (
                                                                    K:3209
                                                                    * K:3209)))
                                                               + (1/4
                                                                    * (
                                                                    (K:3209
                                                                    * K:3209)
                                                                    * (
                                                                    K:3209
                                                                    * K:3209)))))
           /\ (!(1 <= K:3209)
                 \/ ((6 * mid___cost:3214) + mid_l:3212) <= (-1 + k:67
                                                               + ((6
                                                                    * __cost:70)
                                                                    + l:68)
                                                               + -l:68
                                                               + (3/2
                                                                    * K:3209)
                                                               + (-1/2 * k:67
                                                                    * K:3209)
                                                               + (-3/2
                                                                    * (
                                                                    k:67
                                                                    * k:67)
                                                                    * K:3209)
                                                               + ((k:67
                                                                    * (
                                                                    k:67
                                                                    * k:67))
                                                                    * K:3209)
                                                               + (-1/4
                                                                    * (
                                                                    K:3209
                                                                    * K:3209))
                                                               + (-3/2 * k:67
                                                                    * (
                                                                    K:3209
                                                                    * K:3209))
                                                               + (3/2
                                                                    * (
                                                                    k:67
                                                                    * k:67)
                                                                    * (
                                                                    K:3209
                                                                    * K:3209))
                                                               + (-1/2
                                                                    * (
                                                                    K:3209
                                                                    * (
                                                                    K:3209
                                                                    * K:3209)))
                                                               + (k:67
                                                                    * (
                                                                    K:3209
                                                                    * (
                                                                    K:3209
                                                                    * K:3209)))
                                                               + (1/4
                                                                    * (
                                                                    (K:3209
                                                                    * K:3209)
                                                                    * (
                                                                    K:3209
                                                                    * K:3209)))))
           /\ (!((0 <= K:3209 /\ K:3209 <= 0))
                 \/ mid_l:3212 <= (l:68 + (1/2 * K:3209) + (j:66 * K:3209)
                                     + -((k:67 * K:3209))
                                     + (-1/2 * (K:3209 * K:3209))))
           /\ (!(1 <= K:3209)
                 \/ mid_l:3212 <= (-1 + k:67 + l:68 + -l:68 + (1/2 * K:3209)
                                     + (j:66 * K:3209) + -((k:67 * K:3209))
                                     + (-1/2 * (K:3209 * K:3209))))
           /\ (!((0 <= K:3209 /\ K:3209 <= 0))
                 \/ (-mid___cost:3214 + mid_l:3212) <= ((-__cost:70 + l:68)
                                                          + (5/2 * K:3209)
                                                          + -((k:67 * K:3209))
                                                          + (-1/2
                                                               * (K:3209
                                                                    * K:3209))))
           /\ (!(1 <= K:3209)
                 \/ (-mid___cost:3214 + mid_l:3212) <= (-1 + k:67
                                                          + (-__cost:70
                                                               + l:68)
                                                          + -l:68
                                                          + (5/2 * K:3209)
                                                          + -((k:67 * K:3209))
                                                          + (-1/2
                                                               * (K:3209
                                                                    * K:3209))))
           /\ (!(0 <= K:3209) \/ -mid___cost:3214 <= -__cost:70)
           /\ (!((0 <= K:3209 /\ K:3209 <= 0))
                 \/ -mid_l:3212 <= (-l:68 + (-3/2 * K:3209) + (k:67 * K:3209)
                                      + (1/2 * (K:3209 * K:3209))))
           /\ (!(1 <= K:3209)
                 \/ -mid_l:3212 <= (1 + l:68 + -l:68 + -k:67
                                      + (-3/2 * K:3209) + (k:67 * K:3209)
                                      + (1/2 * (K:3209 * K:3209))))
           /\ (!((0 <= K:3209 /\ K:3209 <= 0))
                 \/ ((10 * mid___cost:3214) + (-3 * mid_l:3212)) <= (
                    ((10 * __cost:70) + (-3 * l:68)) + (-9/2 * K:3209)
                      + (7/2 * k:67 * K:3209)
                      + (-3/2 * (k:67 * k:67) * K:3209)
                      + ((k:67 * (k:67 * k:67)) * K:3209)
                      + (7/4 * (K:3209 * K:3209))
                      + (-3/2 * k:67 * (K:3209 * K:3209))
                      + (3/2 * (k:67 * k:67) * (K:3209 * K:3209))
                      + (-1/2 * (K:3209 * (K:3209 * K:3209)))
                      + (k:67 * (K:3209 * (K:3209 * K:3209)))
                      + (1/4 * ((K:3209 * K:3209) * (K:3209 * K:3209)))))
           /\ (!(1 <= K:3209)
                 \/ ((10 * mid___cost:3214) + (-3 * mid_l:3212)) <= (
                    3 + ((10 * __cost:70) + (-3 * l:68)) + (3 * l:68)
                      + (-3 * k:67) + (-9/2 * K:3209) + (7/2 * k:67 * K:3209)
                      + (-3/2 * (k:67 * k:67) * K:3209)
                      + ((k:67 * (k:67 * k:67)) * K:3209)
                      + (7/4 * (K:3209 * K:3209))
                      + (-3/2 * k:67 * (K:3209 * K:3209))
                      + (3/2 * (k:67 * k:67) * (K:3209 * K:3209))
                      + (-1/2 * (K:3209 * (K:3209 * K:3209)))
                      + (k:67 * (K:3209 * (K:3209 * K:3209)))
                      + (1/4 * ((K:3209 * K:3209) * (K:3209 * K:3209)))))
           /\ ((K:3209 = 0 /\ m:69 = mid_m:3211 /\ l:68 = mid_l:3212
                  /\ k:67 = mid_k:3213 /\ __cost:70 = mid___cost:3214)
                 \/ (1 <= K:3209
                       /\ (1 + (-2 * k:67) + -(((-1 + k:67) * (-1 + k:67)))
                             + (k:67 * k:67)) = 0
                       /\ (1 + -k:67 + -(((-1 + k:67) * (-1 + k:67)))
                             + ((-1 + k:67) * k:67)) = 0
                       /\ 0 <= (3 + (-4 * k:67)
                                  + (-3 * ((-1 + k:67) * (-1 + k:67)))
                                  + ((k:67 * k:67) * k:67))
                       /\ 0 <= (5 + (-2 * k:67)
                                  + (-5 * ((-1 + k:67) * (-1 + k:67)))
                                  + ((k:67 * k:67) * k:67))
                       /\ 0 <= (-1 + -k:67 + j:66)
                       /\ 0 <= (1 + -k:67 + ((-1 + k:67) * (-1 + k:67)))
                       /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= (k:67 * __cost:70)
                       /\ 0 <= __cost:70 /\ 0 <= k:67
                       /\ 0 <= (-1 + k:67 + ((-1 + k:67) * (-1 + k:67)))
                       /\ (1 + (-2 * mid_l:3212)
                             + -(((-1 + mid_l:3212) * (-1 + mid_l:3212)))
                             + (mid_l:3212 * mid_l:3212)) = 0
                       /\ (1 + -mid_l:3212
                             + -(((-1 + mid_l:3212) * (-1 + mid_l:3212)))
                             + ((-1 + mid_l:3212) * mid_l:3212)) = 0
                       /\ (-1 + -mid_l:3212 + mid_k:3213) = 0
                       /\ 0 <= (3 + (-4 * mid_l:3212)
                                  + (-3
                                       * ((-1 + mid_l:3212)
                                            * (-1 + mid_l:3212)))
                                  + ((mid_l:3212 * mid_l:3212) * mid_l:3212))
                       /\ 0 <= (5 + (-2 * mid_l:3212)
                                  + (-5
                                       * ((-1 + mid_l:3212)
                                            * (-1 + mid_l:3212)))
                                  + ((mid_l:3212 * mid_l:3212) * mid_l:3212))
                       /\ 0 <= (1 + -mid_l:3212
                                  + -(((-1 + mid_l:3212) * (-1 + mid_l:3212)))
                                  + (2 * mid___cost:3214))
                       /\ 0 <= (-1 + -mid_l:3212 + j:66)
                       /\ 0 <= (1 + -mid_l:3212
                                  + ((-1 + mid_l:3212) * (-1 + mid_l:3212)))
                       /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (mid_l:3212
                                  * ((1/2 * mid_l:3212)
                                       + (-1/2 * (mid_l:3212 * mid_l:3212))
                                       + mid___cost:3214)) /\ 0 <= mid_l:3212
                       /\ 0 <= (-1 + mid_l:3212
                                  + ((-1 + mid_l:3212) * (-1 + mid_l:3212)))))
           /\ (0 = K:3209 \/ !((1 + __cost:70) <= 0))
           /\ (!(0 <= K:3210) \/ k':3091 = (mid_k:3213 + K:3210))
           /\ (!(0 <= K:3210) \/ __cost':2990 = mid___cost:3214)
           /\ (!((0 <= K:3210 /\ K:3210 <= 0))
                 \/ (-k':3091 + l':3019) = (-mid_k:3213 + mid_l:3212))
           /\ (!(1 <= K:3210) \/ (-k':3091 + l':3019) = -1)
           /\ ((K:3210 = 0 /\ mid_m:3211 = m':2991 /\ mid_l:3212 = l':3019
                  /\ mid_k:3213 = k':3091 /\ mid___cost:3214 = __cost':2990)
                 \/ (1 <= K:3210 /\ 0 <= (-1 + -mid___cost:3214)
                       /\ 0 <= (1 + -mid_k:3213)
                       /\ 0 <= (-1 + -mid_k:3213 + j:66)
                       /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= mid_k:3213
                       /\ (1 + -k':3091 + l':3019) = 0
                       /\ 0 <= (-1 + -__cost':2990) /\ 0 <= (2 + -k':3091)
                       /\ 0 <= (-k':3091 + j:66) /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (-1 + k':3091)))
           /\ (0 = K:3210 \/ (1 + mid___cost:3214) <= 0)
           /\ (K:3209 + K:3210) = K:3202
           /\ (!(0 <= K:3215) \/ mid___cost:3220 = __cost:70)
           /\ (!(0 <= K:3215) \/ mid_m:3217 = m:69)
           /\ (!((0 <= K:3215 /\ K:3215 <= 0)) \/ mid_k:3219 = k:67)
           /\ (!(1 <= K:3215) \/ mid_k:3219 = 1)
           /\ (!((0 <= K:3215 /\ K:3215 <= 0)) \/ mid_l:3218 = l:68)
           /\ (!(1 <= K:3215) \/ mid_l:3218 = 0)
           /\ ((K:3215 = 0 /\ m:69 = mid_m:3217 /\ l:68 = mid_l:3218
                  /\ k:67 = mid_k:3219 /\ __cost:70 = mid___cost:3220)
                 \/ (1 <= K:3215 /\ k:67 = 0 /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (-1 + j:66) /\ (-1 + mid_k:3219) = 0
                       /\ mid_l:3218 = 0 /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (-1 + j:66)))
           /\ (0 = K:3215 \/ !((1 + -k:67) <= 0))
           /\ (!((0 <= K:3216 /\ K:3216 <= 0))
                 \/ l':3019 = (mid_l:3218 + K:3216))
           /\ (!(1 <= K:3216)
                 \/ l':3019 = (-1 + mid_l:3218 + mid_k:3219 + -mid_l:3218
                                 + K:3216))
           /\ (!((0 <= K:3216 /\ K:3216 <= 0))
                 \/ m':2991 = (mid_m:3217 + K:3216))
           /\ (!(1 <= K:3216)
                 \/ m':2991 = (-2 + mid_m:3217 + mid_k:3219 + -mid_m:3217
                                 + K:3216))
           /\ (!(0 <= K:3216) \/ k':3091 = (mid_k:3219 + K:3216))
           /\ (!(0 <= K:3216)
                 \/ __cost':2990 = (mid___cost:3220 + (1/3 * K:3216)
                                      + -((mid_k:3219 * K:3216))
                                      + (1/2 * (mid_k:3219 * mid_k:3219)
                                           * K:3216)
                                      + (-1/2 * (K:3216 * K:3216))
                                      + (1/2 * mid_k:3219 * (K:3216 * K:3216))
                                      + (1/6 * (K:3216 * (K:3216 * K:3216)))))
           /\ (!((0 <= K:3216 /\ K:3216 <= 0))
                 \/ l':3019 <= (mid_l:3218 + (1/2 * K:3216) + (j:66 * K:3216)
                                  + -((mid_k:3219 * K:3216))
                                  + (-1/2 * (K:3216 * K:3216))))
           /\ (!(1 <= K:3216)
                 \/ l':3019 <= (-1 + mid_k:3219 + mid_l:3218 + -mid_l:3218
                                  + (1/2 * K:3216) + (j:66 * K:3216)
                                  + -((mid_k:3219 * K:3216))
                                  + (-1/2 * (K:3216 * K:3216))))
           /\ (!((0 <= K:3216 /\ K:3216 <= 0))
                 \/ (-__cost':2990 + l':3019) <= ((-mid___cost:3220
                                                     + mid_l:3218)
                                                    + (5/2 * K:3216)
                                                    + -((mid_k:3219 * K:3216))
                                                    + (-1/2
                                                         * (K:3216 * K:3216))))
           /\ (!(1 <= K:3216)
                 \/ (-__cost':2990 + l':3019) <= (-1 + mid_k:3219
                                                    + (-mid___cost:3220
                                                         + mid_l:3218)
                                                    + -mid_l:3218
                                                    + (5/2 * K:3216)
                                                    + -((mid_k:3219 * K:3216))
                                                    + (-1/2
                                                         * (K:3216 * K:3216))))
           /\ (!((0 <= K:3216 /\ K:3216 <= 0))
                 \/ -l':3019 <= (-mid_l:3218 + (-5/2 * K:3216)
                                   + (mid_k:3219 * K:3216)
                                   + (1/2 * (K:3216 * K:3216))))
           /\ (!(1 <= K:3216)
                 \/ -l':3019 <= (1 + mid_l:3218 + -mid_l:3218 + -mid_k:3219
                                   + (-5/2 * K:3216) + (mid_k:3219 * K:3216)
                                   + (1/2 * (K:3216 * K:3216))))
           /\ (!((0 <= K:3216 /\ K:3216 <= 0))
                 \/ ((10 * __cost':2990) + (-3 * l':3019)) <= (((10
                                                                   * mid___cost:3220)
                                                                  + (
                                                                  -3
                                                                    * mid_l:3218))
                                                                 + (-17/2
                                                                    * K:3216)
                                                                 + (7/2
                                                                    * mid_k:3219
                                                                    * K:3216)
                                                                 + (-3/2
                                                                    * (
                                                                    mid_k:3219
                                                                    * mid_k:3219)
                                                                    * K:3216)
                                                                 + ((mid_k:3219
                                                                    * (mid_k:3219
                                                                    * mid_k:3219))
                                                                    * K:3216)
                                                                 + (7/4
                                                                    * (
                                                                    K:3216
                                                                    * K:3216))
                                                                 + (-3/2
                                                                    * mid_k:3219
                                                                    * (
                                                                    K:3216
                                                                    * K:3216))
                                                                 + (3/2
                                                                    * (
                                                                    mid_k:3219
                                                                    * mid_k:3219)
                                                                    * (
                                                                    K:3216
                                                                    * K:3216))
                                                                 + (-1/2
                                                                    * (
                                                                    K:3216
                                                                    * (
                                                                    K:3216
                                                                    * K:3216)))
                                                                 + (mid_k:3219
                                                                    * (
                                                                    K:3216
                                                                    * (
                                                                    K:3216
                                                                    * K:3216)))
                                                                 + (1/4
                                                                    * (
                                                                    (K:3216
                                                                    * K:3216)
                                                                    * (
                                                                    K:3216
                                                                    * K:3216)))))
           /\ (!(1 <= K:3216)
                 \/ ((10 * __cost':2990) + (-3 * l':3019)) <= (3
                                                                 + ((10
                                                                    * mid___cost:3220)
                                                                    + (
                                                                    -3
                                                                    * mid_l:3218))
                                                                 + (3
                                                                    * mid_l:3218)
                                                                 + (-3
                                                                    * mid_k:3219)
                                                                 + (-17/2
                                                                    * K:3216)
                                                                 + (7/2
                                                                    * mid_k:3219
                                                                    * K:3216)
                                                                 + (-3/2
                                                                    * (
                                                                    mid_k:3219
                                                                    * mid_k:3219)
                                                                    * K:3216)
                                                                 + ((mid_k:3219
                                                                    * (mid_k:3219
                                                                    * mid_k:3219))
                                                                    * K:3216)
                                                                 + (7/4
                                                                    * (
                                                                    K:3216
                                                                    * K:3216))
                                                                 + (-3/2
                                                                    * mid_k:3219
                                                                    * (
                                                                    K:3216
                                                                    * K:3216))
                                                                 + (3/2
                                                                    * (
                                                                    mid_k:3219
                                                                    * mid_k:3219)
                                                                    * (
                                                                    K:3216
                                                                    * K:3216))
                                                                 + (-1/2
                                                                    * (
                                                                    K:3216
                                                                    * (
                                                                    K:3216
                                                                    * K:3216)))
                                                                 + (mid_k:3219
                                                                    * (
                                                                    K:3216
                                                                    * (
                                                                    K:3216
                                                                    * K:3216)))
                                                                 + (1/4
                                                                    * (
                                                                    (K:3216
                                                                    * K:3216)
                                                                    * (
                                                                    K:3216
                                                                    * K:3216)))))
           /\ ((K:3216 = 0 /\ mid_m:3217 = m':2991 /\ mid_l:3218 = l':3019
                  /\ mid_k:3219 = k':3091 /\ mid___cost:3220 = __cost':2990)
                 \/ (1 <= K:3216
                       /\ (1 + (-2 * mid_k:3219)
                             + -(((-1 + mid_k:3219) * (-1 + mid_k:3219)))
                             + (mid_k:3219 * mid_k:3219)) = 0
                       /\ (1 + -mid_k:3219
                             + -(((-1 + mid_k:3219) * (-1 + mid_k:3219)))
                             + ((-1 + mid_k:3219) * mid_k:3219)) = 0
                       /\ 0 <= (1 + (-2 * mid_k:3219)
                                  + (-5
                                       * ((-1 + mid_k:3219)
                                            * (-1 + mid_k:3219)))
                                  + ((mid_k:3219 * mid_k:3219) * mid_k:3219))
                       /\ 0 <= (-1 + -mid_k:3219 + j:66)
                       /\ 0 <= (1 + -mid_k:3219
                                  + ((-1 + mid_k:3219) * (-1 + mid_k:3219)))
                       /\ 0 <= (-mid___cost:3220
                                  + (mid_k:3219 * mid___cost:3220))
                       /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= (-1 + mid_k:3219)
                       /\ (-1 + (-2 * m':2991) + -((m':2991 * m':2991))
                             + ((1 + m':2991) * (1 + m':2991))) = 0
                       /\ (-m':2991 + -((m':2991 * m':2991))
                             + (m':2991 * (1 + m':2991))) = 0
                       /\ (-2 + -m':2991 + k':3091) = 0
                       /\ (-1 + -m':2991 + l':3019) = 0
                       /\ 0 <= (-1 + (-2 * m':2991)
                                  + (-5 * (m':2991 * m':2991))
                                  + ((1 + (2 * m':2991) + (m':2991 * m':2991))
                                       * (1 + m':2991)))
                       /\ 0 <= (-2 + -m':2991 + j:66)
                       /\ 0 <= (-m':2991 + (m':2991 * m':2991))
                       /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= m':2991
                       /\ 0 <= (m':2991 + (m':2991 * m':2991)
                                  + (-2 * __cost':2990)
                                  + (2
                                       * ((1 + m':2991)
                                            * ((-1/2 * m':2991)
                                                 + (-1/2
                                                      * (m':2991 * m':2991))
                                                 + __cost':2990))))))
           /\ (0 = K:3216 \/ (1 + -mid_k:3219) <= 0)
           /\ (K:3215 + K:3216) = K:3202 /\ 0 <= K:3202)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':3252
 j := (j:66 + 1)
 k := k':3251
 l := l':3250
 m := m':3253
 when (0 <= j:66 /\ 0 <= i:64 /\ i:64 < n:65 /\ j:66 < i:64
         /\ (!(0 <= K:3244) \/ mid_k:3245 = K:3244)
         /\ (!(0 <= K:3244) \/ mid___cost:3246 = __cost:70)
         /\ (!((0 <= K:3244 /\ K:3244 <= 0))
               \/ (-mid_k:3245 + mid_l:3247) = l:68)
         /\ (!(1 <= K:3244) \/ (-mid_k:3245 + mid_l:3247) = -1)
         /\ ((K:3244 = 0 /\ m:69 = mid_m:3248 /\ l:68 = mid_l:3247
                /\ 0 = mid_k:3245 /\ __cost:70 = mid___cost:3246)
               \/ (1 <= K:3244 /\ 0 <= (-1 + -__cost:70) /\ 0 <= (-1 + j:66)
                     /\ 0 <= (-1 + -j:66 + i:64)
                     /\ (1 + -mid_k:3245 + mid_l:3247) = 0
                     /\ 0 <= (-1 + -mid___cost:3246)
                     /\ 0 <= (2 + -mid_k:3245) /\ 0 <= (-mid_k:3245 + j:66)
                     /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= (-1 + mid_k:3245)))
         /\ (0 = K:3244 \/ !(-__cost:70 <= 0))
         /\ (!((0 <= K:3249 /\ K:3249 <= 0))
               \/ l':3250 = (mid_l:3247 + K:3249))
         /\ (!(1 <= K:3249)
               \/ l':3250 = (-1 + mid_l:3247 + mid_k:3245 + -mid_l:3247
                               + K:3249))
         /\ (!(0 <= K:3249) \/ k':3251 = (mid_k:3245 + K:3249))
         /\ (!(0 <= K:3249)
               \/ __cost':3252 = (mid___cost:3246 + (1/3 * K:3249)
                                    + -((mid_k:3245 * K:3249))
                                    + (1/2 * (mid_k:3245 * mid_k:3245)
                                         * K:3249)
                                    + (-1/2 * (K:3249 * K:3249))
                                    + (1/2 * mid_k:3245 * (K:3249 * K:3249))
                                    + (1/6 * (K:3249 * (K:3249 * K:3249)))))
         /\ (!((0 <= K:3249 /\ K:3249 <= 0))
               \/ ((6 * __cost':3252) + l':3250) <= (((6 * mid___cost:3246)
                                                        + mid_l:3247)
                                                       + (3/2 * K:3249)
                                                       + (-1/2 * mid_k:3245
                                                            * K:3249)
                                                       + (-3/2
                                                            * (mid_k:3245
                                                                 * mid_k:3245)
                                                            * K:3249)
                                                       + ((mid_k:3245
                                                             * (mid_k:3245
                                                                  * mid_k:3245))
                                                            * K:3249)
                                                       + (-1/4
                                                            * (K:3249
                                                                 * K:3249))
                                                       + (-3/2 * mid_k:3245
                                                            * (K:3249
                                                                 * K:3249))
                                                       + (3/2
                                                            * (mid_k:3245
                                                                 * mid_k:3245)
                                                            * (K:3249
                                                                 * K:3249))
                                                       + (-1/2
                                                            * (K:3249
                                                                 * (K:3249
                                                                    * K:3249)))
                                                       + (mid_k:3245
                                                            * (K:3249
                                                                 * (K:3249
                                                                    * K:3249)))
                                                       + (1/4
                                                            * ((K:3249
                                                                  * K:3249)
                                                                 * (K:3249
                                                                    * K:3249)))))
         /\ (!(1 <= K:3249)
               \/ ((6 * __cost':3252) + l':3250) <= (-1 + mid_k:3245
                                                       + ((6
                                                             * mid___cost:3246)
                                                            + mid_l:3247)
                                                       + -mid_l:3247
                                                       + (3/2 * K:3249)
                                                       + (-1/2 * mid_k:3245
                                                            * K:3249)
                                                       + (-3/2
                                                            * (mid_k:3245
                                                                 * mid_k:3245)
                                                            * K:3249)
                                                       + ((mid_k:3245
                                                             * (mid_k:3245
                                                                  * mid_k:3245))
                                                            * K:3249)
                                                       + (-1/4
                                                            * (K:3249
                                                                 * K:3249))
                                                       + (-3/2 * mid_k:3245
                                                            * (K:3249
                                                                 * K:3249))
                                                       + (3/2
                                                            * (mid_k:3245
                                                                 * mid_k:3245)
                                                            * (K:3249
                                                                 * K:3249))
                                                       + (-1/2
                                                            * (K:3249
                                                                 * (K:3249
                                                                    * K:3249)))
                                                       + (mid_k:3245
                                                            * (K:3249
                                                                 * (K:3249
                                                                    * K:3249)))
                                                       + (1/4
                                                            * ((K:3249
                                                                  * K:3249)
                                                                 * (K:3249
                                                                    * K:3249)))))
         /\ (!((0 <= K:3249 /\ K:3249 <= 0))
               \/ l':3250 <= (mid_l:3247 + (1/2 * K:3249) + (j:66 * K:3249)
                                + -((mid_k:3245 * K:3249))
                                + (-1/2 * (K:3249 * K:3249))))
         /\ (!(1 <= K:3249)
               \/ l':3250 <= (-1 + mid_k:3245 + mid_l:3247 + -mid_l:3247
                                + (1/2 * K:3249) + (j:66 * K:3249)
                                + -((mid_k:3245 * K:3249))
                                + (-1/2 * (K:3249 * K:3249))))
         /\ (!((0 <= K:3249 /\ K:3249 <= 0))
               \/ (-__cost':3252 + l':3250) <= ((-mid___cost:3246
                                                   + mid_l:3247)
                                                  + (5/2 * K:3249)
                                                  + -((mid_k:3245 * K:3249))
                                                  + (-1/2 * (K:3249 * K:3249))))
         /\ (!(1 <= K:3249)
               \/ (-__cost':3252 + l':3250) <= (-1 + mid_k:3245
                                                  + (-mid___cost:3246
                                                       + mid_l:3247)
                                                  + -mid_l:3247
                                                  + (5/2 * K:3249)
                                                  + -((mid_k:3245 * K:3249))
                                                  + (-1/2 * (K:3249 * K:3249))))
         /\ (!(0 <= K:3249) \/ -__cost':3252 <= -mid___cost:3246)
         /\ (!((0 <= K:3249 /\ K:3249 <= 0))
               \/ -l':3250 <= (-mid_l:3247 + (-3/2 * K:3249)
                                 + (mid_k:3245 * K:3249)
                                 + (1/2 * (K:3249 * K:3249))))
         /\ (!(1 <= K:3249)
               \/ -l':3250 <= (1 + mid_l:3247 + -mid_l:3247 + -mid_k:3245
                                 + (-3/2 * K:3249) + (mid_k:3245 * K:3249)
                                 + (1/2 * (K:3249 * K:3249))))
         /\ (!((0 <= K:3249 /\ K:3249 <= 0))
               \/ ((10 * __cost':3252) + (-3 * l':3250)) <= (((10
                                                                 * mid___cost:3246)
                                                                + (-3
                                                                    * mid_l:3247))
                                                               + (-9/2
                                                                    * K:3249)
                                                               + (7/2
                                                                    * mid_k:3245
                                                                    * K:3249)
                                                               + (-3/2
                                                                    * (
                                                                    mid_k:3245
                                                                    * mid_k:3245)
                                                                    * K:3249)
                                                               + ((mid_k:3245
                                                                    * (
                                                                    mid_k:3245
                                                                    * mid_k:3245))
                                                                    * K:3249)
                                                               + (7/4
                                                                    * (
                                                                    K:3249
                                                                    * K:3249))
                                                               + (-3/2
                                                                    * mid_k:3245
                                                                    * (
                                                                    K:3249
                                                                    * K:3249))
                                                               + (3/2
                                                                    * (
                                                                    mid_k:3245
                                                                    * mid_k:3245)
                                                                    * (
                                                                    K:3249
                                                                    * K:3249))
                                                               + (-1/2
                                                                    * (
                                                                    K:3249
                                                                    * (
                                                                    K:3249
                                                                    * K:3249)))
                                                               + (mid_k:3245
                                                                    * (
                                                                    K:3249
                                                                    * (
                                                                    K:3249
                                                                    * K:3249)))
                                                               + (1/4
                                                                    * (
                                                                    (K:3249
                                                                    * K:3249)
                                                                    * (
                                                                    K:3249
                                                                    * K:3249)))))
         /\ (!(1 <= K:3249)
               \/ ((10 * __cost':3252) + (-3 * l':3250)) <= (3
                                                               + ((10
                                                                    * mid___cost:3246)
                                                                    + (
                                                                    -3
                                                                    * mid_l:3247))
                                                               + (3
                                                                    * mid_l:3247)
                                                               + (-3
                                                                    * mid_k:3245)
                                                               + (-9/2
                                                                    * K:3249)
                                                               + (7/2
                                                                    * mid_k:3245
                                                                    * K:3249)
                                                               + (-3/2
                                                                    * (
                                                                    mid_k:3245
                                                                    * mid_k:3245)
                                                                    * K:3249)
                                                               + ((mid_k:3245
                                                                    * (
                                                                    mid_k:3245
                                                                    * mid_k:3245))
                                                                    * K:3249)
                                                               + (7/4
                                                                    * (
                                                                    K:3249
                                                                    * K:3249))
                                                               + (-3/2
                                                                    * mid_k:3245
                                                                    * (
                                                                    K:3249
                                                                    * K:3249))
                                                               + (3/2
                                                                    * (
                                                                    mid_k:3245
                                                                    * mid_k:3245)
                                                                    * (
                                                                    K:3249
                                                                    * K:3249))
                                                               + (-1/2
                                                                    * (
                                                                    K:3249
                                                                    * (
                                                                    K:3249
                                                                    * K:3249)))
                                                               + (mid_k:3245
                                                                    * (
                                                                    K:3249
                                                                    * (
                                                                    K:3249
                                                                    * K:3249)))
                                                               + (1/4
                                                                    * (
                                                                    (K:3249
                                                                    * K:3249)
                                                                    * (
                                                                    K:3249
                                                                    * K:3249)))))
         /\ ((K:3249 = 0 /\ mid_m:3248 = m':3253 /\ mid_l:3247 = l':3250
                /\ mid_k:3245 = k':3251 /\ mid___cost:3246 = __cost':3252)
               \/ (1 <= K:3249
                     /\ (1 + (-2 * mid_k:3245)
                           + -(((-1 + mid_k:3245) * (-1 + mid_k:3245)))
                           + (mid_k:3245 * mid_k:3245)) = 0
                     /\ (1 + -mid_k:3245
                           + -(((-1 + mid_k:3245) * (-1 + mid_k:3245)))
                           + ((-1 + mid_k:3245) * mid_k:3245)) = 0
                     /\ 0 <= (3 + (-4 * mid_k:3245)
                                + (-3
                                     * ((-1 + mid_k:3245) * (-1 + mid_k:3245)))
                                + ((mid_k:3245 * mid_k:3245) * mid_k:3245))
                     /\ 0 <= (5 + (-2 * mid_k:3245)
                                + (-5
                                     * ((-1 + mid_k:3245) * (-1 + mid_k:3245)))
                                + ((mid_k:3245 * mid_k:3245) * mid_k:3245))
                     /\ 0 <= (-1 + -mid_k:3245 + j:66)
                     /\ 0 <= (1 + -mid_k:3245
                                + ((-1 + mid_k:3245) * (-1 + mid_k:3245)))
                     /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= (mid_k:3245 * mid___cost:3246)
                     /\ 0 <= mid___cost:3246 /\ 0 <= mid_k:3245
                     /\ 0 <= (-1 + mid_k:3245
                                + ((-1 + mid_k:3245) * (-1 + mid_k:3245)))
                     /\ (1 + (-2 * l':3250)
                           + -(((-1 + l':3250) * (-1 + l':3250)))
                           + (l':3250 * l':3250)) = 0
                     /\ (1 + -l':3250 + -(((-1 + l':3250) * (-1 + l':3250)))
                           + ((-1 + l':3250) * l':3250)) = 0
                     /\ (-1 + -l':3250 + k':3251) = 0
                     /\ 0 <= (3 + (-4 * l':3250)
                                + (-3 * ((-1 + l':3250) * (-1 + l':3250)))
                                + ((l':3250 * l':3250) * l':3250))
                     /\ 0 <= (5 + (-2 * l':3250)
                                + (-5 * ((-1 + l':3250) * (-1 + l':3250)))
                                + ((l':3250 * l':3250) * l':3250))
                     /\ 0 <= (1 + -l':3250
                                + -(((-1 + l':3250) * (-1 + l':3250)))
                                + (2 * __cost':3252))
                     /\ 0 <= (-1 + -l':3250 + j:66)
                     /\ 0 <= (1 + -l':3250
                                + ((-1 + l':3250) * (-1 + l':3250)))
                     /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= (l':3250
                                * ((1/2 * l':3250)
                                     + (-1/2 * (l':3250 * l':3250))
                                     + __cost':3252)) /\ 0 <= l':3250
                     /\ 0 <= (-1 + l':3250
                                + ((-1 + l':3250) * (-1 + l':3250)))))
         /\ (0 = K:3249 \/ -mid___cost:3246 <= 0)
         /\ (K:3244 + K:3249) = K:3254
         /\ (!((0 <= K:3255 /\ K:3255 <= 0)) \/ mid_l:3256 = (l:68 + K:3255))
         /\ (!(1 <= K:3255) \/ mid_l:3256 = (-1 + l:68 + -l:68 + K:3255))
         /\ (!(0 <= K:3255) \/ mid_k:3257 = K:3255)
         /\ (!(0 <= K:3255)
               \/ mid___cost:3258 = (__cost:70 + (1/3 * K:3255)
                                       + (-1/2 * (K:3255 * K:3255))
                                       + (1/6 * (K:3255 * (K:3255 * K:3255)))))
         /\ (!((0 <= K:3255 /\ K:3255 <= 0))
               \/ ((6 * mid___cost:3258) + mid_l:3256) <= (((6 * __cost:70)
                                                              + l:68)
                                                             + (3/2 * K:3255)
                                                             + (-1/4
                                                                  * (
                                                                  K:3255
                                                                    * K:3255))
                                                             + (-1/2
                                                                  * (
                                                                  K:3255
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))
                                                             + (1/4
                                                                  * (
                                                                  (K:3255
                                                                    * K:3255)
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))))
         /\ (!(1 <= K:3255)
               \/ ((6 * mid___cost:3258) + mid_l:3256) <= (-1
                                                             + ((6
                                                                   * __cost:70)
                                                                  + l:68)
                                                             + -l:68
                                                             + (3/2 * K:3255)
                                                             + (-1/4
                                                                  * (
                                                                  K:3255
                                                                    * K:3255))
                                                             + (-1/2
                                                                  * (
                                                                  K:3255
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))
                                                             + (1/4
                                                                  * (
                                                                  (K:3255
                                                                    * K:3255)
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))))
         /\ (!((0 <= K:3255 /\ K:3255 <= 0))
               \/ mid_l:3256 <= (l:68 + (1/2 * K:3255) + (j:66 * K:3255)
                                   + (-1/2 * (K:3255 * K:3255))))
         /\ (!(1 <= K:3255)
               \/ mid_l:3256 <= (-1 + l:68 + -l:68 + (1/2 * K:3255)
                                   + (j:66 * K:3255)
                                   + (-1/2 * (K:3255 * K:3255))))
         /\ (!((0 <= K:3255 /\ K:3255 <= 0))
               \/ (-mid___cost:3258 + mid_l:3256) <= ((-__cost:70 + l:68)
                                                        + (5/2 * K:3255)
                                                        + (-1/2
                                                             * (K:3255
                                                                  * K:3255))))
         /\ (!(1 <= K:3255)
               \/ (-mid___cost:3258 + mid_l:3256) <= (-1
                                                        + (-__cost:70 + l:68)
                                                        + -l:68
                                                        + (5/2 * K:3255)
                                                        + (-1/2
                                                             * (K:3255
                                                                  * K:3255))))
         /\ (!(0 <= K:3255) \/ -mid___cost:3258 <= -__cost:70)
         /\ (!((0 <= K:3255 /\ K:3255 <= 0))
               \/ -mid_l:3256 <= (-l:68 + (-3/2 * K:3255)
                                    + (1/2 * (K:3255 * K:3255))))
         /\ (!(1 <= K:3255)
               \/ -mid_l:3256 <= (1 + l:68 + -l:68 + (-3/2 * K:3255)
                                    + (1/2 * (K:3255 * K:3255))))
         /\ (!((0 <= K:3255 /\ K:3255 <= 0))
               \/ ((10 * mid___cost:3258) + (-3 * mid_l:3256)) <= (((10
                                                                    * __cost:70)
                                                                    + (
                                                                    -3 * l:68))
                                                                    + (
                                                                    -9/2
                                                                    * K:3255)
                                                                    + (
                                                                    7/4
                                                                    * (
                                                                    K:3255
                                                                    * K:3255))
                                                                    + (
                                                                    -1/2
                                                                    * (
                                                                    K:3255
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))
                                                                    + (
                                                                    1/4
                                                                    * (
                                                                    (K:3255
                                                                    * K:3255)
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))))
         /\ (!(1 <= K:3255)
               \/ ((10 * mid___cost:3258) + (-3 * mid_l:3256)) <= (3
                                                                    + (
                                                                    (10
                                                                    * __cost:70)
                                                                    + (
                                                                    -3 * l:68))
                                                                    + (
                                                                    3 * l:68)
                                                                    + (
                                                                    -9/2
                                                                    * K:3255)
                                                                    + (
                                                                    7/4
                                                                    * (
                                                                    K:3255
                                                                    * K:3255))
                                                                    + (
                                                                    -1/2
                                                                    * (
                                                                    K:3255
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))
                                                                    + (
                                                                    1/4
                                                                    * (
                                                                    (K:3255
                                                                    * K:3255)
                                                                    * (
                                                                    K:3255
                                                                    * K:3255)))))
         /\ ((K:3255 = 0 /\ m:69 = mid_m:3259 /\ l:68 = mid_l:3256
                /\ 0 = mid_k:3257 /\ __cost:70 = mid___cost:3258)
               \/ (1 <= K:3255 /\ (1 + -1) = 0 /\ (1 + -1) = 0
                     /\ 0 <= (3 + -3) /\ 0 <= (5 + -5) /\ 0 <= (-1 + j:66)
                     /\ 0 <= (1 + 1) /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= __cost:70 /\ 0 <= (-1 + 1)
                     /\ (1 + (-2 * mid_l:3256)
                           + -(((-1 + mid_l:3256) * (-1 + mid_l:3256)))
                           + (mid_l:3256 * mid_l:3256)) = 0
                     /\ (1 + -mid_l:3256
                           + -(((-1 + mid_l:3256) * (-1 + mid_l:3256)))
                           + ((-1 + mid_l:3256) * mid_l:3256)) = 0
                     /\ (-1 + -mid_l:3256 + mid_k:3257) = 0
                     /\ 0 <= (3 + (-4 * mid_l:3256)
                                + (-3
                                     * ((-1 + mid_l:3256) * (-1 + mid_l:3256)))
                                + ((mid_l:3256 * mid_l:3256) * mid_l:3256))
                     /\ 0 <= (5 + (-2 * mid_l:3256)
                                + (-5
                                     * ((-1 + mid_l:3256) * (-1 + mid_l:3256)))
                                + ((mid_l:3256 * mid_l:3256) * mid_l:3256))
                     /\ 0 <= (1 + -mid_l:3256
                                + -(((-1 + mid_l:3256) * (-1 + mid_l:3256)))
                                + (2 * mid___cost:3258))
                     /\ 0 <= (-1 + -mid_l:3256 + j:66)
                     /\ 0 <= (1 + -mid_l:3256
                                + ((-1 + mid_l:3256) * (-1 + mid_l:3256)))
                     /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= (mid_l:3256
                                * ((1/2 * mid_l:3256)
                                     + (-1/2 * (mid_l:3256 * mid_l:3256))
                                     + mid___cost:3258)) /\ 0 <= mid_l:3256
                     /\ 0 <= (-1 + mid_l:3256
                                + ((-1 + mid_l:3256) * (-1 + mid_l:3256)))))
         /\ (0 = K:3255 \/ !((1 + __cost:70) <= 0))
         /\ (!(0 <= K:3260) \/ k':3251 = (mid_k:3257 + K:3260))
         /\ (!(0 <= K:3260) \/ __cost':3252 = mid___cost:3258)
         /\ (!((0 <= K:3260 /\ K:3260 <= 0))
               \/ (-k':3251 + l':3250) = (-mid_k:3257 + mid_l:3256))
         /\ (!(1 <= K:3260) \/ (-k':3251 + l':3250) = -1)
         /\ ((K:3260 = 0 /\ mid_m:3259 = m':3253 /\ mid_l:3256 = l':3250
                /\ mid_k:3257 = k':3251 /\ mid___cost:3258 = __cost':3252)
               \/ (1 <= K:3260 /\ 0 <= (-1 + -mid___cost:3258)
                     /\ 0 <= (1 + -mid_k:3257)
                     /\ 0 <= (-1 + -mid_k:3257 + j:66)
                     /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= mid_k:3257
                     /\ (1 + -k':3251 + l':3250) = 0
                     /\ 0 <= (-1 + -__cost':3252) /\ 0 <= (2 + -k':3251)
                     /\ 0 <= (-k':3251 + j:66) /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= (-1 + k':3251)))
         /\ (0 = K:3260 \/ (1 + mid___cost:3258) <= 0)
         /\ (K:3255 + K:3260) = K:3254
         /\ (!(0 <= K:3261) \/ mid___cost:3262 = __cost:70)
         /\ (!(0 <= K:3261) \/ mid_m:3263 = m:69)
         /\ (!((0 <= K:3261 /\ K:3261 <= 0)) \/ mid_k:3264 = 0)
         /\ (!(1 <= K:3261) \/ mid_k:3264 = 1)
         /\ (!((0 <= K:3261 /\ K:3261 <= 0)) \/ mid_l:3265 = l:68)
         /\ (!(1 <= K:3261) \/ mid_l:3265 = 0)
         /\ ((K:3261 = 0 /\ m:69 = mid_m:3263 /\ l:68 = mid_l:3265
                /\ 0 = mid_k:3264 /\ __cost:70 = mid___cost:3262)
               \/ (1 <= K:3261 /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= (-1 + j:66) /\ (-1 + mid_k:3264) = 0
                     /\ mid_l:3265 = 0 /\ 0 <= (-1 + -j:66 + i:64)
                     /\ 0 <= (-1 + j:66)))
         /\ (!((0 <= K:3266 /\ K:3266 <= 0))
               \/ l':3250 = (mid_l:3265 + K:3266))
         /\ (!(1 <= K:3266)
               \/ l':3250 = (-1 + mid_l:3265 + mid_k:3264 + -mid_l:3265
                               + K:3266))
         /\ (!((0 <= K:3266 /\ K:3266 <= 0))
               \/ m':3253 = (mid_m:3263 + K:3266))
         /\ (!(1 <= K:3266)
               \/ m':3253 = (-2 + mid_m:3263 + mid_k:3264 + -mid_m:3263
                               + K:3266))
         /\ (!(0 <= K:3266) \/ k':3251 = (mid_k:3264 + K:3266))
         /\ (!(0 <= K:3266)
               \/ __cost':3252 = (mid___cost:3262 + (1/3 * K:3266)
                                    + -((mid_k:3264 * K:3266))
                                    + (1/2 * (mid_k:3264 * mid_k:3264)
                                         * K:3266)
                                    + (-1/2 * (K:3266 * K:3266))
                                    + (1/2 * mid_k:3264 * (K:3266 * K:3266))
                                    + (1/6 * (K:3266 * (K:3266 * K:3266)))))
         /\ (!((0 <= K:3266 /\ K:3266 <= 0))
               \/ l':3250 <= (mid_l:3265 + (1/2 * K:3266) + (j:66 * K:3266)
                                + -((mid_k:3264 * K:3266))
                                + (-1/2 * (K:3266 * K:3266))))
         /\ (!(1 <= K:3266)
               \/ l':3250 <= (-1 + mid_k:3264 + mid_l:3265 + -mid_l:3265
                                + (1/2 * K:3266) + (j:66 * K:3266)
                                + -((mid_k:3264 * K:3266))
                                + (-1/2 * (K:3266 * K:3266))))
         /\ (!((0 <= K:3266 /\ K:3266 <= 0))
               \/ (-__cost':3252 + l':3250) <= ((-mid___cost:3262
                                                   + mid_l:3265)
                                                  + (5/2 * K:3266)
                                                  + -((mid_k:3264 * K:3266))
                                                  + (-1/2 * (K:3266 * K:3266))))
         /\ (!(1 <= K:3266)
               \/ (-__cost':3252 + l':3250) <= (-1 + mid_k:3264
                                                  + (-mid___cost:3262
                                                       + mid_l:3265)
                                                  + -mid_l:3265
                                                  + (5/2 * K:3266)
                                                  + -((mid_k:3264 * K:3266))
                                                  + (-1/2 * (K:3266 * K:3266))))
         /\ (!((0 <= K:3266 /\ K:3266 <= 0))
               \/ -l':3250 <= (-mid_l:3265 + (-5/2 * K:3266)
                                 + (mid_k:3264 * K:3266)
                                 + (1/2 * (K:3266 * K:3266))))
         /\ (!(1 <= K:3266)
               \/ -l':3250 <= (1 + mid_l:3265 + -mid_l:3265 + -mid_k:3264
                                 + (-5/2 * K:3266) + (mid_k:3264 * K:3266)
                                 + (1/2 * (K:3266 * K:3266))))
         /\ (!((0 <= K:3266 /\ K:3266 <= 0))
               \/ ((10 * __cost':3252) + (-3 * l':3250)) <= (((10
                                                                 * mid___cost:3262)
                                                                + (-3
                                                                    * mid_l:3265))
                                                               + (-17/2
                                                                    * K:3266)
                                                               + (7/2
                                                                    * mid_k:3264
                                                                    * K:3266)
                                                               + (-3/2
                                                                    * (
                                                                    mid_k:3264
                                                                    * mid_k:3264)
                                                                    * K:3266)
                                                               + ((mid_k:3264
                                                                    * (
                                                                    mid_k:3264
                                                                    * mid_k:3264))
                                                                    * K:3266)
                                                               + (7/4
                                                                    * (
                                                                    K:3266
                                                                    * K:3266))
                                                               + (-3/2
                                                                    * mid_k:3264
                                                                    * (
                                                                    K:3266
                                                                    * K:3266))
                                                               + (3/2
                                                                    * (
                                                                    mid_k:3264
                                                                    * mid_k:3264)
                                                                    * (
                                                                    K:3266
                                                                    * K:3266))
                                                               + (-1/2
                                                                    * (
                                                                    K:3266
                                                                    * (
                                                                    K:3266
                                                                    * K:3266)))
                                                               + (mid_k:3264
                                                                    * (
                                                                    K:3266
                                                                    * (
                                                                    K:3266
                                                                    * K:3266)))
                                                               + (1/4
                                                                    * (
                                                                    (K:3266
                                                                    * K:3266)
                                                                    * (
                                                                    K:3266
                                                                    * K:3266)))))
         /\ (!(1 <= K:3266)
               \/ ((10 * __cost':3252) + (-3 * l':3250)) <= (3
                                                               + ((10
                                                                    * mid___cost:3262)
                                                                    + (
                                                                    -3
                                                                    * mid_l:3265))
                                                               + (3
                                                                    * mid_l:3265)
                                                               + (-3
                                                                    * mid_k:3264)
                                                               + (-17/2
                                                                    * K:3266)
                                                               + (7/2
                                                                    * mid_k:3264
                                                                    * K:3266)
                                                               + (-3/2
                                                                    * (
                                                                    mid_k:3264
                                                                    * mid_k:3264)
                                                                    * K:3266)
                                                               + ((mid_k:3264
                                                                    * (
                                                                    mid_k:3264
                                                                    * mid_k:3264))
                                                                    * K:3266)
                                                               + (7/4
                                                                    * (
                                                                    K:3266
                                                                    * K:3266))
                                                               + (-3/2
                                                                    * mid_k:3264
                                                                    * (
                                                                    K:3266
                                                                    * K:3266))
                                                               + (3/2
                                                                    * (
                                                                    mid_k:3264
                                                                    * mid_k:3264)
                                                                    * (
                                                                    K:3266
                                                                    * K:3266))
                                                               + (-1/2
                                                                    * (
                                                                    K:3266
                                                                    * (
                                                                    K:3266
                                                                    * K:3266)))
                                                               + (mid_k:3264
                                                                    * (
                                                                    K:3266
                                                                    * (
                                                                    K:3266
                                                                    * K:3266)))
                                                               + (1/4
                                                                    * (
                                                                    (K:3266
                                                                    * K:3266)
                                                                    * (
                                                                    K:3266
                                                                    * K:3266)))))
         /\ ((K:3266 = 0 /\ mid_m:3263 = m':3253 /\ mid_l:3265 = l':3250
                /\ mid_k:3264 = k':3251 /\ mid___cost:3262 = __cost':3252)
               \/ (1 <= K:3266
                     /\ (1 + (-2 * mid_k:3264)
                           + -(((-1 + mid_k:3264) * (-1 + mid_k:3264)))
                           + (mid_k:3264 * mid_k:3264)) = 0
                     /\ (1 + -mid_k:3264
                           + -(((-1 + mid_k:3264) * (-1 + mid_k:3264)))
                           + ((-1 + mid_k:3264) * mid_k:3264)) = 0
                     /\ 0 <= (1 + (-2 * mid_k:3264)
                                + (-5
                                     * ((-1 + mid_k:3264) * (-1 + mid_k:3264)))
                                + ((mid_k:3264 * mid_k:3264) * mid_k:3264))
                     /\ 0 <= (-1 + -mid_k:3264 + j:66)
                     /\ 0 <= (1 + -mid_k:3264
                                + ((-1 + mid_k:3264) * (-1 + mid_k:3264)))
                     /\ 0 <= (-mid___cost:3262
                                + (mid_k:3264 * mid___cost:3262))
                     /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= (-1 + mid_k:3264)
                     /\ (-1 + (-2 * m':3253) + -((m':3253 * m':3253))
                           + ((1 + m':3253) * (1 + m':3253))) = 0
                     /\ (-m':3253 + -((m':3253 * m':3253))
                           + (m':3253 * (1 + m':3253))) = 0
                     /\ (-2 + -m':3253 + k':3251) = 0
                     /\ (-1 + -m':3253 + l':3250) = 0
                     /\ 0 <= (-1 + (-2 * m':3253)
                                + (-5 * (m':3253 * m':3253))
                                + ((1 + (2 * m':3253) + (m':3253 * m':3253))
                                     * (1 + m':3253)))
                     /\ 0 <= (-2 + -m':3253 + j:66)
                     /\ 0 <= (-m':3253 + (m':3253 * m':3253))
                     /\ 0 <= (-1 + -j:66 + i:64) /\ 0 <= m':3253
                     /\ 0 <= (m':3253 + (m':3253 * m':3253)
                                + (-2 * __cost':3252)
                                + (2
                                     * ((1 + m':3253)
                                          * ((-1/2 * m':3253)
                                               + (-1/2 * (m':3253 * m':3253))
                                               + __cost':3252))))))
         /\ (0 = K:3266 \/ (1 + -mid_k:3264) <= 0)
         /\ (K:3261 + K:3266) = K:3254 /\ 0 <= K:3254 /\ 0 <= k':3251
         /\ 0 <= j:66 /\ j:66 < i:64 /\ j:66 <= k':3251)}
**** alpha hat: 
  {<Split [!(-__cost:70 <= 0)
            (k':3091) = (1)*(j:66) + 0
           (__cost':2990) = (1)*(__cost:70) + 0
           (j':3267) = (1)*(j:66) + 1
           (k':3091) <= (1)*(k:67) + 2*1 + (-1)*k:67
           (k':3091) <= (1)*(k:67) + (-1)*1 + i:64 + (-1)*k:67
           (-k':3091) <= (1)*(-k:67) + k:67
           }
          pre:
            [|-__cost:70-1>=0; -j:66+2>=0; -j:66+i:64-1>=0; -i:64+n:65-1>=0;
              j:66>=0|]
          post:
            [|-k':3091+j':3267-1=0; -__cost':2990-1>=0; -k':3091+2>=0;
              -k':3091+i:64-1>=0; -i:64+n:65-1>=0; k':3091>=0|]
           (j':3267) = (1)*(j:66) + 1
          (k':3091) = (1)*(j:66) + 0
          (__cost':2990) = (1)*(__cost:70) + 1/3*j:66 + (-1/2)*j:66^2
                            + 1/6*j:66^3
          ((156 * __cost':2990)) <= (1)*((156 * __cost:70)) + (-32)*j:66
                                     + 53*j:66^2 + (-28)*j:66^3 + 7*j:66^4
          ((36 * __cost':2990)) <= (1)*((36 * __cost:70)) + 36*1 + (-48)*j:66
                                    + 19*j:66^2 + (-4)*j:66^3 + j:66^4
          ((36 * __cost':2990)) <= (1)*((36 * __cost:70)) + 28*1 + (-44)*j:66
                                    + 19*j:66^2 + (-4)*j:66^3 + j:66^4
          ((36 * __cost':2990)) <= (1)*((36 * __cost:70)) + (-16)*j:66
                                    + 19*j:66^2 + (-4)*j:66^3 + j:66^4
          ((30 * __cost':2990)) <= (1)*((30 * __cost:70)) + 18*1 + (-29)*j:66
                                    + 14*j:66^2 + (-4)*j:66^3 + j:66^4
          ((12 * __cost':2990)) <= (1)*((12 * __cost:70)) + (-2)*j:66
                                    + 5*j:66^2 + (-4)*j:66^3 + j:66^4
          (-__cost':2990) <= (1)*(-__cost:70) + 0
          ((-3 * __cost':2990)) <= (1)*((-3 * __cost:70)) + 2*j:66
                                    + (-1)*j:66^2
          ((-6 * __cost':2990)) <= (1)*((-6 * __cost:70)) + 19*j:66
                                    + (-5)*j:66^2
          ((-6 * __cost':2990)) <= (1)*((-6 * __cost:70)) + (-2)*j:66
                                    + 6*j:66*__cost:70 + 3*j:66^2
                                    + (-1)*j:66^3
          }
  pre:
    [|-28j:66-18((-2 + j:66) * (-2 + j:66))
      -4((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      -((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      +((j:66 * (j:66 * j:66)) * j:66)+41=0;
      -12j:66-6((-2 + j:66) * (-2 + j:66))
      -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((j:66 * j:66) * j:66)+16=0;
      -12j:66-6((-2 + j:66) * (-2 + j:66))
      -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +(j:66 * (j:66 * j:66))+16=0;
      -4j:66-((-2 + j:66) * (-2 + j:66))+(j:66 * j:66)+4=0;
      -3j:66-3((-2 + j:66) * (-2 + j:66))
      -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))+5=0;
      -3j:66-((-2 + j:66) * (-2 + j:66))+((-1 + j:66) * j:66)+4=0;
      -2j:66-3((-2 + j:66) * (-2 + j:66))
      -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))-6__cost:70
      -6((-2 + j:66)
   * ((1/3 * j:66) + (-1/2 * (j:66 * j:66)) + (1/6 * (j:66 * (j:66 * j:66)))
        + __cost:70))
      +6(((1/3 * j:66) + (-1/2 * (j:66 * j:66)) + (1/6 * (j:66 * (j:66 * j:66)))
    + __cost:70) * (-1 + j:66))
      +4=0;
      -2j:66-((-2 + j:66) * (-2 + j:66))+((-1 + j:66) * (-1 + j:66))+3=0;
      -12j:66-67((-2 + j:66) * (-2 + j:66))
      -26((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +7((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      +53>=0;
      -6j:66-7((-2 + j:66) * (-2 + j:66))
      -2((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      +11>=0;
      -4j:66-5((-2 + j:66) * (-2 + j:66))
      -6((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      +7>=0;
      -3j:66-7((-2 + j:66) * (-2 + j:66))
      -5((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      +5>=0;
      -2j:66+((-2 + j:66) * (-2 + j:66))
      +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+4>=0;
      -j:66+i:64-1>=0; -j:66+((-2 + j:66) * (-2 + j:66))+2>=0;
      -5((-2 + j:66) * (-2 + j:66))
      -6((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      -1>=0; -i:64+n:65-1>=0; __cost:70>=0;
      j:66-2((-2 + j:66) * (-2 + j:66))
      +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+16>=0; j:66>=0;
      j:66+((-2 + j:66) * (-2 + j:66))-2>=0;
      2j:66+3((-2 + j:66) * (-2 + j:66))
      +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))-4>=0;
      3j:66+((-2 + j:66) * (-2 + j:66))-4>=0;
      4j:66+4((-2 + j:66) * (-2 + j:66))
      +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      -((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      +12__cost:70
      +6((-2 + j:66)
   * ((1/3 * j:66) + (-1/2 * (j:66 * j:66)) + (1/6 * (j:66 * (j:66 * j:66)))
        + __cost:70))
      -7>=0;
      28j:66-5((-2 + j:66) * (-2 + j:66))
      -6((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
      +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
      -29>=0|]
  post:
    [|-28k':3091-18((-2 + k':3091) * (-2 + k':3091))
      -4((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      -((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      +((k':3091 * (k':3091 * k':3091)) * k':3091)+41=0;
      -12k':3091-6((-2 + k':3091) * (-2 + k':3091))
      -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((k':3091 * k':3091) * k':3091)+16=0;
      -12k':3091-6((-2 + k':3091) * (-2 + k':3091))
      -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +(k':3091 * (k':3091 * k':3091))+16=0;
      -4k':3091-((-2 + k':3091) * (-2 + k':3091))+(k':3091 * k':3091)+4=0;
      -3k':3091-3((-2 + k':3091) * (-2 + k':3091))
      -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((1 + (-2 * k':3091) + (k':3091 * k':3091)) * (-1 + k':3091))+5=0;
      -3k':3091-((-2 + k':3091) * (-2 + k':3091))+((-1 + k':3091) * k':3091)
      +4=0;
      -2k':3091-((-2 + k':3091) * (-2 + k':3091))
      +((-1 + k':3091) * (-1 + k':3091))+3=0; -k':3091+j':3267-1=0;
      -__cost':2990-((-2 + k':3091) * __cost':2990)
      +(__cost':2990 * (-1 + k':3091))=0;
      -12k':3091-67((-2 + k':3091) * (-2 + k':3091))
      -26((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +7((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      +53>=0;
      -6k':3091-7((-2 + k':3091) * (-2 + k':3091))
      -2((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      +11>=0;
      -4k':3091-5((-2 + k':3091) * (-2 + k':3091))
      -6((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      +7>=0;
      -3k':3091-7((-2 + k':3091) * (-2 + k':3091))
      -5((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      +5>=0;
      -2k':3091-3((-2 + k':3091) * (-2 + k':3091))
      -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +6__cost':2990+4>=0;
      -2k':3091+((-2 + k':3091) * (-2 + k':3091))
      +((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))+4>=0;
      -k':3091+i:64-1>=0; -k':3091+((-2 + k':3091) * (-2 + k':3091))+2>=0;
      -5((-2 + k':3091) * (-2 + k':3091))
      -6((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      -1>=0;
      -2((-2 + k':3091) * (-2 + k':3091))
      -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      -((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      +12__cost':2990+6((-2 + k':3091) * __cost':2990)+1>=0; -i:64+n:65-1>=0;
      k':3091-2((-2 + k':3091) * (-2 + k':3091))
      +((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))+16>=0;
      k':3091>=0; k':3091+((-2 + k':3091) * (-2 + k':3091))-2>=0;
      2k':3091+3((-2 + k':3091) * (-2 + k':3091))
      +((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))-4>=0;
      3k':3091+((-2 + k':3091) * (-2 + k':3091))-4>=0;
      28k':3091-5((-2 + k':3091) * (-2 + k':3091))
      -6((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
      +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
      -29>=0|]],
[!((1 + __cost:70) <= 0)
  (j':3267) = (1)*(j:66) + 1
 (k':3091) = (1)*(j:66) + 0
 (__cost':2990) = (1)*(__cost:70) + 1/3*j:66 + (-1/2)*j:66^2 + 1/6*j:66^3
 ((156 * __cost':2990)) <= (1)*((156 * __cost:70)) + (-32)*j:66 + 53*j:66^2
                            + (-28)*j:66^3 + 7*j:66^4
 ((36 * __cost':2990)) <= (1)*((36 * __cost:70)) + 36*1 + (-48)*j:66
                           + 19*j:66^2 + (-4)*j:66^3 + j:66^4
 ((36 * __cost':2990)) <= (1)*((36 * __cost:70)) + 28*1 + (-44)*j:66
                           + 19*j:66^2 + (-4)*j:66^3 + j:66^4
 ((36 * __cost':2990)) <= (1)*((36 * __cost:70)) + (-16)*j:66 + 19*j:66^2
                           + (-4)*j:66^3 + j:66^4
 ((30 * __cost':2990)) <= (1)*((30 * __cost:70)) + 18*1 + (-29)*j:66
                           + 14*j:66^2 + (-4)*j:66^3 + j:66^4
 ((12 * __cost':2990)) <= (1)*((12 * __cost:70)) + (-2)*j:66 + 5*j:66^2
                           + (-4)*j:66^3 + j:66^4
 (-__cost':2990) <= (1)*(-__cost:70) + 0
 ((-3 * __cost':2990)) <= (1)*((-3 * __cost:70)) + 2*j:66 + (-1)*j:66^2
 ((-6 * __cost':2990)) <= (1)*((-6 * __cost:70)) + 19*j:66 + (-5)*j:66^2
 ((-6 * __cost':2990)) <= (1)*((-6 * __cost:70)) + (-2)*j:66
                           + 6*j:66*__cost:70 + 3*j:66^2 + (-1)*j:66^3
 } pre:
  [|-28j:66-18((-2 + j:66) * (-2 + j:66))
    -4((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    -((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +((j:66 * (j:66 * j:66)) * j:66)+41=0;
    -12j:66-6((-2 + j:66) * (-2 + j:66))
    -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+((j:66 * j:66) * j:66)
    +16=0;
    -12j:66-6((-2 + j:66) * (-2 + j:66))
    -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+(j:66 * (j:66 * j:66))
    +16=0; -4j:66-((-2 + j:66) * (-2 + j:66))+(j:66 * j:66)+4=0;
    -3j:66-3((-2 + j:66) * (-2 + j:66))
    -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))+5=0;
    -3j:66-((-2 + j:66) * (-2 + j:66))+((-1 + j:66) * j:66)+4=0;
    -2j:66-3((-2 + j:66) * (-2 + j:66))
    -((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))-6__cost:70
    -6((-2 + j:66)
   * ((1/3 * j:66) + (-1/2 * (j:66 * j:66)) + (1/6 * (j:66 * (j:66 * j:66)))
        + __cost:70))
    +6(((1/3 * j:66) + (-1/2 * (j:66 * j:66)) + (1/6 * (j:66 * (j:66 * j:66)))
    + __cost:70) * (-1 + j:66))
    +4=0; -2j:66-((-2 + j:66) * (-2 + j:66))+((-1 + j:66) * (-1 + j:66))+3=0;
    -12j:66-67((-2 + j:66) * (-2 + j:66))
    -26((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +7((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +53>=0;
    -6j:66-7((-2 + j:66) * (-2 + j:66))
    -2((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +11>=0;
    -4j:66-5((-2 + j:66) * (-2 + j:66))
    -6((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +7>=0;
    -3j:66-7((-2 + j:66) * (-2 + j:66))
    -5((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +5>=0;
    -2j:66+((-2 + j:66) * (-2 + j:66))
    +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+4>=0; -j:66+i:64-1>=0;
    -j:66+((-2 + j:66) * (-2 + j:66))+2>=0;
    -5((-2 + j:66) * (-2 + j:66))
    -6((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    -1>=0; -i:64+n:65-1>=0; __cost:70>=0;
    j:66-2((-2 + j:66) * (-2 + j:66))
    +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+16>=0; j:66>=0;
    j:66+((-2 + j:66) * (-2 + j:66))-2>=0;
    2j:66+3((-2 + j:66) * (-2 + j:66))
    +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))-4>=0;
    3j:66+((-2 + j:66) * (-2 + j:66))-4>=0;
    4j:66+4((-2 + j:66) * (-2 + j:66))
    +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    -((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +12__cost:70
    +6((-2 + j:66)
   * ((1/3 * j:66) + (-1/2 * (j:66 * j:66)) + (1/6 * (j:66 * (j:66 * j:66)))
        + __cost:70))
    -7>=0;
    28j:66-5((-2 + j:66) * (-2 + j:66))
    -6((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))
    +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    -29>=0|] post:
  [|-28k':3091-18((-2 + k':3091) * (-2 + k':3091))
    -4((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    -((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    +((k':3091 * (k':3091 * k':3091)) * k':3091)+41=0;
    -12k':3091-6((-2 + k':3091) * (-2 + k':3091))
    -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((k':3091 * k':3091) * k':3091)+16=0;
    -12k':3091-6((-2 + k':3091) * (-2 + k':3091))
    -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +(k':3091 * (k':3091 * k':3091))+16=0;
    -4k':3091-((-2 + k':3091) * (-2 + k':3091))+(k':3091 * k':3091)+4=0;
    -3k':3091-3((-2 + k':3091) * (-2 + k':3091))
    -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((1 + (-2 * k':3091) + (k':3091 * k':3091)) * (-1 + k':3091))+5=0;
    -3k':3091-((-2 + k':3091) * (-2 + k':3091))+((-1 + k':3091) * k':3091)+4=0;
    -2k':3091-((-2 + k':3091) * (-2 + k':3091))
    +((-1 + k':3091) * (-1 + k':3091))+3=0; -k':3091+j':3267-1=0;
    -__cost':2990-((-2 + k':3091) * __cost':2990)
    +(__cost':2990 * (-1 + k':3091))=0;
    -12k':3091-67((-2 + k':3091) * (-2 + k':3091))
    -26((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +7((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    +53>=0;
    -6k':3091-7((-2 + k':3091) * (-2 + k':3091))
    -2((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    +11>=0;
    -4k':3091-5((-2 + k':3091) * (-2 + k':3091))
    -6((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    +7>=0;
    -3k':3091-7((-2 + k':3091) * (-2 + k':3091))
    -5((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    +5>=0;
    -2k':3091-3((-2 + k':3091) * (-2 + k':3091))
    -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +6__cost':2990+4>=0;
    -2k':3091+((-2 + k':3091) * (-2 + k':3091))
    +((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))+4>=0;
    -k':3091+i:64-1>=0; -k':3091+((-2 + k':3091) * (-2 + k':3091))+2>=0;
    -5((-2 + k':3091) * (-2 + k':3091))
    -6((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    -1>=0;
    -2((-2 + k':3091) * (-2 + k':3091))
    -((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    -((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    +12__cost':2990+6((-2 + k':3091) * __cost':2990)+1>=0; -i:64+n:65-1>=0;
    k':3091-2((-2 + k':3091) * (-2 + k':3091))
    +((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))+16>=0;
    k':3091>=0; k':3091+((-2 + k':3091) * (-2 + k':3091))-2>=0;
    2k':3091+3((-2 + k':3091) * (-2 + k':3091))
    +((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))-4>=0;
    3k':3091+((-2 + k':3091) * (-2 + k':3091))-4>=0;
    28k':3091-5((-2 + k':3091) * (-2 + k':3091))
    -6((4 + (-4 * k':3091) + (k':3091 * k':3091)) * (-2 + k':3091))
    +((-1 + (3 * k':3091) + (-3 * (k':3091 * k':3091))
    + (k':3091 * (k':3091 * k':3091))) * (-1 + k':3091))
    -29>=0|]  (k':3091) = (1)*(j:66) + 0 (__cost':2990) = (1)*(__cost:70) + 0
(j':3267) = (1)*(j:66) + 1 (k':3091) <= (1)*(k:67) + 2*1 + (-1)*k:67
(k':3091) <= (1)*(k:67) + (-1)*1 + i:64 + (-1)*k:67
(-k':3091) <= (1)*(-k:67) + k:67 } pre:
  [|-__cost:70-1>=0; -j:66+2>=0; -j:66+i:64-1>=0; -i:64+n:65-1>=0; j:66>=0|]
post:
  [|-k':3091+j':3267-1=0; -__cost':2990-1>=0; -k':3091+2>=0;
    -k':3091+i:64-1>=0; -i:64+n:65-1>=0; k':3091>=0|]],
[!((1 + -j:66) <= 0)
  (l':3019) = (1)*(l:68) + 0
 (j':3267) = 1
 (m':2991) = (1)*(m:69) + 0
 (k':3091) = 0
 (__cost':2990) = (1)*(__cost:70) + 0
 } pre:   [|j:66=0; -i:64+n:65-1>=0; i:64-1>=0|] post:
  [|j':3267-1=0; k':3091=0; -i:64+n:65-1>=0; i:64-1>=0|]
 ((-j':3267 + l':3019)) = (-2)*1 (j':3267) = (1)*(j:66) + 1
((-j':3267 + k':3091)) = (-1)*1
((210 * __cost':2990)) <= (1)*((210 * __cost:70)) + 58*1 + (-65)*j:66
                           + 3*j:66^2 + 4*j:66^4
((60 * __cost':2990)) <= (1)*((60 * __cost:70)) + 37*1 + (-40)*j:66
                          + 7*j:66^2 + j:66^4
((60 * __cost':2990)) <= (1)*((60 * __cost:70)) + 27*1 + (-35)*j:66
                          + 7*j:66^2 + j:66^4
((-2 * __cost':2990)) <= (1)*((-2 * __cost:70)) + (-2)*1 + 3*j:66
                          + (-1)*j:66^2
((-6 * __cost':2990)) <= (1)*((-6 * __cost:70)) + (-14)*1 + 19*j:66
                          + (-5)*j:66^2 } pre:
  [|-6__cost:70+j:66-((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    -6((-2 + j:66)
   * (__cost:70 + (1/3 * j:66) + (-1/2 * (j:66 * j:66))
        + (1/6 * (j:66 * (j:66 * j:66)))))
    +6((__cost:70 + (1/3 * j:66) + (-1/2 * (j:66 * j:66))
    + (1/6 * (j:66 * (j:66 * j:66)))) * (-1 + j:66))
    -1=0;
    -9j:66+3(j:66 * j:66)-((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +((4 + (-4 * j:66) + (j:66 * j:66)) * (-2 + j:66))+7=0;
    -8j:66+6(j:66 * j:66)+4((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    -((j:66 * (j:66 * j:66)) * j:66)
    +((-1 + (3 * j:66) + (-3 * (j:66 * j:66)) + (j:66 * (j:66 * j:66)))
   * (-1 + j:66))
    +3=0; j:66-(j:66 * j:66)+((-1 + j:66) * j:66)=0;
    2j:66-(j:66 * j:66)+((-1 + j:66) * (-1 + j:66))-1=0;
    3j:66-3(j:66 * j:66)-((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +(j:66 * (j:66 * j:66))-1=0;
    3j:66-3(j:66 * j:66)-((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +((j:66 * j:66) * j:66)-1=0;
    4j:66-(j:66 * j:66)+((-2 + j:66) * (-2 + j:66))-4=0;
    -66j:66+13(j:66 * j:66)
    -37((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +4((j:66 * (j:66 * j:66)) * j:66)+57>=0;
    -57j:66+14(j:66 * j:66)
    -20((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +2((j:66 * (j:66 * j:66)) * j:66)+48>=0;
    -46j:66+12(j:66 * j:66)
    -10((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +((j:66 * (j:66 * j:66)) * j:66)+39>=0;
    -30j:66+7(j:66 * j:66)
    -10((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +((j:66 * (j:66 * j:66)) * j:66)+27>=0;
    -18j:66+7(j:66 * j:66)
    -10((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +((j:66 * (j:66 * j:66)) * j:66)+10>=0; -9j:66+3(j:66 * j:66)+7>=0;
    -6j:66-(j:66 * j:66)-17((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +2((j:66 * (j:66 * j:66)) * j:66)+5>=0; -5j:66+(j:66 * j:66)+6>=0;
    -4j:66+(j:66 * j:66)+4>=0; -2j:66+(j:66 * j:66)+1>=0; -j:66+i:64-1>=0;
    -i:64+n:65-1>=0; ((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))>=0;
    j:66-1>=0;
    2j:66-9(j:66 * j:66)-31((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +4((j:66 * (j:66 * j:66)) * j:66)+3>=0;
    5j:66-2(j:66 * j:66)+((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))-3>=0;
    8j:66-6(j:66 * j:66)-4((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    +((j:66 * (j:66 * j:66)) * j:66)-3>=0;
    8j:66-3(j:66 * j:66)+((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))-5>=0;
    18j:66-5(j:66 * j:66)+((1 + (-2 * j:66) + (j:66 * j:66)) * (-1 + j:66))
    -13>=0|] post:
  [|-9j':3267+3((-1 + j':3267) * (-1 + j':3267))
    -((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((9 + (-6 * j':3267) + (j':3267 * j':3267)) * (-3 + j':3267))+16=0;
    -8j':3267+6((-1 + j':3267) * (-1 + j':3267))
    +4((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    -((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +((-8 + (12 * j':3267) + (-6 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-2 + j':3267))
    +11=0; -j':3267+k':3091+1=0; -j':3267+l':3019+2=0;
    j':3267-((-1 + j':3267) * (-1 + j':3267))
    +((-2 + j':3267) * (-1 + j':3267))-1=0;
    2j':3267-((-1 + j':3267) * (-1 + j':3267))
    +((-2 + j':3267) * (-2 + j':3267))-3=0;
    3j':3267-3((-1 + j':3267) * (-1 + j':3267))
    -((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((-1 + j':3267) * (1 + (-2 * j':3267) + (j':3267 * j':3267)))-4=0;
    3j':3267-3((-1 + j':3267) * (-1 + j':3267))
    -((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((1 + (-2 * j':3267) + (j':3267 * j':3267)) * (-1 + j':3267))-4=0;
    4j':3267-((-1 + j':3267) * (-1 + j':3267))
    +((-3 + j':3267) * (-3 + j':3267))-8=0;
    -66j':3267+13((-1 + j':3267) * (-1 + j':3267))
    -37((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +4((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +123>=0;
    -57j':3267+14((-1 + j':3267) * (-1 + j':3267))
    -20((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +2((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +105>=0;
    -46j':3267+12((-1 + j':3267) * (-1 + j':3267))
    -10((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +85>=0;
    -30j':3267+7((-1 + j':3267) * (-1 + j':3267))
    -10((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +57>=0;
    -18j':3267+7((-1 + j':3267) * (-1 + j':3267))
    -10((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +28>=0; -9j':3267+3((-1 + j':3267) * (-1 + j':3267))+16>=0;
    -6j':3267-((-1 + j':3267) * (-1 + j':3267))
    -17((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +2((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +11>=0; -5j':3267+((-1 + j':3267) * (-1 + j':3267))+11>=0;
    -4j':3267+((-1 + j':3267) * (-1 + j':3267))+8>=0;
    -2j':3267+((-1 + j':3267) * (-1 + j':3267))+3>=0; -j':3267+i:64>=0;
    -i:64+n:65-1>=0;
    ((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))>=0;
    j':3267-2>=0;
    2j':3267-9((-1 + j':3267) * (-1 + j':3267))
    -31((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +4((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    +1>=0;
    5j':3267-2((-1 + j':3267) * (-1 + j':3267))
    +((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))-8>=0;
    8j':3267-6((-1 + j':3267) * (-1 + j':3267))
    -4((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))
    +((-1 + (3 * j':3267) + (-3 * (j':3267 * j':3267))
    + (j':3267 * (j':3267 * j':3267))) * (-1 + j':3267))
    -11>=0;
    8j':3267-3((-1 + j':3267) * (-1 + j':3267))
    +((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))-13>=0;
    18j':3267-5((-1 + j':3267) * (-1 + j':3267))
    +((4 + (-4 * j':3267) + (j':3267 * j':3267)) * (-2 + j':3267))-31>=0|]]>}
**** star transition: 
  {__cost := __cost':2990
   j := j':3267
   k := k':3091
   l := l':3019
   m := m':2991
   when ((!((0 <= K:3565 /\ K:3565 <= 0)) \/ mid_k:3569 = (k:67 + K:3565))
           /\ (!(1 <= K:3565)
                 \/ mid_k:3569 = (-1 + k:67 + j:66 + -k:67 + K:3565))
           /\ (!(0 <= K:3565) \/ mid___cost:3571 = __cost:70)
           /\ (!(0 <= K:3565) \/ mid_j:3570 = (j:66 + K:3565))
           /\ (!((0 <= K:3565 /\ K:3565 <= 0))
                 \/ mid_k:3569 <= (k:67 + (7/2 * K:3565) + -((j:66 * K:3565))
                                     + (-1/2 * (K:3565 * K:3565))))
           /\ (!(1 <= K:3565)
                 \/ mid_k:3569 <= (-1 + j:66 + k:67 + -k:67 + (7/2 * K:3565)
                                     + -((j:66 * K:3565))
                                     + (-1/2 * (K:3565 * K:3565))))
           /\ (!((0 <= K:3565 /\ K:3565 <= 0))
                 \/ mid_k:3569 <= (k:67 + (1/2 * K:3565) + (i:64 * K:3565)
                                     + -((j:66 * K:3565))
                                     + (-1/2 * (K:3565 * K:3565))))
           /\ (!(1 <= K:3565)
                 \/ mid_k:3569 <= (-1 + j:66 + k:67 + -k:67 + (1/2 * K:3565)
                                     + (i:64 * K:3565) + -((j:66 * K:3565))
                                     + (-1/2 * (K:3565 * K:3565))))
           /\ (!((0 <= K:3565 /\ K:3565 <= 0))
                 \/ -mid_k:3569 <= (-k:67 + (-3/2 * K:3565) + (j:66 * K:3565)
                                      + (1/2 * (K:3565 * K:3565))))
           /\ (!(1 <= K:3565)
                 \/ -mid_k:3569 <= (1 + k:67 + -k:67 + -j:66
                                      + (-3/2 * K:3565) + (j:66 * K:3565)
                                      + (1/2 * (K:3565 * K:3565))))
           /\ ((K:3565 = 0 /\ m:69 = mid_m:3567 /\ l:68 = mid_l:3568
                  /\ k:67 = mid_k:3569 /\ j:66 = mid_j:3570
                  /\ __cost:70 = mid___cost:3571)
                 \/ (1 <= K:3565 /\ 0 <= (-1 + -__cost:70)
                       /\ 0 <= (2 + -j:66) /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= j:66
                       /\ (-1 + -mid_k:3569 + mid_j:3570) = 0
                       /\ 0 <= (-1 + -mid___cost:3571)
                       /\ 0 <= (2 + -mid_k:3569)
                       /\ 0 <= (-1 + -mid_k:3569 + i:64)
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= mid_k:3569))
           /\ (0 = K:3565 \/ !(-__cost:70 <= 0))
           /\ (!(0 <= K:3566) \/ j':3267 = (mid_j:3570 + K:3566))
           /\ (!((0 <= K:3566 /\ K:3566 <= 0))
                 \/ k':3091 = (mid_k:3569 + K:3566))
           /\ (!(1 <= K:3566) \/ k':3091 = (-1 + mid_j:3570 + K:3566))
           /\ (!(0 <= K:3566)
                 \/ __cost':2990 = (mid___cost:3571 + (-1/4 * K:3566)
                                      + (11/12 * mid_j:3570 * K:3566)
                                      + (-3/4 * (mid_j:3570 * mid_j:3570)
                                           * K:3566)
                                      + (1/6
                                           * (mid_j:3570
                                                * (mid_j:3570 * mid_j:3570))
                                           * K:3566)
                                      + (11/24 * (K:3566 * K:3566))
                                      + (-3/4 * mid_j:3570
                                           * (K:3566 * K:3566))
                                      + (1/4 * (mid_j:3570 * mid_j:3570)
                                           * (K:3566 * K:3566))
                                      + (-1/4 * (K:3566 * (K:3566 * K:3566)))
                                      + (1/6 * mid_j:3570
                                           * (K:3566 * (K:3566 * K:3566)))
                                      + (1/24
                                           * ((K:3566 * K:3566)
                                                * (K:3566 * K:3566)))))
           /\ (!(0 <= K:3566)
                 \/ (156 * __cost':2990) <= ((156 * mid___cost:3571)
                                               + (123/5 * K:3566)
                                               + (-99 * mid_j:3570 * K:3566)
                                               + (102
                                                    * (mid_j:3570
                                                         * mid_j:3570)
                                                    * K:3566)
                                               + (-42
                                                    * (mid_j:3570
                                                         * (mid_j:3570
                                                              * mid_j:3570))
                                                    * K:3566)
                                               + (7
                                                    * ((mid_j:3570
                                                          * mid_j:3570)
                                                         * (mid_j:3570
                                                              * mid_j:3570))
                                                    * K:3566)
                                               + (-99/2 * (K:3566 * K:3566))
                                               + (102 * mid_j:3570
                                                    * (K:3566 * K:3566))
                                               + (-63
                                                    * (mid_j:3570
                                                         * mid_j:3570)
                                                    * (K:3566 * K:3566))
                                               + (14
                                                    * (mid_j:3570
                                                         * (mid_j:3570
                                                              * mid_j:3570))
                                                    * (K:3566 * K:3566))
                                               + (34
                                                    * (K:3566
                                                         * (K:3566 * K:3566)))
                                               + (-42 * mid_j:3570
                                                    * (K:3566
                                                         * (K:3566 * K:3566)))
                                               + (14
                                                    * (mid_j:3570
                                                         * mid_j:3570)
                                                    * (K:3566
                                                         * (K:3566 * K:3566)))
                                               + (-21/2
                                                    * ((K:3566 * K:3566)
                                                         * (K:3566 * K:3566)))
                                               + (7 * mid_j:3570
                                                    * ((K:3566 * K:3566)
                                                         * (K:3566 * K:3566)))
                                               + (7/5
                                                    * (K:3566
                                                         * ((K:3566 * K:3566)
                                                              * (K:3566
                                                                   * K:3566))))))
           /\ (!(0 <= K:3566)
                 \/ (36 * __cost':2990) <= ((36 * mid___cost:3571)
                                              + (947/15 * K:3566)
                                              + (-69 * mid_j:3570 * K:3566)
                                              + (26
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (-6
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (((mid_j:3570 * mid_j:3570)
                                                    * (mid_j:3570
                                                         * mid_j:3570))
                                                   * K:3566)
                                              + (-69/2 * (K:3566 * K:3566))
                                              + (26 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (-9
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566 * K:3566))
                                              + (2
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (26/3
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-6 * mid_j:3570
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (2
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-3/2
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (mid_j:3570
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (1/5
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))))
           /\ (!(0 <= K:3566)
                 \/ (36 * __cost':2990) <= ((36 * mid___cost:3571)
                                              + (797/15 * K:3566)
                                              + (-65 * mid_j:3570 * K:3566)
                                              + (26
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (-6
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (((mid_j:3570 * mid_j:3570)
                                                    * (mid_j:3570
                                                         * mid_j:3570))
                                                   * K:3566)
                                              + (-65/2 * (K:3566 * K:3566))
                                              + (26 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (-9
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566 * K:3566))
                                              + (2
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (26/3
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-6 * mid_j:3570
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (2
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-3/2
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (mid_j:3570
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (1/5
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))))
           /\ (!(0 <= K:3566)
                 \/ (36 * __cost':2990) <= ((36 * mid___cost:3571)
                                              + (167/15 * K:3566)
                                              + (-37 * mid_j:3570 * K:3566)
                                              + (26
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (-6
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (((mid_j:3570 * mid_j:3570)
                                                    * (mid_j:3570
                                                         * mid_j:3570))
                                                   * K:3566)
                                              + (-37/2 * (K:3566 * K:3566))
                                              + (26 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (-9
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566 * K:3566))
                                              + (2
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (26/3
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-6 * mid_j:3570
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (2
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-3/2
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (mid_j:3570
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (1/5
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))))
           /\ (!(0 <= K:3566)
                 \/ (30 * __cost':2990) <= ((30 * mid___cost:3571)
                                              + (174/5 * K:3566)
                                              + (-45 * mid_j:3570 * K:3566)
                                              + (21
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (-6
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (((mid_j:3570 * mid_j:3570)
                                                    * (mid_j:3570
                                                         * mid_j:3570))
                                                   * K:3566)
                                              + (-45/2 * (K:3566 * K:3566))
                                              + (21 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (-9
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566 * K:3566))
                                              + (2
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (7
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-6 * mid_j:3570
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (2
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-3/2
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (mid_j:3570
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (1/5
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))))
           /\ (!(0 <= K:3566)
                 \/ (12 * __cost':2990) <= ((12 * mid___cost:3571)
                                              + (9/5 * K:3566)
                                              + (-9 * mid_j:3570 * K:3566)
                                              + (12
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (-6
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (((mid_j:3570 * mid_j:3570)
                                                    * (mid_j:3570
                                                         * mid_j:3570))
                                                   * K:3566)
                                              + (-9/2 * (K:3566 * K:3566))
                                              + (12 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (-9
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566 * K:3566))
                                              + (2
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (4
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-6 * mid_j:3570
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (2
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-3/2
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (mid_j:3570
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (1/5
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))))
           /\ (!(0 <= K:3566) \/ -__cost':2990 <= -mid___cost:3571)
           /\ (!(0 <= K:3566)
                 \/ (-3 * __cost':2990) <= ((-3 * mid___cost:3571)
                                              + (-7/6 * K:3566)
                                              + (3 * mid_j:3570 * K:3566)
                                              + -(((mid_j:3570 * mid_j:3570)
                                                     * K:3566))
                                              + (3/2 * (K:3566 * K:3566))
                                              + -((mid_j:3570
                                                     * (K:3566 * K:3566)))
                                              + (-1/3
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))))
           /\ (!(0 <= K:3566)
                 \/ (-6 * __cost':2990) <= ((-6 * mid___cost:3571)
                                              + (-31/3 * K:3566)
                                              + (24 * mid_j:3570 * K:3566)
                                              + (-5
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (12 * (K:3566 * K:3566))
                                              + (-5 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (-5/3
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))))
           /\ (!(0 <= K:3566)
                 \/ (-6 * __cost':2990) <= ((-6 * mid___cost:3571)
                                              + (13/10 * K:3566)
                                              + (-41/12 * mid_j:3570 * K:3566)
                                              + (-3 * mid___cost:3571
                                                   * K:3566)
                                              + (6 * mid_j:3570
                                                   * mid___cost:3571 * K:3566)
                                              + (1/4
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * K:3566)
                                              + (5/3
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (-1/2
                                                   * ((mid_j:3570
                                                         * mid_j:3570)
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * K:3566)
                                              + (-4/3 * (K:3566 * K:3566))
                                              + (-15/8 * mid_j:3570
                                                   * (K:3566 * K:3566))
                                              + (3 * mid___cost:3571
                                                   * (K:3566 * K:3566))
                                              + (51/8
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566 * K:3566))
                                              + (-7/2
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (1/2
                                                   * ((mid_j:3570
                                                         * mid_j:3570)
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566 * K:3566))
                                              + (-7/8
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (31/6 * mid_j:3570
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (-17/4
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (5/6
                                                   * (mid_j:3570
                                                        * (mid_j:3570
                                                             * mid_j:3570))
                                                   * (K:3566
                                                        * (K:3566 * K:3566)))
                                              + (31/24
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (-17/8 * mid_j:3570
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (5/8
                                                   * (mid_j:3570 * mid_j:3570)
                                                   * ((K:3566 * K:3566)
                                                        * (K:3566 * K:3566)))
                                              + (-17/40
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))
                                              + (1/4 * mid_j:3570
                                                   * (K:3566
                                                        * ((K:3566 * K:3566)
                                                             * (K:3566
                                                                  * K:3566))))
                                              + (1/24
                                                   * ((K:3566
                                                         * (K:3566 * K:3566))
                                                        * (K:3566
                                                             * (K:3566
                                                                  * K:3566))))))
           /\ ((K:3566 = 0 /\ mid_m:3567 = m':2991 /\ mid_l:3568 = l':3019
                  /\ mid_k:3569 = k':3091 /\ mid_j:3570 = j':3267
                  /\ mid___cost:3571 = __cost':2990)
                 \/ (1 <= K:3566
                       /\ (41 + (-28 * mid_j:3570)
                             + (-18 * ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + (-4
                                  * ((4 + (-4 * mid_j:3570)
                                        + (mid_j:3570 * mid_j:3570))
                                       * (-2 + mid_j:3570)))
                             + -(((-1 + (3 * mid_j:3570)
                                     + (-3 * (mid_j:3570 * mid_j:3570))
                                     + (mid_j:3570
                                          * (mid_j:3570 * mid_j:3570)))
                                    * (-1 + mid_j:3570)))
                             + ((mid_j:3570 * (mid_j:3570 * mid_j:3570))
                                  * mid_j:3570)) = 0
                       /\ (16 + (-12 * mid_j:3570)
                             + (-6 * ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + -(((4 + (-4 * mid_j:3570)
                                     + (mid_j:3570 * mid_j:3570))
                                    * (-2 + mid_j:3570)))
                             + ((mid_j:3570 * mid_j:3570) * mid_j:3570)) = 0
                       /\ (16 + (-12 * mid_j:3570)
                             + (-6 * ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + -(((4 + (-4 * mid_j:3570)
                                     + (mid_j:3570 * mid_j:3570))
                                    * (-2 + mid_j:3570)))
                             + (mid_j:3570 * (mid_j:3570 * mid_j:3570))) = 0
                       /\ (4 + (-4 * mid_j:3570)
                             + -(((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + (mid_j:3570 * mid_j:3570)) = 0
                       /\ (5 + (-3 * mid_j:3570)
                             + (-3 * ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + -(((4 + (-4 * mid_j:3570)
                                     + (mid_j:3570 * mid_j:3570))
                                    * (-2 + mid_j:3570)))
                             + ((1 + (-2 * mid_j:3570)
                                   + (mid_j:3570 * mid_j:3570))
                                  * (-1 + mid_j:3570))) = 0
                       /\ (4 + (-3 * mid_j:3570)
                             + -(((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + ((-1 + mid_j:3570) * mid_j:3570)) = 0
                       /\ (4 + (-2 * mid_j:3570)
                             + (-3 * ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + -(((4 + (-4 * mid_j:3570)
                                     + (mid_j:3570 * mid_j:3570))
                                    * (-2 + mid_j:3570)))
                             + (-6 * mid___cost:3571)
                             + (-6
                                  * ((-2 + mid_j:3570)
                                       * ((1/3 * mid_j:3570)
                                            + (-1/2
                                                 * (mid_j:3570 * mid_j:3570))
                                            + (1/6
                                                 * (mid_j:3570
                                                      * (mid_j:3570
                                                           * mid_j:3570)))
                                            + mid___cost:3571)))
                             + (6
                                  * (((1/3 * mid_j:3570)
                                        + (-1/2 * (mid_j:3570 * mid_j:3570))
                                        + (1/6
                                             * (mid_j:3570
                                                  * (mid_j:3570 * mid_j:3570)))
                                        + mid___cost:3571)
                                       * (-1 + mid_j:3570)))) = 0
                       /\ (3 + (-2 * mid_j:3570)
                             + -(((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                             + ((-1 + mid_j:3570) * (-1 + mid_j:3570))) = 0
                       /\ 0 <= (53 + (-12 * mid_j:3570)
                                  + (-67
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + (-26
                                       * ((4 + (-4 * mid_j:3570)
                                             + (mid_j:3570 * mid_j:3570))
                                            * (-2 + mid_j:3570)))
                                  + (7
                                       * ((-1 + (3 * mid_j:3570)
                                             + (-3
                                                  * (mid_j:3570 * mid_j:3570))
                                             + (mid_j:3570
                                                  * (mid_j:3570 * mid_j:3570)))
                                            * (-1 + mid_j:3570))))
                       /\ 0 <= (11 + (-6 * mid_j:3570)
                                  + (-7
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + (-2
                                       * ((4 + (-4 * mid_j:3570)
                                             + (mid_j:3570 * mid_j:3570))
                                            * (-2 + mid_j:3570)))
                                  + ((-1 + (3 * mid_j:3570)
                                        + (-3 * (mid_j:3570 * mid_j:3570))
                                        + (mid_j:3570
                                             * (mid_j:3570 * mid_j:3570)))
                                       * (-1 + mid_j:3570)))
                       /\ 0 <= (7 + (-4 * mid_j:3570)
                                  + (-5
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + (-6
                                       * ((4 + (-4 * mid_j:3570)
                                             + (mid_j:3570 * mid_j:3570))
                                            * (-2 + mid_j:3570)))
                                  + ((-1 + (3 * mid_j:3570)
                                        + (-3 * (mid_j:3570 * mid_j:3570))
                                        + (mid_j:3570
                                             * (mid_j:3570 * mid_j:3570)))
                                       * (-1 + mid_j:3570)))
                       /\ 0 <= (5 + (-3 * mid_j:3570)
                                  + (-7
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + (-5
                                       * ((4 + (-4 * mid_j:3570)
                                             + (mid_j:3570 * mid_j:3570))
                                            * (-2 + mid_j:3570)))
                                  + ((-1 + (3 * mid_j:3570)
                                        + (-3 * (mid_j:3570 * mid_j:3570))
                                        + (mid_j:3570
                                             * (mid_j:3570 * mid_j:3570)))
                                       * (-1 + mid_j:3570)))
                       /\ 0 <= (4 + (-2 * mid_j:3570)
                                  + ((-2 + mid_j:3570) * (-2 + mid_j:3570))
                                  + ((4 + (-4 * mid_j:3570)
                                        + (mid_j:3570 * mid_j:3570))
                                       * (-2 + mid_j:3570)))
                       /\ 0 <= (-1 + -mid_j:3570 + i:64)
                       /\ 0 <= (2 + -mid_j:3570
                                  + ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                       /\ 0 <= (-1
                                  + (-5
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + (-6
                                       * ((4 + (-4 * mid_j:3570)
                                             + (mid_j:3570 * mid_j:3570))
                                            * (-2 + mid_j:3570)))
                                  + ((-1 + (3 * mid_j:3570)
                                        + (-3 * (mid_j:3570 * mid_j:3570))
                                        + (mid_j:3570
                                             * (mid_j:3570 * mid_j:3570)))
                                       * (-1 + mid_j:3570)))
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= mid___cost:3571
                       /\ 0 <= (16 + mid_j:3570
                                  + (-2
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + ((4 + (-4 * mid_j:3570)
                                        + (mid_j:3570 * mid_j:3570))
                                       * (-2 + mid_j:3570)))
                       /\ 0 <= mid_j:3570
                       /\ 0 <= (-2 + mid_j:3570
                                  + ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                       /\ 0 <= (-4 + (2 * mid_j:3570)
                                  + (3
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + ((4 + (-4 * mid_j:3570)
                                        + (mid_j:3570 * mid_j:3570))
                                       * (-2 + mid_j:3570)))
                       /\ 0 <= (-4 + (3 * mid_j:3570)
                                  + ((-2 + mid_j:3570) * (-2 + mid_j:3570)))
                       /\ 0 <= (-7 + (4 * mid_j:3570)
                                  + (4
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + ((4 + (-4 * mid_j:3570)
                                        + (mid_j:3570 * mid_j:3570))
                                       * (-2 + mid_j:3570))
                                  + -(((-1 + (3 * mid_j:3570)
                                          + (-3 * (mid_j:3570 * mid_j:3570))
                                          + (mid_j:3570
                                               * (mid_j:3570 * mid_j:3570)))
                                         * (-1 + mid_j:3570)))
                                  + (12 * mid___cost:3571)
                                  + (6
                                       * ((-2 + mid_j:3570)
                                            * ((1/3 * mid_j:3570)
                                                 + (-1/2
                                                      * (mid_j:3570
                                                           * mid_j:3570))
                                                 + (1/6
                                                      * (mid_j:3570
                                                           * (mid_j:3570
                                                                * mid_j:3570)))
                                                 + mid___cost:3571))))
                       /\ 0 <= (-29 + (28 * mid_j:3570)
                                  + (-5
                                       * ((-2 + mid_j:3570)
                                            * (-2 + mid_j:3570)))
                                  + (-6
                                       * ((4 + (-4 * mid_j:3570)
                                             + (mid_j:3570 * mid_j:3570))
                                            * (-2 + mid_j:3570)))
                                  + ((-1 + (3 * mid_j:3570)
                                        + (-3 * (mid_j:3570 * mid_j:3570))
                                        + (mid_j:3570
                                             * (mid_j:3570 * mid_j:3570)))
                                       * (-1 + mid_j:3570)))
                       /\ (41 + (-28 * k':3091)
                             + (-18 * ((-2 + k':3091) * (-2 + k':3091)))
                             + (-4
                                  * ((4 + (-4 * k':3091)
                                        + (k':3091 * k':3091))
                                       * (-2 + k':3091)))
                             + -(((-1 + (3 * k':3091)
                                     + (-3 * (k':3091 * k':3091))
                                     + (k':3091 * (k':3091 * k':3091)))
                                    * (-1 + k':3091)))
                             + ((k':3091 * (k':3091 * k':3091)) * k':3091)) = 0
                       /\ (16 + (-12 * k':3091)
                             + (-6 * ((-2 + k':3091) * (-2 + k':3091)))
                             + -(((4 + (-4 * k':3091) + (k':3091 * k':3091))
                                    * (-2 + k':3091)))
                             + ((k':3091 * k':3091) * k':3091)) = 0
                       /\ (16 + (-12 * k':3091)
                             + (-6 * ((-2 + k':3091) * (-2 + k':3091)))
                             + -(((4 + (-4 * k':3091) + (k':3091 * k':3091))
                                    * (-2 + k':3091)))
                             + (k':3091 * (k':3091 * k':3091))) = 0
                       /\ (4 + (-4 * k':3091)
                             + -(((-2 + k':3091) * (-2 + k':3091)))
                             + (k':3091 * k':3091)) = 0
                       /\ (5 + (-3 * k':3091)
                             + (-3 * ((-2 + k':3091) * (-2 + k':3091)))
                             + -(((4 + (-4 * k':3091) + (k':3091 * k':3091))
                                    * (-2 + k':3091)))
                             + ((1 + (-2 * k':3091) + (k':3091 * k':3091))
                                  * (-1 + k':3091))) = 0
                       /\ (4 + (-3 * k':3091)
                             + -(((-2 + k':3091) * (-2 + k':3091)))
                             + ((-1 + k':3091) * k':3091)) = 0
                       /\ (3 + (-2 * k':3091)
                             + -(((-2 + k':3091) * (-2 + k':3091)))
                             + ((-1 + k':3091) * (-1 + k':3091))) = 0
                       /\ (-1 + -k':3091 + j':3267) = 0
                       /\ (-__cost':2990 + -(((-2 + k':3091) * __cost':2990))
                             + (__cost':2990 * (-1 + k':3091))) = 0
                       /\ 0 <= (53 + (-12 * k':3091)
                                  + (-67 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + (-26
                                       * ((4 + (-4 * k':3091)
                                             + (k':3091 * k':3091))
                                            * (-2 + k':3091)))
                                  + (7
                                       * ((-1 + (3 * k':3091)
                                             + (-3 * (k':3091 * k':3091))
                                             + (k':3091 * (k':3091 * k':3091)))
                                            * (-1 + k':3091))))
                       /\ 0 <= (11 + (-6 * k':3091)
                                  + (-7 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + (-2
                                       * ((4 + (-4 * k':3091)
                                             + (k':3091 * k':3091))
                                            * (-2 + k':3091)))
                                  + ((-1 + (3 * k':3091)
                                        + (-3 * (k':3091 * k':3091))
                                        + (k':3091 * (k':3091 * k':3091)))
                                       * (-1 + k':3091)))
                       /\ 0 <= (7 + (-4 * k':3091)
                                  + (-5 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + (-6
                                       * ((4 + (-4 * k':3091)
                                             + (k':3091 * k':3091))
                                            * (-2 + k':3091)))
                                  + ((-1 + (3 * k':3091)
                                        + (-3 * (k':3091 * k':3091))
                                        + (k':3091 * (k':3091 * k':3091)))
                                       * (-1 + k':3091)))
                       /\ 0 <= (5 + (-3 * k':3091)
                                  + (-7 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + (-5
                                       * ((4 + (-4 * k':3091)
                                             + (k':3091 * k':3091))
                                            * (-2 + k':3091)))
                                  + ((-1 + (3 * k':3091)
                                        + (-3 * (k':3091 * k':3091))
                                        + (k':3091 * (k':3091 * k':3091)))
                                       * (-1 + k':3091)))
                       /\ 0 <= (4 + (-2 * k':3091)
                                  + (-3 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + -(((4 + (-4 * k':3091)
                                          + (k':3091 * k':3091))
                                         * (-2 + k':3091)))
                                  + (6 * __cost':2990))
                       /\ 0 <= (4 + (-2 * k':3091)
                                  + ((-2 + k':3091) * (-2 + k':3091))
                                  + ((4 + (-4 * k':3091)
                                        + (k':3091 * k':3091))
                                       * (-2 + k':3091)))
                       /\ 0 <= (-1 + -k':3091 + i:64)
                       /\ 0 <= (2 + -k':3091
                                  + ((-2 + k':3091) * (-2 + k':3091)))
                       /\ 0 <= (-1 + (-5 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + (-6
                                       * ((4 + (-4 * k':3091)
                                             + (k':3091 * k':3091))
                                            * (-2 + k':3091)))
                                  + ((-1 + (3 * k':3091)
                                        + (-3 * (k':3091 * k':3091))
                                        + (k':3091 * (k':3091 * k':3091)))
                                       * (-1 + k':3091)))
                       /\ 0 <= (1 + (-2 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + -(((4 + (-4 * k':3091)
                                          + (k':3091 * k':3091))
                                         * (-2 + k':3091)))
                                  + -(((-1 + (3 * k':3091)
                                          + (-3 * (k':3091 * k':3091))
                                          + (k':3091 * (k':3091 * k':3091)))
                                         * (-1 + k':3091)))
                                  + (12 * __cost':2990)
                                  + (6 * ((-2 + k':3091) * __cost':2990)))
                       /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= (16 + k':3091
                                  + (-2 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + ((4 + (-4 * k':3091)
                                        + (k':3091 * k':3091))
                                       * (-2 + k':3091))) /\ 0 <= k':3091
                       /\ 0 <= (-2 + k':3091
                                  + ((-2 + k':3091) * (-2 + k':3091)))
                       /\ 0 <= (-4 + (2 * k':3091)
                                  + (3 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + ((4 + (-4 * k':3091)
                                        + (k':3091 * k':3091))
                                       * (-2 + k':3091)))
                       /\ 0 <= (-4 + (3 * k':3091)
                                  + ((-2 + k':3091) * (-2 + k':3091)))
                       /\ 0 <= (-29 + (28 * k':3091)
                                  + (-5 * ((-2 + k':3091) * (-2 + k':3091)))
                                  + (-6
                                       * ((4 + (-4 * k':3091)
                                             + (k':3091 * k':3091))
                                            * (-2 + k':3091)))
                                  + ((-1 + (3 * k':3091)
                                        + (-3 * (k':3091 * k':3091))
                                        + (k':3091 * (k':3091 * k':3091)))
                                       * (-1 + k':3091)))))
           /\ (0 = K:3566 \/ -mid___cost:3571 <= 0)
           /\ (K:3565 + K:3566) = K:3564
           /\ (!(0 <= K:3572) \/ mid_j:3577 = (j:66 + K:3572))
           /\ (!((0 <= K:3572 /\ K:3572 <= 0))
                 \/ mid_k:3576 = (k:67 + K:3572))
           /\ (!(1 <= K:3572) \/ mid_k:3576 = (-1 + j:66 + K:3572))
           /\ (!(0 <= K:3572)
                 \/ mid___cost:3578 = (__cost:70 + (-1/4 * K:3572)
                                         + (11/12 * j:66 * K:3572)
                                         + (-3/4 * (j:66 * j:66) * K:3572)
                                         + (1/6 * (j:66 * (j:66 * j:66))
                                              * K:3572)
                                         + (11/24 * (K:3572 * K:3572))
                                         + (-3/4 * j:66 * (K:3572 * K:3572))
                                         + (1/4 * (j:66 * j:66)
                                              * (K:3572 * K:3572))
                                         + (-1/4
                                              * (K:3572 * (K:3572 * K:3572)))
                                         + (1/6 * j:66
                                              * (K:3572 * (K:3572 * K:3572)))
                                         + (1/24
                                              * ((K:3572 * K:3572)
                                                   * (K:3572 * K:3572)))))
           /\ (!(0 <= K:3572)
                 \/ (156 * mid___cost:3578) <= ((156 * __cost:70)
                                                  + (123/5 * K:3572)
                                                  + (-99 * j:66 * K:3572)
                                                  + (102 * (j:66 * j:66)
                                                       * K:3572)
                                                  + (-42
                                                       * (j:66
                                                            * (j:66 * j:66))
                                                       * K:3572)
                                                  + (7
                                                       * ((j:66 * j:66)
                                                            * (j:66 * j:66))
                                                       * K:3572)
                                                  + (-99/2
                                                       * (K:3572 * K:3572))
                                                  + (102 * j:66
                                                       * (K:3572 * K:3572))
                                                  + (-63 * (j:66 * j:66)
                                                       * (K:3572 * K:3572))
                                                  + (14
                                                       * (j:66
                                                            * (j:66 * j:66))
                                                       * (K:3572 * K:3572))
                                                  + (34
                                                       * (K:3572
                                                            * (K:3572
                                                                 * K:3572)))
                                                  + (-42 * j:66
                                                       * (K:3572
                                                            * (K:3572
                                                                 * K:3572)))
                                                  + (14 * (j:66 * j:66)
                                                       * (K:3572
                                                            * (K:3572
                                                                 * K:3572)))
                                                  + (-21/2
                                                       * ((K:3572 * K:3572)
                                                            * (K:3572
                                                                 * K:3572)))
                                                  + (7 * j:66
                                                       * ((K:3572 * K:3572)
                                                            * (K:3572
                                                                 * K:3572)))
                                                  + (7/5
                                                       * (K:3572
                                                            * ((K:3572
                                                                  * K:3572)
                                                                 * (K:3572
                                                                    * K:3572))))))
           /\ (!(0 <= K:3572)
                 \/ (36 * mid___cost:3578) <= ((36 * __cost:70)
                                                 + (947/15 * K:3572)
                                                 + (-69 * j:66 * K:3572)
                                                 + (26 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (-6
                                                      * (j:66 * (j:66 * j:66))
                                                      * K:3572)
                                                 + (((j:66 * j:66)
                                                       * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-69/2 * (K:3572 * K:3572))
                                                 + (26 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (-9 * (j:66 * j:66)
                                                      * (K:3572 * K:3572))
                                                 + (2
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (26/3
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-6 * j:66
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (2 * (j:66 * j:66)
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-3/2
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (j:66
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (1/5
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))))
           /\ (!(0 <= K:3572)
                 \/ (36 * mid___cost:3578) <= ((36 * __cost:70)
                                                 + (797/15 * K:3572)
                                                 + (-65 * j:66 * K:3572)
                                                 + (26 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (-6
                                                      * (j:66 * (j:66 * j:66))
                                                      * K:3572)
                                                 + (((j:66 * j:66)
                                                       * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-65/2 * (K:3572 * K:3572))
                                                 + (26 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (-9 * (j:66 * j:66)
                                                      * (K:3572 * K:3572))
                                                 + (2
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (26/3
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-6 * j:66
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (2 * (j:66 * j:66)
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-3/2
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (j:66
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (1/5
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))))
           /\ (!(0 <= K:3572)
                 \/ (36 * mid___cost:3578) <= ((36 * __cost:70)
                                                 + (167/15 * K:3572)
                                                 + (-37 * j:66 * K:3572)
                                                 + (26 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (-6
                                                      * (j:66 * (j:66 * j:66))
                                                      * K:3572)
                                                 + (((j:66 * j:66)
                                                       * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-37/2 * (K:3572 * K:3572))
                                                 + (26 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (-9 * (j:66 * j:66)
                                                      * (K:3572 * K:3572))
                                                 + (2
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (26/3
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-6 * j:66
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (2 * (j:66 * j:66)
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-3/2
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (j:66
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (1/5
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))))
           /\ (!(0 <= K:3572)
                 \/ (30 * mid___cost:3578) <= ((30 * __cost:70)
                                                 + (174/5 * K:3572)
                                                 + (-45 * j:66 * K:3572)
                                                 + (21 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (-6
                                                      * (j:66 * (j:66 * j:66))
                                                      * K:3572)
                                                 + (((j:66 * j:66)
                                                       * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-45/2 * (K:3572 * K:3572))
                                                 + (21 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (-9 * (j:66 * j:66)
                                                      * (K:3572 * K:3572))
                                                 + (2
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (7
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-6 * j:66
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (2 * (j:66 * j:66)
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-3/2
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (j:66
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (1/5
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))))
           /\ (!(0 <= K:3572)
                 \/ (12 * mid___cost:3578) <= ((12 * __cost:70)
                                                 + (9/5 * K:3572)
                                                 + (-9 * j:66 * K:3572)
                                                 + (12 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (-6
                                                      * (j:66 * (j:66 * j:66))
                                                      * K:3572)
                                                 + (((j:66 * j:66)
                                                       * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-9/2 * (K:3572 * K:3572))
                                                 + (12 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (-9 * (j:66 * j:66)
                                                      * (K:3572 * K:3572))
                                                 + (2
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (4
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-6 * j:66
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (2 * (j:66 * j:66)
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-3/2
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (j:66
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (1/5
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))))
           /\ (!(0 <= K:3572) \/ -mid___cost:3578 <= -__cost:70)
           /\ (!(0 <= K:3572)
                 \/ (-3 * mid___cost:3578) <= ((-3 * __cost:70)
                                                 + (-7/6 * K:3572)
                                                 + (3 * j:66 * K:3572)
                                                 + -(((j:66 * j:66) * K:3572))
                                                 + (3/2 * (K:3572 * K:3572))
                                                 + -((j:66
                                                        * (K:3572 * K:3572)))
                                                 + (-1/3
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))))
           /\ (!(0 <= K:3572)
                 \/ (-6 * mid___cost:3578) <= ((-6 * __cost:70)
                                                 + (-31/3 * K:3572)
                                                 + (24 * j:66 * K:3572)
                                                 + (-5 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (12 * (K:3572 * K:3572))
                                                 + (-5 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (-5/3
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))))
           /\ (!(0 <= K:3572)
                 \/ (-6 * mid___cost:3578) <= ((-6 * __cost:70)
                                                 + (13/10 * K:3572)
                                                 + (-41/12 * j:66 * K:3572)
                                                 + (-3 * __cost:70 * K:3572)
                                                 + (6 * j:66 * __cost:70
                                                      * K:3572)
                                                 + (1/4 * (j:66 * j:66)
                                                      * K:3572)
                                                 + (5/3
                                                      * (j:66 * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-1/2
                                                      * ((j:66 * j:66)
                                                           * (j:66 * j:66))
                                                      * K:3572)
                                                 + (-4/3 * (K:3572 * K:3572))
                                                 + (-15/8 * j:66
                                                      * (K:3572 * K:3572))
                                                 + (3 * __cost:70
                                                      * (K:3572 * K:3572))
                                                 + (51/8 * (j:66 * j:66)
                                                      * (K:3572 * K:3572))
                                                 + (-7/2
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (1/2
                                                      * ((j:66 * j:66)
                                                           * (j:66 * j:66))
                                                      * (K:3572 * K:3572))
                                                 + (-7/8
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (31/6 * j:66
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (-17/4 * (j:66 * j:66)
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (5/6
                                                      * (j:66 * (j:66 * j:66))
                                                      * (K:3572
                                                           * (K:3572 * K:3572)))
                                                 + (31/24
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (-17/8 * j:66
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (5/8 * (j:66 * j:66)
                                                      * ((K:3572 * K:3572)
                                                           * (K:3572 * K:3572)))
                                                 + (-17/40
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))
                                                 + (1/4 * j:66
                                                      * (K:3572
                                                           * ((K:3572
                                                                 * K:3572)
                                                                * (K:3572
                                                                    * K:3572))))
                                                 + (1/24
                                                      * ((K:3572
                                                            * (K:3572
                                                                 * K:3572))
                                                           * (K:3572
                                                                * (K:3572
                                                                    * K:3572))))))
           /\ ((K:3572 = 0 /\ m:69 = mid_m:3574 /\ l:68 = mid_l:3575
                  /\ k:67 = mid_k:3576 /\ j:66 = mid_j:3577
                  /\ __cost:70 = mid___cost:3578)
                 \/ (1 <= K:3572
                       /\ (41 + (-28 * j:66)
                             + (-18 * ((-2 + j:66) * (-2 + j:66)))
                             + (-4
                                  * ((4 + (-4 * j:66) + (j:66 * j:66))
                                       * (-2 + j:66)))
                             + -(((-1 + (3 * j:66) + (-3 * (j:66 * j:66))
                                     + (j:66 * (j:66 * j:66))) * (-1 + j:66)))
                             + ((j:66 * (j:66 * j:66)) * j:66)) = 0
                       /\ (16 + (-12 * j:66)
                             + (-6 * ((-2 + j:66) * (-2 + j:66)))
                             + -(((4 + (-4 * j:66) + (j:66 * j:66))
                                    * (-2 + j:66))) + ((j:66 * j:66) * j:66)) = 0
                       /\ (16 + (-12 * j:66)
                             + (-6 * ((-2 + j:66) * (-2 + j:66)))
                             + -(((4 + (-4 * j:66) + (j:66 * j:66))
                                    * (-2 + j:66))) + (j:66 * (j:66 * j:66))) = 0
                       /\ (4 + (-4 * j:66) + -(((-2 + j:66) * (-2 + j:66)))
                             + (j:66 * j:66)) = 0
                       /\ (5 + (-3 * j:66)
                             + (-3 * ((-2 + j:66) * (-2 + j:66)))
                             + -(((4 + (-4 * j:66) + (j:66 * j:66))
                                    * (-2 + j:66)))
                             + ((1 + (-2 * j:66) + (j:66 * j:66))
                                  * (-1 + j:66))) = 0
                       /\ (4 + (-3 * j:66) + -(((-2 + j:66) * (-2 + j:66)))
                             + ((-1 + j:66) * j:66)) = 0
                       /\ (4 + (-2 * j:66)
                             + (-3 * ((-2 + j:66) * (-2 + j:66)))
                             + -(((4 + (-4 * j:66) + (j:66 * j:66))
                                    * (-2 + j:66))) + (-6 * __cost:70)
                             + (-6
                                  * ((-2 + j:66)
                                       * ((1/3 * j:66)
                                            + (-1/2 * (j:66 * j:66))
                                            + (1/6 * (j:66 * (j:66 * j:66)))
                                            + __cost:70)))
                             + (6
                                  * (((1/3 * j:66) + (-1/2 * (j:66 * j:66))
                                        + (1/6 * (j:66 * (j:66 * j:66)))
                                        + __cost:70) * (-1 + j:66)))) = 0
                       /\ (3 + (-2 * j:66) + -(((-2 + j:66) * (-2 + j:66)))
                             + ((-1 + j:66) * (-1 + j:66))) = 0
                       /\ 0 <= (53 + (-12 * j:66)
                                  + (-67 * ((-2 + j:66) * (-2 + j:66)))
                                  + (-26
                                       * ((4 + (-4 * j:66) + (j:66 * j:66))
                                            * (-2 + j:66)))
                                  + (7
                                       * ((-1 + (3 * j:66)
                                             + (-3 * (j:66 * j:66))
                                             + (j:66 * (j:66 * j:66)))
                                            * (-1 + j:66))))
                       /\ 0 <= (11 + (-6 * j:66)
                                  + (-7 * ((-2 + j:66) * (-2 + j:66)))
                                  + (-2
                                       * ((4 + (-4 * j:66) + (j:66 * j:66))
                                            * (-2 + j:66)))
                                  + ((-1 + (3 * j:66) + (-3 * (j:66 * j:66))
                                        + (j:66 * (j:66 * j:66)))
                                       * (-1 + j:66)))
                       /\ 0 <= (7 + (-4 * j:66)
                                  + (-5 * ((-2 + j:66) * (-2 + j:66)))
                                  + (-6
                                       * ((4 + (-4 * j:66) + (j:66 * j:66))
                                            * (-2 + j:66)))
                                  + ((-1 + (3 * j:66) + (-3 * (j:66 * j:66))
                                        + (j:66 * (j:66 * j:66)))
                                       * (-1 + j:66)))
                       /\ 0 <= (5 + (-3 * j:66)
                                  + (-7 * ((-2 + j:66) * (-2 + j:66)))
                                  + (-5
                                       * ((4 + (-4 * j:66) + (j:66 * j:66))
                                            * (-2 + j:66)))
                                  + ((-1 + (3 * j:66) + (-3 * (j:66 * j:66))
                                        + (j:66 * (j:66 * j:66)))
                                       * (-1 + j:66)))
                       /\ 0 <= (4 + (-2 * j:66) + ((-2 + j:66) * (-2 + j:66))
                                  + ((4 + (-4 * j:66) + (j:66 * j:66))
                                       * (-2 + j:66)))
                       /\ 0 <= (-1 + -j:66 + i:64)
                       /\ 0 <= (2 + -j:66 + ((-2 + j:66) * (-2 + j:66)))
                       /\ 0 <= (-1 + (-5 * ((-2 + j:66) * (-2 + j:66)))
                                  + (-6
                                       * ((4 + (-4 * j:66) + (j:66 * j:66))
                                            * (-2 + j:66)))
                                  + ((-1 + (3 * j:66) + (-3 * (j:66 * j:66))
                                        + (j:66 * (j:66 * j:66)))
                                       * (-1 + j:66)))
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= __cost:70
                       /\ 0 <= (16 + j:66
                                  + (-2 * ((-2 + j:66) * (-2 + j:66)))
                                  + ((4 + (-4 * j:66) + (j:66 * j:66))
                                       * (-2 + j:66))) /\ 0 <= j:66
                       /\ 0 <= (-2 + j:66 + ((-2 + j:66) * (-2 + j:66)))
                       /\ 0 <= (-4 + (2 * j:66)
                                  + (3 * ((-2 + j:66) * (-2 + j:66)))
                                  + ((4 + (-4 * j:66) + (j:66 * j:66))
                                       * (-2 + j:66)))
                       /\ 0 <= (-4 + (3 * j:66) + ((-2 + j:66) * (-2 + j:66)))
                       /\ 0 <= (-7 + (4 * j:66)
                                  + (4 * ((-2 + j:66) * (-2 + j:66)))
                                  + ((4 + (-4 * j:66) + (j:66 * j:66))
                                       * (-2 + j:66))
                                  + -(((-1 + (3 * j:66)
                                          + (-3 * (j:66 * j:66))
                                          + (j:66 * (j:66 * j:66)))
                                         * (-1 + j:66))) + (12 * __cost:70)
                                  + (6
                                       * ((-2 + j:66)
                                            * ((1/3 * j:66)
                                                 + (-1/2 * (j:66 * j:66))
                                                 + (1/6
                                                      * (j:66 * (j:66 * j:66)))
                                                 + __cost:70))))
                       /\ 0 <= (-29 + (28 * j:66)
                                  + (-5 * ((-2 + j:66) * (-2 + j:66)))
                                  + (-6
                                       * ((4 + (-4 * j:66) + (j:66 * j:66))
                                            * (-2 + j:66)))
                                  + ((-1 + (3 * j:66) + (-3 * (j:66 * j:66))
                                        + (j:66 * (j:66 * j:66)))
                                       * (-1 + j:66)))
                       /\ (41 + (-28 * mid_k:3576)
                             + (-18 * ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + (-4
                                  * ((4 + (-4 * mid_k:3576)
                                        + (mid_k:3576 * mid_k:3576))
                                       * (-2 + mid_k:3576)))
                             + -(((-1 + (3 * mid_k:3576)
                                     + (-3 * (mid_k:3576 * mid_k:3576))
                                     + (mid_k:3576
                                          * (mid_k:3576 * mid_k:3576)))
                                    * (-1 + mid_k:3576)))
                             + ((mid_k:3576 * (mid_k:3576 * mid_k:3576))
                                  * mid_k:3576)) = 0
                       /\ (16 + (-12 * mid_k:3576)
                             + (-6 * ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + -(((4 + (-4 * mid_k:3576)
                                     + (mid_k:3576 * mid_k:3576))
                                    * (-2 + mid_k:3576)))
                             + ((mid_k:3576 * mid_k:3576) * mid_k:3576)) = 0
                       /\ (16 + (-12 * mid_k:3576)
                             + (-6 * ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + -(((4 + (-4 * mid_k:3576)
                                     + (mid_k:3576 * mid_k:3576))
                                    * (-2 + mid_k:3576)))
                             + (mid_k:3576 * (mid_k:3576 * mid_k:3576))) = 0
                       /\ (4 + (-4 * mid_k:3576)
                             + -(((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + (mid_k:3576 * mid_k:3576)) = 0
                       /\ (5 + (-3 * mid_k:3576)
                             + (-3 * ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + -(((4 + (-4 * mid_k:3576)
                                     + (mid_k:3576 * mid_k:3576))
                                    * (-2 + mid_k:3576)))
                             + ((1 + (-2 * mid_k:3576)
                                   + (mid_k:3576 * mid_k:3576))
                                  * (-1 + mid_k:3576))) = 0
                       /\ (4 + (-3 * mid_k:3576)
                             + -(((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + ((-1 + mid_k:3576) * mid_k:3576)) = 0
                       /\ (3 + (-2 * mid_k:3576)
                             + -(((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                             + ((-1 + mid_k:3576) * (-1 + mid_k:3576))) = 0
                       /\ (-1 + -mid_k:3576 + mid_j:3577) = 0
                       /\ (-mid___cost:3578
                             + -(((-2 + mid_k:3576) * mid___cost:3578))
                             + (mid___cost:3578 * (-1 + mid_k:3576))) = 0
                       /\ 0 <= (53 + (-12 * mid_k:3576)
                                  + (-67
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + (-26
                                       * ((4 + (-4 * mid_k:3576)
                                             + (mid_k:3576 * mid_k:3576))
                                            * (-2 + mid_k:3576)))
                                  + (7
                                       * ((-1 + (3 * mid_k:3576)
                                             + (-3
                                                  * (mid_k:3576 * mid_k:3576))
                                             + (mid_k:3576
                                                  * (mid_k:3576 * mid_k:3576)))
                                            * (-1 + mid_k:3576))))
                       /\ 0 <= (11 + (-6 * mid_k:3576)
                                  + (-7
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + (-2
                                       * ((4 + (-4 * mid_k:3576)
                                             + (mid_k:3576 * mid_k:3576))
                                            * (-2 + mid_k:3576)))
                                  + ((-1 + (3 * mid_k:3576)
                                        + (-3 * (mid_k:3576 * mid_k:3576))
                                        + (mid_k:3576
                                             * (mid_k:3576 * mid_k:3576)))
                                       * (-1 + mid_k:3576)))
                       /\ 0 <= (7 + (-4 * mid_k:3576)
                                  + (-5
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + (-6
                                       * ((4 + (-4 * mid_k:3576)
                                             + (mid_k:3576 * mid_k:3576))
                                            * (-2 + mid_k:3576)))
                                  + ((-1 + (3 * mid_k:3576)
                                        + (-3 * (mid_k:3576 * mid_k:3576))
                                        + (mid_k:3576
                                             * (mid_k:3576 * mid_k:3576)))
                                       * (-1 + mid_k:3576)))
                       /\ 0 <= (5 + (-3 * mid_k:3576)
                                  + (-7
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + (-5
                                       * ((4 + (-4 * mid_k:3576)
                                             + (mid_k:3576 * mid_k:3576))
                                            * (-2 + mid_k:3576)))
                                  + ((-1 + (3 * mid_k:3576)
                                        + (-3 * (mid_k:3576 * mid_k:3576))
                                        + (mid_k:3576
                                             * (mid_k:3576 * mid_k:3576)))
                                       * (-1 + mid_k:3576)))
                       /\ 0 <= (4 + (-2 * mid_k:3576)
                                  + (-3
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + -(((4 + (-4 * mid_k:3576)
                                          + (mid_k:3576 * mid_k:3576))
                                         * (-2 + mid_k:3576)))
                                  + (6 * mid___cost:3578))
                       /\ 0 <= (4 + (-2 * mid_k:3576)
                                  + ((-2 + mid_k:3576) * (-2 + mid_k:3576))
                                  + ((4 + (-4 * mid_k:3576)
                                        + (mid_k:3576 * mid_k:3576))
                                       * (-2 + mid_k:3576)))
                       /\ 0 <= (-1 + -mid_k:3576 + i:64)
                       /\ 0 <= (2 + -mid_k:3576
                                  + ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                       /\ 0 <= (-1
                                  + (-5
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + (-6
                                       * ((4 + (-4 * mid_k:3576)
                                             + (mid_k:3576 * mid_k:3576))
                                            * (-2 + mid_k:3576)))
                                  + ((-1 + (3 * mid_k:3576)
                                        + (-3 * (mid_k:3576 * mid_k:3576))
                                        + (mid_k:3576
                                             * (mid_k:3576 * mid_k:3576)))
                                       * (-1 + mid_k:3576)))
                       /\ 0 <= (1
                                  + (-2
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + -(((4 + (-4 * mid_k:3576)
                                          + (mid_k:3576 * mid_k:3576))
                                         * (-2 + mid_k:3576)))
                                  + -(((-1 + (3 * mid_k:3576)
                                          + (-3 * (mid_k:3576 * mid_k:3576))
                                          + (mid_k:3576
                                               * (mid_k:3576 * mid_k:3576)))
                                         * (-1 + mid_k:3576)))
                                  + (12 * mid___cost:3578)
                                  + (6
                                       * ((-2 + mid_k:3576) * mid___cost:3578)))
                       /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= (16 + mid_k:3576
                                  + (-2
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + ((4 + (-4 * mid_k:3576)
                                        + (mid_k:3576 * mid_k:3576))
                                       * (-2 + mid_k:3576)))
                       /\ 0 <= mid_k:3576
                       /\ 0 <= (-2 + mid_k:3576
                                  + ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                       /\ 0 <= (-4 + (2 * mid_k:3576)
                                  + (3
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + ((4 + (-4 * mid_k:3576)
                                        + (mid_k:3576 * mid_k:3576))
                                       * (-2 + mid_k:3576)))
                       /\ 0 <= (-4 + (3 * mid_k:3576)
                                  + ((-2 + mid_k:3576) * (-2 + mid_k:3576)))
                       /\ 0 <= (-29 + (28 * mid_k:3576)
                                  + (-5
                                       * ((-2 + mid_k:3576)
                                            * (-2 + mid_k:3576)))
                                  + (-6
                                       * ((4 + (-4 * mid_k:3576)
                                             + (mid_k:3576 * mid_k:3576))
                                            * (-2 + mid_k:3576)))
                                  + ((-1 + (3 * mid_k:3576)
                                        + (-3 * (mid_k:3576 * mid_k:3576))
                                        + (mid_k:3576
                                             * (mid_k:3576 * mid_k:3576)))
                                       * (-1 + mid_k:3576)))))
           /\ (0 = K:3572 \/ !((1 + __cost:70) <= 0))
           /\ (!((0 <= K:3573 /\ K:3573 <= 0))
                 \/ k':3091 = (mid_k:3576 + K:3573))
           /\ (!(1 <= K:3573)
                 \/ k':3091 = (-1 + mid_k:3576 + mid_j:3577 + -mid_k:3576
                                 + K:3573))
           /\ (!(0 <= K:3573) \/ __cost':2990 = mid___cost:3578)
           /\ (!(0 <= K:3573) \/ j':3267 = (mid_j:3577 + K:3573))
           /\ (!((0 <= K:3573 /\ K:3573 <= 0))
                 \/ k':3091 <= (mid_k:3576 + (7/2 * K:3573)
                                  + -((mid_j:3577 * K:3573))
                                  + (-1/2 * (K:3573 * K:3573))))
           /\ (!(1 <= K:3573)
                 \/ k':3091 <= (-1 + mid_j:3577 + mid_k:3576 + -mid_k:3576
                                  + (7/2 * K:3573) + -((mid_j:3577 * K:3573))
                                  + (-1/2 * (K:3573 * K:3573))))
           /\ (!((0 <= K:3573 /\ K:3573 <= 0))
                 \/ k':3091 <= (mid_k:3576 + (1/2 * K:3573) + (i:64 * K:3573)
                                  + -((mid_j:3577 * K:3573))
                                  + (-1/2 * (K:3573 * K:3573))))
           /\ (!(1 <= K:3573)
                 \/ k':3091 <= (-1 + mid_j:3577 + mid_k:3576 + -mid_k:3576
                                  + (1/2 * K:3573) + (i:64 * K:3573)
                                  + -((mid_j:3577 * K:3573))
                                  + (-1/2 * (K:3573 * K:3573))))
           /\ (!((0 <= K:3573 /\ K:3573 <= 0))
                 \/ -k':3091 <= (-mid_k:3576 + (-3/2 * K:3573)
                                   + (mid_j:3577 * K:3573)
                                   + (1/2 * (K:3573 * K:3573))))
           /\ (!(1 <= K:3573)
                 \/ -k':3091 <= (1 + mid_k:3576 + -mid_k:3576 + -mid_j:3577
                                   + (-3/2 * K:3573) + (mid_j:3577 * K:3573)
                                   + (1/2 * (K:3573 * K:3573))))
           /\ ((K:3573 = 0 /\ mid_m:3574 = m':2991 /\ mid_l:3575 = l':3019
                  /\ mid_k:3576 = k':3091 /\ mid_j:3577 = j':3267
                  /\ mid___cost:3578 = __cost':2990)
                 \/ (1 <= K:3573 /\ 0 <= (-1 + -mid___cost:3578)
                       /\ 0 <= (2 + -mid_j:3577)
                       /\ 0 <= (-1 + -mid_j:3577 + i:64)
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= mid_j:3577
                       /\ (-1 + -k':3091 + j':3267) = 0
                       /\ 0 <= (-1 + -__cost':2990) /\ 0 <= (2 + -k':3091)
                       /\ 0 <= (-1 + -k':3091 + i:64)
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= k':3091))
           /\ (0 = K:3573 \/ (1 + mid___cost:3578) <= 0)
           /\ (K:3572 + K:3573) = K:3564
           /\ (!(0 <= K:3579) \/ mid_l:3582 = l:68)
           /\ (!((0 <= K:3579 /\ K:3579 <= 0)) \/ mid_j:3584 = j:66)
           /\ (!(1 <= K:3579) \/ mid_j:3584 = 1)
           /\ (!(0 <= K:3579) \/ mid_m:3581 = m:69)
           /\ (!((0 <= K:3579 /\ K:3579 <= 0)) \/ mid_k:3583 = k:67)
           /\ (!(1 <= K:3579) \/ mid_k:3583 = 0)
           /\ (!(0 <= K:3579) \/ mid___cost:3585 = __cost:70)
           /\ ((K:3579 = 0 /\ m:69 = mid_m:3581 /\ l:68 = mid_l:3582
                  /\ k:67 = mid_k:3583 /\ j:66 = mid_j:3584
                  /\ __cost:70 = mid___cost:3585)
                 \/ (1 <= K:3579 /\ j:66 = 0 /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= (-1 + i:64) /\ (-1 + mid_j:3584) = 0
                       /\ mid_k:3583 = 0 /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= (-1 + i:64)))
           /\ (0 = K:3579 \/ !((1 + -j:66) <= 0))
           /\ (!((0 <= K:3580 /\ K:3580 <= 0))
                 \/ (-j':3267 + l':3019) = (-mid_j:3584 + mid_l:3582))
           /\ (!(1 <= K:3580) \/ (-j':3267 + l':3019) = -2)
           /\ (!(0 <= K:3580) \/ j':3267 = (mid_j:3584 + K:3580))
           /\ (!((0 <= K:3580 /\ K:3580 <= 0))
                 \/ (-j':3267 + k':3091) = (-mid_j:3584 + mid_k:3583))
           /\ (!(1 <= K:3580) \/ (-j':3267 + k':3091) = -1)
           /\ (!(0 <= K:3580)
                 \/ (210 * __cost':2990) <= ((210 * mid___cost:3585)
                                               + (1363/15 * K:3580)
                                               + (-68 * mid_j:3584 * K:3580)
                                               + (7
                                                    * (mid_j:3584
                                                         * mid_j:3584)
                                                    * K:3580)
                                               + (-8
                                                    * (mid_j:3584
                                                         * (mid_j:3584
                                                              * mid_j:3584))
                                                    * K:3580)
                                               + (4
                                                    * ((mid_j:3584
                                                          * mid_j:3584)
                                                         * (mid_j:3584
                                                              * mid_j:3584))
                                                    * K:3580)
                                               + (-34 * (K:3580 * K:3580))
                                               + (7 * mid_j:3584
                                                    * (K:3580 * K:3580))
                                               + (-12
                                                    * (mid_j:3584
                                                         * mid_j:3584)
                                                    * (K:3580 * K:3580))
                                               + (8
                                                    * (mid_j:3584
                                                         * (mid_j:3584
                                                              * mid_j:3584))
                                                    * (K:3580 * K:3580))
                                               + (7/3
                                                    * (K:3580
                                                         * (K:3580 * K:3580)))
                                               + (-8 * mid_j:3584
                                                    * (K:3580
                                                         * (K:3580 * K:3580)))
                                               + (8
                                                    * (mid_j:3584
                                                         * mid_j:3584)
                                                    * (K:3580
                                                         * (K:3580 * K:3580)))
                                               + (-2
                                                    * ((K:3580 * K:3580)
                                                         * (K:3580 * K:3580)))
                                               + (4 * mid_j:3584
                                                    * ((K:3580 * K:3580)
                                                         * (K:3580 * K:3580)))
                                               + (4/5
                                                    * (K:3580
                                                         * ((K:3580 * K:3580)
                                                              * (K:3580
                                                                   * K:3580))))))
           /\ (!(0 <= K:3580)
                 \/ (60 * __cost':2990) <= ((60 * mid___cost:3585)
                                              + (872/15 * K:3580)
                                              + (-47 * mid_j:3584 * K:3580)
                                              + (8
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * K:3580)
                                              + (-2
                                                   * (mid_j:3584
                                                        * (mid_j:3584
                                                             * mid_j:3584))
                                                   * K:3580)
                                              + (((mid_j:3584 * mid_j:3584)
                                                    * (mid_j:3584
                                                         * mid_j:3584))
                                                   * K:3580)
                                              + (-47/2 * (K:3580 * K:3580))
                                              + (8 * mid_j:3584
                                                   * (K:3580 * K:3580))
                                              + (-3
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * (K:3580 * K:3580))
                                              + (2
                                                   * (mid_j:3584
                                                        * (mid_j:3584
                                                             * mid_j:3584))
                                                   * (K:3580 * K:3580))
                                              + (8/3
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))
                                              + (-2 * mid_j:3584
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))
                                              + (2
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))
                                              + (-1/2
                                                   * ((K:3580 * K:3580)
                                                        * (K:3580 * K:3580)))
                                              + (mid_j:3584
                                                   * ((K:3580 * K:3580)
                                                        * (K:3580 * K:3580)))
                                              + (1/5
                                                   * (K:3580
                                                        * ((K:3580 * K:3580)
                                                             * (K:3580
                                                                  * K:3580))))))
           /\ (!(0 <= K:3580)
                 \/ (60 * __cost':2990) <= ((60 * mid___cost:3585)
                                              + (1369/30 * K:3580)
                                              + (-42 * mid_j:3584 * K:3580)
                                              + (8
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * K:3580)
                                              + (-2
                                                   * (mid_j:3584
                                                        * (mid_j:3584
                                                             * mid_j:3584))
                                                   * K:3580)
                                              + (((mid_j:3584 * mid_j:3584)
                                                    * (mid_j:3584
                                                         * mid_j:3584))
                                                   * K:3580)
                                              + (-21 * (K:3580 * K:3580))
                                              + (8 * mid_j:3584
                                                   * (K:3580 * K:3580))
                                              + (-3
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * (K:3580 * K:3580))
                                              + (2
                                                   * (mid_j:3584
                                                        * (mid_j:3584
                                                             * mid_j:3584))
                                                   * (K:3580 * K:3580))
                                              + (8/3
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))
                                              + (-2 * mid_j:3584
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))
                                              + (2
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))
                                              + (-1/2
                                                   * ((K:3580 * K:3580)
                                                        * (K:3580 * K:3580)))
                                              + (mid_j:3584
                                                   * ((K:3580 * K:3580)
                                                        * (K:3580 * K:3580)))
                                              + (1/5
                                                   * (K:3580
                                                        * ((K:3580 * K:3580)
                                                             * (K:3580
                                                                  * K:3580))))))
           /\ (!(0 <= K:3580)
                 \/ (-2 * __cost':2990) <= ((-2 * mid___cost:3585)
                                              + (-11/3 * K:3580)
                                              + (4 * mid_j:3584 * K:3580)
                                              + -(((mid_j:3584 * mid_j:3584)
                                                     * K:3580))
                                              + (2 * (K:3580 * K:3580))
                                              + -((mid_j:3584
                                                     * (K:3580 * K:3580)))
                                              + (-1/3
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))))
           /\ (!(0 <= K:3580)
                 \/ (-6 * __cost':2990) <= ((-6 * mid___cost:3585)
                                              + (-73/3 * K:3580)
                                              + (24 * mid_j:3584 * K:3580)
                                              + (-5
                                                   * (mid_j:3584 * mid_j:3584)
                                                   * K:3580)
                                              + (12 * (K:3580 * K:3580))
                                              + (-5 * mid_j:3584
                                                   * (K:3580 * K:3580))
                                              + (-5/3
                                                   * (K:3580
                                                        * (K:3580 * K:3580)))))
           /\ ((K:3580 = 0 /\ mid_m:3581 = m':2991 /\ mid_l:3582 = l':3019
                  /\ mid_k:3583 = k':3091 /\ mid_j:3584 = j':3267
                  /\ mid___cost:3585 = __cost':2990)
                 \/ (1 <= K:3580
                       /\ (-1 + (-6 * mid___cost:3585) + mid_j:3584
                             + -(((1 + (-2 * mid_j:3584)
                                     + (mid_j:3584 * mid_j:3584))
                                    * (-1 + mid_j:3584)))
                             + (-6
                                  * ((-2 + mid_j:3584)
                                       * (mid___cost:3585
                                            + (1/3 * mid_j:3584)
                                            + (-1/2
                                                 * (mid_j:3584 * mid_j:3584))
                                            + (1/6
                                                 * (mid_j:3584
                                                      * (mid_j:3584
                                                           * mid_j:3584))))))
                             + (6
                                  * ((mid___cost:3585 + (1/3 * mid_j:3584)
                                        + (-1/2 * (mid_j:3584 * mid_j:3584))
                                        + (1/6
                                             * (mid_j:3584
                                                  * (mid_j:3584 * mid_j:3584))))
                                       * (-1 + mid_j:3584)))) = 0
                       /\ (7 + (-9 * mid_j:3584)
                             + (3 * (mid_j:3584 * mid_j:3584))
                             + -(((1 + (-2 * mid_j:3584)
                                     + (mid_j:3584 * mid_j:3584))
                                    * (-1 + mid_j:3584)))
                             + ((4 + (-4 * mid_j:3584)
                                   + (mid_j:3584 * mid_j:3584))
                                  * (-2 + mid_j:3584))) = 0
                       /\ (3 + (-8 * mid_j:3584)
                             + (6 * (mid_j:3584 * mid_j:3584))
                             + (4
                                  * ((1 + (-2 * mid_j:3584)
                                        + (mid_j:3584 * mid_j:3584))
                                       * (-1 + mid_j:3584)))
                             + -(((mid_j:3584 * (mid_j:3584 * mid_j:3584))
                                    * mid_j:3584))
                             + ((-1 + (3 * mid_j:3584)
                                   + (-3 * (mid_j:3584 * mid_j:3584))
                                   + (mid_j:3584 * (mid_j:3584 * mid_j:3584)))
                                  * (-1 + mid_j:3584))) = 0
                       /\ (mid_j:3584 + -((mid_j:3584 * mid_j:3584))
                             + ((-1 + mid_j:3584) * mid_j:3584)) = 0
                       /\ (-1 + (2 * mid_j:3584)
                             + -((mid_j:3584 * mid_j:3584))
                             + ((-1 + mid_j:3584) * (-1 + mid_j:3584))) = 0
                       /\ (-1 + (3 * mid_j:3584)
                             + (-3 * (mid_j:3584 * mid_j:3584))
                             + -(((1 + (-2 * mid_j:3584)
                                     + (mid_j:3584 * mid_j:3584))
                                    * (-1 + mid_j:3584)))
                             + (mid_j:3584 * (mid_j:3584 * mid_j:3584))) = 0
                       /\ (-1 + (3 * mid_j:3584)
                             + (-3 * (mid_j:3584 * mid_j:3584))
                             + -(((1 + (-2 * mid_j:3584)
                                     + (mid_j:3584 * mid_j:3584))
                                    * (-1 + mid_j:3584)))
                             + ((mid_j:3584 * mid_j:3584) * mid_j:3584)) = 0
                       /\ (-4 + (4 * mid_j:3584)
                             + -((mid_j:3584 * mid_j:3584))
                             + ((-2 + mid_j:3584) * (-2 + mid_j:3584))) = 0
                       /\ 0 <= (57 + (-66 * mid_j:3584)
                                  + (13 * (mid_j:3584 * mid_j:3584))
                                  + (-37
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + (4
                                       * ((mid_j:3584
                                             * (mid_j:3584 * mid_j:3584))
                                            * mid_j:3584)))
                       /\ 0 <= (48 + (-57 * mid_j:3584)
                                  + (14 * (mid_j:3584 * mid_j:3584))
                                  + (-20
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + (2
                                       * ((mid_j:3584
                                             * (mid_j:3584 * mid_j:3584))
                                            * mid_j:3584)))
                       /\ 0 <= (39 + (-46 * mid_j:3584)
                                  + (12 * (mid_j:3584 * mid_j:3584))
                                  + (-10
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + ((mid_j:3584 * (mid_j:3584 * mid_j:3584))
                                       * mid_j:3584))
                       /\ 0 <= (27 + (-30 * mid_j:3584)
                                  + (7 * (mid_j:3584 * mid_j:3584))
                                  + (-10
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + ((mid_j:3584 * (mid_j:3584 * mid_j:3584))
                                       * mid_j:3584))
                       /\ 0 <= (10 + (-18 * mid_j:3584)
                                  + (7 * (mid_j:3584 * mid_j:3584))
                                  + (-10
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + ((mid_j:3584 * (mid_j:3584 * mid_j:3584))
                                       * mid_j:3584))
                       /\ 0 <= (7 + (-9 * mid_j:3584)
                                  + (3 * (mid_j:3584 * mid_j:3584)))
                       /\ 0 <= (5 + (-6 * mid_j:3584)
                                  + -((mid_j:3584 * mid_j:3584))
                                  + (-17
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + (2
                                       * ((mid_j:3584
                                             * (mid_j:3584 * mid_j:3584))
                                            * mid_j:3584)))
                       /\ 0 <= (6 + (-5 * mid_j:3584)
                                  + (mid_j:3584 * mid_j:3584))
                       /\ 0 <= (4 + (-4 * mid_j:3584)
                                  + (mid_j:3584 * mid_j:3584))
                       /\ 0 <= (1 + (-2 * mid_j:3584)
                                  + (mid_j:3584 * mid_j:3584))
                       /\ 0 <= (-1 + -mid_j:3584 + i:64)
                       /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= ((1 + (-2 * mid_j:3584)
                                   + (mid_j:3584 * mid_j:3584))
                                  * (-1 + mid_j:3584))
                       /\ 0 <= (-1 + mid_j:3584)
                       /\ 0 <= (3 + (2 * mid_j:3584)
                                  + (-9 * (mid_j:3584 * mid_j:3584))
                                  + (-31
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + (4
                                       * ((mid_j:3584
                                             * (mid_j:3584 * mid_j:3584))
                                            * mid_j:3584)))
                       /\ 0 <= (-3 + (5 * mid_j:3584)
                                  + (-2 * (mid_j:3584 * mid_j:3584))
                                  + ((1 + (-2 * mid_j:3584)
                                        + (mid_j:3584 * mid_j:3584))
                                       * (-1 + mid_j:3584)))
                       /\ 0 <= (-3 + (8 * mid_j:3584)
                                  + (-6 * (mid_j:3584 * mid_j:3584))
                                  + (-4
                                       * ((1 + (-2 * mid_j:3584)
                                             + (mid_j:3584 * mid_j:3584))
                                            * (-1 + mid_j:3584)))
                                  + ((mid_j:3584 * (mid_j:3584 * mid_j:3584))
                                       * mid_j:3584))
                       /\ 0 <= (-5 + (8 * mid_j:3584)
                                  + (-3 * (mid_j:3584 * mid_j:3584))
                                  + ((1 + (-2 * mid_j:3584)
                                        + (mid_j:3584 * mid_j:3584))
                                       * (-1 + mid_j:3584)))
                       /\ 0 <= (-13 + (18 * mid_j:3584)
                                  + (-5 * (mid_j:3584 * mid_j:3584))
                                  + ((1 + (-2 * mid_j:3584)
                                        + (mid_j:3584 * mid_j:3584))
                                       * (-1 + mid_j:3584)))
                       /\ (16 + (-9 * j':3267)
                             + (3 * ((-1 + j':3267) * (-1 + j':3267)))
                             + -(((4 + (-4 * j':3267) + (j':3267 * j':3267))
                                    * (-2 + j':3267)))
                             + ((9 + (-6 * j':3267) + (j':3267 * j':3267))
                                  * (-3 + j':3267))) = 0
                       /\ (11 + (-8 * j':3267)
                             + (6 * ((-1 + j':3267) * (-1 + j':3267)))
                             + (4
                                  * ((4 + (-4 * j':3267)
                                        + (j':3267 * j':3267))
                                       * (-2 + j':3267)))
                             + -(((-1 + (3 * j':3267)
                                     + (-3 * (j':3267 * j':3267))
                                     + (j':3267 * (j':3267 * j':3267)))
                                    * (-1 + j':3267)))
                             + ((-8 + (12 * j':3267)
                                   + (-6 * (j':3267 * j':3267))
                                   + (j':3267 * (j':3267 * j':3267)))
                                  * (-2 + j':3267))) = 0
                       /\ (1 + -j':3267 + k':3091) = 0
                       /\ (2 + -j':3267 + l':3019) = 0
                       /\ (-1 + j':3267
                             + -(((-1 + j':3267) * (-1 + j':3267)))
                             + ((-2 + j':3267) * (-1 + j':3267))) = 0
                       /\ (-3 + (2 * j':3267)
                             + -(((-1 + j':3267) * (-1 + j':3267)))
                             + ((-2 + j':3267) * (-2 + j':3267))) = 0
                       /\ (-4 + (3 * j':3267)
                             + (-3 * ((-1 + j':3267) * (-1 + j':3267)))
                             + -(((4 + (-4 * j':3267) + (j':3267 * j':3267))
                                    * (-2 + j':3267)))
                             + ((-1 + j':3267)
                                  * (1 + (-2 * j':3267) + (j':3267 * j':3267)))) = 0
                       /\ (-4 + (3 * j':3267)
                             + (-3 * ((-1 + j':3267) * (-1 + j':3267)))
                             + -(((4 + (-4 * j':3267) + (j':3267 * j':3267))
                                    * (-2 + j':3267)))
                             + ((1 + (-2 * j':3267) + (j':3267 * j':3267))
                                  * (-1 + j':3267))) = 0
                       /\ (-8 + (4 * j':3267)
                             + -(((-1 + j':3267) * (-1 + j':3267)))
                             + ((-3 + j':3267) * (-3 + j':3267))) = 0
                       /\ 0 <= (123 + (-66 * j':3267)
                                  + (13 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-37
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + (4
                                       * ((-1 + (3 * j':3267)
                                             + (-3 * (j':3267 * j':3267))
                                             + (j':3267 * (j':3267 * j':3267)))
                                            * (-1 + j':3267))))
                       /\ 0 <= (105 + (-57 * j':3267)
                                  + (14 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-20
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + (2
                                       * ((-1 + (3 * j':3267)
                                             + (-3 * (j':3267 * j':3267))
                                             + (j':3267 * (j':3267 * j':3267)))
                                            * (-1 + j':3267))))
                       /\ 0 <= (85 + (-46 * j':3267)
                                  + (12 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-10
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + ((-1 + (3 * j':3267)
                                        + (-3 * (j':3267 * j':3267))
                                        + (j':3267 * (j':3267 * j':3267)))
                                       * (-1 + j':3267)))
                       /\ 0 <= (57 + (-30 * j':3267)
                                  + (7 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-10
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + ((-1 + (3 * j':3267)
                                        + (-3 * (j':3267 * j':3267))
                                        + (j':3267 * (j':3267 * j':3267)))
                                       * (-1 + j':3267)))
                       /\ 0 <= (28 + (-18 * j':3267)
                                  + (7 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-10
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + ((-1 + (3 * j':3267)
                                        + (-3 * (j':3267 * j':3267))
                                        + (j':3267 * (j':3267 * j':3267)))
                                       * (-1 + j':3267)))
                       /\ 0 <= (16 + (-9 * j':3267)
                                  + (3 * ((-1 + j':3267) * (-1 + j':3267))))
                       /\ 0 <= (11 + (-6 * j':3267)
                                  + -(((-1 + j':3267) * (-1 + j':3267)))
                                  + (-17
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + (2
                                       * ((-1 + (3 * j':3267)
                                             + (-3 * (j':3267 * j':3267))
                                             + (j':3267 * (j':3267 * j':3267)))
                                            * (-1 + j':3267))))
                       /\ 0 <= (11 + (-5 * j':3267)
                                  + ((-1 + j':3267) * (-1 + j':3267)))
                       /\ 0 <= (8 + (-4 * j':3267)
                                  + ((-1 + j':3267) * (-1 + j':3267)))
                       /\ 0 <= (3 + (-2 * j':3267)
                                  + ((-1 + j':3267) * (-1 + j':3267)))
                       /\ 0 <= (-j':3267 + i:64) /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= ((4 + (-4 * j':3267) + (j':3267 * j':3267))
                                  * (-2 + j':3267)) /\ 0 <= (-2 + j':3267)
                       /\ 0 <= (1 + (2 * j':3267)
                                  + (-9 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-31
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + (4
                                       * ((-1 + (3 * j':3267)
                                             + (-3 * (j':3267 * j':3267))
                                             + (j':3267 * (j':3267 * j':3267)))
                                            * (-1 + j':3267))))
                       /\ 0 <= (-8 + (5 * j':3267)
                                  + (-2 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + ((4 + (-4 * j':3267)
                                        + (j':3267 * j':3267))
                                       * (-2 + j':3267)))
                       /\ 0 <= (-11 + (8 * j':3267)
                                  + (-6 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + (-4
                                       * ((4 + (-4 * j':3267)
                                             + (j':3267 * j':3267))
                                            * (-2 + j':3267)))
                                  + ((-1 + (3 * j':3267)
                                        + (-3 * (j':3267 * j':3267))
                                        + (j':3267 * (j':3267 * j':3267)))
                                       * (-1 + j':3267)))
                       /\ 0 <= (-13 + (8 * j':3267)
                                  + (-3 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + ((4 + (-4 * j':3267)
                                        + (j':3267 * j':3267))
                                       * (-2 + j':3267)))
                       /\ 0 <= (-31 + (18 * j':3267)
                                  + (-5 * ((-1 + j':3267) * (-1 + j':3267)))
                                  + ((4 + (-4 * j':3267)
                                        + (j':3267 * j':3267))
                                       * (-2 + j':3267)))))
           /\ (0 = K:3580 \/ (1 + -mid_j:3584) <= 0)
           /\ (K:3579 + K:3580) = K:3564 /\ 0 <= K:3564)}
}