MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            appmin(min,Cons(x,xs),xs') -> appmin[Ite][True][Ite](<(x,min),min,Cons(x,xs),xs')
            appmin(min,Nil(),xs) -> Cons(min,minsort(remove(min,xs)))
            minsort(Cons(x,xs)) -> appmin(x,xs,Cons(x,xs))
            minsort(Nil()) -> Nil()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            appmin[Ite][True][Ite](False(),min,Cons(x,xs),xs') -> appmin(min,xs,xs')
            appmin[Ite][True][Ite](True(),min,Cons(x,xs),xs') -> appmin(x,xs,xs')
            remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,minsort/1,notEmpty/1,remove/2,remove[Ite]/3} / {0/0,Cons/2
            ,False/0,Nil/0,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,<,appmin,appmin[Ite][True][Ite],minsort,notEmpty
            ,remove,remove[Ite]} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
          appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
          minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
          minsort#(Nil()) -> c_4()
          notEmpty#(Cons(x,xs)) -> c_5()
          notEmpty#(Nil()) -> c_6()
          remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        Weak DPs
          !EQ#(0(),0()) -> c_8()
          !EQ#(0(),S(y)) -> c_9()
          !EQ#(S(x),0()) -> c_10()
          !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
          <#(x,0()) -> c_12()
          <#(0(),S(y)) -> c_13()
          <#(S(x),S(y)) -> c_14(<#(x,y))
          appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
          appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
          remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
          remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
            appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
            minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
            minsort#(Nil()) -> c_4()
            notEmpty#(Cons(x,xs)) -> c_5()
            notEmpty#(Nil()) -> c_6()
            remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            !EQ#(0(),0()) -> c_8()
            !EQ#(0(),S(y)) -> c_9()
            !EQ#(S(x),0()) -> c_10()
            !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
            <#(x,0()) -> c_12()
            <#(0(),S(y)) -> c_13()
            <#(S(x),S(y)) -> c_14(<#(x,y))
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
            remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
            remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            appmin(min,Cons(x,xs),xs') -> appmin[Ite][True][Ite](<(x,min),min,Cons(x,xs),xs')
            appmin(min,Nil(),xs) -> Cons(min,minsort(remove(min,xs)))
            appmin[Ite][True][Ite](False(),min,Cons(x,xs),xs') -> appmin(min,xs,xs')
            appmin[Ite][True][Ite](True(),min,Cons(x,xs),xs') -> appmin(x,xs,xs')
            minsort(Cons(x,xs)) -> appmin(x,xs,Cons(x,xs))
            minsort(Nil()) -> Nil()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,minsort/1,notEmpty/1,remove/2,remove[Ite]/3,!EQ#/2,<#/2
            ,appmin#/3,appmin[Ite][True][Ite]#/4,minsort#/1,notEmpty#/1,remove#/2,remove[Ite]#/3} / {0/0,Cons/2,False/0
            ,Nil/0,S/1,True/0,c_1/2,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1
            ,c_15/1,c_16/1,c_17/1,c_18/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,minsort#
            ,notEmpty#,remove#,remove[Ite]#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          !EQ(0(),0()) -> True()
          !EQ(0(),S(y)) -> False()
          !EQ(S(x),0()) -> False()
          !EQ(S(x),S(y)) -> !EQ(x,y)
          <(x,0()) -> False()
          <(0(),S(y)) -> True()
          <(S(x),S(y)) -> <(x,y)
          remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
          remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
          remove[Ite](True(),x',Cons(x,xs)) -> xs
          !EQ#(0(),0()) -> c_8()
          !EQ#(0(),S(y)) -> c_9()
          !EQ#(S(x),0()) -> c_10()
          !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
          <#(x,0()) -> c_12()
          <#(0(),S(y)) -> c_13()
          <#(S(x),S(y)) -> c_14(<#(x,y))
          appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
          appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
          appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
          appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
          minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
          minsort#(Nil()) -> c_4()
          notEmpty#(Cons(x,xs)) -> c_5()
          notEmpty#(Nil()) -> c_6()
          remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
          remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
          remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
            appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
            minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
            minsort#(Nil()) -> c_4()
            notEmpty#(Cons(x,xs)) -> c_5()
            notEmpty#(Nil()) -> c_6()
            remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            !EQ#(0(),0()) -> c_8()
            !EQ#(0(),S(y)) -> c_9()
            !EQ#(S(x),0()) -> c_10()
            !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
            <#(x,0()) -> c_12()
            <#(0(),S(y)) -> c_13()
            <#(S(x),S(y)) -> c_14(<#(x,y))
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
            remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
            remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,minsort/1,notEmpty/1,remove/2,remove[Ite]/3,!EQ#/2,<#/2
            ,appmin#/3,appmin[Ite][True][Ite]#/4,minsort#/1,notEmpty#/1,remove#/2,remove[Ite]#/3} / {0/0,Cons/2,False/0
            ,Nil/0,S/1,True/0,c_1/2,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1
            ,c_15/1,c_16/1,c_17/1,c_18/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,minsort#
            ,notEmpty#,remove#,remove[Ite]#} 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
          {4,5,6}
        by application of
          Pre({4,5,6}) = {2}.
        Here rules are labelled as follows:
          1: appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
          2: appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
          3: minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
          4: minsort#(Nil()) -> c_4()
          5: notEmpty#(Cons(x,xs)) -> c_5()
          6: notEmpty#(Nil()) -> c_6()
          7: remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
          8: !EQ#(0(),0()) -> c_8()
          9: !EQ#(0(),S(y)) -> c_9()
          10: !EQ#(S(x),0()) -> c_10()
          11: !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
          12: <#(x,0()) -> c_12()
          13: <#(0(),S(y)) -> c_13()
          14: <#(S(x),S(y)) -> c_14(<#(x,y))
          15: appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
          16: appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
          17: remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
          18: remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
            appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
            minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
            remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            !EQ#(0(),0()) -> c_8()
            !EQ#(0(),S(y)) -> c_9()
            !EQ#(S(x),0()) -> c_10()
            !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
            <#(x,0()) -> c_12()
            <#(0(),S(y)) -> c_13()
            <#(S(x),S(y)) -> c_14(<#(x,y))
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
            minsort#(Nil()) -> c_4()
            notEmpty#(Cons(x,xs)) -> c_5()
            notEmpty#(Nil()) -> c_6()
            remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
            remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,minsort/1,notEmpty/1,remove/2,remove[Ite]/3,!EQ#/2,<#/2
            ,appmin#/3,appmin[Ite][True][Ite]#/4,minsort#/1,notEmpty#/1,remove#/2,remove[Ite]#/3} / {0/0,Cons/2,False/0
            ,Nil/0,S/1,True/0,c_1/2,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1
            ,c_15/1,c_16/1,c_17/1,c_18/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,minsort#
            ,notEmpty#,remove#,remove[Ite]#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
             -->_1 appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs')):13
             -->_1 appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs')):12
             -->_2 <#(S(x),S(y)) -> c_14(<#(x,y)):11
             -->_2 <#(0(),S(y)) -> c_13():10
             -->_2 <#(x,0()) -> c_12():9
          
          2:S:appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
             -->_2 remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):4
             -->_1 minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs))):3
             -->_1 minsort#(Nil()) -> c_4():14
          
          3:S:minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
             -->_1 appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs)):2
             -->_1 appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min)):1
          
          4:S:remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
             -->_1 remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs)):17
             -->_2 !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)):8
             -->_1 remove[Ite]#(True(),x',Cons(x,xs)) -> c_18():18
             -->_2 !EQ#(S(x),0()) -> c_10():7
             -->_2 !EQ#(0(),S(y)) -> c_9():6
             -->_2 !EQ#(0(),0()) -> c_8():5
          
          5:W:!EQ#(0(),0()) -> c_8()
             
          
          6:W:!EQ#(0(),S(y)) -> c_9()
             
          
          7:W:!EQ#(S(x),0()) -> c_10()
             
          
          8:W:!EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
             -->_1 !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)):8
             -->_1 !EQ#(S(x),0()) -> c_10():7
             -->_1 !EQ#(0(),S(y)) -> c_9():6
             -->_1 !EQ#(0(),0()) -> c_8():5
          
          9:W:<#(x,0()) -> c_12()
             
          
          10:W:<#(0(),S(y)) -> c_13()
             
          
          11:W:<#(S(x),S(y)) -> c_14(<#(x,y))
             -->_1 <#(S(x),S(y)) -> c_14(<#(x,y)):11
             -->_1 <#(0(),S(y)) -> c_13():10
             -->_1 <#(x,0()) -> c_12():9
          
          12:W:appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
             -->_1 appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs)):2
             -->_1 appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min)):1
          
          13:W:appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
             -->_1 appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs)):2
             -->_1 appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min)):1
          
          14:W:minsort#(Nil()) -> c_4()
             
          
          15:W:notEmpty#(Cons(x,xs)) -> c_5()
             
          
          16:W:notEmpty#(Nil()) -> c_6()
             
          
          17:W:remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
             -->_1 remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):4
          
          18:W:remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          16: notEmpty#(Nil()) -> c_6()
          15: notEmpty#(Cons(x,xs)) -> c_5()
          11: <#(S(x),S(y)) -> c_14(<#(x,y))
          9: <#(x,0()) -> c_12()
          10: <#(0(),S(y)) -> c_13()
          14: minsort#(Nil()) -> c_4()
          18: remove[Ite]#(True(),x',Cons(x,xs)) -> c_18()
          8: !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y))
          5: !EQ#(0(),0()) -> c_8()
          6: !EQ#(0(),S(y)) -> c_9()
          7: !EQ#(S(x),0()) -> c_10()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
            appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
            minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
            remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
            remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,minsort/1,notEmpty/1,remove/2,remove[Ite]/3,!EQ#/2,<#/2
            ,appmin#/3,appmin[Ite][True][Ite]#/4,minsort#/1,notEmpty#/1,remove#/2,remove[Ite]#/3} / {0/0,Cons/2,False/0
            ,Nil/0,S/1,True/0,c_1/2,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1
            ,c_15/1,c_16/1,c_17/1,c_18/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,minsort#
            ,notEmpty#,remove#,remove[Ite]#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min))
             -->_1 appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs')):13
             -->_1 appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs')):12
          
          2:S:appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
             -->_2 remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):4
             -->_1 minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs))):3
          
          3:S:minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
             -->_1 appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs)):2
             -->_1 appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min)):1
          
          4:S:remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
             -->_1 remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs)):17
          
          12:W:appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
             -->_1 appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs)):2
             -->_1 appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min)):1
          
          13:W:appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
             -->_1 appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs)):2
             -->_1 appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'),<#(x,min)):1
          
          17:W:remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
             -->_1 remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'))
          remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)))
