MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          #and(#false(),#false()) -> #false()
          #and(#false(),#true()) -> #false()
          #and(#true(),#false()) -> #false()
          #and(#true(),#true()) -> #true()
          #ckgt(#EQ()) -> #false()
          #ckgt(#GT()) -> #true()
          #ckgt(#LT()) -> #false()
          #compare(#0(),#0()) -> #EQ()
          #compare(#0(),#neg(y)) -> #GT()
          #compare(#0(),#pos(y)) -> #LT()
          #compare(#0(),#s(y)) -> #LT()
          #compare(#neg(x),#0()) -> #LT()
          #compare(#neg(x),#neg(y)) -> #compare(y,x)
          #compare(#neg(x),#pos(y)) -> #LT()
          #compare(#pos(x),#0()) -> #GT()
          #compare(#pos(x),#neg(y)) -> #GT()
          #compare(#pos(x),#pos(y)) -> #compare(x,y)
          #compare(#s(x),#0()) -> #GT()
          #compare(#s(x),#s(y)) -> #compare(x,y)
          #eq(#0(),#0()) -> #true()
          #eq(#0(),#neg(y)) -> #false()
          #eq(#0(),#pos(y)) -> #false()
          #eq(#0(),#s(y)) -> #false()
          #eq(#neg(x),#0()) -> #false()
          #eq(#neg(x),#neg(y)) -> #eq(x,y)
          #eq(#neg(x),#pos(y)) -> #false()
          #eq(#pos(x),#0()) -> #false()
          #eq(#pos(x),#neg(y)) -> #false()
          #eq(#pos(x),#pos(y)) -> #eq(x,y)
          #eq(#s(x),#0()) -> #false()
          #eq(#s(x),#s(y)) -> #eq(x,y)
          #eq(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2))
          #eq(dd(x'1,x'2),nil()) -> #false()
          #eq(dd(x'1,x'2),tuple#2(y'1,y'2)) -> #false()
          #eq(nil(),dd(y'1,y'2)) -> #false()
          #eq(nil(),nil()) -> #true()
          #eq(nil(),tuple#2(y'1,y'2)) -> #false()
          #eq(tuple#2(x'1,x'2),dd(y'1,y'2)) -> #false()
          #eq(tuple#2(x'1,x'2),nil()) -> #false()
          #eq(tuple#2(x'1,x'2),tuple#2(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2))
          #equal(x,y) -> #eq(x,y)
          #greater(x,y) -> #ckgt(#compare(x,y))
          append(l,ys) -> append#1(l,ys)
          append#1(dd(x,xs),ys) -> dd(x,append(xs,ys))
          append#1(nil(),ys) -> ys
          insert(x,l) -> insert#1(x,l,x)
          insert#1(tuple#2(valX,keyX),l,x) -> insert#2(l,keyX,valX,x)
          insert#2(dd(l1,ls),keyX,valX,x) -> insert#3(l1,keyX,ls,valX,x)
          insert#2(nil(),keyX,valX,x) -> dd(tuple#2(dd(valX,nil()),keyX),nil())
          insert#3(tuple#2(vals1,key1),keyX,ls,valX,x) -> insert#4(#equal(key1,keyX),key1,ls,valX,vals1,x)
          insert#4(#false(),key1,ls,valX,vals1,x) -> dd(tuple#2(vals1,key1),insert(x,ls))
          insert#4(#true(),key1,ls,valX,vals1,x) -> dd(tuple#2(dd(valX,vals1),key1),ls)
          quicksort(l) -> quicksort#1(l)
          quicksort#1(dd(z,zs)) -> quicksort#2(splitqs(z,zs),z)
          quicksort#1(nil()) -> nil()
          quicksort#2(tuple#2(xs,ys),z) -> append(quicksort(xs),dd(z,quicksort(ys)))
          sortAll(l) -> sortAll#1(l)
          sortAll#1(dd(x,xs)) -> sortAll#2(x,xs)
          sortAll#1(nil()) -> nil()
          sortAll#2(tuple#2(vals,key),xs) -> dd(tuple#2(quicksort(vals),key),sortAll(xs))
          split(l) -> split#1(l)
          split#1(dd(x,xs)) -> insert(x,split(xs))
          split#1(nil()) -> nil()
          splitAndSort(l) -> sortAll(split(l))
          splitqs(pivot,l) -> splitqs#1(l,pivot)
          splitqs#1(dd(x,xs),pivot) -> splitqs#2(splitqs(pivot,xs),pivot,x)
          splitqs#1(nil(),pivot) -> tuple#2(nil(),nil())
          splitqs#2(tuple#2(ls,rs),pivot,x) -> splitqs#3(#greater(x,pivot),ls,rs,x)
          splitqs#3(#false(),ls,rs,x) -> tuple#2(dd(x,ls),rs)
          splitqs#3(#true(),ls,rs,x) -> tuple#2(ls,dd(x,rs))
      - Signature:
          {#and/2,#ckgt/1,#compare/2,#eq/2,#equal/2,#greater/2,append/2,append#1/2,insert/2,insert#1/3,insert#2/4
          ,insert#3/5,insert#4/6,quicksort/1,quicksort#1/1,quicksort#2/2,sortAll/1,sortAll#1/1,sortAll#2/2,split/1
          ,split#1/1,splitAndSort/1,splitqs/2,splitqs#1/2,splitqs#2/3,splitqs#3/4} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0
          ,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,tuple#2/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {#and,#ckgt,#compare,#eq,#equal,#greater,append,append#1
          ,insert,insert#1,insert#2,insert#3,insert#4,quicksort,quicksort#1,quicksort#2,sortAll,sortAll#1,sortAll#2
          ,split,split#1,splitAndSort,splitqs,splitqs#1,splitqs#2,splitqs#3} and constructors {#0,#EQ,#GT,#LT,#false
          ,#neg,#pos,#s,#true,dd,nil,tuple#2}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE