MAYBE
Time: 0.015454
TRS:
 {                     eq(0(), 0()) -> true(),
                       eq(0(), s x) -> false(),
                       eq(s x, 0()) -> false(),
                       eq(s x, s y) -> eq(x, y),
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                      app(nil(), y) -> y,
                  app(add(n, x), y) -> add(n, app(x, y)),
                          min nil() -> 0(),
                      min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
       minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
           minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
            if_min(true(), x, y, m) -> m,
           if_min(false(), x, y, m) -> minIter(x, y, m),
                     head add(n, x) -> n,
                         tail nil() -> nil(),
                     tail add(n, x) -> x,
                         null nil() -> true(),
                     null add(n, x) -> false(),
                       rm(n, nil()) -> nil(),
                   rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
        if_rm(true(), n, add(m, x)) -> rm(n, x),
       if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
              minsort(nil(), nil()) -> nil(),
              minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
   if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
  if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
 DP:
  DP:
   {                     eq#(s x, s y) -> eq#(x, y),
                         le#(s x, s y) -> le#(x, y),
                    app#(add(n, x), y) -> app#(x, y),
                        min# add(n, x) -> minIter#(add(n, x), add(n, x), 0()),
         minIter#(nil(), add(n, y), m) -> minIter#(add(n, y), add(n, y), s m),
             minIter#(add(n, x), y, m) -> le#(n, m),
             minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m),
             if_min#(false(), x, y, m) -> minIter#(x, y, m),
                     rm#(n, add(m, x)) -> eq#(n, m),
                     rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
          if_rm#(true(), n, add(m, x)) -> rm#(n, x),
         if_rm#(false(), n, add(m, x)) -> rm#(n, x),
                minsort#(add(n, x), y) -> eq#(n, min add(n, x)),
                minsort#(add(n, x), y) -> min# add(n, x),
                minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y),
     if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y),
     if_minsort#(true(), add(n, x), y) -> rm#(n, x),
     if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()),
    if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
  TRS:
  {                     eq(0(), 0()) -> true(),
                        eq(0(), s x) -> false(),
                        eq(s x, 0()) -> false(),
                        eq(s x, s y) -> eq(x, y),
                          le(0(), y) -> true(),
                        le(s x, 0()) -> false(),
                        le(s x, s y) -> le(x, y),
                       app(nil(), y) -> y,
                   app(add(n, x), y) -> add(n, app(x, y)),
                           min nil() -> 0(),
                       min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
        minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
            minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
             if_min(true(), x, y, m) -> m,
            if_min(false(), x, y, m) -> minIter(x, y, m),
                      head add(n, x) -> n,
                          tail nil() -> nil(),
                      tail add(n, x) -> x,
                          null nil() -> true(),
                      null add(n, x) -> false(),
                        rm(n, nil()) -> nil(),
                    rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
         if_rm(true(), n, add(m, x)) -> rm(n, x),
        if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
               minsort(nil(), nil()) -> nil(),
               minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
    if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
   if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
  EDG:
   {(rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x))
    (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))
    (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y), app#(add(n, x), y) -> app#(x, y))
    (minsort#(add(n, x), y) -> min# add(n, x), min# add(n, x) -> minIter#(add(n, x), add(n, x), 0()))
    (minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m), if_min#(false(), x, y, m) -> minIter#(x, y, m))
    (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y))
    (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> min# add(n, x))
    (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> eq#(n, min add(n, x)))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (minIter#(add(n, x), y, m) -> le#(n, m), le#(s x, s y) -> le#(x, y))
    (rm#(n, add(m, x)) -> eq#(n, m), eq#(s x, s y) -> eq#(x, y))
    (min# add(n, x) -> minIter#(add(n, x), add(n, x), 0()), minIter#(add(n, x), y, m) -> le#(n, m))
    (min# add(n, x) -> minIter#(add(n, x), add(n, x), 0()), minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m))
    (if_min#(false(), x, y, m) -> minIter#(x, y, m), minIter#(nil(), add(n, y), m) -> minIter#(add(n, y), add(n, y), s m))
    (if_min#(false(), x, y, m) -> minIter#(x, y, m), minIter#(add(n, x), y, m) -> le#(n, m))
    (if_min#(false(), x, y, m) -> minIter#(x, y, m), minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> rm#(n, x))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()))
    (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)))
    (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> eq#(n, min add(n, x)))
    (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> min# add(n, x))
    (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y))
    (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m))
    (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)))
    (minsort#(add(n, x), y) -> eq#(n, min add(n, x)), eq#(s x, s y) -> eq#(x, y))
    (minIter#(nil(), add(n, y), m) -> minIter#(add(n, y), add(n, y), s m), minIter#(add(n, x), y, m) -> le#(n, m))
    (minIter#(nil(), add(n, y), m) -> minIter#(add(n, y), add(n, y), s m), minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m))}
   STATUS:
    arrows: 0.905817
    SCCS (6):
     Scc:
      {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y),
        if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()),
       if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
     Scc:
      {app#(add(n, x), y) -> app#(x, y)}
     Scc:
      {            rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
        if_rm#(true(), n, add(m, x)) -> rm#(n, x),
       if_rm#(false(), n, add(m, x)) -> rm#(n, x)}
     Scc:
      {eq#(s x, s y) -> eq#(x, y)}
     Scc:
      {minIter#(nil(), add(n, y), m) -> minIter#(add(n, y), add(n, y), s m),
           minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m),
           if_min#(false(), x, y, m) -> minIter#(x, y, m)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     SCC (3):
      Strict:
       {            minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y),
         if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()),
        if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))}
      Weak:
      {                     eq(0(), 0()) -> true(),
                            eq(0(), s x) -> false(),
                            eq(s x, 0()) -> false(),
                            eq(s x, s y) -> eq(x, y),
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                               min nil() -> 0(),
                           min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
            minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
                minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
                 if_min(true(), x, y, m) -> m,
                if_min(false(), x, y, m) -> minIter(x, y, m),
                          head add(n, x) -> n,
                              tail nil() -> nil(),
                          tail add(n, x) -> x,
                              null nil() -> true(),
                          null add(n, x) -> false(),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      Open
     
     
     
     
     SCC (1):
      Strict:
       {app#(add(n, x), y) -> app#(x, y)}
      Weak:
      {                     eq(0(), 0()) -> true(),
                            eq(0(), s x) -> false(),
                            eq(s x, 0()) -> false(),
                            eq(s x, s y) -> eq(x, y),
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                               min nil() -> 0(),
                           min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
            minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
                minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
                 if_min(true(), x, y, m) -> m,
                if_min(false(), x, y, m) -> minIter(x, y, m),
                          head add(n, x) -> n,
                              tail nil() -> nil(),
                          tail add(n, x) -> x,
                              null nil() -> true(),
                          null add(n, x) -> false(),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      Open
     
     SCC (3):
      Strict:
       {            rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)),
         if_rm#(true(), n, add(m, x)) -> rm#(n, x),
        if_rm#(false(), n, add(m, x)) -> rm#(n, x)}
      Weak:
      {                     eq(0(), 0()) -> true(),
                            eq(0(), s x) -> false(),
                            eq(s x, 0()) -> false(),
                            eq(s x, s y) -> eq(x, y),
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                               min nil() -> 0(),
                           min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
            minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
                minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
                 if_min(true(), x, y, m) -> m,
                if_min(false(), x, y, m) -> minIter(x, y, m),
                          head add(n, x) -> n,
                              tail nil() -> nil(),
                          tail add(n, x) -> x,
                              null nil() -> true(),
                          null add(n, x) -> false(),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      Open
     
     SCC (1):
      Strict:
       {eq#(s x, s y) -> eq#(x, y)}
      Weak:
      {                     eq(0(), 0()) -> true(),
                            eq(0(), s x) -> false(),
                            eq(s x, 0()) -> false(),
                            eq(s x, s y) -> eq(x, y),
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                               min nil() -> 0(),
                           min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
            minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
                minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
                 if_min(true(), x, y, m) -> m,
                if_min(false(), x, y, m) -> minIter(x, y, m),
                          head add(n, x) -> n,
                              tail nil() -> nil(),
                          tail add(n, x) -> x,
                              null nil() -> true(),
                          null add(n, x) -> false(),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      Open
     SCC (3):
      Strict:
       {minIter#(nil(), add(n, y), m) -> minIter#(add(n, y), add(n, y), s m),
            minIter#(add(n, x), y, m) -> if_min#(le(n, m), x, y, m),
            if_min#(false(), x, y, m) -> minIter#(x, y, m)}
      Weak:
      {                     eq(0(), 0()) -> true(),
                            eq(0(), s x) -> false(),
                            eq(s x, 0()) -> false(),
                            eq(s x, s y) -> eq(x, y),
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                               min nil() -> 0(),
                           min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
            minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
                minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
                 if_min(true(), x, y, m) -> m,
                if_min(false(), x, y, m) -> minIter(x, y, m),
                          head add(n, x) -> n,
                              tail nil() -> nil(),
                          tail add(n, x) -> x,
                              null nil() -> true(),
                          null add(n, x) -> false(),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      Open
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {                     eq(0(), 0()) -> true(),
                            eq(0(), s x) -> false(),
                            eq(s x, 0()) -> false(),
                            eq(s x, s y) -> eq(x, y),
                              le(0(), y) -> true(),
                            le(s x, 0()) -> false(),
                            le(s x, s y) -> le(x, y),
                           app(nil(), y) -> y,
                       app(add(n, x), y) -> add(n, app(x, y)),
                               min nil() -> 0(),
                           min add(n, x) -> minIter(add(n, x), add(n, x), 0()),
            minIter(nil(), add(n, y), m) -> minIter(add(n, y), add(n, y), s m),
                minIter(add(n, x), y, m) -> if_min(le(n, m), x, y, m),
                 if_min(true(), x, y, m) -> m,
                if_min(false(), x, y, m) -> minIter(x, y, m),
                          head add(n, x) -> n,
                              tail nil() -> nil(),
                          tail add(n, x) -> x,
                              null nil() -> true(),
                          null add(n, x) -> false(),
                            rm(n, nil()) -> nil(),
                        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)),
             if_rm(true(), n, add(m, x)) -> rm(n, x),
            if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)),
                   minsort(nil(), nil()) -> nil(),
                   minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y),
        if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())),
       if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))}
      Open