MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          'cklt('EQ()) -> 'false()
          'cklt('GT()) -> 'false()
          'cklt('LT()) -> 'true()
          '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)
          'less(x,y) -> 'cklt('compare(x,y))
          merge(l1,l2) -> merge'1(l1,l2)
          merge'1(dd(x,xs),l2) -> merge'2(l2,x,xs)
          merge'1(nil(),l2) -> l2
          merge'2(dd(y,ys),x,xs) -> merge'3('less(x,y),x,xs,y,ys)
          merge'2(nil(),x,xs) -> dd(x,xs)
          merge'3('false(),x,xs,y,ys) -> dd(y,merge(dd(x,xs),ys))
          merge'3('true(),x,xs,y,ys) -> dd(x,merge(xs,dd(y,ys)))
          mergesort(l) -> mergesort'1(l)
          mergesort'1(dd(x1,xs)) -> mergesort'2(xs,x1)
          mergesort'1(nil()) -> nil()
          mergesort'2(dd(x2,xs'),x1) -> mergesort'3(msplit(dd(x1,dd(x2,xs'))))
          mergesort'2(nil(),x1) -> dd(x1,nil())
          mergesort'3(tuple'2(l1,l2)) -> merge(mergesort(l1),mergesort(l2))
          msplit(l) -> msplit'1(l)
          msplit'1(dd(x1,xs)) -> msplit'2(xs,x1)
          msplit'1(nil()) -> tuple'2(nil(),nil())
          msplit'2(dd(x2,xs'),x1) -> msplit'3(msplit(xs'),x1,x2)
          msplit'2(nil(),x1) -> tuple'2(dd(x1,nil()),nil())
          msplit'3(tuple'2(l1,l2),x1,x2) -> tuple'2(dd(x1,l1),dd(x2,l2))
      - Signature:
          {'cklt/1,'compare/2,'less/2,merge/2,merge'1/2,merge'2/3,merge'3/5,mergesort/1,mergesort'1/1,mergesort'2/2
          ,mergesort'3/1,msplit/1,msplit'1/1,msplit'2/2,msplit'3/3} / {'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 {'cklt,'compare,'less,merge,merge'1,merge'2,merge'3
          ,mergesort,mergesort'1,mergesort'2,mergesort'3,msplit,msplit'1,msplit'2,msplit'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