MAYBE
Time: 0.003391
TRS:
 {                     sort nil() -> nil(),
                  sort cons(x, y) -> insert(x, sort y),
                 insert(x, nil()) -> cons(x, nil()),
            insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
    choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
  choose(x, cons(v, w), 0(), s z) -> cons(v, insert(x, w)),
  choose(x, cons(v, w), s y, s z) -> choose(x, cons(v, w), y, z)}
 DP:
  DP:
   {                sort# cons(x, y) -> sort# y,
                    sort# cons(x, y) -> insert#(x, sort y),
              insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
    choose#(x, cons(v, w), 0(), s z) -> insert#(x, w),
    choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z)}
  TRS:
  {                     sort nil() -> nil(),
                   sort cons(x, y) -> insert(x, sort y),
                  insert(x, nil()) -> cons(x, nil()),
             insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
     choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
   choose(x, cons(v, w), 0(), s z) -> cons(v, insert(x, w)),
   choose(x, cons(v, w), s y, s z) -> choose(x, cons(v, w), y, z)}
  EDG:
   {(sort# cons(x, y) -> insert#(x, sort y), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
    (choose#(x, cons(v, w), 0(), s z) -> insert#(x, w), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
    (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), 0(), s z) -> insert#(x, w))
    (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z))
    (choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), 0(), s z) -> insert#(x, w))
    (choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z))
    (sort# cons(x, y) -> sort# y, sort# cons(x, y) -> sort# y)
    (sort# cons(x, y) -> sort# y, sort# cons(x, y) -> insert#(x, sort y))}
   EDG:
    {(sort# cons(x, y) -> insert#(x, sort y), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
     (choose#(x, cons(v, w), 0(), s z) -> insert#(x, w), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
     (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), 0(), s z) -> insert#(x, w))
     (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z))
     (choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), 0(), s z) -> insert#(x, w))
     (choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z))
     (sort# cons(x, y) -> sort# y, sort# cons(x, y) -> sort# y)
     (sort# cons(x, y) -> sort# y, sort# cons(x, y) -> insert#(x, sort y))}
    EDG:
     {(sort# cons(x, y) -> insert#(x, sort y), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
      (choose#(x, cons(v, w), 0(), s z) -> insert#(x, w), insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v))
      (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), 0(), s z) -> insert#(x, w))
      (insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v), choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z))
      (choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), 0(), s z) -> insert#(x, w))
      (choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z), choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z))
      (sort# cons(x, y) -> sort# y, sort# cons(x, y) -> sort# y)
      (sort# cons(x, y) -> sort# y, sort# cons(x, y) -> insert#(x, sort y))}
     STATUS:
      arrows: 0.680000
      SCCS (2):
       Scc:
        {sort# cons(x, y) -> sort# y}
       Scc:
        {          insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
         choose#(x, cons(v, w), 0(), s z) -> insert#(x, w),
         choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z)}
       
       SCC (1):
        Strict:
         {sort# cons(x, y) -> sort# y}
        Weak:
        {                     sort nil() -> nil(),
                         sort cons(x, y) -> insert(x, sort y),
                        insert(x, nil()) -> cons(x, nil()),
                   insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
           choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
         choose(x, cons(v, w), 0(), s z) -> cons(v, insert(x, w)),
         choose(x, cons(v, w), s y, s z) -> choose(x, cons(v, w), y, z)}
        Open
       
       SCC (3):
        Strict:
         {          insert#(x, cons(v, w)) -> choose#(x, cons(v, w), x, v),
          choose#(x, cons(v, w), 0(), s z) -> insert#(x, w),
          choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z)}
        Weak:
        {                     sort nil() -> nil(),
                         sort cons(x, y) -> insert(x, sort y),
                        insert(x, nil()) -> cons(x, nil()),
                   insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
           choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
         choose(x, cons(v, w), 0(), s z) -> cons(v, insert(x, w)),
         choose(x, cons(v, w), s y, s z) -> choose(x, cons(v, w), y, z)}
        Open