* Step 6: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          appmin#(min,Cons(x,xs),xs') -> c_1(appmin[Ite][True][Ite]#(<(x,min),min,Cons(x,xs),xs'))
          appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
          minsort#(Cons(x,xs)) -> c_3(appmin#(x,xs,Cons(x,xs)))
          remove#(x',Cons(x,xs)) -> c_7(remove[Ite]#(!EQ(x',x),x',Cons(x,xs)))
      - Weak DPs:
          appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_15(appmin#(min,xs,xs'))
          appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_16(appmin#(x,xs,xs'))
          remove[Ite]#(False(),x',Cons(x,xs)) -> c_17(remove#(x',xs))
      - Weak TRS:
          !EQ(0(),0()) -> True()
          !EQ(0(),S(y)) -> False()
          !EQ(S(x),0()) -> False()
          !EQ(S(x),S(y)) -> !EQ(x,y)
          <(x,0()) -> False()
          <(0(),S(y)) -> True()
          <(S(x),S(y)) -> <(x,y)
          remove(x',Cons(x,xs)) -> remove[Ite](!EQ(x',x),x',Cons(x,xs))
          remove[Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
          remove[Ite](True(),x',Cons(x,xs)) -> xs
      - Signature:
          {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,minsort/1,notEmpty/1,remove/2,remove[Ite]/3,!EQ#/2,<#/2
          ,appmin#/3,appmin[Ite][True][Ite]#/4,minsort#/1,notEmpty#/1,remove#/2,remove[Ite]#/3} / {0/0,Cons/2,False/0
          ,Nil/0,S/1,True/0,c_1/1,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1
          ,c_15/1,c_16/1,c_17/1,c_18/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,minsort#
          ,notEmpty#,remove#,remove[Ite]#} and constructors {0,Cons,False,Nil,S,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE