MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            goal(xs) -> mergesort(xs)
            merge(Cons(x,xs),Nil()) -> Cons(x,xs)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
            merge(Nil(),xs2) -> xs2
            mergesort(Cons(x,Nil())) -> Cons(x,Nil())
            mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
            mergesort(Nil()) -> Nil()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
            splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
        - Weak TRS:
            <=(0(),y) -> True()
            <=(S(x),0()) -> False()
            <=(S(x),S(y)) -> <=(x,y)
            merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
            merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
        - Signature:
            {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3} / {0/0,Cons/2,False/0,Nil/0,S/1
            ,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite],mergesort,notEmpty
            ,splitmerge} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          goal#(xs) -> c_1(mergesort#(xs))
          merge#(Cons(x,xs),Nil()) -> c_2()
          merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
          merge#(Nil(),xs2) -> c_4()
          mergesort#(Cons(x,Nil())) -> c_5()
          mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
          mergesort#(Nil()) -> c_7()
          notEmpty#(Cons(x,xs)) -> c_8()
          notEmpty#(Nil()) -> c_9()
          splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
          splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
        Weak DPs
          <=#(0(),y) -> c_12()
          <=#(S(x),0()) -> c_13()
          <=#(S(x),S(y)) -> c_14(<=#(x,y))
          merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
          merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(mergesort#(xs))
            merge#(Cons(x,xs),Nil()) -> c_2()
            merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
            merge#(Nil(),xs2) -> c_4()
            mergesort#(Cons(x,Nil())) -> c_5()
            mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
            mergesort#(Nil()) -> c_7()
            notEmpty#(Cons(x,xs)) -> c_8()
            notEmpty#(Nil()) -> c_9()
            splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
            splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
        - Weak DPs:
            <=#(0(),y) -> c_12()
            <=#(S(x),0()) -> c_13()
            <=#(S(x),S(y)) -> c_14(<=#(x,y))
            merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
            merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
        - Weak TRS:
            <=(0(),y) -> True()
            <=(S(x),0()) -> False()
            <=(S(x),S(y)) -> <=(x,y)
            goal(xs) -> mergesort(xs)
            merge(Cons(x,xs),Nil()) -> Cons(x,xs)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
            merge(Nil(),xs2) -> xs2
            merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
            merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
            mergesort(Cons(x,Nil())) -> Cons(x,Nil())
            mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
            mergesort(Nil()) -> Nil()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
            splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
        - Signature:
            {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3,<=#/2,goal#/1,merge#/2,merge[Ite]#/3
            ,mergesort#/1,notEmpty#/1,splitmerge#/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0
            ,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#,mergesort#,notEmpty#
            ,splitmerge#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          <=(0(),y) -> True()
          <=(S(x),0()) -> False()
          <=(S(x),S(y)) -> <=(x,y)
          merge(Cons(x,xs),Nil()) -> Cons(x,xs)
          merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
          merge(Nil(),xs2) -> xs2
          merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
          merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
          mergesort(Cons(x,Nil())) -> Cons(x,Nil())
          mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
          mergesort(Nil()) -> Nil()
          splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
          splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
          <=#(0(),y) -> c_12()
          <=#(S(x),0()) -> c_13()
          <=#(S(x),S(y)) -> c_14(<=#(x,y))
          goal#(xs) -> c_1(mergesort#(xs))
          merge#(Cons(x,xs),Nil()) -> c_2()
          merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
          merge#(Nil(),xs2) -> c_4()
          merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
          merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
          mergesort#(Cons(x,Nil())) -> c_5()
          mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
          mergesort#(Nil()) -> c_7()
          notEmpty#(Cons(x,xs)) -> c_8()
          notEmpty#(Nil()) -> c_9()
          splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
          splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(mergesort#(xs))
            merge#(Cons(x,xs),Nil()) -> c_2()
            merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
            merge#(Nil(),xs2) -> c_4()
            mergesort#(Cons(x,Nil())) -> c_5()
            mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
            mergesort#(Nil()) -> c_7()
            notEmpty#(Cons(x,xs)) -> c_8()
            notEmpty#(Nil()) -> c_9()
            splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
            splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
        - Weak DPs:
            <=#(0(),y) -> c_12()
            <=#(S(x),0()) -> c_13()
            <=#(S(x),S(y)) -> c_14(<=#(x,y))
            merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
            merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
        - Weak TRS:
            <=(0(),y) -> True()
            <=(S(x),0()) -> False()
            <=(S(x),S(y)) -> <=(x,y)
            merge(Cons(x,xs),Nil()) -> Cons(x,xs)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
            merge(Nil(),xs2) -> xs2
            merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
            merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
            mergesort(Cons(x,Nil())) -> Cons(x,Nil())
            mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
            mergesort(Nil()) -> Nil()
            splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
            splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
        - Signature:
            {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3,<=#/2,goal#/1,merge#/2,merge[Ite]#/3
            ,mergesort#/1,notEmpty#/1,splitmerge#/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0
            ,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#,mergesort#,notEmpty#
            ,splitmerge#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {5,7,8,9}
        by application of
          Pre({5,7,8,9}) = {1,11}.
        Here rules are labelled as follows:
          1: goal#(xs) -> c_1(mergesort#(xs))
          2: merge#(Cons(x,xs),Nil()) -> c_2()
          3: merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
          4: merge#(Nil(),xs2) -> c_4()
          5: mergesort#(Cons(x,Nil())) -> c_5()
          6: mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
          7: mergesort#(Nil()) -> c_7()
          8: notEmpty#(Cons(x,xs)) -> c_8()
          9: notEmpty#(Nil()) -> c_9()
          10: splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
          11: splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                                ,mergesort#(xs1)
                                                ,mergesort#(xs2))
          12: <=#(0(),y) -> c_12()
          13: <=#(S(x),0()) -> c_13()
          14: <=#(S(x),S(y)) -> c_14(<=#(x,y))
          15: merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
          16: merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(mergesort#(xs))
            merge#(Cons(x,xs),Nil()) -> c_2()
            merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
            merge#(Nil(),xs2) -> c_4()
            mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
            splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
            splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
        - Weak DPs:
            <=#(0(),y) -> c_12()
            <=#(S(x),0()) -> c_13()
            <=#(S(x),S(y)) -> c_14(<=#(x,y))
            merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
            merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
            mergesort#(Cons(x,Nil())) -> c_5()
            mergesort#(Nil()) -> c_7()
            notEmpty#(Cons(x,xs)) -> c_8()
            notEmpty#(Nil()) -> c_9()
        - Weak TRS:
            <=(0(),y) -> True()
            <=(S(x),0()) -> False()
            <=(S(x),S(y)) -> <=(x,y)
            merge(Cons(x,xs),Nil()) -> Cons(x,xs)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
            merge(Nil(),xs2) -> xs2
            merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
            merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
            mergesort(Cons(x,Nil())) -> Cons(x,Nil())
            mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
            mergesort(Nil()) -> Nil()
            splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
            splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
        - Signature:
            {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3,<=#/2,goal#/1,merge#/2,merge[Ite]#/3
            ,mergesort#/1,notEmpty#/1,splitmerge#/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0
            ,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#,mergesort#,notEmpty#
            ,splitmerge#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:goal#(xs) -> c_1(mergesort#(xs))
             -->_1 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
             -->_1 mergesort#(Nil()) -> c_7():14
             -->_1 mergesort#(Cons(x,Nil())) -> c_5():13
          
          2:S:merge#(Cons(x,xs),Nil()) -> c_2()
             
          
          3:S:merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
             -->_1 merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2)):12
             -->_1 merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs)):11
             -->_2 <=#(S(x),S(y)) -> c_14(<=#(x,y)):10
             -->_2 <=#(S(x),0()) -> c_13():9
             -->_2 <=#(0(),y) -> c_12():8
          
          4:S:merge#(Nil(),xs2) -> c_4()
             
          
          5:S:mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
             -->_1 splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1)):6
          
          6:S:splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
             -->_1 splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                                     ,mergesort#(xs1)
                                                     ,mergesort#(xs2)):7
             -->_1 splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1)):6
          
          7:S:splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                                ,mergesort#(xs1)
                                                ,mergesort#(xs2))
             -->_3 mergesort#(Nil()) -> c_7():14
             -->_2 mergesort#(Nil()) -> c_7():14
             -->_3 mergesort#(Cons(x,Nil())) -> c_5():13
             -->_2 mergesort#(Cons(x,Nil())) -> c_5():13
             -->_3 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
             -->_2 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
             -->_1 merge#(Nil(),xs2) -> c_4():4
             -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3
             -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
          
          8:W:<=#(0(),y) -> c_12()
             
          
          9:W:<=#(S(x),0()) -> c_13()
             
          
          10:W:<=#(S(x),S(y)) -> c_14(<=#(x,y))
             -->_1 <=#(S(x),S(y)) -> c_14(<=#(x,y)):10
             -->_1 <=#(S(x),0()) -> c_13():9
             -->_1 <=#(0(),y) -> c_12():8
          
          11:W:merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
             -->_1 merge#(Nil(),xs2) -> c_4():4
             -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3
             -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
          
          12:W:merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
             -->_1 merge#(Nil(),xs2) -> c_4():4
             -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3
             -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
          
          13:W:mergesort#(Cons(x,Nil())) -> c_5()
             
          
          14:W:mergesort#(Nil()) -> c_7()
             
          
          15:W:notEmpty#(Cons(x,xs)) -> c_8()
             
          
          16:W:notEmpty#(Nil()) -> c_9()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          16: notEmpty#(Nil()) -> c_9()
          15: notEmpty#(Cons(x,xs)) -> c_8()
          10: <=#(S(x),S(y)) -> c_14(<=#(x,y))
          8: <=#(0(),y) -> c_12()
          9: <=#(S(x),0()) -> c_13()
          13: mergesort#(Cons(x,Nil())) -> c_5()
          14: mergesort#(Nil()) -> c_7()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(mergesort#(xs))
            merge#(Cons(x,xs),Nil()) -> c_2()
            merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
            merge#(Nil(),xs2) -> c_4()
            mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
            splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
            splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
        - Weak DPs:
            merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
            merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
        - Weak TRS:
            <=(0(),y) -> True()
            <=(S(x),0()) -> False()
            <=(S(x),S(y)) -> <=(x,y)
            merge(Cons(x,xs),Nil()) -> Cons(x,xs)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
            merge(Nil(),xs2) -> xs2
            merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
            merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
            mergesort(Cons(x,Nil())) -> Cons(x,Nil())
            mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
            mergesort(Nil()) -> Nil()
            splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
            splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
        - Signature:
            {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3,<=#/2,goal#/1,merge#/2,merge[Ite]#/3
            ,mergesort#/1,notEmpty#/1,splitmerge#/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0
            ,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#,mergesort#,notEmpty#
            ,splitmerge#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:goal#(xs) -> c_1(mergesort#(xs))
             -->_1 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
          
          2:S:merge#(Cons(x,xs),Nil()) -> c_2()
             
          
          3:S:merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x))
             -->_1 merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2)):12
             -->_1 merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs)):11
          
          4:S:merge#(Nil(),xs2) -> c_4()
             
          
          5:S:mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
             -->_1 splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1)):6
          
          6:S:splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
             -->_1 splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                                     ,mergesort#(xs1)
                                                     ,mergesort#(xs2)):7
             -->_1 splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1)):6
          
          7:S:splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                                ,mergesort#(xs1)
                                                ,mergesort#(xs2))
             -->_3 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
             -->_2 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
             -->_1 merge#(Nil(),xs2) -> c_4():4
             -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3
             -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
          
          11:W:merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
             -->_1 merge#(Nil(),xs2) -> c_4():4
             -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3
             -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
          
          12:W:merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
             -->_1 merge#(Nil(),xs2) -> c_4():4
             -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3
             -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)))
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(mergesort#(xs))
            merge#(Cons(x,xs),Nil()) -> c_2()
            merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)))
            merge#(Nil(),xs2) -> c_4()
            mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
            splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
            splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
        - Weak DPs:
            merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
            merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
        - Weak TRS:
            <=(0(),y) -> True()
            <=(S(x),0()) -> False()
            <=(S(x),S(y)) -> <=(x,y)
            merge(Cons(x,xs),Nil()) -> Cons(x,xs)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
            merge(Nil(),xs2) -> xs2
            merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
            merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
            mergesort(Cons(x,Nil())) -> Cons(x,Nil())
            mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
            mergesort(Nil()) -> Nil()
            splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
            splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
        - Signature:
            {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3,<=#/2,goal#/1,merge#/2,merge[Ite]#/3
            ,mergesort#/1,notEmpty#/1,splitmerge#/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0
            ,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#,mergesort#,notEmpty#
            ,splitmerge#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:goal#(xs) -> c_1(mergesort#(xs))
           -->_1 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
        
        2:S:merge#(Cons(x,xs),Nil()) -> c_2()
           
        
        3:S:merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)))
           -->_1 merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2)):9
           -->_1 merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs)):8
        
        4:S:merge#(Nil(),xs2) -> c_4()
           
        
        5:S:mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
           -->_1 splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1)):6
        
        6:S:splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
           -->_1 splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                                   ,mergesort#(xs1)
                                                   ,mergesort#(xs2)):7
           -->_1 splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1)):6
        
        7:S:splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2))
                                              ,mergesort#(xs1)
                                              ,mergesort#(xs2))
           -->_3 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
           -->_2 mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil())):5
           -->_1 merge#(Nil(),xs2) -> c_4():4
           -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))):3
           -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
        
        8:W:merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
           -->_1 merge#(Nil(),xs2) -> c_4():4
           -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))):3
           -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
        
        9:W:merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
           -->_1 merge#(Nil(),xs2) -> c_4():4
           -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))):3
           -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(1,goal#(xs) -> c_1(mergesort#(xs)))]
* Step 7: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          merge#(Cons(x,xs),Nil()) -> c_2()
          merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)))
          merge#(Nil(),xs2) -> c_4()
          mergesort#(Cons(x',Cons(x,xs))) -> c_6(splitmerge#(Cons(x',Cons(x,xs)),Nil(),Nil()))
          splitmerge#(Cons(x,xs),xs1,xs2) -> c_10(splitmerge#(xs,Cons(x,xs2),xs1))
          splitmerge#(Nil(),xs1,xs2) -> c_11(merge#(mergesort(xs1),mergesort(xs2)),mergesort#(xs1),mergesort#(xs2))
      - Weak DPs:
          merge[Ite]#(False(),xs1,Cons(x,xs)) -> c_15(merge#(xs1,xs))
          merge[Ite]#(True(),Cons(x,xs),xs2) -> c_16(merge#(xs,xs2))
      - Weak TRS:
          <=(0(),y) -> True()
          <=(S(x),0()) -> False()
          <=(S(x),S(y)) -> <=(x,y)
          merge(Cons(x,xs),Nil()) -> Cons(x,xs)
          merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
          merge(Nil(),xs2) -> xs2
          merge[Ite](False(),xs1,Cons(x,xs)) -> Cons(x,merge(xs1,xs))
          merge[Ite](True(),Cons(x,xs),xs2) -> Cons(x,merge(xs,xs2))
          mergesort(Cons(x,Nil())) -> Cons(x,Nil())
          mergesort(Cons(x',Cons(x,xs))) -> splitmerge(Cons(x',Cons(x,xs)),Nil(),Nil())
          mergesort(Nil()) -> Nil()
          splitmerge(Cons(x,xs),xs1,xs2) -> splitmerge(xs,Cons(x,xs2),xs1)
          splitmerge(Nil(),xs1,xs2) -> merge(mergesort(xs1),mergesort(xs2))
      - Signature:
          {<=/2,goal/1,merge/2,merge[Ite]/3,mergesort/1,notEmpty/1,splitmerge/3,<=#/2,goal#/1,merge#/2,merge[Ite]#/3
          ,mergesort#/1,notEmpty#/1,splitmerge#/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0
          ,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#,mergesort#,notEmpty#
          ,splitmerge#} and constructors {0,Cons,False,Nil,S,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE