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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
            partGt(x,Nil()) -> Nil()
            partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
            partLt(x,Nil()) -> Nil()
            partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
            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)
            partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
            partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
            partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
            partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
            ,quicksort/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,>,app,goal,notEmpty,part,partGt,partGt[Ite][True][Ite]
            ,partLt,partLt[Ite][True][Ite],quicksort} and constructors {0,Cons,False,Nil,S,True}
    + 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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                            ,quicksort#(partLt(x,xs))
                            ,partLt#(x,xs)
                            ,quicksort#(partGt(x,xs))
                            ,partGt#(x,xs))
          partGt#(x,Nil()) -> c_7()
          partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
          partLt#(x,Nil()) -> c_9()
          partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
          quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
          quicksort#(Cons(x,Nil())) -> c_12()
          quicksort#(Nil()) -> c_13()
        Weak DPs
          <#(x,0()) -> c_14()
          <#(0(),S(y)) -> c_15()
          <#(S(x),S(y)) -> c_16(<#(x,y))
          >#(0(),y) -> c_17()
          >#(S(x),0()) -> c_18()
          >#(S(x),S(y)) -> c_19(>#(x,y))
          partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
          partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
          partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
          partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
        
        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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                              ,quicksort#(partLt(x,xs))
                              ,partLt#(x,xs)
                              ,quicksort#(partGt(x,xs))
                              ,partGt#(x,xs))
            partGt#(x,Nil()) -> c_7()
            partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
            partLt#(x,Nil()) -> c_9()
            partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
            quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
            quicksort#(Cons(x,Nil())) -> c_12()
            quicksort#(Nil()) -> c_13()
        - Weak DPs:
            <#(x,0()) -> c_14()
            <#(0(),S(y)) -> c_15()
            <#(S(x),S(y)) -> c_16(<#(x,y))
            >#(0(),y) -> c_17()
            >#(S(x),0()) -> c_18()
            >#(S(x),S(y)) -> c_19(>#(x,y))
            partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
            partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
            partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
            partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
        - 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
            partGt(x,Nil()) -> Nil()
            partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
            partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
            partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
            partLt(x,Nil()) -> Nil()
            partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
            partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
            partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
            ,quicksort/1,<#/2,>#/2,app#/2,goal#/1,notEmpty#/1,part#/2,partGt#/2,partGt[Ite][True][Ite]#/3,partLt#/2
            ,partLt[Ite][True][Ite]#/3,quicksort#/1} / {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/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1
            ,c_21/1,c_22/1,c_23/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt#
            ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S
            ,True}
    + 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
          partGt(x,Nil()) -> Nil()
          partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
          partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
          partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
          partLt(x,Nil()) -> Nil()
          partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
          partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
          partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
          quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
          <#(x,0()) -> c_14()
          <#(0(),S(y)) -> c_15()
          <#(S(x),S(y)) -> c_16(<#(x,y))
          >#(0(),y) -> c_17()
          >#(S(x),0()) -> c_18()
          >#(S(x),S(y)) -> c_19(>#(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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                            ,quicksort#(partLt(x,xs))
                            ,partLt#(x,xs)
                            ,quicksort#(partGt(x,xs))
                            ,partGt#(x,xs))
          partGt#(x,Nil()) -> c_7()
          partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
          partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
          partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
          partLt#(x,Nil()) -> c_9()
          partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
          partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
          partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
          quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
          quicksort#(Cons(x,Nil())) -> c_12()
          quicksort#(Nil()) -> c_13()
