MAYBE
Time: 0.006458
TRS:
 {               lt(0(), s X) -> true(),
                 lt(s X, 0()) -> false(),
                 lt(s X, s Y) -> lt(X, Y),
             append(nil(), Y) -> Y,
         append(add(N, X), Y) -> add(N, append(X, Y)),
              split(N, nil()) -> pair(nil(), nil()),
          split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
     f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
   f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
  f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                  qsort nil() -> nil(),
              qsort add(N, X) -> f_3(split(N, X), N, X),
        f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))}
 DP:
  DP:
   {            lt#(s X, s Y) -> lt#(X, Y),
        append#(add(N, X), Y) -> append#(X, Y),
         split#(N, add(M, Y)) -> split#(N, Y),
         split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y),
    f_1#(pair(X, Z), N, M, Y) -> lt#(N, M),
    f_1#(pair(X, Z), N, M, Y) -> f_2#(lt(N, M), N, M, Y, X, Z),
             qsort# add(N, X) -> split#(N, X),
             qsort# add(N, X) -> f_3#(split(N, X), N, X),
       f_3#(pair(Y, Z), N, X) -> append#(qsort Y, add(X, qsort Z)),
       f_3#(pair(Y, Z), N, X) -> qsort# Y,
       f_3#(pair(Y, Z), N, X) -> qsort# Z}
  TRS:
  {               lt(0(), s X) -> true(),
                  lt(s X, 0()) -> false(),
                  lt(s X, s Y) -> lt(X, Y),
              append(nil(), Y) -> Y,
          append(add(N, X), Y) -> add(N, append(X, Y)),
               split(N, nil()) -> pair(nil(), nil()),
           split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
      f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
    f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
   f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                   qsort nil() -> nil(),
               qsort add(N, X) -> f_3(split(N, X), N, X),
         f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))}
  UR:
   {               lt(0(), s X) -> true(),
                   lt(s X, 0()) -> false(),
                   lt(s X, s Y) -> lt(X, Y),
               append(nil(), Y) -> Y,
           append(add(N, X), Y) -> add(N, append(X, Y)),
                split(N, nil()) -> pair(nil(), nil()),
            split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
       f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
     f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
    f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                    qsort nil() -> nil(),
                qsort add(N, X) -> f_3(split(N, X), N, X),
          f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z)),
                        a(x, y) -> x,
                        a(x, y) -> y}
   EDG:
    {(lt#(s X, s Y) -> lt#(X, Y), lt#(s X, s Y) -> lt#(X, Y))
     (split#(N, add(M, Y)) -> split#(N, Y), split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y))
     (split#(N, add(M, Y)) -> split#(N, Y), split#(N, add(M, Y)) -> split#(N, Y))
     (f_1#(pair(X, Z), N, M, Y) -> lt#(N, M), lt#(s X, s Y) -> lt#(X, Y))
     (qsort# add(N, X) -> split#(N, X), split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y))
     (qsort# add(N, X) -> split#(N, X), split#(N, add(M, Y)) -> split#(N, Y))
     (split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y), f_1#(pair(X, Z), N, M, Y) -> lt#(N, M))
     (split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y), f_1#(pair(X, Z), N, M, Y) -> f_2#(lt(N, M), N, M, Y, X, Z))
     (f_3#(pair(Y, Z), N, X) -> append#(qsort Y, add(X, qsort Z)), append#(add(N, X), Y) -> append#(X, Y))
     (f_3#(pair(Y, Z), N, X) -> qsort# Z, qsort# add(N, X) -> split#(N, X))
     (f_3#(pair(Y, Z), N, X) -> qsort# Z, qsort# add(N, X) -> f_3#(split(N, X), N, X))
     (f_3#(pair(Y, Z), N, X) -> qsort# Y, qsort# add(N, X) -> split#(N, X))
     (f_3#(pair(Y, Z), N, X) -> qsort# Y, qsort# add(N, X) -> f_3#(split(N, X), N, X))
     (append#(add(N, X), Y) -> append#(X, Y), append#(add(N, X), Y) -> append#(X, Y))
     (qsort# add(N, X) -> f_3#(split(N, X), N, X), f_3#(pair(Y, Z), N, X) -> append#(qsort Y, add(X, qsort Z)))
     (qsort# add(N, X) -> f_3#(split(N, X), N, X), f_3#(pair(Y, Z), N, X) -> qsort# Y)
     (qsort# add(N, X) -> f_3#(split(N, X), N, X), f_3#(pair(Y, Z), N, X) -> qsort# Z)}
    STATUS:
     arrows: 0.859504
     SCCS (4):
      Scc:
       {      qsort# add(N, X) -> f_3#(split(N, X), N, X),
        f_3#(pair(Y, Z), N, X) -> qsort# Y,
        f_3#(pair(Y, Z), N, X) -> qsort# Z}
      Scc:
       {split#(N, add(M, Y)) -> split#(N, Y)}
      Scc:
       {lt#(s X, s Y) -> lt#(X, Y)}
      Scc:
       {append#(add(N, X), Y) -> append#(X, Y)}
      
      SCC (3):
       Strict:
        {      qsort# add(N, X) -> f_3#(split(N, X), N, X),
         f_3#(pair(Y, Z), N, X) -> qsort# Y,
         f_3#(pair(Y, Z), N, X) -> qsort# Z}
       Weak:
       {               lt(0(), s X) -> true(),
                       lt(s X, 0()) -> false(),
                       lt(s X, s Y) -> lt(X, Y),
                   append(nil(), Y) -> Y,
               append(add(N, X), Y) -> add(N, append(X, Y)),
                    split(N, nil()) -> pair(nil(), nil()),
                split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
           f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
         f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
        f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                        qsort nil() -> nil(),
                    qsort add(N, X) -> f_3(split(N, X), N, X),
              f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))}
       Open
      
      SCC (1):
       Strict:
        {split#(N, add(M, Y)) -> split#(N, Y)}
       Weak:
       {               lt(0(), s X) -> true(),
                       lt(s X, 0()) -> false(),
                       lt(s X, s Y) -> lt(X, Y),
                   append(nil(), Y) -> Y,
               append(add(N, X), Y) -> add(N, append(X, Y)),
                    split(N, nil()) -> pair(nil(), nil()),
                split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
           f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
         f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
        f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                        qsort nil() -> nil(),
                    qsort add(N, X) -> f_3(split(N, X), N, X),
              f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))}
       Open
      
      
      
      SCC (1):
       Strict:
        {lt#(s X, s Y) -> lt#(X, Y)}
       Weak:
       {               lt(0(), s X) -> true(),
                       lt(s X, 0()) -> false(),
                       lt(s X, s Y) -> lt(X, Y),
                   append(nil(), Y) -> Y,
               append(add(N, X), Y) -> add(N, append(X, Y)),
                    split(N, nil()) -> pair(nil(), nil()),
                split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
           f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
         f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
        f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                        qsort nil() -> nil(),
                    qsort add(N, X) -> f_3(split(N, X), N, X),
              f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))}
       Open
      
      SCC (1):
       Strict:
        {append#(add(N, X), Y) -> append#(X, Y)}
       Weak:
       {               lt(0(), s X) -> true(),
                       lt(s X, 0()) -> false(),
                       lt(s X, s Y) -> lt(X, Y),
                   append(nil(), Y) -> Y,
               append(add(N, X), Y) -> add(N, append(X, Y)),
                    split(N, nil()) -> pair(nil(), nil()),
                split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y),
           f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z),
         f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)),
        f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z),
                        qsort nil() -> nil(),
                    qsort add(N, X) -> f_3(split(N, X), N, X),
              f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))}
       Open