MAYBE
Time: 0.012901
TRS:
 {                         eq(0(), 0()) -> true(),
                           eq(0(), s m) -> false(),
                           eq(s n, 0()) -> false(),
                           eq(s n, s m) -> eq(n, m),
                             le(0(), m) -> true(),
                           le(s n, 0()) -> false(),
                           le(s n, s m) -> le(n, m),
                min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                   min cons(0(), nil()) -> 0(),
                   min cons(s n, nil()) -> s n,
    if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
   if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
              replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                   replace(n, m, nil()) -> nil(),
   if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
  if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                        sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                             sort nil() -> nil()}
 DP:
  DP:
   {                         eq#(s n, s m) -> eq#(n, m),
                             le#(s n, s m) -> le#(n, m),
                  min# cons(n, cons(m, x)) -> le#(n, m),
                  min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))),
      if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x),
     if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x),
                replace#(n, m, cons(k, x)) -> eq#(n, k),
                replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
    if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x),
                          sort# cons(n, x) -> min# cons(n, x),
                          sort# cons(n, x) -> replace#(min cons(n, x), n, x),
                          sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)}
  TRS:
  {                         eq(0(), 0()) -> true(),
                            eq(0(), s m) -> false(),
                            eq(s n, 0()) -> false(),
                            eq(s n, s m) -> eq(n, m),
                              le(0(), m) -> true(),
                            le(s n, 0()) -> false(),
                            le(s n, s m) -> le(n, m),
                 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                    min cons(0(), nil()) -> 0(),
                    min cons(s n, nil()) -> s n,
     if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
    if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
               replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                    replace(n, m, nil()) -> nil(),
    if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
   if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                         sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                              sort nil() -> nil()}
  UR:
   {                         eq(0(), 0()) -> true(),
                             eq(0(), s m) -> false(),
                             eq(s n, 0()) -> false(),
                             eq(s n, s m) -> eq(n, m),
                               le(0(), m) -> true(),
                             le(s n, 0()) -> false(),
                             le(s n, s m) -> le(n, m),
                  min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                     min cons(0(), nil()) -> 0(),
                     min cons(s n, nil()) -> s n,
      if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
     if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                     replace(n, m, nil()) -> nil(),
     if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
    if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                                  a(y, z) -> y,
                                  a(y, z) -> z}
   EDG:
    {(if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
     (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
     (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
     (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
     (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
     (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m))
     (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m))
     (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x))
     (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x))
     (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m))
     (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m))
     (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> min# cons(n, x))
     (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x))
     (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x))
     (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
     (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m))
     (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))}
    EDG:
     {(if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
      (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
      (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
      (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
      (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
      (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
      (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m))
      (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m))
      (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x))
      (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x))
      (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m))
      (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m))
      (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> min# cons(n, x))
      (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x))
      (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x))
      (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
      (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
      (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m))
      (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
      (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))}
     EDG:
      {(if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
       (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
       (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
       (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
       (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
       (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
       (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m))
       (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m))
       (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x))
       (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x))
       (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m))
       (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m))
       (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> min# cons(n, x))
       (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x))
       (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x))
       (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
       (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
       (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m))
       (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
       (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))}
      EDG:
       {(if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
        (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
        (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
        (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
        (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
        (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
        (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m))
        (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m))
        (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x))
        (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x))
        (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m))
        (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m))
        (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> min# cons(n, x))
        (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x))
        (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x))
        (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
        (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
        (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m))
        (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
        (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))}
       STATUS:
        arrows: 0.861111
        SCCS (5):
         Scc:
          {sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)}
         Scc:
          {             min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))),
            if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x),
           if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)}
         Scc:
          {le#(s n, s m) -> le#(n, m)}
         Scc:
          {            replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
           if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)}
         Scc:
          {eq#(s n, s m) -> eq#(n, m)}
         
         SCC (1):
          Strict:
           {sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)}
          Weak:
          {                         eq(0(), 0()) -> true(),
                                    eq(0(), s m) -> false(),
                                    eq(s n, 0()) -> false(),
                                    eq(s n, s m) -> eq(n, m),
                                      le(0(), m) -> true(),
                                    le(s n, 0()) -> false(),
                                    le(s n, s m) -> le(n, m),
                         min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                            min cons(0(), nil()) -> 0(),
                            min cons(s n, nil()) -> s n,
             if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
            if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                       replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                            replace(n, m, nil()) -> nil(),
            if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
           if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                                 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                                      sort nil() -> nil()}
          Open
         
         
         SCC (3):
          Strict:
           {             min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))),
             if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x),
            if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)}
          Weak:
          {                         eq(0(), 0()) -> true(),
                                    eq(0(), s m) -> false(),
                                    eq(s n, 0()) -> false(),
                                    eq(s n, s m) -> eq(n, m),
                                      le(0(), m) -> true(),
                                    le(s n, 0()) -> false(),
                                    le(s n, s m) -> le(n, m),
                         min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                            min cons(0(), nil()) -> 0(),
                            min cons(s n, nil()) -> s n,
             if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
            if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                       replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                            replace(n, m, nil()) -> nil(),
            if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
           if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                                 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                                      sort nil() -> nil()}
          Open
         
         SCC (1):
          Strict:
           {le#(s n, s m) -> le#(n, m)}
          Weak:
          {                         eq(0(), 0()) -> true(),
                                    eq(0(), s m) -> false(),
                                    eq(s n, 0()) -> false(),
                                    eq(s n, s m) -> eq(n, m),
                                      le(0(), m) -> true(),
                                    le(s n, 0()) -> false(),
                                    le(s n, s m) -> le(n, m),
                         min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                            min cons(0(), nil()) -> 0(),
                            min cons(s n, nil()) -> s n,
             if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
            if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                       replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                            replace(n, m, nil()) -> nil(),
            if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
           if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                                 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                                      sort nil() -> nil()}
          Open
         SCC (2):
          Strict:
           {            replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
            if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)}
          Weak:
          {                         eq(0(), 0()) -> true(),
                                    eq(0(), s m) -> false(),
                                    eq(s n, 0()) -> false(),
                                    eq(s n, s m) -> eq(n, m),
                                      le(0(), m) -> true(),
                                    le(s n, 0()) -> false(),
                                    le(s n, s m) -> le(n, m),
                         min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                            min cons(0(), nil()) -> 0(),
                            min cons(s n, nil()) -> s n,
             if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
            if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                       replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                            replace(n, m, nil()) -> nil(),
            if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
           if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                                 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                                      sort nil() -> nil()}
          Open
         
         SCC (1):
          Strict:
           {eq#(s n, s m) -> eq#(n, m)}
          Weak:
          {                         eq(0(), 0()) -> true(),
                                    eq(0(), s m) -> false(),
                                    eq(s n, 0()) -> false(),
                                    eq(s n, s m) -> eq(n, m),
                                      le(0(), m) -> true(),
                                    le(s n, 0()) -> false(),
                                    le(s n, s m) -> le(n, m),
                         min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                            min cons(0(), nil()) -> 0(),
                            min cons(s n, nil()) -> s n,
             if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
            if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                       replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                            replace(n, m, nil()) -> nil(),
            if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
           if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                                 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)),
                                      sort nil() -> nil()}
          Open