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)))
            goal(xs) -> minsort(xs)
            minsort(Cons(x,xs)) -> appmin(x,xs,Cons(x,xs))
            minsort(Nil()) -> Nil()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            remove(x,Nil()) -> Nil()
            remove(x',Cons(x,xs)) -> remove[Ite][True][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][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2
            ,remove[Ite][True][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],goal,minsort,notEmpty
            ,remove,remove[Ite][True][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))
          goal#(xs) -> c_3(minsort#(xs))
          minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
          minsort#(Nil()) -> c_5()
          notEmpty#(Cons(x,xs)) -> c_6()
          notEmpty#(Nil()) -> c_7()
          remove#(x,Nil()) -> c_8()
          remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        Weak DPs
          !EQ#(0(),0()) -> c_10()
          !EQ#(0(),S(y)) -> c_11()
          !EQ#(S(x),0()) -> c_12()
          !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
          <#(x,0()) -> c_14()
          <#(0(),S(y)) -> c_15()
          <#(S(x),S(y)) -> c_16(<#(x,y))
          appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
          appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
          remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
          remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
        
        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))
            goal#(xs) -> c_3(minsort#(xs))
            minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
            minsort#(Nil()) -> c_5()
            notEmpty#(Cons(x,xs)) -> c_6()
            notEmpty#(Nil()) -> c_7()
            remove#(x,Nil()) -> c_8()
            remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            !EQ#(0(),0()) -> c_10()
            !EQ#(0(),S(y)) -> c_11()
            !EQ#(S(x),0()) -> c_12()
            !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
            <#(x,0()) -> c_14()
            <#(0(),S(y)) -> c_15()
            <#(S(x),S(y)) -> c_16(<#(x,y))
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
            remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
            remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
        - 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')
            goal(xs) -> minsort(xs)
            minsort(Cons(x,xs)) -> appmin(x,xs,Cons(x,xs))
            minsort(Nil()) -> Nil()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            remove(x,Nil()) -> Nil()
            remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2,remove[Ite][True][Ite]/3
            ,!EQ#/2,<#/2,appmin#/3,appmin[Ite][True][Ite]#/4,goal#/1,minsort#/1,notEmpty#/1,remove#/2
            ,remove[Ite][True][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/1,c_5/0,c_6/0,c_7/0
            ,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,goal#,minsort#
            ,notEmpty#,remove#,remove[Ite][True][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,Nil()) -> Nil()
          remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
          remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
          remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
          !EQ#(0(),0()) -> c_10()
          !EQ#(0(),S(y)) -> c_11()
          !EQ#(S(x),0()) -> c_12()
          !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
          <#(x,0()) -> c_14()
          <#(0(),S(y)) -> c_15()
          <#(S(x),S(y)) -> c_16(<#(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_17(appmin#(min,xs,xs'))
          appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
          goal#(xs) -> c_3(minsort#(xs))
          minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
          minsort#(Nil()) -> c_5()
          notEmpty#(Cons(x,xs)) -> c_6()
          notEmpty#(Nil()) -> c_7()
          remove#(x,Nil()) -> c_8()
          remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
          remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
          remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
* 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))
            goal#(xs) -> c_3(minsort#(xs))
            minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
            minsort#(Nil()) -> c_5()
            notEmpty#(Cons(x,xs)) -> c_6()
            notEmpty#(Nil()) -> c_7()
            remove#(x,Nil()) -> c_8()
            remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            !EQ#(0(),0()) -> c_10()
            !EQ#(0(),S(y)) -> c_11()
            !EQ#(S(x),0()) -> c_12()
            !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
            <#(x,0()) -> c_14()
            <#(0(),S(y)) -> c_15()
            <#(S(x),S(y)) -> c_16(<#(x,y))
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
            remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
            remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
        - 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,Nil()) -> Nil()
            remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2,remove[Ite][True][Ite]/3
            ,!EQ#/2,<#/2,appmin#/3,appmin[Ite][True][Ite]#/4,goal#/1,minsort#/1,notEmpty#/1,remove#/2
            ,remove[Ite][True][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/1,c_5/0,c_6/0,c_7/0
            ,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,goal#,minsort#
            ,notEmpty#,remove#,remove[Ite][True][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
          {5,6,7}
        by application of
          Pre({5,6,7}) = {2,3}.
        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: goal#(xs) -> c_3(minsort#(xs))
          4: minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
          5: minsort#(Nil()) -> c_5()
          6: notEmpty#(Cons(x,xs)) -> c_6()
          7: notEmpty#(Nil()) -> c_7()
          8: remove#(x,Nil()) -> c_8()
          9: remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
          10: !EQ#(0(),0()) -> c_10()
          11: !EQ#(0(),S(y)) -> c_11()
          12: !EQ#(S(x),0()) -> c_12()
          13: !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
          14: <#(x,0()) -> c_14()
          15: <#(0(),S(y)) -> c_15()
          16: <#(S(x),S(y)) -> c_16(<#(x,y))
          17: appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
          18: appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
          19: remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
          20: remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
* 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))
            goal#(xs) -> c_3(minsort#(xs))
            minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
            remove#(x,Nil()) -> c_8()
            remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            !EQ#(0(),0()) -> c_10()
            !EQ#(0(),S(y)) -> c_11()
            !EQ#(S(x),0()) -> c_12()
            !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
            <#(x,0()) -> c_14()
            <#(0(),S(y)) -> c_15()
            <#(S(x),S(y)) -> c_16(<#(x,y))
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
            minsort#(Nil()) -> c_5()
            notEmpty#(Cons(x,xs)) -> c_6()
            notEmpty#(Nil()) -> c_7()
            remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
            remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
        - 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,Nil()) -> Nil()
            remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2,remove[Ite][True][Ite]/3
            ,!EQ#/2,<#/2,appmin#/3,appmin[Ite][True][Ite]#/4,goal#/1,minsort#/1,notEmpty#/1,remove#/2
            ,remove[Ite][True][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/1,c_5/0,c_6/0,c_7/0
            ,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,goal#,minsort#
            ,notEmpty#,remove#,remove[Ite][True][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_18(appmin#(x,xs,xs')):15
             -->_1 appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs')):14
             -->_2 <#(S(x),S(y)) -> c_16(<#(x,y)):13
             -->_2 <#(0(),S(y)) -> c_15():12
             -->_2 <#(x,0()) -> c_14():11
          
          2:S:appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
             -->_2 remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):6
             -->_1 minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs))):4
             -->_1 minsort#(Nil()) -> c_5():16
             -->_2 remove#(x,Nil()) -> c_8():5
          
          3:S:goal#(xs) -> c_3(minsort#(xs))
             -->_1 minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs))):4
             -->_1 minsort#(Nil()) -> c_5():16
          
          4:S:minsort#(Cons(x,xs)) -> c_4(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
          
          5:S:remove#(x,Nil()) -> c_8()
             
          
          6:S:remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
             -->_1 remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs)):19
             -->_2 !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y)):10
             -->_1 remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20():20
             -->_2 !EQ#(S(x),0()) -> c_12():9
             -->_2 !EQ#(0(),S(y)) -> c_11():8
             -->_2 !EQ#(0(),0()) -> c_10():7
          
          7:W:!EQ#(0(),0()) -> c_10()
             
          
          8:W:!EQ#(0(),S(y)) -> c_11()
             
          
          9:W:!EQ#(S(x),0()) -> c_12()
             
          
          10:W:!EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
             -->_1 !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y)):10
             -->_1 !EQ#(S(x),0()) -> c_12():9
             -->_1 !EQ#(0(),S(y)) -> c_11():8
             -->_1 !EQ#(0(),0()) -> c_10():7
          
          11:W:<#(x,0()) -> c_14()
             
          
          12:W:<#(0(),S(y)) -> c_15()
             
          
          13:W:<#(S(x),S(y)) -> c_16(<#(x,y))
             -->_1 <#(S(x),S(y)) -> c_16(<#(x,y)):13
             -->_1 <#(0(),S(y)) -> c_15():12
             -->_1 <#(x,0()) -> c_14():11
          
          14:W:appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(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
          
          15:W:appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(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
          
          16:W:minsort#(Nil()) -> c_5()
             
          
          17:W:notEmpty#(Cons(x,xs)) -> c_6()
             
          
          18:W:notEmpty#(Nil()) -> c_7()
             
          
          19:W:remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
             -->_1 remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):6
             -->_1 remove#(x,Nil()) -> c_8():5
          
          20:W:remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          18: notEmpty#(Nil()) -> c_7()
          17: notEmpty#(Cons(x,xs)) -> c_6()
          13: <#(S(x),S(y)) -> c_16(<#(x,y))
          11: <#(x,0()) -> c_14()
          12: <#(0(),S(y)) -> c_15()
          16: minsort#(Nil()) -> c_5()
          20: remove[Ite][True][Ite]#(True(),x',Cons(x,xs)) -> c_20()
          10: !EQ#(S(x),S(y)) -> c_13(!EQ#(x,y))
          7: !EQ#(0(),0()) -> c_10()
          8: !EQ#(0(),S(y)) -> c_11()
          9: !EQ#(S(x),0()) -> c_12()
* 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))
            goal#(xs) -> c_3(minsort#(xs))
            minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
            remove#(x,Nil()) -> c_8()
            remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
        - Weak DPs:
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
            remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(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,Nil()) -> Nil()
            remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2,remove[Ite][True][Ite]/3
            ,!EQ#/2,<#/2,appmin#/3,appmin[Ite][True][Ite]#/4,goal#/1,minsort#/1,notEmpty#/1,remove#/2
            ,remove[Ite][True][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/1,c_5/0,c_6/0,c_7/0
            ,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,goal#,minsort#
            ,notEmpty#,remove#,remove[Ite][True][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_18(appmin#(x,xs,xs')):15
             -->_1 appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs')):14
          
          2:S:appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
             -->_2 remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):6
             -->_1 minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs))):4
             -->_2 remove#(x,Nil()) -> c_8():5
          
          3:S:goal#(xs) -> c_3(minsort#(xs))
             -->_1 minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs))):4
          
          4:S:minsort#(Cons(x,xs)) -> c_4(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
          
          5:S:remove#(x,Nil()) -> c_8()
             
          
          6:S:remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x))
             -->_1 remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs)):19
          
          14:W:appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(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
          
          15:W:appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(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
          
          19:W:remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
             -->_1 remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)),!EQ#(x',x)):6
             -->_1 remove#(x,Nil()) -> c_8():5
          
        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_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)))
* Step 6: RemoveHeads 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))
            goal#(xs) -> c_3(minsort#(xs))
            minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs)))
            remove#(x,Nil()) -> c_8()
            remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)))
        - Weak DPs:
            appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
            appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
            remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(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,Nil()) -> Nil()
            remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
            remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
            remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
        - Signature:
            {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2,remove[Ite][True][Ite]/3
            ,!EQ#/2,<#/2,appmin#/3,appmin[Ite][True][Ite]#/4,goal#/1,minsort#/1,notEmpty#/1,remove#/2
            ,remove[Ite][True][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/1,c_5/0,c_6/0,c_7/0
            ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,goal#,minsort#
            ,notEmpty#,remove#,remove[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True}
    + Applied Processor:
        RemoveHeads
    + 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'))
           -->_1 appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs')):8
           -->_1 appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs')):7
        
        2:S:appmin#(min,Nil(),xs) -> c_2(minsort#(remove(min,xs)),remove#(min,xs))
           -->_2 remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs))):6
           -->_1 minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs))):4
           -->_2 remove#(x,Nil()) -> c_8():5
        
        3:S:goal#(xs) -> c_3(minsort#(xs))
           -->_1 minsort#(Cons(x,xs)) -> c_4(appmin#(x,xs,Cons(x,xs))):4
        
        4:S:minsort#(Cons(x,xs)) -> c_4(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')):1
        
        5:S:remove#(x,Nil()) -> c_8()
           
        
        6:S:remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)))
           -->_1 remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs)):9
        
        7:W:appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(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')):1
        
        8:W:appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(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')):1
        
        9:W:remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(remove#(x',xs))
           -->_1 remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs))):6
           -->_1 remove#(x,Nil()) -> c_8():5
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(3,goal#(xs) -> c_3(minsort#(xs)))]
* Step 7: 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_4(appmin#(x,xs,Cons(x,xs)))
          remove#(x,Nil()) -> c_8()
          remove#(x',Cons(x,xs)) -> c_9(remove[Ite][True][Ite]#(!EQ(x',x),x',Cons(x,xs)))
      - Weak DPs:
          appmin[Ite][True][Ite]#(False(),min,Cons(x,xs),xs') -> c_17(appmin#(min,xs,xs'))
          appmin[Ite][True][Ite]#(True(),min,Cons(x,xs),xs') -> c_18(appmin#(x,xs,xs'))
          remove[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_19(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,Nil()) -> Nil()
          remove(x',Cons(x,xs)) -> remove[Ite][True][Ite](!EQ(x',x),x',Cons(x,xs))
          remove[Ite][True][Ite](False(),x',Cons(x,xs)) -> Cons(x,remove(x',xs))
          remove[Ite][True][Ite](True(),x',Cons(x,xs)) -> xs
      - Signature:
          {!EQ/2,</2,appmin/3,appmin[Ite][True][Ite]/4,goal/1,minsort/1,notEmpty/1,remove/2,remove[Ite][True][Ite]/3
          ,!EQ#/2,<#/2,appmin#/3,appmin[Ite][True][Ite]#/4,goal#/1,minsort#/1,notEmpty#/1,remove#/2
          ,remove[Ite][True][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/1,c_5/0,c_6/0,c_7/0
          ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1,c_19/1,c_20/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {!EQ#,<#,appmin#,appmin[Ite][True][Ite]#,goal#,minsort#
          ,notEmpty#,remove#,remove[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE