YES
Time: 0.003140
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))}
   SCCS (2):
    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:
     {sort# cons(x, y) -> sort# y}
    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)}
     SPSC:
      Simple Projection:
       pi(choose#) = 1, pi(insert#) = 1
      Strict:
       {          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)}
      EDG:
       {(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), s y, s z) -> choose#(x, cons(v, w), y, z))}
       SCCS (1):
        Scc:
         {choose#(x, cons(v, w), s y, s z) -> choose#(x, cons(v, w), y, z)}
        SCC (1):
         Strict:
          {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)}
         SPSC:
          Simple Projection:
           pi(choose#) = 3
          Strict:
           {}
          Qed
    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)}
     SPSC:
      Simple Projection:
       pi(sort#) = 0
      Strict:
       {}
      Qed