* 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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                              ,quicksort#(partLt(x,xs))
                              ,partLt#(x,xs)
                              ,quicksort#(partGt(x,xs))
                              ,partGt#(x,xs))
            partGt#(x,Nil()) -> c_7()
            partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
            partLt#(x,Nil()) -> c_9()
            partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
            quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
            quicksort#(Cons(x,Nil())) -> c_12()
            quicksort#(Nil()) -> c_13()
        - Weak DPs:
            <#(x,0()) -> c_14()
            <#(0(),S(y)) -> c_15()
            <#(S(x),S(y)) -> c_16(<#(x,y))
            >#(0(),y) -> c_17()
            >#(S(x),0()) -> c_18()
            >#(S(x),S(y)) -> c_19(>#(x,y))
            partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
            partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
            partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
            partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
        - 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
            partGt(x,Nil()) -> Nil()
            partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
            partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
            partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
            partLt(x,Nil()) -> Nil()
            partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
            partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
            partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
            ,quicksort/1,<#/2,>#/2,app#/2,goal#/1,notEmpty#/1,part#/2,partGt#/2,partGt[Ite][True][Ite]#/3,partLt#/2
            ,partLt[Ite][True][Ite]#/3,quicksort#/1} / {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/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1
            ,c_21/1,c_22/1,c_23/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt#
            ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} 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
          {2,4,5,12,13}
        by application of
          Pre({2,4,5,12,13}) = {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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                               ,quicksort#(partLt(x,xs))
                               ,partLt#(x,xs)
                               ,quicksort#(partGt(x,xs))
                               ,partGt#(x,xs))
          7: partGt#(x,Nil()) -> c_7()
          8: partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
          9: partLt#(x,Nil()) -> c_9()
          10: partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
          11: quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
          12: quicksort#(Cons(x,Nil())) -> c_12()
          13: quicksort#(Nil()) -> c_13()
          14: <#(x,0()) -> c_14()
          15: <#(0(),S(y)) -> c_15()
          16: <#(S(x),S(y)) -> c_16(<#(x,y))
          17: >#(0(),y) -> c_17()
          18: >#(S(x),0()) -> c_18()
          19: >#(S(x),S(y)) -> c_19(>#(x,y))
          20: partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
          21: partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
          22: partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
          23: partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
* 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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                              ,quicksort#(partLt(x,xs))
                              ,partLt#(x,xs)
                              ,quicksort#(partGt(x,xs))
                              ,partGt#(x,xs))
            partGt#(x,Nil()) -> c_7()
            partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
            partLt#(x,Nil()) -> c_9()
            partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
            quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
        - Weak DPs:
            <#(x,0()) -> c_14()
            <#(0(),S(y)) -> c_15()
            <#(S(x),S(y)) -> c_16(<#(x,y))
            >#(0(),y) -> c_17()
            >#(S(x),0()) -> c_18()
            >#(S(x),S(y)) -> c_19(>#(x,y))
            app#(Nil(),ys) -> c_2()
            notEmpty#(Cons(x,xs)) -> c_4()
            notEmpty#(Nil()) -> c_5()
            partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
            partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
            partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
            partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
            quicksort#(Cons(x,Nil())) -> c_12()
            quicksort#(Nil()) -> c_13()
        - 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
            partGt(x,Nil()) -> Nil()
            partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
            partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
            partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
            partLt(x,Nil()) -> Nil()
            partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
            partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
            partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
            ,quicksort/1,<#/2,>#/2,app#/2,goal#/1,notEmpty#/1,part#/2,partGt#/2,partGt[Ite][True][Ite]#/3,partLt#/2
            ,partLt[Ite][True][Ite]#/3,quicksort#/1} / {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/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1
            ,c_21/1,c_22/1,c_23/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt#
            ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S
            ,True}
    + 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():15
             -->_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_11(part#(x,Cons(x',xs))):8
             -->_1 quicksort#(Nil()) -> c_13():23
             -->_1 quicksort#(Cons(x,Nil())) -> c_12():22
          
          3:S:part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                                ,quicksort#(partLt(x,xs))
                                ,partLt#(x,xs)
                                ,quicksort#(partGt(x,xs))
                                ,partGt#(x,xs))
             -->_4 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8
             -->_3 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7
             -->_5 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5
             -->_4 quicksort#(Nil()) -> c_13():23
             -->_2 quicksort#(Nil()) -> c_13():23
             -->_4 quicksort#(Cons(x,Nil())) -> c_12():22
             -->_2 quicksort#(Cons(x,Nil())) -> c_12():22
             -->_1 app#(Nil(),ys) -> c_2():15
             -->_3 partLt#(x,Nil()) -> c_9():6
             -->_5 partGt#(x,Nil()) -> c_7():4
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
          
          4:S:partGt#(x,Nil()) -> c_7()
             
          
          5:S:partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
             -->_1 partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)):19
             -->_1 partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)):18
             -->_2 >#(S(x),S(y)) -> c_19(>#(x,y)):14
             -->_2 >#(S(x),0()) -> c_18():13
             -->_2 >#(0(),y) -> c_17():12
          
          6:S:partLt#(x,Nil()) -> c_9()
             
          
          7:S:partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
             -->_1 partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)):21
             -->_1 partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)):20
             -->_2 <#(S(x),S(y)) -> c_16(<#(x,y)):11
             -->_2 <#(0(),S(y)) -> c_15():10
             -->_2 <#(x,0()) -> c_14():9
          
          8:S:quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
             -->_1 part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                                     ,quicksort#(partLt(x,xs))
                                     ,partLt#(x,xs)
                                     ,quicksort#(partGt(x,xs))
                                     ,partGt#(x,xs)):3
          
          9:W:<#(x,0()) -> c_14()
             
          
          10:W:<#(0(),S(y)) -> c_15()
             
          
          11:W:<#(S(x),S(y)) -> c_16(<#(x,y))
             -->_1 <#(S(x),S(y)) -> c_16(<#(x,y)):11
             -->_1 <#(0(),S(y)) -> c_15():10
             -->_1 <#(x,0()) -> c_14():9
          
          12:W:>#(0(),y) -> c_17()
             
          
          13:W:>#(S(x),0()) -> c_18()
             
          
          14:W:>#(S(x),S(y)) -> c_19(>#(x,y))
             -->_1 >#(S(x),S(y)) -> c_19(>#(x,y)):14
             -->_1 >#(S(x),0()) -> c_18():13
             -->_1 >#(0(),y) -> c_17():12
          
          15:W:app#(Nil(),ys) -> c_2()
             
          
          16:W:notEmpty#(Cons(x,xs)) -> c_4()
             
          
          17:W:notEmpty#(Nil()) -> c_5()
             
          
          18:W:partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
             -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5
             -->_1 partGt#(x,Nil()) -> c_7():4
          
          19:W:partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
             -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5
             -->_1 partGt#(x,Nil()) -> c_7():4
          
          20:W:partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
             -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7
             -->_1 partLt#(x,Nil()) -> c_9():6
          
          21:W:partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
             -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7
             -->_1 partLt#(x,Nil()) -> c_9():6
          
          22:W:quicksort#(Cons(x,Nil())) -> c_12()
             
          
          23:W:quicksort#(Nil()) -> c_13()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          17: notEmpty#(Nil()) -> c_5()
          16: notEmpty#(Cons(x,xs)) -> c_4()
          22: quicksort#(Cons(x,Nil())) -> c_12()
          23: quicksort#(Nil()) -> c_13()
          14: >#(S(x),S(y)) -> c_19(>#(x,y))
          12: >#(0(),y) -> c_17()
          13: >#(S(x),0()) -> c_18()
          11: <#(S(x),S(y)) -> c_16(<#(x,y))
          9: <#(x,0()) -> c_14()
          10: <#(0(),S(y)) -> c_15()
          15: 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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                              ,quicksort#(partLt(x,xs))
                              ,partLt#(x,xs)
                              ,quicksort#(partGt(x,xs))
                              ,partGt#(x,xs))
            partGt#(x,Nil()) -> c_7()
            partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
            partLt#(x,Nil()) -> c_9()
            partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
            quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
        - Weak DPs:
            partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
            partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
            partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
            partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
        - 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
            partGt(x,Nil()) -> Nil()
            partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
            partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
            partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
            partLt(x,Nil()) -> Nil()
            partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
            partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
            partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
            ,quicksort/1,<#/2,>#/2,app#/2,goal#/1,notEmpty#/1,part#/2,partGt#/2,partGt[Ite][True][Ite]#/3,partLt#/2
            ,partLt[Ite][True][Ite]#/3,quicksort#/1} / {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/5,c_7/0,c_8/2,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1
            ,c_21/1,c_22/1,c_23/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt#
            ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S
            ,True}
    + 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_11(part#(x,Cons(x',xs))):8
          
          3:S:part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                                ,quicksort#(partLt(x,xs))
                                ,partLt#(x,xs)
                                ,quicksort#(partGt(x,xs))
                                ,partGt#(x,xs))
             -->_4 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8
             -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8
             -->_3 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7
             -->_5 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5
             -->_3 partLt#(x,Nil()) -> c_9():6
             -->_5 partGt#(x,Nil()) -> c_7():4
             -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
          
          4:S:partGt#(x,Nil()) -> c_7()
             
          
          5:S:partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x'))
             -->_1 partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)):19
             -->_1 partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)):18
          
          6:S:partLt#(x,Nil()) -> c_9()
             
          
          7:S:partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x'))
             -->_1 partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)):21
             -->_1 partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)):20
          
          8:S:quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
             -->_1 part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                                     ,quicksort#(partLt(x,xs))
                                     ,partLt#(x,xs)
                                     ,quicksort#(partGt(x,xs))
                                     ,partGt#(x,xs)):3
          
          18:W:partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
             -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5
             -->_1 partGt#(x,Nil()) -> c_7():4
          
          19:W:partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
             -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)),>#(x,x')):5
             -->_1 partGt#(x,Nil()) -> c_7():4
          
          20:W:partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
             -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7
             -->_1 partLt#(x,Nil()) -> c_9():6
          
          21:W:partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
             -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)),<#(x,x')):7
             -->_1 partLt#(x,Nil()) -> c_9():6
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)))
          partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)))
* 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,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                              ,quicksort#(partLt(x,xs))
                              ,partLt#(x,xs)
                              ,quicksort#(partGt(x,xs))
                              ,partGt#(x,xs))
            partGt#(x,Nil()) -> c_7()
            partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)))
            partLt#(x,Nil()) -> c_9()
            partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)))
            quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
        - Weak DPs:
            partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
            partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
            partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
            partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
        - 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
            partGt(x,Nil()) -> Nil()
            partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
            partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
            partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
            partLt(x,Nil()) -> Nil()
            partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
            partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
            partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
            quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
            quicksort(Cons(x,Nil())) -> Cons(x,Nil())
            quicksort(Nil()) -> Nil()
        - Signature:
            {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
            ,quicksort/1,<#/2,>#/2,app#/2,goal#/1,notEmpty#/1,part#/2,partGt#/2,partGt[Ite][True][Ite]#/3,partLt#/2
            ,partLt[Ite][True][Ite]#/3,quicksort#/1} / {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/5,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1
            ,c_21/1,c_22/1,c_23/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt#
            ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S
            ,True}
    + 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_11(part#(x,Cons(x',xs))):8
        
        3:S:part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                              ,quicksort#(partLt(x,xs))
                              ,partLt#(x,xs)
                              ,quicksort#(partGt(x,xs))
                              ,partGt#(x,xs))
           -->_4 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8
           -->_2 quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs))):8
           -->_3 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))):7
           -->_5 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))):5
           -->_3 partLt#(x,Nil()) -> c_9():6
           -->_5 partGt#(x,Nil()) -> c_7():4
           -->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
        
        4:S:partGt#(x,Nil()) -> c_7()
           
        
        5:S:partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)))
           -->_1 partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs)):10
           -->_1 partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs)):9
        
        6:S:partLt#(x,Nil()) -> c_9()
           
        
        7:S:partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)))
           -->_1 partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs)):12
           -->_1 partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs)):11
        
        8:S:quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
           -->_1 part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                                   ,quicksort#(partLt(x,xs))
                                   ,partLt#(x,xs)
                                   ,quicksort#(partGt(x,xs))
                                   ,partGt#(x,xs)):3
        
        9:W:partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
           -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))):5
           -->_1 partGt#(x,Nil()) -> c_7():4
        
        10:W:partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
           -->_1 partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs))):5
           -->_1 partGt#(x,Nil()) -> c_7():4
        
        11:W:partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
           -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))):7
           -->_1 partLt#(x,Nil()) -> c_9():6
        
        12:W:partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
           -->_1 partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs))):7
           -->_1 partLt#(x,Nil()) -> c_9():6
        
        
        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: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
          part#(x,xs) -> c_6(app#(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
                            ,quicksort#(partLt(x,xs))
                            ,partLt#(x,xs)
                            ,quicksort#(partGt(x,xs))
                            ,partGt#(x,xs))
          partGt#(x,Nil()) -> c_7()
          partGt#(x',Cons(x,xs)) -> c_8(partGt[Ite][True][Ite]#(>(x,x'),x',Cons(x,xs)))
          partLt#(x,Nil()) -> c_9()
          partLt#(x',Cons(x,xs)) -> c_10(partLt[Ite][True][Ite]#(<(x,x'),x',Cons(x,xs)))
          quicksort#(Cons(x,Cons(x',xs))) -> c_11(part#(x,Cons(x',xs)))
      - Weak DPs:
          partGt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_20(partGt#(x',xs))
          partGt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_21(partGt#(x',xs))
          partLt[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_22(partLt#(x',xs))
          partLt[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_23(partLt#(x',xs))
      - 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,xs) -> app(quicksort(partLt(x,xs)),Cons(x,quicksort(partGt(x,xs))))
          partGt(x,Nil()) -> Nil()
          partGt(x',Cons(x,xs)) -> partGt[Ite][True][Ite](>(x,x'),x',Cons(x,xs))
          partGt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partGt(x',xs)
          partGt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partGt(x',xs))
          partLt(x,Nil()) -> Nil()
          partLt(x',Cons(x,xs)) -> partLt[Ite][True][Ite](<(x,x'),x',Cons(x,xs))
          partLt[Ite][True][Ite](False(),x',Cons(x,xs)) -> partLt(x',xs)
          partLt[Ite][True][Ite](True(),x',Cons(x,xs)) -> Cons(x,partLt(x',xs))
          quicksort(Cons(x,Cons(x',xs))) -> part(x,Cons(x',xs))
          quicksort(Cons(x,Nil())) -> Cons(x,Nil())
          quicksort(Nil()) -> Nil()
      - Signature:
          {</2,>/2,app/2,goal/1,notEmpty/1,part/2,partGt/2,partGt[Ite][True][Ite]/3,partLt/2,partLt[Ite][True][Ite]/3
          ,quicksort/1,<#/2,>#/2,app#/2,goal#/1,notEmpty#/1,part#/2,partGt#/2,partGt[Ite][True][Ite]#/3,partLt#/2
          ,partLt[Ite][True][Ite]#/3,quicksort#/1} / {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/5,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/0,c_18/0,c_19/1,c_20/1
          ,c_21/1,c_22/1,c_23/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {<#,>#,app#,goal#,notEmpty#,part#,partGt#
          ,partGt[Ite][True][Ite]#,partLt#,partLt[Ite][True][Ite]#,quicksort#} and constructors {0,Cons,False,Nil,S
          ,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE