MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            div(x,y) -> ify(ge(y,s(0())),x,y)
            ge(0(),0()) -> true()
            ge(0(),s(0())) -> false()
            ge(0(),s(s(x))) -> ge(0(),s(x))
            ge(s(x),0()) -> ge(x,0())
            ge(s(x),s(y)) -> ge(x,y)
            if(false(),x,y) -> 0()
            if(true(),x,y) -> s(div(minus(x,y),y))
            ify(false(),x,y) -> divByZeroError()
            ify(true(),x,y) -> if(ge(x,y),x,y)
            minus(0(),0()) -> 0()
            minus(0(),s(x)) -> minus(0(),x)
            minus(s(x),0()) -> s(minus(x,0()))
            minus(s(x),s(y)) -> minus(x,y)
            plus(0(),0()) -> 0()
            plus(0(),s(x)) -> s(plus(0(),x))
            plus(s(x),y) -> s(plus(x,y))
        - Signature:
            {div/2,ge/2,if/3,ify/3,minus/2,plus/2} / {0/0,divByZeroError/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div,ge,if,ify,minus,plus} and constructors {0
            ,divByZeroError,false,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
          ge#(0(),0()) -> c_2()
          ge#(0(),s(0())) -> c_3()
          ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
          ge#(s(x),0()) -> c_5(ge#(x,0()))
          ge#(s(x),s(y)) -> c_6(ge#(x,y))
          if#(false(),x,y) -> c_7()
          if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
          ify#(false(),x,y) -> c_9()
          ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
          minus#(0(),0()) -> c_11()
          minus#(0(),s(x)) -> c_12(minus#(0(),x))
          minus#(s(x),0()) -> c_13(minus#(x,0()))
          minus#(s(x),s(y)) -> c_14(minus#(x,y))
          plus#(0(),0()) -> c_15()
          plus#(0(),s(x)) -> c_16(plus#(0(),x))
          plus#(s(x),y) -> c_17(plus#(x,y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
            ge#(0(),0()) -> c_2()
            ge#(0(),s(0())) -> c_3()
            ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
            ge#(s(x),0()) -> c_5(ge#(x,0()))
            ge#(s(x),s(y)) -> c_6(ge#(x,y))
            if#(false(),x,y) -> c_7()
            if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
            ify#(false(),x,y) -> c_9()
            ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
            minus#(0(),0()) -> c_11()
            minus#(0(),s(x)) -> c_12(minus#(0(),x))
            minus#(s(x),0()) -> c_13(minus#(x,0()))
            minus#(s(x),s(y)) -> c_14(minus#(x,y))
            plus#(0(),0()) -> c_15()
            plus#(0(),s(x)) -> c_16(plus#(0(),x))
            plus#(s(x),y) -> c_17(plus#(x,y))
        - Weak TRS:
            div(x,y) -> ify(ge(y,s(0())),x,y)
            ge(0(),0()) -> true()
            ge(0(),s(0())) -> false()
            ge(0(),s(s(x))) -> ge(0(),s(x))
            ge(s(x),0()) -> ge(x,0())
            ge(s(x),s(y)) -> ge(x,y)
            if(false(),x,y) -> 0()
            if(true(),x,y) -> s(div(minus(x,y),y))
            ify(false(),x,y) -> divByZeroError()
            ify(true(),x,y) -> if(ge(x,y),x,y)
            minus(0(),0()) -> 0()
            minus(0(),s(x)) -> minus(0(),x)
            minus(s(x),0()) -> s(minus(x,0()))
            minus(s(x),s(y)) -> minus(x,y)
            plus(0(),0()) -> 0()
            plus(0(),s(x)) -> s(plus(0(),x))
            plus(s(x),y) -> s(plus(x,y))
        - Signature:
            {div/2,ge/2,if/3,ify/3,minus/2,plus/2,div#/2,ge#/2,if#/3,ify#/3,minus#/2,plus#/2} / {0/0,divByZeroError/0
            ,false/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/1,c_13/1,c_14/1
            ,c_15/0,c_16/1,c_17/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,ge#,if#,ify#,minus#,plus#} and constructors {0
            ,divByZeroError,false,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          ge(0(),0()) -> true()
          ge(0(),s(0())) -> false()
          ge(0(),s(s(x))) -> ge(0(),s(x))
          ge(s(x),0()) -> ge(x,0())
          ge(s(x),s(y)) -> ge(x,y)
          minus(0(),0()) -> 0()
          minus(0(),s(x)) -> minus(0(),x)
          minus(s(x),0()) -> s(minus(x,0()))
          minus(s(x),s(y)) -> minus(x,y)
          div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
          ge#(0(),0()) -> c_2()
          ge#(0(),s(0())) -> c_3()
          ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
          ge#(s(x),0()) -> c_5(ge#(x,0()))
          ge#(s(x),s(y)) -> c_6(ge#(x,y))
          if#(false(),x,y) -> c_7()
          if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
          ify#(false(),x,y) -> c_9()
          ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
          minus#(0(),0()) -> c_11()
          minus#(0(),s(x)) -> c_12(minus#(0(),x))
          minus#(s(x),0()) -> c_13(minus#(x,0()))
          minus#(s(x),s(y)) -> c_14(minus#(x,y))
          plus#(0(),0()) -> c_15()
          plus#(0(),s(x)) -> c_16(plus#(0(),x))
          plus#(s(x),y) -> c_17(plus#(x,y))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
            ge#(0(),0()) -> c_2()
            ge#(0(),s(0())) -> c_3()
            ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
            ge#(s(x),0()) -> c_5(ge#(x,0()))
            ge#(s(x),s(y)) -> c_6(ge#(x,y))
            if#(false(),x,y) -> c_7()
            if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
            ify#(false(),x,y) -> c_9()
            ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
            minus#(0(),0()) -> c_11()
            minus#(0(),s(x)) -> c_12(minus#(0(),x))
            minus#(s(x),0()) -> c_13(minus#(x,0()))
            minus#(s(x),s(y)) -> c_14(minus#(x,y))
            plus#(0(),0()) -> c_15()
            plus#(0(),s(x)) -> c_16(plus#(0(),x))
            plus#(s(x),y) -> c_17(plus#(x,y))
        - Weak TRS:
            ge(0(),0()) -> true()
            ge(0(),s(0())) -> false()
            ge(0(),s(s(x))) -> ge(0(),s(x))
            ge(s(x),0()) -> ge(x,0())
            ge(s(x),s(y)) -> ge(x,y)
            minus(0(),0()) -> 0()
            minus(0(),s(x)) -> minus(0(),x)
            minus(s(x),0()) -> s(minus(x,0()))
            minus(s(x),s(y)) -> minus(x,y)
        - Signature:
            {div/2,ge/2,if/3,ify/3,minus/2,plus/2,div#/2,ge#/2,if#/3,ify#/3,minus#/2,plus#/2} / {0/0,divByZeroError/0
            ,false/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/1,c_13/1,c_14/1
            ,c_15/0,c_16/1,c_17/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,ge#,if#,ify#,minus#,plus#} and constructors {0
            ,divByZeroError,false,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,3,7,9,11,15}
        by application of
          Pre({2,3,7,9,11,15}) = {1,4,5,6,8,10,12,13,14,16,17}.
        Here rules are labelled as follows:
          1: div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
          2: ge#(0(),0()) -> c_2()
          3: ge#(0(),s(0())) -> c_3()
          4: ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
          5: ge#(s(x),0()) -> c_5(ge#(x,0()))
          6: ge#(s(x),s(y)) -> c_6(ge#(x,y))
          7: if#(false(),x,y) -> c_7()
          8: if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
          9: ify#(false(),x,y) -> c_9()
          10: ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
          11: minus#(0(),0()) -> c_11()
          12: minus#(0(),s(x)) -> c_12(minus#(0(),x))
          13: minus#(s(x),0()) -> c_13(minus#(x,0()))
          14: minus#(s(x),s(y)) -> c_14(minus#(x,y))
          15: plus#(0(),0()) -> c_15()
          16: plus#(0(),s(x)) -> c_16(plus#(0(),x))
          17: plus#(s(x),y) -> c_17(plus#(x,y))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
            ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
            ge#(s(x),0()) -> c_5(ge#(x,0()))
            ge#(s(x),s(y)) -> c_6(ge#(x,y))
            if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
            ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
            minus#(0(),s(x)) -> c_12(minus#(0(),x))
            minus#(s(x),0()) -> c_13(minus#(x,0()))
            minus#(s(x),s(y)) -> c_14(minus#(x,y))
            plus#(0(),s(x)) -> c_16(plus#(0(),x))
            plus#(s(x),y) -> c_17(plus#(x,y))
        - Weak DPs:
            ge#(0(),0()) -> c_2()
            ge#(0(),s(0())) -> c_3()
            if#(false(),x,y) -> c_7()
            ify#(false(),x,y) -> c_9()
            minus#(0(),0()) -> c_11()
            plus#(0(),0()) -> c_15()
        - Weak TRS:
            ge(0(),0()) -> true()
            ge(0(),s(0())) -> false()
            ge(0(),s(s(x))) -> ge(0(),s(x))
            ge(s(x),0()) -> ge(x,0())
            ge(s(x),s(y)) -> ge(x,y)
            minus(0(),0()) -> 0()
            minus(0(),s(x)) -> minus(0(),x)
            minus(s(x),0()) -> s(minus(x,0()))
            minus(s(x),s(y)) -> minus(x,y)
        - Signature:
            {div/2,ge/2,if/3,ify/3,minus/2,plus/2,div#/2,ge#/2,if#/3,ify#/3,minus#/2,plus#/2} / {0/0,divByZeroError/0
            ,false/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/1,c_13/1,c_14/1
            ,c_15/0,c_16/1,c_17/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,ge#,if#,ify#,minus#,plus#} and constructors {0
            ,divByZeroError,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
             -->_1 ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y)):6
             -->_2 ge#(s(x),s(y)) -> c_6(ge#(x,y)):4
             -->_1 ify#(false(),x,y) -> c_9():15
             -->_2 ge#(0(),s(0())) -> c_3():13
          
          2:S:ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
             -->_1 ge#(0(),s(0())) -> c_3():13
             -->_1 ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x))):2
          
          3:S:ge#(s(x),0()) -> c_5(ge#(x,0()))
             -->_1 ge#(0(),0()) -> c_2():12
             -->_1 ge#(s(x),0()) -> c_5(ge#(x,0())):3
          
          4:S:ge#(s(x),s(y)) -> c_6(ge#(x,y))
             -->_1 ge#(0(),s(0())) -> c_3():13
             -->_1 ge#(0(),0()) -> c_2():12
             -->_1 ge#(s(x),s(y)) -> c_6(ge#(x,y)):4
             -->_1 ge#(s(x),0()) -> c_5(ge#(x,0())):3
             -->_1 ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x))):2
          
          5:S:if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
             -->_2 minus#(s(x),s(y)) -> c_14(minus#(x,y)):9
             -->_2 minus#(s(x),0()) -> c_13(minus#(x,0())):8
             -->_2 minus#(0(),s(x)) -> c_12(minus#(0(),x)):7
             -->_2 minus#(0(),0()) -> c_11():16
             -->_1 div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0()))):1
          
          6:S:ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
             -->_1 if#(false(),x,y) -> c_7():14
             -->_2 ge#(0(),s(0())) -> c_3():13
             -->_2 ge#(0(),0()) -> c_2():12
             -->_1 if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y)):5
             -->_2 ge#(s(x),s(y)) -> c_6(ge#(x,y)):4
             -->_2 ge#(s(x),0()) -> c_5(ge#(x,0())):3
             -->_2 ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x))):2
          
          7:S:minus#(0(),s(x)) -> c_12(minus#(0(),x))
             -->_1 minus#(0(),0()) -> c_11():16
             -->_1 minus#(0(),s(x)) -> c_12(minus#(0(),x)):7
          
          8:S:minus#(s(x),0()) -> c_13(minus#(x,0()))
             -->_1 minus#(0(),0()) -> c_11():16
             -->_1 minus#(s(x),0()) -> c_13(minus#(x,0())):8
          
          9:S:minus#(s(x),s(y)) -> c_14(minus#(x,y))
             -->_1 minus#(0(),0()) -> c_11():16
             -->_1 minus#(s(x),s(y)) -> c_14(minus#(x,y)):9
             -->_1 minus#(s(x),0()) -> c_13(minus#(x,0())):8
             -->_1 minus#(0(),s(x)) -> c_12(minus#(0(),x)):7
          
          10:S:plus#(0(),s(x)) -> c_16(plus#(0(),x))
             -->_1 plus#(0(),0()) -> c_15():17
             -->_1 plus#(0(),s(x)) -> c_16(plus#(0(),x)):10
          
          11:S:plus#(s(x),y) -> c_17(plus#(x,y))
             -->_1 plus#(0(),0()) -> c_15():17
             -->_1 plus#(s(x),y) -> c_17(plus#(x,y)):11
             -->_1 plus#(0(),s(x)) -> c_16(plus#(0(),x)):10
          
          12:W:ge#(0(),0()) -> c_2()
             
          
          13:W:ge#(0(),s(0())) -> c_3()
             
          
          14:W:if#(false(),x,y) -> c_7()
             
          
          15:W:ify#(false(),x,y) -> c_9()
             
          
          16:W:minus#(0(),0()) -> c_11()
             
          
          17:W:plus#(0(),0()) -> c_15()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          17: plus#(0(),0()) -> c_15()
          15: ify#(false(),x,y) -> c_9()
          16: minus#(0(),0()) -> c_11()
          12: ge#(0(),0()) -> c_2()
          13: ge#(0(),s(0())) -> c_3()
          14: if#(false(),x,y) -> c_7()
* Step 5: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
          ge#(0(),s(s(x))) -> c_4(ge#(0(),s(x)))
          ge#(s(x),0()) -> c_5(ge#(x,0()))
          ge#(s(x),s(y)) -> c_6(ge#(x,y))
          if#(true(),x,y) -> c_8(div#(minus(x,y),y),minus#(x,y))
          ify#(true(),x,y) -> c_10(if#(ge(x,y),x,y),ge#(x,y))
          minus#(0(),s(x)) -> c_12(minus#(0(),x))
          minus#(s(x),0()) -> c_13(minus#(x,0()))
          minus#(s(x),s(y)) -> c_14(minus#(x,y))
          plus#(0(),s(x)) -> c_16(plus#(0(),x))
          plus#(s(x),y) -> c_17(plus#(x,y))
      - Weak TRS:
          ge(0(),0()) -> true()
          ge(0(),s(0())) -> false()
          ge(0(),s(s(x))) -> ge(0(),s(x))
          ge(s(x),0()) -> ge(x,0())
          ge(s(x),s(y)) -> ge(x,y)
          minus(0(),0()) -> 0()
          minus(0(),s(x)) -> minus(0(),x)
          minus(s(x),0()) -> s(minus(x,0()))
          minus(s(x),s(y)) -> minus(x,y)
      - Signature:
          {div/2,ge/2,if/3,ify/3,minus/2,plus/2,div#/2,ge#/2,if#/3,ify#/3,minus#/2,plus#/2} / {0/0,divByZeroError/0
          ,false/0,s/1,true/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/2,c_9/0,c_10/2,c_11/0,c_12/1,c_13/1,c_14/1
          ,c_15/0,c_16/1,c_17/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {div#,ge#,if#,ify#,minus#,plus#} and constructors {0
          ,divByZeroError,false,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE