MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            if3(false(),xs) -> sort(del(max(xs),xs))
            if3(true(),xs) -> nil()
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
            sort(xs) -> if3(empty(xs),xs)
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del,empty,eq,ge,if1,if2,if3,max,sort} and constructors {0
            ,cons,false,nil,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
          del#(x,nil()) -> c_2()
          empty#(cons(x,xs)) -> c_3()
          empty#(nil()) -> c_4()
          eq#(0(),0()) -> c_5()
          eq#(0(),s(y)) -> c_6()
          eq#(s(x),0()) -> c_7()
          eq#(s(x),s(y)) -> c_8(eq#(x,y))
          ge#(x,0()) -> c_9()
          ge#(0(),s(x)) -> c_10()
          ge#(s(x),s(y)) -> c_11(ge#(x,y))
          if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
          if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          if2#(false(),x,y,xs) -> c_14(del#(x,xs))
          if2#(true(),x,y,xs) -> c_15()
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
          if3#(true(),xs) -> c_17()
          max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
          max#(cons(x,nil())) -> c_19()
          max#(nil()) -> c_20()
          sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            del#(x,nil()) -> c_2()
            empty#(cons(x,xs)) -> c_3()
            empty#(nil()) -> c_4()
            eq#(0(),0()) -> c_5()
            eq#(0(),s(y)) -> c_6()
            eq#(s(x),0()) -> c_7()
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            ge#(x,0()) -> c_9()
            ge#(0(),s(x)) -> c_10()
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
            if2#(true(),x,y,xs) -> c_15()
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            if3#(true(),xs) -> c_17()
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            max#(cons(x,nil())) -> c_19()
            max#(nil()) -> c_20()
            sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            if3(false(),xs) -> sort(del(max(xs),xs))
            if3(true(),xs) -> nil()
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
            sort(xs) -> if3(empty(xs),xs)
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
          del(x,nil()) -> nil()
          empty(cons(x,xs)) -> false()
          empty(nil()) -> true()
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          ge(x,0()) -> true()
          ge(0(),s(x)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          if1(false(),x,y,xs) -> max(cons(y,xs))
          if1(true(),x,y,xs) -> max(cons(x,xs))
          if2(false(),x,y,xs) -> cons(y,del(x,xs))
          if2(true(),x,y,xs) -> xs
          max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
          max(cons(x,nil())) -> x
          max(nil()) -> 0()
          del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
          del#(x,nil()) -> c_2()
          empty#(cons(x,xs)) -> c_3()
          empty#(nil()) -> c_4()
          eq#(0(),0()) -> c_5()
          eq#(0(),s(y)) -> c_6()
          eq#(s(x),0()) -> c_7()
          eq#(s(x),s(y)) -> c_8(eq#(x,y))
          ge#(x,0()) -> c_9()
          ge#(0(),s(x)) -> c_10()
          ge#(s(x),s(y)) -> c_11(ge#(x,y))
          if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
          if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          if2#(false(),x,y,xs) -> c_14(del#(x,xs))
          if2#(true(),x,y,xs) -> c_15()
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
          if3#(true(),xs) -> c_17()
          max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
          max#(cons(x,nil())) -> c_19()
          max#(nil()) -> c_20()
          sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            del#(x,nil()) -> c_2()
            empty#(cons(x,xs)) -> c_3()
            empty#(nil()) -> c_4()
            eq#(0(),0()) -> c_5()
            eq#(0(),s(y)) -> c_6()
            eq#(s(x),0()) -> c_7()
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            ge#(x,0()) -> c_9()
            ge#(0(),s(x)) -> c_10()
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
            if2#(true(),x,y,xs) -> c_15()
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            if3#(true(),xs) -> c_17()
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            max#(cons(x,nil())) -> c_19()
            max#(nil()) -> c_20()
            sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} 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,3,4,5,6,7,9,10,15,17,19,20}
        by application of
          Pre({2,3,4,5,6,7,9,10,15,17,19,20}) = {1,8,11,12,13,14,16,18,21}.
        Here rules are labelled as follows:
          1: del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
          2: del#(x,nil()) -> c_2()
          3: empty#(cons(x,xs)) -> c_3()
          4: empty#(nil()) -> c_4()
          5: eq#(0(),0()) -> c_5()
          6: eq#(0(),s(y)) -> c_6()
          7: eq#(s(x),0()) -> c_7()
          8: eq#(s(x),s(y)) -> c_8(eq#(x,y))
          9: ge#(x,0()) -> c_9()
          10: ge#(0(),s(x)) -> c_10()
          11: ge#(s(x),s(y)) -> c_11(ge#(x,y))
          12: if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
          13: if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          14: if2#(false(),x,y,xs) -> c_14(del#(x,xs))
          15: if2#(true(),x,y,xs) -> c_15()
          16: if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
          17: if3#(true(),xs) -> c_17()
          18: max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
          19: max#(cons(x,nil())) -> c_19()
          20: max#(nil()) -> c_20()
          21: sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
        - Weak DPs:
            del#(x,nil()) -> c_2()
            empty#(cons(x,xs)) -> c_3()
            empty#(nil()) -> c_4()
            eq#(0(),0()) -> c_5()
            eq#(0(),s(y)) -> c_6()
            eq#(s(x),0()) -> c_7()
            ge#(x,0()) -> c_9()
            ge#(0(),s(x)) -> c_10()
            if2#(true(),x,y,xs) -> c_15()
            if3#(true(),xs) -> c_17()
            max#(cons(x,nil())) -> c_19()
            max#(nil()) -> c_20()
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
             -->_1 if2#(false(),x,y,xs) -> c_14(del#(x,xs)):6
             -->_2 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
             -->_1 if2#(true(),x,y,xs) -> c_15():18
             -->_2 eq#(s(x),0()) -> c_7():15
             -->_2 eq#(0(),s(y)) -> c_6():14
             -->_2 eq#(0(),0()) -> c_5():13
          
          2:S:eq#(s(x),s(y)) -> c_8(eq#(x,y))
             -->_1 eq#(s(x),0()) -> c_7():15
             -->_1 eq#(0(),s(y)) -> c_6():14
             -->_1 eq#(0(),0()) -> c_5():13
             -->_1 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          3:S:ge#(s(x),s(y)) -> c_11(ge#(x,y))
             -->_1 ge#(0(),s(x)) -> c_10():17
             -->_1 ge#(x,0()) -> c_9():16
             -->_1 ge#(s(x),s(y)) -> c_11(ge#(x,y)):3
          
          4:S:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
             -->_1 max#(cons(x,nil())) -> c_19():20
          
          5:S:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
             -->_1 max#(cons(x,nil())) -> c_19():20
          
          6:S:if2#(false(),x,y,xs) -> c_14(del#(x,xs))
             -->_1 del#(x,nil()) -> c_2():10
             -->_1 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
          
          7:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs)):9
             -->_3 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
             -->_3 max#(nil()) -> c_20():21
             -->_3 max#(cons(x,nil())) -> c_19():20
             -->_2 del#(x,nil()) -> c_2():10
             -->_2 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
          
          8:S:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_2 ge#(0(),s(x)) -> c_10():17
             -->_2 ge#(x,0()) -> c_9():16
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):5
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):4
             -->_2 ge#(s(x),s(y)) -> c_11(ge#(x,y)):3
          
          9:S:sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
             -->_1 if3#(true(),xs) -> c_17():19
             -->_2 empty#(nil()) -> c_4():12
             -->_2 empty#(cons(x,xs)) -> c_3():11
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs)):7
          
          10:W:del#(x,nil()) -> c_2()
             
          
          11:W:empty#(cons(x,xs)) -> c_3()
             
          
          12:W:empty#(nil()) -> c_4()
             
          
          13:W:eq#(0(),0()) -> c_5()
             
          
          14:W:eq#(0(),s(y)) -> c_6()
             
          
          15:W:eq#(s(x),0()) -> c_7()
             
          
          16:W:ge#(x,0()) -> c_9()
             
          
          17:W:ge#(0(),s(x)) -> c_10()
             
          
          18:W:if2#(true(),x,y,xs) -> c_15()
             
          
          19:W:if3#(true(),xs) -> c_17()
             
          
          20:W:max#(cons(x,nil())) -> c_19()
             
          
          21:W:max#(nil()) -> c_20()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          21: max#(nil()) -> c_20()
          11: empty#(cons(x,xs)) -> c_3()
          12: empty#(nil()) -> c_4()
          19: if3#(true(),xs) -> c_17()
          20: max#(cons(x,nil())) -> c_19()
          16: ge#(x,0()) -> c_9()
          17: ge#(0(),s(x)) -> c_10()
          18: if2#(true(),x,y,xs) -> c_15()
          13: eq#(0(),0()) -> c_5()
          14: eq#(0(),s(y)) -> c_6()
          15: eq#(s(x),0()) -> c_7()
          10: del#(x,nil()) -> c_2()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
             -->_1 if2#(false(),x,y,xs) -> c_14(del#(x,xs)):6
             -->_2 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          2:S:eq#(s(x),s(y)) -> c_8(eq#(x,y))
             -->_1 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          3:S:ge#(s(x),s(y)) -> c_11(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_11(ge#(x,y)):3
          
          4:S:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
          
          5:S:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
          
          6:S:if2#(false(),x,y,xs) -> c_14(del#(x,xs))
             -->_1 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
          
          7:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs)):9
             -->_3 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
             -->_2 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
          
          8:S:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):5
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):4
             -->_2 ge#(s(x),s(y)) -> c_11(ge#(x,y)):3
          
          9:S:sort#(xs) -> c_21(if3#(empty(xs),xs),empty#(xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs)):7
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          sort#(xs) -> c_21(if3#(empty(xs),xs))
* Step 6: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + 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:
              del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
              eq#(s(x),s(y)) -> c_8(eq#(x,y))
              if2#(false(),x,y,xs) -> c_14(del#(x,xs))
          - Weak DPs:
              ge#(s(x),s(y)) -> c_11(ge#(x,y))
              if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
              if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
              if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
              max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
              sort#(xs) -> c_21(if3#(empty(xs),xs))
          - Weak TRS:
              del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
              del(x,nil()) -> nil()
              empty(cons(x,xs)) -> false()
              empty(nil()) -> true()
              eq(0(),0()) -> true()
              eq(0(),s(y)) -> false()
              eq(s(x),0()) -> false()
              eq(s(x),s(y)) -> eq(x,y)
              ge(x,0()) -> true()
              ge(0(),s(x)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              if1(false(),x,y,xs) -> max(cons(y,xs))
              if1(true(),x,y,xs) -> max(cons(x,xs))
              if2(false(),x,y,xs) -> cons(y,del(x,xs))
              if2(true(),x,y,xs) -> xs
              max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
              max(cons(x,nil())) -> x
              max(nil()) -> 0()
          - Signature:
              {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
              ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
              ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
              ,sort#} and constructors {0,cons,false,nil,s,true}
        
        Problem (S)
          - Strict DPs:
              ge#(s(x),s(y)) -> c_11(ge#(x,y))
              if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
              if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
              if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
              max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
              sort#(xs) -> c_21(if3#(empty(xs),xs))
          - Weak DPs:
              del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
              eq#(s(x),s(y)) -> c_8(eq#(x,y))
              if2#(false(),x,y,xs) -> c_14(del#(x,xs))
          - Weak TRS:
              del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
              del(x,nil()) -> nil()
              empty(cons(x,xs)) -> false()
              empty(nil()) -> true()
              eq(0(),0()) -> true()
              eq(0(),s(y)) -> false()
              eq(s(x),0()) -> false()
              eq(s(x),s(y)) -> eq(x,y)
              ge(x,0()) -> true()
              ge(0(),s(x)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              if1(false(),x,y,xs) -> max(cons(y,xs))
              if1(true(),x,y,xs) -> max(cons(x,xs))
              if2(false(),x,y,xs) -> cons(y,del(x,xs))
              if2(true(),x,y,xs) -> xs
              max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
              max(cons(x,nil())) -> x
              max(nil()) -> 0()
          - Signature:
              {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
              ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
              ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
              ,sort#} and constructors {0,cons,false,nil,s,true}
** Step 6.a:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
        - Weak DPs:
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
             -->_1 if2#(false(),x,y,xs) -> c_14(del#(x,xs)):6
             -->_2 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          2:S:eq#(s(x),s(y)) -> c_8(eq#(x,y))
             -->_1 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          3:W:ge#(s(x),s(y)) -> c_11(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_11(ge#(x,y)):3
          
          4:W:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
          
          5:W:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
          
          6:S:if2#(false(),x,y,xs) -> c_14(del#(x,xs))
             -->_1 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
          
          7:W:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
             -->_2 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):9
             -->_3 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):8
          
          8:W:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_2 ge#(s(x),s(y)) -> c_11(ge#(x,y)):3
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):4
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):5
          
          9:W:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs)):7
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
          8: max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
          5: if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          3: ge#(s(x),s(y)) -> c_11(ge#(x,y))
