Time: 3.609392
TRS:
 {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                  min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                  min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                         min(x, e()) -> pair(x, e()),
                    msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                           msort e() -> nil(),
         if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
  Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
       greater_int(pos 0(), pos 0()) -> false(),
       greater_int(pos 0(), pos s y) -> false(),
       greater_int(pos 0(), neg 0()) -> false(),
       greater_int(pos 0(), neg s y) -> true(),
       greater_int(pos s x, pos 0()) -> true(),
       greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
       greater_int(pos s x, neg 0()) -> true(),
       greater_int(pos s x, neg s y) -> true(),
       greater_int(neg 0(), pos 0()) -> false(),
       greater_int(neg 0(), pos s y) -> false(),
       greater_int(neg 0(), neg 0()) -> false(),
       greater_int(neg 0(), neg s y) -> true(),
       greater_int(neg s x, pos 0()) -> false(),
       greater_int(neg s x, pos s y) -> false(),
       greater_int(neg s x, neg 0()) -> false(),
       greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
            if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
  Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
       greatereq_int(pos x, pos 0()) -> true(),
         greatereq_int(pos x, neg y) -> true(),
     greatereq_int(pos 0(), pos s y) -> false(),
     greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
       greatereq_int(neg x, pos s y) -> false(),
     greatereq_int(neg 0(), pos 0()) -> true(),
       greatereq_int(neg 0(), neg y) -> true(),
     greatereq_int(neg s x, pos 0()) -> false(),
     greatereq_int(neg s x, neg 0()) -> false(),
     greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
 SRS: We consider a TRS.
  Trs:
   {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                    min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                    min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                           min(x, e()) -> pair(x, e()),
                      msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                             msort e() -> nil(),
           if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
    Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
         greater_int(pos 0(), pos 0()) -> false(),
         greater_int(pos 0(), pos s y) -> false(),
         greater_int(pos 0(), neg 0()) -> false(),
         greater_int(pos 0(), neg s y) -> true(),
         greater_int(pos s x, pos 0()) -> true(),
         greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
         greater_int(pos s x, neg 0()) -> true(),
         greater_int(pos s x, neg s y) -> true(),
         greater_int(neg 0(), pos 0()) -> false(),
         greater_int(neg 0(), pos s y) -> false(),
         greater_int(neg 0(), neg 0()) -> false(),
         greater_int(neg 0(), neg s y) -> true(),
         greater_int(neg s x, pos 0()) -> false(),
         greater_int(neg s x, pos s y) -> false(),
         greater_int(neg s x, neg 0()) -> false(),
         greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
              if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
    Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
         greatereq_int(pos x, pos 0()) -> true(),
           greatereq_int(pos x, neg y) -> true(),
       greatereq_int(pos 0(), pos s y) -> false(),
       greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
         greatereq_int(neg x, pos s y) -> false(),
       greatereq_int(neg 0(), pos 0()) -> true(),
         greatereq_int(neg 0(), neg y) -> true(),
       greatereq_int(neg s x, pos 0()) -> false(),
       greatereq_int(neg s x, neg 0()) -> false(),
       greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
  APP: We consider a non-applicative system.
   Trs:
    {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                     min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                     min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                            min(x, e()) -> pair(x, e()),
                       msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                              msort e() -> nil(),
            if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
     Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), neg 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
               if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
     Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
          greatereq_int(pos x, pos 0()) -> true(),
            greatereq_int(pos x, neg y) -> true(),
        greatereq_int(pos 0(), pos s y) -> false(),
        greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
          greatereq_int(neg x, pos s y) -> false(),
        greatereq_int(neg 0(), pos 0()) -> true(),
          greatereq_int(neg 0(), neg y) -> true(),
        greatereq_int(neg s x, pos 0()) -> false(),
        greatereq_int(neg s x, neg 0()) -> false(),
        greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
   DP:
    DP:
     {if_1#(pair(m, zh), x, y, zs) -> Cond_if_1#(greater_int(m, x), m, zh, x, y, zs),
      if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x),
              min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs),
              min#(x, ins(y, zs)) -> min#(y, zs),
              min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs),
                   msort# ins(x, ys) -> min#(x, ys),
                   msort# ins(x, ys) -> if_3#(min(x, ys), x, ys),
      if_2#(pair(m, zh), x, y, zs) -> Cond_if_2#(greatereq_int(x, m), m, zh, x, y, zs),
      if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m),
           greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y),
           greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y),
         if_3#(pair(m, zs), x, ys) -> msort# zs,
           greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y),
           greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y)}
    TRS:
    {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                     min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                     min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                            min(x, e()) -> pair(x, e()),
                       msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                              msort e() -> nil(),
            if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
     Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
          greater_int(pos 0(), pos 0()) -> false(),
          greater_int(pos 0(), pos s y) -> false(),
          greater_int(pos 0(), neg 0()) -> false(),
          greater_int(pos 0(), neg s y) -> true(),
          greater_int(pos s x, pos 0()) -> true(),
          greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
          greater_int(pos s x, neg 0()) -> true(),
          greater_int(pos s x, neg s y) -> true(),
          greater_int(neg 0(), pos 0()) -> false(),
          greater_int(neg 0(), pos s y) -> false(),
          greater_int(neg 0(), neg 0()) -> false(),
          greater_int(neg 0(), neg s y) -> true(),
          greater_int(neg s x, pos 0()) -> false(),
          greater_int(neg s x, pos s y) -> false(),
          greater_int(neg s x, neg 0()) -> false(),
          greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
               if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
     Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
          greatereq_int(pos x, pos 0()) -> true(),
            greatereq_int(pos x, neg y) -> true(),
        greatereq_int(pos 0(), pos s y) -> false(),
        greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
          greatereq_int(neg x, pos s y) -> false(),
        greatereq_int(neg 0(), pos 0()) -> true(),
          greatereq_int(neg 0(), neg y) -> true(),
        greatereq_int(neg s x, pos 0()) -> false(),
        greatereq_int(neg s x, neg 0()) -> false(),
        greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
    EDG:
     {(if_3#(pair(m, zs), x, ys) -> msort# zs, msort# ins(x, ys) -> if_3#(min(x, ys), x, ys))
      (if_3#(pair(m, zs), x, ys) -> msort# zs, msort# ins(x, ys) -> min#(x, ys))
      (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
      (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
      (greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
      (greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
      (min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs), if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x))
      (min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs), if_1#(pair(m, zh), x, y, zs) -> Cond_if_1#(greater_int(m, x), m, zh, x, y, zs))
      (min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs), if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m))
      (min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs), if_2#(pair(m, zh), x, y, zs) -> Cond_if_2#(greatereq_int(x, m), m, zh, x, y, zs))
      (if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
      (if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
      (if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
      (if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
      (min#(x, ins(y, zs)) -> min#(y, zs), min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs))
      (min#(x, ins(y, zs)) -> min#(y, zs), min#(x, ins(y, zs)) -> min#(y, zs))
      (min#(x, ins(y, zs)) -> min#(y, zs), min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs))
      (greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
      (greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
      (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
      (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
      (msort# ins(x, ys) -> if_3#(min(x, ys), x, ys), if_3#(pair(m, zs), x, ys) -> msort# zs)
      (msort# ins(x, ys) -> min#(x, ys), min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs))
      (msort# ins(x, ys) -> min#(x, ys), min#(x, ins(y, zs)) -> min#(y, zs))
      (msort# ins(x, ys) -> min#(x, ys), min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs))}
     EDG:
      {(if_3#(pair(m, zs), x, ys) -> msort# zs, msort# ins(x, ys) -> if_3#(min(x, ys), x, ys))
       (if_3#(pair(m, zs), x, ys) -> msort# zs, msort# ins(x, ys) -> min#(x, ys))
       (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
       (min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs), if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x))
       (min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs), if_1#(pair(m, zh), x, y, zs) -> Cond_if_1#(greater_int(m, x), m, zh, x, y, zs))
       (min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs), if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m))
       (min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs), if_2#(pair(m, zh), x, y, zs) -> Cond_if_2#(greatereq_int(x, m), m, zh, x, y, zs))
       (if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
       (if_2#(pair(m, zh), x, y, zs) -> greatereq_int#(x, m), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
       (if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (if_1#(pair(m, zh), x, y, zs) -> greater_int#(m, x), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (min#(x, ins(y, zs)) -> min#(y, zs), min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs))
       (min#(x, ins(y, zs)) -> min#(y, zs), min#(x, ins(y, zs)) -> min#(y, zs))
       (min#(x, ins(y, zs)) -> min#(y, zs), min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs))
       (greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
       (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (msort# ins(x, ys) -> if_3#(min(x, ys), x, ys), if_3#(pair(m, zs), x, ys) -> msort# zs)
       (msort# ins(x, ys) -> min#(x, ys), min#(x, ins(y, zs)) -> if_1#(min(y, zs), x, y, zs))
       (msort# ins(x, ys) -> min#(x, ys), min#(x, ins(y, zs)) -> min#(y, zs))
       (msort# ins(x, ys) -> min#(x, ys), min#(x, ins(y, zs)) -> if_2#(min(y, zs), x, y, zs))}
      SCCS (6):
       Scc:
        {greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y)}
       Scc:
        {greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y)}
       Scc:
        {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
       Scc:
        {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
       Scc:
        {          msort# ins(x, ys) -> if_3#(min(x, ys), x, ys),
         if_3#(pair(m, zs), x, ys) -> msort# zs}
       Scc:
        {min#(x, ins(y, zs)) -> min#(y, zs)}
       SCC:
        Strict:
         {greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y)}
        Weak:
        {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                                min(x, e()) -> pair(x, e()),
                           msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                                  msort e() -> nil(),
                if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
         Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
              greater_int(pos 0(), pos 0()) -> false(),
              greater_int(pos 0(), pos s y) -> false(),
              greater_int(pos 0(), neg 0()) -> false(),
              greater_int(pos 0(), neg s y) -> true(),
              greater_int(pos s x, pos 0()) -> true(),
              greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
              greater_int(pos s x, neg 0()) -> true(),
              greater_int(pos s x, neg s y) -> true(),
              greater_int(neg 0(), pos 0()) -> false(),
              greater_int(neg 0(), pos s y) -> false(),
              greater_int(neg 0(), neg 0()) -> false(),
              greater_int(neg 0(), neg s y) -> true(),
              greater_int(neg s x, pos 0()) -> false(),
              greater_int(neg s x, pos s y) -> false(),
              greater_int(neg s x, neg 0()) -> false(),
              greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
         Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
              greatereq_int(pos x, pos 0()) -> true(),
                greatereq_int(pos x, neg y) -> true(),
            greatereq_int(pos 0(), pos s y) -> false(),
            greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
              greatereq_int(neg x, pos s y) -> false(),
            greatereq_int(neg 0(), pos 0()) -> true(),
              greatereq_int(neg 0(), neg y) -> true(),
            greatereq_int(neg s x, pos 0()) -> false(),
            greatereq_int(neg s x, neg 0()) -> false(),
            greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(neg) = [0], pi(greatereq_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 1x0 + 0,
           
           [neg](x0) = 1x0 + 0,
           
           [greatereq_int#](x0) = 0x0 + 0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y)}
        Weak:
        {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                                min(x, e()) -> pair(x, e()),
                           msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                                  msort e() -> nil(),
                if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
         Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
              greater_int(pos 0(), pos 0()) -> false(),
              greater_int(pos 0(), pos s y) -> false(),
              greater_int(pos 0(), neg 0()) -> false(),
              greater_int(pos 0(), neg s y) -> true(),
              greater_int(pos s x, pos 0()) -> true(),
              greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
              greater_int(pos s x, neg 0()) -> true(),
              greater_int(pos s x, neg s y) -> true(),
              greater_int(neg 0(), pos 0()) -> false(),
              greater_int(neg 0(), pos s y) -> false(),
              greater_int(neg 0(), neg 0()) -> false(),
              greater_int(neg 0(), neg s y) -> true(),
              greater_int(neg s x, pos 0()) -> false(),
              greater_int(neg s x, pos s y) -> false(),
              greater_int(neg s x, neg 0()) -> false(),
              greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
         Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
              greatereq_int(pos x, pos 0()) -> true(),
                greatereq_int(pos x, neg y) -> true(),
            greatereq_int(pos 0(), pos s y) -> false(),
            greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
              greatereq_int(neg x, pos s y) -> false(),
            greatereq_int(neg 0(), pos 0()) -> true(),
              greatereq_int(neg 0(), neg y) -> true(),
            greatereq_int(neg s x, pos 0()) -> false(),
            greatereq_int(neg s x, neg 0()) -> false(),
            greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(pos) = [0], pi(greatereq_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 1x0 + 0,
           
           [pos](x0) = 1x0 + 0,
           
           [greatereq_int#](x0) = 0x0 + 0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
        Weak:
        {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                                min(x, e()) -> pair(x, e()),
                           msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                                  msort e() -> nil(),
                if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
         Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
              greater_int(pos 0(), pos 0()) -> false(),
              greater_int(pos 0(), pos s y) -> false(),
              greater_int(pos 0(), neg 0()) -> false(),
              greater_int(pos 0(), neg s y) -> true(),
              greater_int(pos s x, pos 0()) -> true(),
              greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
              greater_int(pos s x, neg 0()) -> true(),
              greater_int(pos s x, neg s y) -> true(),
              greater_int(neg 0(), pos 0()) -> false(),
              greater_int(neg 0(), pos s y) -> false(),
              greater_int(neg 0(), neg 0()) -> false(),
              greater_int(neg 0(), neg s y) -> true(),
              greater_int(neg s x, pos 0()) -> false(),
              greater_int(neg s x, pos s y) -> false(),
              greater_int(neg s x, neg 0()) -> false(),
              greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
         Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
              greatereq_int(pos x, pos 0()) -> true(),
                greatereq_int(pos x, neg y) -> true(),
            greatereq_int(pos 0(), pos s y) -> false(),
            greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
              greatereq_int(neg x, pos s y) -> false(),
            greatereq_int(neg 0(), pos 0()) -> true(),
              greatereq_int(neg 0(), neg y) -> true(),
            greatereq_int(neg s x, pos 0()) -> false(),
            greatereq_int(neg s x, neg 0()) -> false(),
            greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(neg) = [0], pi(greater_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 1x0 + 0,
           
           [neg](x0) = 1x0 + 0,
           
           [greater_int#](x0) = 0x0 + 0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
        Weak:
        {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                                min(x, e()) -> pair(x, e()),
                           msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                                  msort e() -> nil(),
                if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
         Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
              greater_int(pos 0(), pos 0()) -> false(),
              greater_int(pos 0(), pos s y) -> false(),
              greater_int(pos 0(), neg 0()) -> false(),
              greater_int(pos 0(), neg s y) -> true(),
              greater_int(pos s x, pos 0()) -> true(),
              greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
              greater_int(pos s x, neg 0()) -> true(),
              greater_int(pos s x, neg s y) -> true(),
              greater_int(neg 0(), pos 0()) -> false(),
              greater_int(neg 0(), pos s y) -> false(),
              greater_int(neg 0(), neg 0()) -> false(),
              greater_int(neg 0(), neg s y) -> true(),
              greater_int(neg s x, pos 0()) -> false(),
              greater_int(neg s x, pos s y) -> false(),
              greater_int(neg s x, neg 0()) -> false(),
              greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
         Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
              greatereq_int(pos x, pos 0()) -> true(),
                greatereq_int(pos x, neg y) -> true(),
            greatereq_int(pos 0(), pos s y) -> false(),
            greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
              greatereq_int(neg x, pos s y) -> false(),
            greatereq_int(neg 0(), pos 0()) -> true(),
              greatereq_int(neg 0(), neg y) -> true(),
            greatereq_int(neg s x, pos 0()) -> false(),
            greatereq_int(neg s x, neg 0()) -> false(),
            greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(pos) = [0], pi(greater_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 1x0 + 0,
           
           [pos](x0) = 1x0 + 0,
           
           [greater_int#](x0) = 0x0 + 0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {          msort# ins(x, ys) -> if_3#(min(x, ys), x, ys),
          if_3#(pair(m, zs), x, ys) -> msort# zs}
        Weak:
        {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                                min(x, e()) -> pair(x, e()),
                           msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                                  msort e() -> nil(),
                if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
         Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
              greater_int(pos 0(), pos 0()) -> false(),
              greater_int(pos 0(), pos s y) -> false(),
              greater_int(pos 0(), neg 0()) -> false(),
              greater_int(pos 0(), neg s y) -> true(),
              greater_int(pos s x, pos 0()) -> true(),
              greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
              greater_int(pos s x, neg 0()) -> true(),
              greater_int(pos s x, neg s y) -> true(),
              greater_int(neg 0(), pos 0()) -> false(),
              greater_int(neg 0(), pos s y) -> false(),
              greater_int(neg 0(), neg 0()) -> false(),
              greater_int(neg 0(), neg s y) -> true(),
              greater_int(neg s x, pos 0()) -> false(),
              greater_int(neg s x, pos s y) -> false(),
              greater_int(neg s x, neg 0()) -> false(),
              greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
         Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
              greatereq_int(pos x, pos 0()) -> true(),
                greatereq_int(pos x, neg y) -> true(),
            greatereq_int(pos 0(), pos s y) -> false(),
            greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
              greatereq_int(neg x, pos s y) -> false(),
            greatereq_int(neg 0(), pos 0()) -> true(),
              greatereq_int(neg 0(), neg y) -> true(),
            greatereq_int(neg s x, pos 0()) -> false(),
            greatereq_int(neg s x, neg 0()) -> false(),
            greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
        UR:
         {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                          min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                          min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                                 min(x, e()) -> pair(x, e()),
                 if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
          Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
               greater_int(pos 0(), pos 0()) -> false(),
               greater_int(pos 0(), pos s y) -> false(),
               greater_int(pos 0(), neg 0()) -> false(),
               greater_int(pos 0(), neg s y) -> true(),
               greater_int(pos s x, pos 0()) -> true(),
               greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
               greater_int(pos s x, neg 0()) -> true(),
               greater_int(pos s x, neg s y) -> true(),
               greater_int(neg 0(), pos 0()) -> false(),
               greater_int(neg 0(), pos s y) -> false(),
               greater_int(neg 0(), neg 0()) -> false(),
               greater_int(neg 0(), neg s y) -> true(),
               greater_int(neg s x, pos 0()) -> false(),
               greater_int(neg s x, pos s y) -> false(),
               greater_int(neg s x, neg 0()) -> false(),
               greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
               greatereq_int(pos x, pos 0()) -> true(),
                 greatereq_int(pos x, neg y) -> true(),
             greatereq_int(pos 0(), pos s y) -> false(),
             greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
               greatereq_int(neg x, pos s y) -> false(),
             greatereq_int(neg 0(), pos 0()) -> true(),
               greatereq_int(neg 0(), neg y) -> true(),
             greatereq_int(neg s x, pos 0()) -> false(),
             greatereq_int(neg s x, neg 0()) -> false(),
             greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                                     a(z, w) -> z,
                                     a(z, w) -> w}
         POLY:
          Mode: weak, max_in=15, output_bits=10, dnum=4, ur=true
          Interpretation:
           [Cond_if_1](x0, x1, x2, x3, x4, x5) = 9 / 4x0 + 3x1 + 2x2 + 2,
           
           [Cond_if_2](x0, x1, x2, x3, x4, x5) = 2x0 + x1 + 3x2 + 2x3,
           
           [if_1](x0, x1, x2, x3) = 3x0 + 2x1 + 13 / 4,
           
           [if_2](x0, x1, x2, x3) = 3x0 + 2x1 + 3,
           
           [min](x0, x1) = 2x0 + 3x1 + 1 / 4,
           
           [ins](x0, x1) = 2x0 + 3x1 + 2,
           
           [greater_int](x0, x1) = 0,
           
           [pair](x0, x1) = x0 + x1,
           
           [greatereq_int](x0, x1) = x0 + 3 / 2,
           
           [a](x0, x1) = 0,
           
           [pos](x0) = 0,
           
           [neg](x0) = 1 / 4x0 + 7 / 4,
           
           [s](x0) = 2x0 + 1,
           
           [e] = 5 / 4,
           
           [true] = 1,
           
           [false] = 0,
           
           [0] = 7 / 2,
           
           [if_3#](x0, x1, x2) = 2x0 + 7 / 2,
           
           [msort#](x0) = 2x0
          Strict:
           if_3#(pair(m, zs), x, ys) -> msort# zs
           7/2 + 2zs + 0x + 2m + 0ys >= 0 + 2zs
           msort# ins(x, ys) -> if_3#(min(x, ys), x, ys)
           4 + 4x + 6ys >= 4 + 4x + 6ys
          Weak:
           
         SCCS (0):
          
          Qed
      SCC:
       Strict:
        {min#(x, ins(y, zs)) -> min#(y, zs)}
       Weak:
       {       if_1(pair(m, zh), x, y, zs) -> Cond_if_1(greater_int(m, x), m, zh, x, y, zs),
                        min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs),
                        min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs),
                               min(x, e()) -> pair(x, e()),
                          msort ins(x, ys) -> if_3(min(x, ys), x, ys),
                                 msort e() -> nil(),
               if_2(pair(m, zh), x, y, zs) -> Cond_if_2(greatereq_int(x, m), m, zh, x, y, zs),
        Cond_if_1(true(), m, zh, x, y, zs) -> pair(x, ins(m, zh)),
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                  if_3(pair(m, zs), x, ys) -> cons(m, msort zs),
        Cond_if_2(true(), m, zh, x, y, zs) -> pair(m, ins(x, zh)),
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y)}
       SPSC:
        Simple Projection:
         pi(min#) = 1
        Strict:
         {}
        Qed