% Steiner--Lehmus Theorem

off rlabout;



rlset reals;


{}


h1 := u2>=0 and x1>=0$


h2 := r^2=1+x1^2=u1^2+(u2-x1)^2$


h3 := x2<=0 and r^2=(x2-x1)^2$


h4 := u1*x2+u2*x3-x2*x3=0$


h5 := x4<=1 and (x4-1)^2=(u1-1)^2+u2^2$


h6 := (x4-x5)^2+x6^2=(u1-x5)^2+(u2-x6)^2 and u1*x6-u2*x5-u2+x6=0$


h7 := (-1-u1)^2+u2^2<2^2$



h := h1 and h2 and h3 and h4 and h5 and h6 and h7$



g := (u1-x3)^2+u2^2<(x5-1)^2+x6^2$



sl9 := all({x6,x5,x4,x3,x2,x1,r},h impl g)$



rlgqe sl9;


            2            2
{{u2 <> 0,u1  - 2*u1 + u2  - 3 <> 0},

   2            2                4       2   2       2     4       2
 u1  - 2*u1 + u2  + 1 < 0 or ((u1  + 2*u1 *u2  - 2*u1  + u2  + 2*u2  + 1 < 0 or 

                2            2               2            2
 ((u2 <= 0 or u1  - 2*u1 + u2  + 1 <> 0 or u1  + 2*u1 + u2  - 3 >= 0

       2        3                            11          10          9   3
  or u1 *u2 + u2  - u2 < 0 or (u1 <> 0 and u1  *u2 - 3*u1  *u2 + 5*u1 *u2

         9          8   3       8           7   5        7   3        7
  - 25*u1 *u2 - 9*u1 *u2  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2

        6   5        6   3        6           5   7         5   5         5   3
  - 6*u1 *u2  - 52*u1 *u2  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2

          5          4   7         4   5         4   3        4          3   9
  - 130*u1 *u2 + 6*u1 *u2  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2

         3   7         3   5         3   3        3          2   9        2   7
  - 76*u1 *u2  + 110*u1 *u2  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2

         2   5         2   3        2           11           9           7
  + 30*u1 *u2  - 100*u1 *u2  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2

            5           3                  11        9       7        5        3
  + 70*u1*u2  + 13*u1*u2  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2

                    12   2       12       11   2        11       10   4
  - 9*u2 <= 0 and u1  *u2  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2

         10   2         10        9   4         9   2         9        8   6
  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2

         8   4         8   2         8        7   6         7   4         7   2
  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2

          7        6   8         6   6         6   4          6   2          6
  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1

         5   8         5   6         5   4         5   2         5        4   10
  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                 7        6        5   3
  - 113*u2  - 194*u2  - 159*u2  - 72 > 0 and (u1 *u2 + u1 *u2 + u1 *u2

        5          4   3       4        3   5       3        2   5       2   3
  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2 + u1 *u2  - 4*u1 *u2

        2           7        5        3               7       5     3
  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2  + 5*u2  + u2  - u2 > 0 

      12   2        12       11   2       10   4        10   2         10
 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2  - 70*u1  *u2  + 160*u1

         9   4        9   2         9        8   6         8   4         8   2
  - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2

          8        7   6        7   4        7   2         7        6   8
  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2  + 512*u1  + 20*u1 *u2

          6   6         6   4        6   2         6        5   8        5   6
  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1  - 40*u1 *u2  + 72*u1 *u2

          5   4         5   2         5        4   10         4   8
  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2   - 148*u1 *u2

          4   6        4   4         4   2         4        3   10        3   8
  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2   + 16*u1 *u2

         3   6         3   4         3   2         3       2   12        2   10
  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2   - 78*u1 *u2

         2   8        2   6        2   4         2   2        2          12
  - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1  - 4*u1*u2

           10            8            6            4            2
  - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2  - 128*u1

      14        12        10        8         6         4         2
  + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2  + 48 > 0) 

        8   2       8       7   2       6   4        6   2        6        5   4
 and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1  - 12*u1 *u2

         5   2       4   6        4   4        4   2        4        3   6
  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1  - 12*u1 *u2

         3   4        3   2       2   8        2   6        2   4        2   2
  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2  + 28*u1 *u2

         2          8          6           4           2     10        8
  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2   - 12*u2

         6        4        2              12   2        12       11   2
  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0)) or (

     4          2   3       2             3     5     3
 2*u1 *u2 + 3*u1 *u2  - 4*u1 *u2 + 2*u1*u2  + u2  - u2  + 2*u2 <= 0 and 

   5     4       3   2       3       2        4          2          4
 u1  - u1  + 2*u1 *u2  - 2*u1  + 2*u1  + u1*u2  - 2*u1*u2  + u1 + u2  - 1 < 0) 

                     11          10          9   3        9          8   3
 or (((u1 <> 0 and u1  *u2 - 3*u1  *u2 + 5*u1 *u2  - 25*u1 *u2 - 9*u1 *u2

        8           7   5        7   3        7          6   5        6   3
  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2 - 6*u1 *u2  - 52*u1 *u2

         6           5   7         5   5         5   3         5          4   7
  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2  - 130*u1 *u2 + 6*u1 *u2

          4   5         4   3        4          3   9        3   7         3   5
  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2  - 76*u1 *u2  + 110*u1 *u2

          3   3        3          2   9        2   7        2   5         2   3
  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2  + 30*u1 *u2  - 100*u1 *u2

         2           11           9           7           5           3
  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2  + 70*u1*u2  + 13*u1*u2

                   11        9       7        5        3                  12   2
  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2  - 9*u2 > 0 and u1  *u2

        12       11   2        11       10   4        10   2         10
  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2  - 38*u1  *u2  + 176*u1

         9   4         9   2         9        8   6        8   4         8   2
  - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2  - 90*u1 *u2  + 559*u1 *u2

          8        7   6         7   4         7   2         7        6   8
  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2  + 576*u1  + 20*u1 *u2

          6   6         6   4          6   2          6        5   8
  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1  - 80*u1 *u2

          5   6         5   4         5   2         5        4   10
  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                  7        6        5   3
  - 113*u2  - 194*u2  - 159*u2  - 72 < 0) or ((u1 *u2 + u1 *u2 + u1 *u2

        5          4   3       4        3   5       3        2   5       2   3
  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2 + u1 *u2  - 4*u1 *u2

        2           7        5        3               7       5     3
  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2  + 5*u2  + u2  - u2 > 0 

      12   2        12       11   2       10   4        10   2         10
 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2  - 70*u1  *u2  + 160*u1

         9   4        9   2         9        8   6         8   4         8   2
  - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2

          8        7   6        7   4        7   2         7        6   8
  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2  + 512*u1  + 20*u1 *u2

          6   6         6   4        6   2         6        5   8        5   6
  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1  - 40*u1 *u2  + 72*u1 *u2

          5   4         5   2         5        4   10         4   8
  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2   - 148*u1 *u2

          4   6        4   4         4   2         4        3   10        3   8
  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2   + 16*u1 *u2

         3   6         3   4         3   2         3       2   12        2   10
  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2   - 78*u1 *u2

         2   8        2   6        2   4         2   2        2          12
  - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1  - 4*u1*u2

           10            8            6            4            2
  - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2  - 128*u1

      14        12        10        8         6         4         2
  + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2  + 48 > 0) 

        8   2       8       7   2       6   4        6   2        6        5   4
 and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1  - 12*u1 *u2

         5   2       4   6        4   4        4   2        4        3   6
  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1  - 12*u1 *u2

         3   4        3   2       2   8        2   6        2   4        2   2
  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2  + 28*u1 *u2

         2          8          6           4           2     10        8
  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2   - 12*u2

         6        4        2              12   2        12       11   2
  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2                     5        4          3
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0))) and ((u1 *u2 + u1 *u2 - 2*u1 *u2

        2   3       2           5               5       3
  + 2*u1 *u2  - 2*u1 *u2 - u1*u2  + u1*u2 - 3*u2  - 2*u2  + u2 <= 0 and (

   2     2              4   2        4       3   2       2   4        2   2
 u1  - u2  - 1 = 0 or u1 *u2  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2

         2          4           2              6        4        2
  + 96*u1  - 4*u1*u2  + 12*u1*u2  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 <= 0)) 

       6   2       6       5   2     4   4        4   2        4        3   2
 or (u1 *u2  - 8*u1  - 4*u1 *u2  + u1 *u2  - 11*u1 *u2  + 24*u1  + 16*u1 *u2

      2   6       2   4       2   2        2          6          4           2
  - u1 *u2  + 2*u1 *u2  - 5*u1 *u2  - 24*u1  + 4*u1*u2  - 8*u1*u2  - 12*u1*u2

      8        6        4        2                 2     2              4   2
  - u2  + 13*u2  + 21*u2  + 15*u2  + 8 >= 0 and (u1  - u2  - 1 = 0 or u1 *u2

         4       3   2       2   4        2   2        2          4           2
  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2  + 96*u1  - 4*u1*u2  + 12*u1*u2

               6        4        2
  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 >= 0))))) and (u2 <= 0

       2            2               2        3                             7
  or u1  + 2*u1 + u2  - 3 >= 0 or u1 *u2 + u2  - u2 < 0 or (u1 <> 0 and (u1 *u2

      6        5   3       5          4   3       4        3   5       3
  + u1 *u2 + u1 *u2  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2

      2   5       2   3       2           7        5        3               7
  + u1 *u2  - 4*u1 *u2  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2

        5     3               12   2        12       11   2       10   4
  + 5*u2  + u2  - u2 > 0 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2

         10   2         10        9   4        9   2         9        8   6
  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2

          8   4         8   2         8        7   6        7   4        7   2
  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2

          7        6   8         6   6         6   4        6   2         6
  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1

         5   8        5   6         5   4         5   2         5        4   10
  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2

          4   8         4   6        4   4         4   2         4        3   10
  - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2

         3   8        3   6         3   4         3   2         3       2   12
  + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2

         2   10        2   8        2   6        2   4         2   2        2
  - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1

           12          10            8            6            4            2
  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2

               14        12        10        8         6         4         2
  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2

                   8   2       8       7   2       6   4        6   2        6
  + 48 > 0) and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1

         5   4        5   2       4   6        4   4        4   2        4
  - 12*u1 *u2  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1

         3   6        3   4        3   2       2   8        2   6        2   4
  - 12*u1 *u2  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2

         2   2        2          8          6           4           2     10
  + 28*u1 *u2  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2

         8        6        4        2              12   2        12       11   2
  - 12*u2  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2                   2            2
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0) and ((u1  - 2*u1 + u2  + 1 <> 0 and 

   8   2        8       7   2        7       6   4        6   2         6
 u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2  - 44*u1 *u2  + 256*u1

         5   4         5   2        5       4   6        4   4         4   2
  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2  - 60*u1 *u2  + 606*u1 *u2

          4        3   6         3   4         3   2         3       2   8
  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2  - 320*u1  + 4*u1 *u2

         2   6         2   4         2   2         2          8           6
  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1  - 8*u1*u2  + 56*u1*u2

             4            2              10        8       6         4         2
  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2  - 2*u2  + 108*u2  + 137*u2

                 12   2       12       11   2        11       10   4
  + 48 > 0 and u1  *u2  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2

         10   2         10        9   4         9   2         9        8   6
  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2

         8   4         8   2         8        7   6         7   4         7   2
  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2

          7        6   8         6   6         6   4          6   2          6
  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1

         5   8         5   6         5   4         5   2         5        4   10
  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                 11          10          9   3
  - 113*u2  - 194*u2  - 159*u2  - 72 > 0) or (u1  *u2 - 3*u1  *u2 + 5*u1 *u2

         9          8   3       8           7   5        7   3        7
  - 25*u1 *u2 - 9*u1 *u2  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2

        6   5        6   3        6           5   7         5   5         5   3
  - 6*u1 *u2  - 52*u1 *u2  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2

          5          4   7         4   5         4   3        4          3   9
  - 130*u1 *u2 + 6*u1 *u2  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2

         3   7         3   5         3   3        3          2   9        2   7
  - 76*u1 *u2  + 110*u1 *u2  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2

         2   5         2   3        2           11           9           7
  + 30*u1 *u2  - 100*u1 *u2  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2

            5           3                  11        9       7        5        3
  + 70*u1*u2  + 13*u1*u2  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2

                     12   2       12       11   2        11       10   4
  - 9*u2 <= 0 and (u1  *u2  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2

         10   2         10        9   4         9   2         9        8   6
  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2

         8   4         8   2         8        7   6         7   4         7   2
  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2

          7        6   8         6   6         6   4          6   2          6
  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1

         5   8         5   6         5   4         5   2         5        4   10
  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                2            2
  - 113*u2  - 194*u2  - 159*u2  - 72 > 0 or (u1  - 2*u1 + u2  + 1 <> 0 and 

   8   2        8       7   2        7       6   4        6   2         6
 u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2  - 44*u1 *u2  + 256*u1

         5   4         5   2        5       4   6        4   4         4   2
  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2  - 60*u1 *u2  + 606*u1 *u2

          4        3   6         3   4         3   2         3       2   8
  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2  - 320*u1  + 4*u1 *u2

         2   6         2   4         2   2         2          8           6
  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1  - 8*u1*u2  + 56*u1*u2

             4            2              10        8       6         4         2
  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2  - 2*u2  + 108*u2  + 137*u2

  + 48 < 0))))) or (

     4          2   3       2             3     5     3
 2*u1 *u2 + 3*u1 *u2  - 4*u1 *u2 + 2*u1*u2  + u2  - u2  + 2*u2 > 0 and (

   2            2
 u1  - 2*u1 + u2  + 1 <> 0 or 

   5     4       3   2       3       2        4          2          4
 u1  - u1  + 2*u1 *u2  - 2*u1  + 2*u1  + u1*u2  - 2*u1*u2  + u1 + u2  - 1 > 0)) 

                      11          10          9   3        9          8   3
 or (((u1 <> 0 and (u1  *u2 - 3*u1  *u2 + 5*u1 *u2  - 25*u1 *u2 - 9*u1 *u2

        8           7   5        7   3        7          6   5        6   3
  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2 - 6*u1 *u2  - 52*u1 *u2

         6           5   7         5   5         5   3         5          4   7
  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2  - 130*u1 *u2 + 6*u1 *u2

          4   5         4   3        4          3   9        3   7         3   5
  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2  - 76*u1 *u2  + 110*u1 *u2

          3   3        3          2   9        2   7        2   5         2   3
  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2  + 30*u1 *u2  - 100*u1 *u2

         2           11           9           7           5           3
  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2  + 70*u1*u2  + 13*u1*u2

                   11        9       7        5        3
  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2  - 9*u2 > 0 or (

   2            2                8   2        8       7   2        7       6   4
 u1  - 2*u1 + u2  + 1 <> 0 and u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2

         6   2         6        5   4         5   2        5       4   6
  - 44*u1 *u2  + 256*u1  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2

         4   4         4   2         4        3   6         3   4         3   2
  - 60*u1 *u2  + 606*u1 *u2  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2

          3       2   8        2   6         2   4         2   2         2
  - 320*u1  + 4*u1 *u2  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1

           8           6            4            2              10        8
  - 8*u1*u2  + 56*u1*u2  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2

        6         4         2                   12   2       12       11   2
  - 2*u2  + 108*u2  + 137*u2  + 48 > 0)) and (u1  *u2  - 8*u1   - 8*u1  *u2

         11       10   4        10   2         10        9   4         9   2
  + 32*u1   + 6*u1  *u2  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2

          9        8   6        8   4         8   2         8        7   6
  - 224*u1  + 15*u1 *u2  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2

          7   4         7   2         7        6   8         6   6         6   4
  + 544*u1 *u2  - 464*u1 *u2  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2

           6   2          6        5   8         5   6         5   4
  - 1300*u1 *u2  + 1184*u1  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2

          5   2         5        4   10         4   8         4   6
  + 176*u1 *u2  - 704*u1  + 15*u1 *u2   - 140*u1 *u2  + 570*u1 *u2

          4   4         4   2          4        3   10         3   8
  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1  - 40*u1 *u2   + 384*u1 *u2

          3   6         3   4         3   2         3       2   12        2   10
  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2  + 416*u1  + 6*u1 *u2   - 78*u1 *u2

          2   8         2   6         2   4        2   2         2          12
  + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2  + 26*u1 *u2  + 432*u1  - 8*u1*u2

            10           8            6            4            2             14
  + 88*u1*u2   - 48*u1*u2  - 336*u1*u2  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2

         12        10        8         6         4         2
  - 18*u2   + 47*u2   + 60*u2  - 113*u2  - 194*u2  - 159*u2  - 72 < 0 or (

   2            2                8   2        8       7   2        7       6   4
 u1  - 2*u1 + u2  + 1 <> 0 and u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2

         6   2         6        5   4         5   2        5       4   6
  - 44*u1 *u2  + 256*u1  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2

         4   4         4   2         4        3   6         3   4         3   2
  - 60*u1 *u2  + 606*u1 *u2  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2

          3       2   8        2   6         2   4         2   2         2
  - 320*u1  + 4*u1 *u2  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1

           8           6            4            2              10        8
  - 8*u1*u2  + 56*u1*u2  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2

        6         4         2                    7        6        5   3
  - 2*u2  + 108*u2  + 137*u2  + 48 < 0))) or ((u1 *u2 + u1 *u2 + u1 *u2

        5          4   3       4        3   5       3        2   5       2   3
  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2 + u1 *u2  - 4*u1 *u2

        2           7        5        3               7       5     3
  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2  + 5*u2  + u2  - u2 > 0 

      12   2        12       11   2       10   4        10   2         10
 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2  - 70*u1  *u2  + 160*u1

         9   4        9   2         9        8   6         8   4         8   2
  - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2

          8        7   6        7   4        7   2         7        6   8
  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2  + 512*u1  + 20*u1 *u2

          6   6         6   4        6   2         6        5   8        5   6
  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1  - 40*u1 *u2  + 72*u1 *u2

          5   4         5   2         5        4   10         4   8
  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2   - 148*u1 *u2

          4   6        4   4         4   2         4        3   10        3   8
  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2   + 16*u1 *u2

         3   6         3   4         3   2         3       2   12        2   10
  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2   - 78*u1 *u2

         2   8        2   6        2   4         2   2        2          12
  - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1  - 4*u1*u2

           10            8            6            4            2
  - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2  - 128*u1

      14        12        10        8         6         4         2
  + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2  + 48 > 0) 

        8   2       8       7   2       6   4        6   2        6        5   4
 and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1  - 12*u1 *u2

         5   2       4   6        4   4        4   2        4        3   6
  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1  - 12*u1 *u2

         3   4        3   2       2   8        2   6        2   4        2   2
  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2  + 28*u1 *u2

         2          8          6           4           2     10        8
  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2   - 12*u2

         6        4        2              12   2        12       11   2
  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2                     5        4          3
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0))) and ((u1 *u2 + u1 *u2 - 2*u1 *u2

        2   3       2           5               5       3
  + 2*u1 *u2  - 2*u1 *u2 - u1*u2  + u1*u2 - 3*u2  - 2*u2  + u2 <= 0 and (

   2     2              4   2        4       3   2       2   4        2   2
 u1  - u2  - 1 = 0 or u1 *u2  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2

         2          4           2              6        4        2
  + 96*u1  - 4*u1*u2  + 12*u1*u2  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 <= 0)) 

       6   2       6       5   2     4   4        4   2        4        3   2
 or (u1 *u2  - 8*u1  - 4*u1 *u2  + u1 *u2  - 11*u1 *u2  + 24*u1  + 16*u1 *u2

      2   6       2   4       2   2        2          6          4           2
  - u1 *u2  + 2*u1 *u2  - 5*u1 *u2  - 24*u1  + 4*u1*u2  - 8*u1*u2  - 12*u1*u2

      8        6        4        2                 2     2              4   2
  - u2  + 13*u2  + 21*u2  + 15*u2  + 8 >= 0 and (u1  - u2  - 1 = 0 or u1 *u2

         4       3   2       2   4        2   2        2          4           2
  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2  + 96*u1  - 4*u1*u2  + 12*u1*u2

               6        4        2
  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 >= 0))))))) and (

   4       2   2       2     4       2
 u1  + 2*u1 *u2  - 2*u1  + u2  + 2*u2  + 1 < 0 or ((u2 <= 0

       2            2               2            2
  or u1  - 2*u1 + u2  + 1 <> 0 or u1  + 2*u1 + u2  - 3 >= 0

       2        3                            11          10          9   3
  or u1 *u2 + u2  - u2 < 0 or (u1 <> 0 and u1  *u2 - 3*u1  *u2 + 5*u1 *u2

         9          8   3       8           7   5        7   3        7
  - 25*u1 *u2 - 9*u1 *u2  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2

        6   5        6   3        6           5   7         5   5         5   3
  - 6*u1 *u2  - 52*u1 *u2  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2

          5          4   7         4   5         4   3        4          3   9
  - 130*u1 *u2 + 6*u1 *u2  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2

         3   7         3   5         3   3        3          2   9        2   7
  - 76*u1 *u2  + 110*u1 *u2  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2

         2   5         2   3        2           11           9           7
  + 30*u1 *u2  - 100*u1 *u2  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2

            5           3                  11        9       7        5        3
  + 70*u1*u2  + 13*u1*u2  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2

                    12   2       12       11   2        11       10   4
  - 9*u2 >= 0 and u1  *u2  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2

         10   2         10        9   4         9   2         9        8   6
  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2

         8   4         8   2         8        7   6         7   4         7   2
  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2

          7        6   8         6   6         6   4          6   2          6
  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1

         5   8         5   6         5   4         5   2         5        4   10
  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                 7        6        5   3
  - 113*u2  - 194*u2  - 159*u2  - 72 > 0 and (u1 *u2 + u1 *u2 + u1 *u2

        5          4   3       4        3   5       3        2   5       2   3
  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2 + u1 *u2  - 4*u1 *u2

        2           7        5        3               7       5     3
  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2  + 5*u2  + u2  - u2 < 0 

      12   2        12       11   2       10   4        10   2         10
 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2  - 70*u1  *u2  + 160*u1

         9   4        9   2         9        8   6         8   4         8   2
  - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2

          8        7   6        7   4        7   2         7        6   8
  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2  + 512*u1  + 20*u1 *u2

          6   6         6   4        6   2         6        5   8        5   6
  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1  - 40*u1 *u2  + 72*u1 *u2

          5   4         5   2         5        4   10         4   8
  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2   - 148*u1 *u2

          4   6        4   4         4   2         4        3   10        3   8
  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2   + 16*u1 *u2

         3   6         3   4         3   2         3       2   12        2   10
  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2   - 78*u1 *u2

         2   8        2   6        2   4         2   2        2          12
  - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1  - 4*u1*u2

           10            8            6            4            2
  - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2  - 128*u1

      14        12        10        8         6         4         2
  + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2  + 48 > 0) 

        8   2       8       7   2       6   4        6   2        6        5   4
 and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1  - 12*u1 *u2

         5   2       4   6        4   4        4   2        4        3   6
  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1  - 12*u1 *u2

         3   4        3   2       2   8        2   6        2   4        2   2
  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2  + 28*u1 *u2

         2          8          6           4           2     10        8
  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2   - 12*u2

         6        4        2              12   2        12       11   2
  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0)) or (

     4          2   3       2             3     5     3
 2*u1 *u2 + 3*u1 *u2  - 4*u1 *u2 + 2*u1*u2  + u2  - u2  + 2*u2 >= 0 and 

   5     4       3   2       3       2        4          2          4
 u1  - u1  + 2*u1 *u2  - 2*u1  + 2*u1  + u1*u2  - 2*u1*u2  + u1 + u2  - 1 < 0) 

                     11          10          9   3        9          8   3
 or (((u1 <> 0 and u1  *u2 - 3*u1  *u2 + 5*u1 *u2  - 25*u1 *u2 - 9*u1 *u2

        8           7   5        7   3        7          6   5        6   3
  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2 - 6*u1 *u2  - 52*u1 *u2

         6           5   7         5   5         5   3         5          4   7
  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2  - 130*u1 *u2 + 6*u1 *u2

          4   5         4   3        4          3   9        3   7         3   5
  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2  - 76*u1 *u2  + 110*u1 *u2

          3   3        3          2   9        2   7        2   5         2   3
  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2  + 30*u1 *u2  - 100*u1 *u2

         2           11           9           7           5           3
  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2  + 70*u1*u2  + 13*u1*u2

                   11        9       7        5        3                  12   2
  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2  - 9*u2 < 0 and u1  *u2

        12       11   2        11       10   4        10   2         10
  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2  - 38*u1  *u2  + 176*u1

         9   4         9   2         9        8   6        8   4         8   2
  - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2  - 90*u1 *u2  + 559*u1 *u2

          8        7   6         7   4         7   2         7        6   8
  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2  + 576*u1  + 20*u1 *u2

          6   6         6   4          6   2          6        5   8
  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1  - 80*u1 *u2

          5   6         5   4         5   2         5        4   10
  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                  7        6        5   3
  - 113*u2  - 194*u2  - 159*u2  - 72 < 0) or ((u1 *u2 + u1 *u2 + u1 *u2

        5          4   3       4        3   5       3        2   5       2   3
  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2 + u1 *u2  - 4*u1 *u2

        2           7        5        3               7       5     3
  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2  + 5*u2  + u2  - u2 < 0 

      12   2        12       11   2       10   4        10   2         10
 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2  - 70*u1  *u2  + 160*u1

         9   4        9   2         9        8   6         8   4         8   2
  - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2

          8        7   6        7   4        7   2         7        6   8
  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2  + 512*u1  + 20*u1 *u2

          6   6         6   4        6   2         6        5   8        5   6
  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1  - 40*u1 *u2  + 72*u1 *u2

          5   4         5   2         5        4   10         4   8
  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2   - 148*u1 *u2

          4   6        4   4         4   2         4        3   10        3   8
  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2   + 16*u1 *u2

         3   6         3   4         3   2         3       2   12        2   10
  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2   - 78*u1 *u2

         2   8        2   6        2   4         2   2        2          12
  - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1  - 4*u1*u2

           10            8            6            4            2
  - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2  - 128*u1

      14        12        10        8         6         4         2
  + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2  + 48 > 0) 

        8   2       8       7   2       6   4        6   2        6        5   4
 and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1  - 12*u1 *u2

         5   2       4   6        4   4        4   2        4        3   6
  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1  - 12*u1 *u2

         3   4        3   2       2   8        2   6        2   4        2   2
  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2  + 28*u1 *u2

         2          8          6           4           2     10        8
  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2   - 12*u2

         6        4        2              12   2        12       11   2
  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2                     5        4          3
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0))) and ((u1 *u2 + u1 *u2 - 2*u1 *u2

        2   3       2           5               5       3
  + 2*u1 *u2  - 2*u1 *u2 - u1*u2  + u1*u2 - 3*u2  - 2*u2  + u2 >= 0 and (

   2     2              4   2        4       3   2       2   4        2   2
 u1  - u2  - 1 = 0 or u1 *u2  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2

         2          4           2              6        4        2
  + 96*u1  - 4*u1*u2  + 12*u1*u2  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 <= 0)) 

       6   2       6       5   2     4   4        4   2        4        3   2
 or (u1 *u2  - 8*u1  - 4*u1 *u2  + u1 *u2  - 11*u1 *u2  + 24*u1  + 16*u1 *u2

      2   6       2   4       2   2        2          6          4           2
  - u1 *u2  + 2*u1 *u2  - 5*u1 *u2  - 24*u1  + 4*u1*u2  - 8*u1*u2  - 12*u1*u2

      8        6        4        2                 2     2              4   2
  - u2  + 13*u2  + 21*u2  + 15*u2  + 8 >= 0 and (u1  - u2  - 1 = 0 or u1 *u2

         4       3   2       2   4        2   2        2          4           2
  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2  + 96*u1  - 4*u1*u2  + 12*u1*u2

               6        4        2
  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 >= 0))))) and (u2 <= 0

       2            2               2        3                             7
  or u1  + 2*u1 + u2  - 3 >= 0 or u1 *u2 + u2  - u2 < 0 or (u1 <> 0 and (u1 *u2

      6        5   3       5          4   3       4        3   5       3
  + u1 *u2 + u1 *u2  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2

      2   5       2   3       2           7        5        3               7
  + u1 *u2  - 4*u1 *u2  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2

        5     3               12   2        12       11   2       10   4
  + 5*u2  + u2  - u2 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2

         10   2         10        9   4        9   2         9        8   6
  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2

          8   4         8   2         8        7   6        7   4        7   2
  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2

          7        6   8         6   6         6   4        6   2         6
  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1

         5   8        5   6         5   4         5   2         5        4   10
  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2

          4   8         4   6        4   4         4   2         4        3   10
  - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2

         3   8        3   6         3   4         3   2         3       2   12
  + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2

         2   10        2   8        2   6        2   4         2   2        2
  - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1

           12          10            8            6            4            2
  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2

               14        12        10        8         6         4         2
  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2

                   8   2       8       7   2       6   4        6   2        6
  + 48 > 0) and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1

         5   4        5   2       4   6        4   4        4   2        4
  - 12*u1 *u2  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1

         3   6        3   4        3   2       2   8        2   6        2   4
  - 12*u1 *u2  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2

         2   2        2          8          6           4           2     10
  + 28*u1 *u2  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2

         8        6        4        2              12   2        12       11   2
  - 12*u2  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2                   2            2
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0) and ((u1  - 2*u1 + u2  + 1 <> 0 and 

   8   2        8       7   2        7       6   4        6   2         6
 u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2  - 44*u1 *u2  + 256*u1

         5   4         5   2        5       4   6        4   4         4   2
  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2  - 60*u1 *u2  + 606*u1 *u2

          4        3   6         3   4         3   2         3       2   8
  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2  - 320*u1  + 4*u1 *u2

         2   6         2   4         2   2         2          8           6
  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1  - 8*u1*u2  + 56*u1*u2

             4            2              10        8       6         4         2
  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2  - 2*u2  + 108*u2  + 137*u2

                 12   2       12       11   2        11       10   4
  + 48 > 0 and u1  *u2  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2

         10   2         10        9   4         9   2         9        8   6
  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2

         8   4         8   2         8        7   6         7   4         7   2
  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2

          7        6   8         6   6         6   4          6   2          6
  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1

         5   8         5   6         5   4         5   2         5        4   10
  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                 11          10          9   3
  - 113*u2  - 194*u2  - 159*u2  - 72 > 0) or (u1  *u2 - 3*u1  *u2 + 5*u1 *u2

         9          8   3       8           7   5        7   3        7
  - 25*u1 *u2 - 9*u1 *u2  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2

        6   5        6   3        6           5   7         5   5         5   3
  - 6*u1 *u2  - 52*u1 *u2  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2

          5          4   7         4   5         4   3        4          3   9
  - 130*u1 *u2 + 6*u1 *u2  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2

         3   7         3   5         3   3        3          2   9        2   7
  - 76*u1 *u2  + 110*u1 *u2  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2

         2   5         2   3        2           11           9           7
  + 30*u1 *u2  - 100*u1 *u2  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2

            5           3                  11        9       7        5        3
  + 70*u1*u2  + 13*u1*u2  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2

                     12   2       12       11   2        11       10   4
  - 9*u2 >= 0 and (u1  *u2  - 8*u1   - 8*u1  *u2  + 32*u1   + 6*u1  *u2

         10   2         10        9   4         9   2         9        8   6
  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2  - 224*u1  + 15*u1 *u2

         8   4         8   2         8        7   6         7   4         7   2
  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2  + 544*u1 *u2  - 464*u1 *u2

          7        6   8         6   6         6   4          6   2          6
  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2  - 1300*u1 *u2  + 1184*u1

         5   8         5   6         5   4         5   2         5        4   10
  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2  + 176*u1 *u2  - 704*u1  + 15*u1 *u2

          4   8         4   6         4   4         4   2          4
  - 140*u1 *u2  + 570*u1 *u2  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1

         3   10         3   8         3   6         3   4         3   2
  - 40*u1 *u2   + 384*u1 *u2  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2

          3       2   12        2   10         2   8         2   6         2   4
  + 416*u1  + 6*u1 *u2   - 78*u1 *u2   + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2

         2   2         2          12           10           8            6
  + 26*u1 *u2  + 432*u1  - 8*u1*u2   + 88*u1*u2   - 48*u1*u2  - 336*u1*u2

             4            2             14        12        10        8
  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2   - 18*u2   + 47*u2   + 60*u2

          6         4         2                2            2
  - 113*u2  - 194*u2  - 159*u2  - 72 > 0 or (u1  - 2*u1 + u2  + 1 <> 0 and 

   8   2        8       7   2        7       6   4        6   2         6
 u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2  - 44*u1 *u2  + 256*u1

         5   4         5   2        5       4   6        4   4         4   2
  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2  - 60*u1 *u2  + 606*u1 *u2

          4        3   6         3   4         3   2         3       2   8
  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2  - 320*u1  + 4*u1 *u2

         2   6         2   4         2   2         2          8           6
  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1  - 8*u1*u2  + 56*u1*u2

             4            2              10        8       6         4         2
  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2  - 2*u2  + 108*u2  + 137*u2

  + 48 < 0))))) or (

     4          2   3       2             3     5     3
 2*u1 *u2 + 3*u1 *u2  - 4*u1 *u2 + 2*u1*u2  + u2  - u2  + 2*u2 < 0 and (

   2            2
 u1  - 2*u1 + u2  + 1 <> 0 or 

   5     4       3   2       3       2        4          2          4
 u1  - u1  + 2*u1 *u2  - 2*u1  + 2*u1  + u1*u2  - 2*u1*u2  + u1 + u2  - 1 > 0)) 

                      11          10          9   3        9          8   3
 or (((u1 <> 0 and (u1  *u2 - 3*u1  *u2 + 5*u1 *u2  - 25*u1 *u2 - 9*u1 *u2

        8           7   5        7   3        7          6   5        6   3
  + 3*u1 *u2 + 10*u1 *u2  - 92*u1 *u2  + 90*u1 *u2 - 6*u1 *u2  - 52*u1 *u2

         6           5   7         5   5         5   3         5          4   7
  + 18*u1 *u2 + 10*u1 *u2  - 126*u1 *u2  + 182*u1 *u2  - 130*u1 *u2 + 6*u1 *u2

          4   5         4   3        4          3   9        3   7         3   5
  - 126*u1 *u2  + 146*u1 *u2  - 42*u1 *u2 + 5*u1 *u2  - 76*u1 *u2  + 110*u1 *u2

          3   3        3          2   9        2   7        2   5         2   3
  - 108*u1 *u2  + 85*u1 *u2 + 9*u1 *u2  - 84*u1 *u2  + 30*u1 *u2  - 100*u1 *u2

         2           11           9           7           5           3
  + 33*u1 *u2 + u1*u2   - 17*u1*u2  + 18*u1*u2  + 70*u1*u2  + 13*u1*u2

                   11        9       7        5        3
  - 21*u1*u2 + 3*u2   - 13*u2  - 2*u2  + 38*u2  + 15*u2  - 9*u2 < 0 or (

   2            2                8   2        8       7   2        7       6   4
 u1  - 2*u1 + u2  + 1 <> 0 and u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2

         6   2         6        5   4         5   2        5       4   6
  - 44*u1 *u2  + 256*u1  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2

         4   4         4   2         4        3   6         3   4         3   2
  - 60*u1 *u2  + 606*u1 *u2  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2

          3       2   8        2   6         2   4         2   2         2
  - 320*u1  + 4*u1 *u2  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1

           8           6            4            2              10        8
  - 8*u1*u2  + 56*u1*u2  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2

        6         4         2                   12   2       12       11   2
  - 2*u2  + 108*u2  + 137*u2  + 48 > 0)) and (u1  *u2  - 8*u1   - 8*u1  *u2

         11       10   4        10   2         10        9   4         9   2
  + 32*u1   + 6*u1  *u2  - 38*u1  *u2  + 176*u1   - 40*u1 *u2  + 216*u1 *u2

          9        8   6        8   4         8   2         8        7   6
  - 224*u1  + 15*u1 *u2  - 90*u1 *u2  + 559*u1 *u2  - 696*u1  - 80*u1 *u2

          7   4         7   2         7        6   8         6   6         6   4
  + 544*u1 *u2  - 464*u1 *u2  + 576*u1  + 20*u1 *u2  - 140*u1 *u2  + 748*u1 *u2

           6   2          6        5   8         5   6         5   4
  - 1300*u1 *u2  + 1184*u1  - 80*u1 *u2  + 656*u1 *u2  - 432*u1 *u2

          5   2         5        4   10         4   8         4   6
  + 176*u1 *u2  - 704*u1  + 15*u1 *u2   - 140*u1 *u2  + 570*u1 *u2

          4   4         4   2          4        3   10         3   8
  - 164*u1 *u2  + 911*u1 *u2  - 1016*u1  - 40*u1 *u2   + 384*u1 *u2

          3   6         3   4         3   2         3       2   12        2   10
  - 240*u1 *u2  - 864*u1 *u2  + 216*u1 *u2  + 416*u1  + 6*u1 *u2   - 78*u1 *u2

          2   8         2   6         2   4        2   2         2          12
  + 252*u1 *u2  + 436*u1 *u2  + 718*u1 *u2  + 26*u1 *u2  + 432*u1  - 8*u1*u2

            10           8            6            4            2             14
  + 88*u1*u2   - 48*u1*u2  - 336*u1*u2  - 232*u1*u2  - 136*u1*u2  - 96*u1 + u2

         12        10        8         6         4         2
  - 18*u2   + 47*u2   + 60*u2  - 113*u2  - 194*u2  - 159*u2  - 72 < 0 or (

   2            2                8   2        8       7   2        7       6   4
 u1  - 2*u1 + u2  + 1 <> 0 and u1 *u2  - 16*u1  - 8*u1 *u2  + 64*u1  + 4*u1 *u2

         6   2         6        5   4         5   2        5       4   6
  - 44*u1 *u2  + 256*u1  - 24*u1 *u2  + 152*u1 *u2  + 64*u1  + 6*u1 *u2

         4   4         4   2         4        3   6         3   4         3   2
  - 60*u1 *u2  + 606*u1 *u2  - 416*u1  - 24*u1 *u2  + 144*u1 *u2  + 360*u1 *u2

          3       2   8        2   6         2   4         2   2         2
  - 320*u1  + 4*u1 *u2  - 52*u1 *u2  + 332*u1 *u2  + 580*u1 *u2  + 128*u1

           8           6            4            2              10        8
  - 8*u1*u2  + 56*u1*u2  + 392*u1*u2  + 520*u1*u2  + 192*u1 + u2   - 20*u2

        6         4         2                    7        6        5   3
  - 2*u2  + 108*u2  + 137*u2  + 48 < 0))) or ((u1 *u2 + u1 *u2 + u1 *u2

        5          4   3       4        3   5       3        2   5       2   3
  - 3*u1 *u2 + 3*u1 *u2  - 3*u1 *u2 + u1 *u2  + 3*u1 *u2 + u1 *u2  - 4*u1 *u2

        2           7        5        3               7       5     3
  + 3*u1 *u2 + u1*u2  + u1*u2  - u1*u2  - u1*u2 + 3*u2  + 5*u2  + u2  - u2 < 0 

      12   2        12       11   2       10   4        10   2         10
 or u1  *u2  - 16*u1   - 4*u1  *u2  + 6*u1  *u2  - 70*u1  *u2  + 160*u1

         9   4        9   2         9        8   6         8   4         8   2
  - 20*u1 *u2  + 28*u1 *u2  - 128*u1  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2

          8        7   6        7   4        7   2         7        6   8
  - 432*u1  - 40*u1 *u2  + 80*u1 *u2  - 72*u1 *u2  + 512*u1  + 20*u1 *u2

          6   6         6   4        6   2         6        5   8        5   6
  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2  + 448*u1  - 40*u1 *u2  + 72*u1 *u2

          5   4         5   2         5        4   10         4   8
  - 312*u1 *u2  - 424*u1 *u2  - 768*u1  + 15*u1 *u2   - 148*u1 *u2

          4   6        4   4         4   2         4        3   10        3   8
  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1  - 20*u1 *u2   + 16*u1 *u2

         3   6         3   4         3   2         3       2   12        2   10
  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1  + 6*u1 *u2   - 78*u1 *u2

         2   8        2   6        2   4         2   2        2          12
  - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2  - 230*u1 *u2  - 96*u1  - 4*u1*u2

           10            8            6            4            2
  - 4*u1*u2   - 104*u1*u2  - 456*u1*u2  - 724*u1*u2  - 500*u1*u2  - 128*u1

      14        12        10        8         6         4         2
  + u2   - 18*u2   - 41*u2   + 84*u2  + 351*u2  + 430*u2  + 233*u2  + 48 > 0) 

        8   2       8       7   2       6   4        6   2        6        5   4
 and (u1 *u2  - 8*u1  - 4*u1 *u2  + 4*u1 *u2  - 20*u1 *u2  + 32*u1  - 12*u1 *u2

         5   2       4   6        4   4        4   2        4        3   6
  + 20*u1 *u2  + 6*u1 *u2  - 28*u1 *u2  + 14*u1 *u2  - 48*u1  - 12*u1 *u2

         3   4        3   2       2   8        2   6        2   4        2   2
  + 24*u1 *u2  - 28*u1 *u2  + 4*u1 *u2  - 28*u1 *u2  + 28*u1 *u2  + 28*u1 *u2

         2          8          6           4           2     10        8
  + 32*u1  - 4*u1*u2  + 4*u1*u2  + 20*u1*u2  + 12*u1*u2  + u2   - 12*u2

         6        4        2              12   2        12       11   2
  - 34*u2  - 36*u2  - 23*u2  - 8 < 0 or u1  *u2  - 16*u1   - 4*u1  *u2

        10   4        10   2         10        9   4        9   2         9
  + 6*u1  *u2  - 70*u1  *u2  + 160*u1   - 20*u1 *u2  + 28*u1 *u2  - 128*u1

         8   6         8   4         8   2         8        7   6        7   4
  + 15*u1 *u2  - 138*u1 *u2  + 247*u1 *u2  - 432*u1  - 40*u1 *u2  + 80*u1 *u2

         7   2         7        6   8         6   6         6   4        6   2
  - 72*u1 *u2  + 512*u1  + 20*u1 *u2  - 172*u1 *u2  + 268*u1 *u2  - 52*u1 *u2

          6        5   8        5   6         5   4         5   2         5
  + 448*u1  - 40*u1 *u2  + 72*u1 *u2  - 312*u1 *u2  - 424*u1 *u2  - 768*u1

         4   10         4   8         4   6        4   4         4   2         4
  + 15*u1 *u2   - 148*u1 *u2  + 138*u1 *u2  + 28*u1 *u2  - 129*u1 *u2  - 112*u1

         3   10        3   8        3   6         3   4         3   2         3
  - 20*u1 *u2   + 16*u1 *u2  + 40*u1 *u2  + 464*u1 *u2  + 972*u1 *u2  + 512*u1

        2   12        2   10        2   8        2   6        2   4
  + 6*u1 *u2   - 78*u1 *u2   - 84*u1 *u2  + 52*u1 *u2  - 82*u1 *u2

          2   2        2          12          10            8            6
  - 230*u1 *u2  - 96*u1  - 4*u1*u2   - 4*u1*u2   - 104*u1*u2  - 456*u1*u2

             4            2              14        12        10        8
  - 724*u1*u2  - 500*u1*u2  - 128*u1 + u2   - 18*u2   - 41*u2   + 84*u2

          6         4         2                     5        4          3
  + 351*u2  + 430*u2  + 233*u2  + 48 < 0))) and ((u1 *u2 + u1 *u2 - 2*u1 *u2

        2   3       2           5               5       3
  + 2*u1 *u2  - 2*u1 *u2 - u1*u2  + u1*u2 - 3*u2  - 2*u2  + u2 >= 0 and (

   2     2              4   2        4       3   2       2   4        2   2
 u1  - u2  - 1 = 0 or u1 *u2  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2

         2          4           2              6        4        2
  + 96*u1  - 4*u1*u2  + 12*u1*u2  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 <= 0)) 

       6   2       6       5   2     4   4        4   2        4        3   2
 or (u1 *u2  - 8*u1  - 4*u1 *u2  + u1 *u2  - 11*u1 *u2  + 24*u1  + 16*u1 *u2

      2   6       2   4       2   2        2          6          4           2
  - u1 *u2  + 2*u1 *u2  - 5*u1 *u2  - 24*u1  + 4*u1*u2  - 8*u1*u2  - 12*u1*u2

      8        6        4        2                 2     2              4   2
  - u2  + 13*u2  + 21*u2  + 15*u2  + 8 >= 0 and (u1  - u2  - 1 = 0 or u1 *u2

         4       3   2       2   4        2   2        2          4           2
  - 16*u1  - 4*u1 *u2  + 2*u1 *u2  - 34*u1 *u2  + 96*u1  - 4*u1*u2  + 12*u1*u2

               6        4        2
  - 128*u1 + u2  - 22*u2  + 41*u2  + 48 >= 0))))))))}


end;