** Step 6.a:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
        - Weak DPs:
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
             -->_1 if2#(false(),x,y,xs) -> c_14(del#(x,xs)):6
             -->_2 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          2:S:eq#(s(x),s(y)) -> c_8(eq#(x,y))
             -->_1 eq#(s(x),s(y)) -> c_8(eq#(x,y)):2
          
          6:S:if2#(false(),x,y,xs) -> c_14(del#(x,xs))
             -->_1 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
          
          7:W:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
             -->_2 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):1
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):9
          
          9:W:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs)):7
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs))
** Step 6.a:3: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
          eq#(s(x),s(y)) -> c_8(eq#(x,y))
          if2#(false(),x,y,xs) -> c_14(del#(x,xs))
      - Weak DPs:
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs))
          sort#(xs) -> c_21(if3#(empty(xs),xs))
      - Weak TRS:
          del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
          del(x,nil()) -> nil()
          empty(cons(x,xs)) -> false()
          empty(nil()) -> true()
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          ge(x,0()) -> true()
          ge(0(),s(x)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          if1(false(),x,y,xs) -> max(cons(y,xs))
          if1(true(),x,y,xs) -> max(cons(x,xs))
          if2(false(),x,y,xs) -> cons(y,del(x,xs))
          if2(true(),x,y,xs) -> xs
          max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
          max(cons(x,nil())) -> x
          max(nil()) -> 0()
      - Signature:
          {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
          ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
          ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
          ,sort#} and constructors {0,cons,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
** Step 6.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak DPs:
            del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
            eq#(s(x),s(y)) -> c_8(eq#(x,y))
            if2#(false(),x,y,xs) -> c_14(del#(x,xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ge#(s(x),s(y)) -> c_11(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_11(ge#(x,y)):1
          
          2:S:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):5
          
          3:S:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):5
          
          4:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
             -->_2 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):7
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):6
             -->_3 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):5
          
          5:S:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):3
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):2
             -->_2 ge#(s(x),s(y)) -> c_11(ge#(x,y)):1
          
          6:S:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs)):4
          
          7:W:del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
             -->_1 if2#(false(),x,y,xs) -> c_14(del#(x,xs)):9
             -->_2 eq#(s(x),s(y)) -> c_8(eq#(x,y)):8
          
          8:W:eq#(s(x),s(y)) -> c_8(eq#(x,y))
             -->_1 eq#(s(x),s(y)) -> c_8(eq#(x,y)):8
          
          9:W:if2#(false(),x,y,xs) -> c_14(del#(x,xs))
             -->_1 del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y)):7
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: del#(x,cons(y,xs)) -> c_1(if2#(eq(x,y),x,y,xs),eq#(x,y))
          9: if2#(false(),x,y,xs) -> c_14(del#(x,xs))
          8: eq#(s(x),s(y)) -> c_8(eq#(x,y))
** Step 6.b:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/3,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:ge#(s(x),s(y)) -> c_11(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_11(ge#(x,y)):1
          
          2:S:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):5
          
          3:S:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):5
          
          4:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs))
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):6
             -->_3 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):5
          
          5:S:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):3
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):2
             -->_2 ge#(s(x),s(y)) -> c_11(ge#(x,y)):1
          
          6:S:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),del#(max(xs),xs),max#(xs)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
** Step 6.b:3: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + 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:
              ge#(s(x),s(y)) -> c_11(ge#(x,y))
          - Weak DPs:
              if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
              if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
              if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
              max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
              sort#(xs) -> c_21(if3#(empty(xs),xs))
          - Weak TRS:
              del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
              del(x,nil()) -> nil()
              empty(cons(x,xs)) -> false()
              empty(nil()) -> true()
              eq(0(),0()) -> true()
              eq(0(),s(y)) -> false()
              eq(s(x),0()) -> false()
              eq(s(x),s(y)) -> eq(x,y)
              ge(x,0()) -> true()
              ge(0(),s(x)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              if1(false(),x,y,xs) -> max(cons(y,xs))
              if1(true(),x,y,xs) -> max(cons(x,xs))
              if2(false(),x,y,xs) -> cons(y,del(x,xs))
              if2(true(),x,y,xs) -> xs
              max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
              max(cons(x,nil())) -> x
              max(nil()) -> 0()
          - Signature:
              {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
              ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
              ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
              ,sort#} and constructors {0,cons,false,nil,s,true}
        
        Problem (S)
          - Strict DPs:
              if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
              if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
              if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
              max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
              sort#(xs) -> c_21(if3#(empty(xs),xs))
          - Weak DPs:
              ge#(s(x),s(y)) -> c_11(ge#(x,y))
          - Weak TRS:
              del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
              del(x,nil()) -> nil()
              empty(cons(x,xs)) -> false()
              empty(nil()) -> true()
              eq(0(),0()) -> true()
              eq(0(),s(y)) -> false()
              eq(s(x),0()) -> false()
              eq(s(x),s(y)) -> eq(x,y)
              ge(x,0()) -> true()
              ge(0(),s(x)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              if1(false(),x,y,xs) -> max(cons(y,xs))
              if1(true(),x,y,xs) -> max(cons(x,xs))
              if2(false(),x,y,xs) -> cons(y,del(x,xs))
              if2(true(),x,y,xs) -> xs
              max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
              max(cons(x,nil())) -> x
              max(nil()) -> 0()
          - Signature:
              {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
              ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
              ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
              ,sort#} and constructors {0,cons,false,nil,s,true}
*** Step 6.b:3.a:1: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ge#(s(x),s(y)) -> c_11(ge#(x,y))
      - Weak DPs:
          if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
          if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
          max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
          sort#(xs) -> c_21(if3#(empty(xs),xs))
      - Weak TRS:
          del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
          del(x,nil()) -> nil()
          empty(cons(x,xs)) -> false()
          empty(nil()) -> true()
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          ge(x,0()) -> true()
          ge(0(),s(x)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          if1(false(),x,y,xs) -> max(cons(y,xs))
          if1(true(),x,y,xs) -> max(cons(x,xs))
          if2(false(),x,y,xs) -> cons(y,del(x,xs))
          if2(true(),x,y,xs) -> xs
          max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
          max(cons(x,nil())) -> x
          max(nil()) -> 0()
      - Signature:
          {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
          ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
          ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
          ,sort#} and constructors {0,cons,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
*** Step 6.b:3.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak DPs:
            ge#(s(x),s(y)) -> c_11(ge#(x,y))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):4
          
          2:S:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):4
          
          3:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):5
             -->_2 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):4
          
          4:S:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_2 ge#(s(x),s(y)) -> c_11(ge#(x,y)):6
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):2
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):1
          
          5:S:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs)):3
          
          6:W:ge#(s(x),s(y)) -> c_11(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_11(ge#(x,y)):6
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          6: ge#(s(x),s(y)) -> c_11(ge#(x,y))
*** Step 6.b:3.b:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/2,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):4
          
          2:S:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):4
          
          3:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):5
             -->_2 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y)):4
          
          4:S:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs),ge#(x,y))
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):2
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):1
          
          5:S:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
*** Step 6.b:3.b:3: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + 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:
              if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
              if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
              max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
          - Weak DPs:
              if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
              sort#(xs) -> c_21(if3#(empty(xs),xs))
          - Weak TRS:
              del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
              del(x,nil()) -> nil()
              empty(cons(x,xs)) -> false()
              empty(nil()) -> true()
              eq(0(),0()) -> true()
              eq(0(),s(y)) -> false()
              eq(s(x),0()) -> false()
              eq(s(x),s(y)) -> eq(x,y)
              ge(x,0()) -> true()
              ge(0(),s(x)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              if1(false(),x,y,xs) -> max(cons(y,xs))
              if1(true(),x,y,xs) -> max(cons(x,xs))
              if2(false(),x,y,xs) -> cons(y,del(x,xs))
              if2(true(),x,y,xs) -> xs
              max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
              max(cons(x,nil())) -> x
              max(nil()) -> 0()
          - Signature:
              {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
              ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
              ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
              ,sort#} and constructors {0,cons,false,nil,s,true}
        
        Problem (S)
          - Strict DPs:
              if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
              sort#(xs) -> c_21(if3#(empty(xs),xs))
          - Weak DPs:
              if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
              if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
              max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
          - Weak TRS:
              del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
              del(x,nil()) -> nil()
              empty(cons(x,xs)) -> false()
              empty(nil()) -> true()
              eq(0(),0()) -> true()
              eq(0(),s(y)) -> false()
              eq(s(x),0()) -> false()
              eq(s(x),s(y)) -> eq(x,y)
              ge(x,0()) -> true()
              ge(0(),s(x)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              if1(false(),x,y,xs) -> max(cons(y,xs))
              if1(true(),x,y,xs) -> max(cons(x,xs))
              if2(false(),x,y,xs) -> cons(y,del(x,xs))
              if2(true(),x,y,xs) -> xs
              max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
              max(cons(x,nil())) -> x
              max(nil()) -> 0()
          - Signature:
              {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
              ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
              ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
              ,sort#} and constructors {0,cons,false,nil,s,true}
**** Step 6.b:3.b:3.a:1: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
          if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
      - Weak DPs:
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
          sort#(xs) -> c_21(if3#(empty(xs),xs))
      - Weak TRS:
          del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
          del(x,nil()) -> nil()
          empty(cons(x,xs)) -> false()
          empty(nil()) -> true()
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          ge(x,0()) -> true()
          ge(0(),s(x)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          if1(false(),x,y,xs) -> max(cons(y,xs))
          if1(true(),x,y,xs) -> max(cons(x,xs))
          if2(false(),x,y,xs) -> cons(y,del(x,xs))
          if2(true(),x,y,xs) -> xs
          max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
          max(cons(x,nil())) -> x
          max(nil()) -> 0()
      - Signature:
          {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
          ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
          ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
          ,sort#} and constructors {0,cons,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
**** Step 6.b:3.b:3.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak DPs:
            if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
            if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
            max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
             -->_2 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs)):5
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):2
          
          2:S:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs)):1
          
          3:W:if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs)):5
          
          4:W:if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
             -->_1 max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs)):5
          
          5:W:max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
             -->_1 if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs))):4
             -->_1 if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs))):3
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          5: max#(cons(x,cons(y,xs))) -> c_18(if1#(ge(x,y),x,y,xs))
          4: if1#(true(),x,y,xs) -> c_13(max#(cons(x,xs)))
          3: if1#(false(),x,y,xs) -> c_12(max#(cons(y,xs)))
**** Step 6.b:3.b:3.b:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
            sort#(xs) -> c_21(if3#(empty(xs),xs))
        - Weak TRS:
            del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
            del(x,nil()) -> nil()
            empty(cons(x,xs)) -> false()
            empty(nil()) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            ge(x,0()) -> true()
            ge(0(),s(x)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            if1(false(),x,y,xs) -> max(cons(y,xs))
            if1(true(),x,y,xs) -> max(cons(x,xs))
            if2(false(),x,y,xs) -> cons(y,del(x,xs))
            if2(true(),x,y,xs) -> xs
            max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
            max(cons(x,nil())) -> x
            max(nil()) -> 0()
        - Signature:
            {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
            ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
            ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/2,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
            ,sort#} and constructors {0,cons,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs))
             -->_1 sort#(xs) -> c_21(if3#(empty(xs),xs)):2
          
          2:S:sort#(xs) -> c_21(if3#(empty(xs),xs))
             -->_1 if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)),max#(xs)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)))
**** Step 6.b:3.b:3.b:3: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          if3#(false(),xs) -> c_16(sort#(del(max(xs),xs)))
          sort#(xs) -> c_21(if3#(empty(xs),xs))
      - Weak TRS:
          del(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
          del(x,nil()) -> nil()
          empty(cons(x,xs)) -> false()
          empty(nil()) -> true()
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          ge(x,0()) -> true()
          ge(0(),s(x)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          if1(false(),x,y,xs) -> max(cons(y,xs))
          if1(true(),x,y,xs) -> max(cons(x,xs))
          if2(false(),x,y,xs) -> cons(y,del(x,xs))
          if2(true(),x,y,xs) -> xs
          max(cons(x,cons(y,xs))) -> if1(ge(x,y),x,y,xs)
          max(cons(x,nil())) -> x
          max(nil()) -> 0()
      - Signature:
          {del/2,empty/1,eq/2,ge/2,if1/4,if2/4,if3/2,max/1,sort/1,del#/2,empty#/1,eq#/2,ge#/2,if1#/4,if2#/4,if3#/2
          ,max#/1,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
          ,c_9/0,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {del#,empty#,eq#,ge#,if1#,if2#,if3#,max#
          ,sort#} and constructors {0,cons,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE