MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          #equal(@x,@y) -> #eq(@x,@y)
          #greater(@x,@y) -> #ckgt(#compare(@x,@y))
          append(@l,@ys) -> append#1(@l,@ys)
          append#1(::(@x,@xs),@ys) -> ::(@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(::(@l1,@ls),@keyX,@valX,@x) -> insert#3(@l1,@keyX,@ls,@valX,@x)
          insert#2(nil(),@keyX,@valX,@x) -> ::(tuple#2(::(@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) -> ::(tuple#2(@vals1,@key1),insert(@x,@ls))
          insert#4(#true(),@key1,@ls,@valX,@vals1,@x) -> ::(tuple#2(::(@valX,@vals1),@key1),@ls)
          quicksort(@l) -> quicksort#1(@l)
          quicksort#1(::(@z,@zs)) -> quicksort#2(splitqs(@z,@zs),@z)
          quicksort#1(nil()) -> nil()
          quicksort#2(tuple#2(@xs,@ys),@z) -> append(quicksort(@xs),::(@z,quicksort(@ys)))
          sortAll(@l) -> sortAll#1(@l)
          sortAll#1(::(@x,@xs)) -> sortAll#2(@x,@xs)
          sortAll#1(nil()) -> nil()
          sortAll#2(tuple#2(@vals,@key),@xs) -> ::(tuple#2(quicksort(@vals),@key),sortAll(@xs))
          split(@l) -> split#1(@l)
          split#1(::(@x,@xs)) -> insert(@x,split(@xs))
          split#1(nil()) -> nil()
          splitAndSort(@l) -> sortAll(split(@l))
          splitqs(@pivot,@l) -> splitqs#1(@l,@pivot)
          splitqs#1(::(@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(::(@x,@ls),@rs)
          splitqs#3(#true(),@ls,@rs,@x) -> tuple#2(@ls,::(@x,@rs))
      - Weak 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(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          #eq(::(@x_1,@x_2),nil()) -> #false()
          #eq(::(@x_1,@x_2),tuple#2(@y_1,@y_2)) -> #false()
          #eq(nil(),::(@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),::(@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))
      - 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,::/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,::,nil,tuple#2}
  + Applied Processor:
      NaturalPI {shape = Mixed 3, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE