MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            goal(xs) -> quicksort(xs)
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1
            ,True/0,part[Ite][True][Ite][False][Ite]/5}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,>,app,goal,notEmpty,part,part[Ite][True][Ite]
            ,quicksort} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          app#(Nil(),ys) -> c_2()
          goal#(xs) -> c_3(quicksort#(xs))
          notEmpty#(Cons(x,xs)) -> c_4()
          notEmpty#(Nil()) -> c_5()
          part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
          quicksort#(Cons(x,Nil())) -> c_9()
          quicksort#(Nil()) -> c_10()
        Weak DPs
          <#(x,0()) -> c_11()
          <#(0(),S(y)) -> c_12()
          <#(S(x),S(y)) -> c_13(<#(x,y))
          >#(0(),y) -> c_14()
          >#(S(x),0()) -> c_15()
          >#(S(x),S(y)) -> c_16(>#(x,y))
          part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
          part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            app#(Nil(),ys) -> c_2()
            goal#(xs) -> c_3(quicksort#(xs))
            notEmpty#(Cons(x,xs)) -> c_4()
            notEmpty#(Nil()) -> c_5()
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
            quicksort#(Cons(x,Nil())) -> c_9()
            quicksort#(Nil()) -> c_10()
        - Weak DPs:
            <#(x,0()) -> c_11()
            <#(0(),S(y)) -> c_12()
            <#(S(x),S(y)) -> c_13(<#(x,y))
            >#(0(),y) -> c_14()
            >#(S(x),0()) -> c_15()
            >#(S(x),S(y)) -> c_16(>#(x,y))
            part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            goal(xs) -> quicksort(xs)
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/2,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          <(x,0()) -> False()
          <(0(),S(y)) -> True()
          <(S(x),S(y)) -> <(x,y)
          >(0(),y) -> False()
          >(S(x),0()) -> True()
          >(S(x),S(y)) -> >(x,y)
          app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
          app(Nil(),ys) -> ys
          part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                 ,x'
                                                                                                 ,Cons(x,xs)
                                                                                                 ,xs1
                                                                                                 ,xs2)
          part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
          <#(x,0()) -> c_11()
          <#(0(),S(y)) -> c_12()
          <#(S(x),S(y)) -> c_13(<#(x,y))
          >#(0(),y) -> c_14()
          >#(S(x),0()) -> c_15()
          >#(S(x),S(y)) -> c_16(>#(x,y))
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          app#(Nil(),ys) -> c_2()
          goal#(xs) -> c_3(quicksort#(xs))
          notEmpty#(Cons(x,xs)) -> c_4()
          notEmpty#(Nil()) -> c_5()
          part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
          part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
          part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
          quicksort#(Cons(x,Nil())) -> c_9()
          quicksort#(Nil()) -> c_10()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            app#(Nil(),ys) -> c_2()
            goal#(xs) -> c_3(quicksort#(xs))
            notEmpty#(Cons(x,xs)) -> c_4()
            notEmpty#(Nil()) -> c_5()
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
            quicksort#(Cons(x,Nil())) -> c_9()
            quicksort#(Nil()) -> c_10()
        - Weak DPs:
            <#(x,0()) -> c_11()
            <#(0(),S(y)) -> c_12()
            <#(S(x),S(y)) -> c_13(<#(x,y))
            >#(0(),y) -> c_14()
            >#(S(x),0()) -> c_15()
            >#(S(x),S(y)) -> c_16(>#(x,y))
            part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/2,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,5,9,10}
        by application of
          Pre({2,4,5,9,10}) = {1,3,6}.
        Here rules are labelled as follows:
          1: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          2: app#(Nil(),ys) -> c_2()
          3: goal#(xs) -> c_3(quicksort#(xs))
          4: notEmpty#(Cons(x,xs)) -> c_4()
          5: notEmpty#(Nil()) -> c_5()
          6: part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
          7: part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
          8: quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
          9: quicksort#(Cons(x,Nil())) -> c_9()
          10: quicksort#(Nil()) -> c_10()
          11: <#(x,0()) -> c_11()
          12: <#(0(),S(y)) -> c_12()
          13: <#(S(x),S(y)) -> c_13(<#(x,y))
          14: >#(0(),y) -> c_14()
          15: >#(S(x),0()) -> c_15()
          16: >#(S(x),S(y)) -> c_16(>#(x,y))
          17: part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
          18: part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            goal#(xs) -> c_3(quicksort#(xs))
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            <#(x,0()) -> c_11()
            <#(0(),S(y)) -> c_12()
            <#(S(x),S(y)) -> c_13(<#(x,y))
            >#(0(),y) -> c_14()
            >#(S(x),0()) -> c_15()
            >#(S(x),S(y)) -> c_16(>#(x,y))
            app#(Nil(),ys) -> c_2()
            notEmpty#(Cons(x,xs)) -> c_4()
            notEmpty#(Nil()) -> c_5()
            part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
            quicksort#(Cons(x,Nil())) -> c_9()
            quicksort#(Nil()) -> c_10()
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/2,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
             -->_1 app#(Nil(),ys) -> c_2():12
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
          
          2:S:goal#(xs) -> c_3(quicksort#(xs))
             -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
             -->_1 quicksort#(Nil()) -> c_10():18
             -->_1 quicksort#(Cons(x,Nil())) -> c_9():17
          
          3:S:part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
             -->_3 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
             -->_3 quicksort#(Nil()) -> c_10():18
             -->_2 quicksort#(Nil()) -> c_10():18
             -->_3 quicksort#(Cons(x,Nil())) -> c_9():17
             -->_2 quicksort#(Cons(x,Nil())) -> c_9():17
             -->_1 app#(Nil(),ys) -> c_2():12
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
          
          4:S:part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
             -->_1 part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2)):16
             -->_1 part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x)):15
             -->_2 >#(S(x),S(y)) -> c_16(>#(x,y)):11
             -->_2 >#(S(x),0()) -> c_15():10
             -->_2 >#(0(),y) -> c_14():9
          
          5:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)
                                                      ,>#(x',x)):4
          
          6:W:<#(x,0()) -> c_11()
             
          
          7:W:<#(0(),S(y)) -> c_12()
             
          
          8:W:<#(S(x),S(y)) -> c_13(<#(x,y))
             -->_1 <#(S(x),S(y)) -> c_13(<#(x,y)):8
             -->_1 <#(0(),S(y)) -> c_12():7
             -->_1 <#(x,0()) -> c_11():6
          
          9:W:>#(0(),y) -> c_14()
             
          
          10:W:>#(S(x),0()) -> c_15()
             
          
          11:W:>#(S(x),S(y)) -> c_16(>#(x,y))
             -->_1 >#(S(x),S(y)) -> c_16(>#(x,y)):11
             -->_1 >#(S(x),0()) -> c_15():10
             -->_1 >#(0(),y) -> c_14():9
          
          12:W:app#(Nil(),ys) -> c_2()
             
          
          13:W:notEmpty#(Cons(x,xs)) -> c_4()
             
          
          14:W:notEmpty#(Nil()) -> c_5()
             
          
          15:W:part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
             -->_1 <#(S(x),S(y)) -> c_13(<#(x,y)):8
             -->_1 <#(0(),S(y)) -> c_12():7
             -->_1 <#(x,0()) -> c_11():6
          
          16:W:part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)
                                                      ,>#(x',x)):4
             -->_1 part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2)):3
          
          17:W:quicksort#(Cons(x,Nil())) -> c_9()
             
          
          18:W:quicksort#(Nil()) -> c_10()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          14: notEmpty#(Nil()) -> c_5()
          13: notEmpty#(Cons(x,xs)) -> c_4()
          11: >#(S(x),S(y)) -> c_16(>#(x,y))
          9: >#(0(),y) -> c_14()
          10: >#(S(x),0()) -> c_15()
          15: part[Ite][True][Ite]#(False(),x',Cons(x,xs),xs1,xs2) -> c_17(<#(x',x))
          8: <#(S(x),S(y)) -> c_13(<#(x,y))
          6: <#(x,0()) -> c_11()
          7: <#(0(),S(y)) -> c_12()
          17: quicksort#(Cons(x,Nil())) -> c_9()
          18: quicksort#(Nil()) -> c_10()
          12: app#(Nil(),ys) -> c_2()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            goal#(xs) -> c_3(quicksort#(xs))
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/2,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
          
          2:S:goal#(xs) -> c_3(quicksort#(xs))
             -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
          
          3:S:part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
             -->_3 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
          
          4:S:part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2),>#(x',x))
             -->_1 part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2)):16
          
          5:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)
                                                      ,>#(x',x)):4
          
          16:W:part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)
                                                      ,>#(x',x)):4
             -->_1 part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            goal#(xs) -> c_3(quicksort#(xs))
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        2:S:goal#(xs) -> c_3(quicksort#(xs))
           -->_1 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
        
        3:S:part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
           -->_3 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
           -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):5
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        4:S:part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
           -->_1 part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2)):6
        
        5:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):4
        
        6:W:part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
           -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):4
           -->_1 part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2)):3
        
        
        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).
        
        [(2,goal#(xs) -> c_3(quicksort#(xs)))]
* Step 7: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          - Weak DPs:
              part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
              part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
          - Weak TRS:
              <(x,0()) -> False()
              <(0(),S(y)) -> True()
              <(S(x),S(y)) -> <(x,y)
              >(0(),y) -> False()
              >(S(x),0()) -> True()
              >(S(x),S(y)) -> >(x,y)
              app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
              app(Nil(),ys) -> ys
              part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                     ,x'
                                                                                                     ,Cons(x,xs)
                                                                                                     ,xs1
                                                                                                     ,xs2)
              part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
          - Signature:
              {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
              ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
              ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
              ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
              ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
        
        Problem (S)
          - Strict DPs:
              part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
              part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
              quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
          - Weak DPs:
              app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
              part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
          - Weak TRS:
              <(x,0()) -> False()
              <(0(),S(y)) -> True()
              <(S(x),S(y)) -> <(x,y)
              >(0(),y) -> False()
              >(S(x),0()) -> True()
              >(S(x),S(y)) -> >(x,y)
              app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
              app(Nil(),ys) -> ys
              part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
              part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
              part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                     ,x'
                                                                                                     ,Cons(x,xs)
                                                                                                     ,xs1
                                                                                                     ,xs2)
              part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
              quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
              quicksort(Cons(x,Nil())) -> Cons(x,Nil())
              quicksort(Nil()) -> Nil()
          - Signature:
              {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
              ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
              ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
              ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
              ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
** Step 7.a:1: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
      - Weak DPs:
          part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
      - Weak TRS:
          <(x,0()) -> False()
          <(0(),S(y)) -> True()
          <(S(x),S(y)) -> <(x,y)
          >(0(),y) -> False()
          >(S(x),0()) -> True()
          >(S(x),S(y)) -> >(x,y)
          app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
          app(Nil(),ys) -> ys
          part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
          part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
          part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                 ,x'
                                                                                                 ,Cons(x,xs)
                                                                                                 ,xs1
                                                                                                 ,xs2)
          part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
          quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
      - Signature:
          {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
          ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
          ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
          ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
          ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
** Step 7.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):4
             -->_3 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):3
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):3
          
          2:S:part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
             -->_1 part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2)):5
          
          3:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
          
          4:W:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):4
          
          5:W:part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2)):1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
** Step 7.b:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/3,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2))
             -->_3 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):3
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())):3
          
          2:S:part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
             -->_1 part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2)):5
          
          3:S:quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
          
          5:W:part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
             -->_1 part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2)):2
             -->_1 part#(x,Nil(),xs1,xs2) -> c_6(app#(quicksort(xs1),quicksort(xs2)),quicksort#(xs1),quicksort#(xs2)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          part#(x,Nil(),xs1,xs2) -> c_6(quicksort#(xs1),quicksort#(xs2))
** Step 7.b:3: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            part#(x,Nil(),xs1,xs2) -> c_6(quicksort#(xs1),quicksort#(xs2))
            part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
            quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
        - Weak DPs:
            part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            >(0(),y) -> False()
            >(S(x),0()) -> True()
            >(S(x),S(y)) -> >(x,y)
            app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
            app(Nil(),ys) -> ys
            part(x,Nil(),xs1,xs2) -> app(quicksort(xs1),quicksort(xs2))
            part(x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite](>(x',x),x',Cons(x,xs),xs1,xs2)
            part[Ite][True][Ite](False(),x',Cons(x,xs),xs1,xs2) -> part[Ite][True][Ite][False][Ite](<(x',x)
                                                                                                   ,x'
                                                                                                   ,Cons(x,xs)
                                                                                                   ,xs1
                                                                                                   ,xs2)
            part[Ite][True][Ite](True(),x',Cons(x,xs),xs1,xs2) -> part(x',xs,Cons(x,xs1),xs2)
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil())
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
            ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
            ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
            ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
            ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          >(0(),y) -> False()
          >(S(x),0()) -> True()
          >(S(x),S(y)) -> >(x,y)
          part#(x,Nil(),xs1,xs2) -> c_6(quicksort#(xs1),quicksort#(xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
** Step 7.b:4: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          part#(x,Nil(),xs1,xs2) -> c_6(quicksort#(xs1),quicksort#(xs2))
          part#(x',Cons(x,xs),xs1,xs2) -> c_7(part[Ite][True][Ite]#(>(x',x),x',Cons(x,xs),xs1,xs2))
          quicksort#(Cons(x,Cons(x',xs))) -> c_8(part#(x,Cons(x,Cons(x',xs)),Cons(x,Nil()),Nil()))
      - Weak DPs:
          part[Ite][True][Ite]#(True(),x',Cons(x,xs),xs1,xs2) -> c_18(part#(x',xs,Cons(x,xs1),xs2))
      - Weak TRS:
          >(0(),y) -> False()
          >(S(x),0()) -> True()
          >(S(x),S(y)) -> >(x,y)
      - Signature:
          {</2,>/2,app/2,goal/1,notEmpty/1,part/4,part[Ite][True][Ite]/5,quicksort/1,<#/2,>#/2,app#/2,goal#/1
          ,notEmpty#/1,part#/4,part[Ite][True][Ite]#/5,quicksort#/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0
          ,part[Ite][True][Ite][False][Ite]/5,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/1,c_8/1,c_9/0,c_10/0,c_11/0
          ,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,part[Ite][True][Ite]#
          ,quicksort#} and constructors {0,Cons,False,Nil,S,True,part[Ite][True][Ite][False][Ite]}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE