MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            div(x,y) -> ify(ge(y,s(0())),x,y)
            div(plus(x,y),z) -> plus(div(x,z),div(y,z))
            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())))
          div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
          ge#(0(),0()) -> c_3()
          ge#(0(),s(0())) -> c_4()
          ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x)))
          ge#(s(x),0()) -> c_6(ge#(x,0()))
          ge#(s(x),s(y)) -> c_7(ge#(x,y))
          if#(false(),x,y) -> c_8()
          if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
          ify#(false(),x,y) -> c_10()
          ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
          minus#(0(),0()) -> c_12()
          minus#(0(),s(x)) -> c_13(minus#(0(),x))
          minus#(s(x),0()) -> c_14(minus#(x,0()))
          minus#(s(x),s(y)) -> c_15(minus#(x,y))
          plus#(0(),0()) -> c_16()
          plus#(0(),s(x)) -> c_17(plus#(0(),x))
          plus#(s(x),y) -> c_18(plus#(x,y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
            div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
            ge#(0(),0()) -> c_3()
            ge#(0(),s(0())) -> c_4()
            ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x)))
            ge#(s(x),0()) -> c_6(ge#(x,0()))
            ge#(s(x),s(y)) -> c_7(ge#(x,y))
            if#(false(),x,y) -> c_8()
            if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
            ify#(false(),x,y) -> c_10()
            ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
            minus#(0(),0()) -> c_12()
            minus#(0(),s(x)) -> c_13(minus#(0(),x))
            minus#(s(x),0()) -> c_14(minus#(x,0()))
            minus#(s(x),s(y)) -> c_15(minus#(x,y))
            plus#(0(),0()) -> c_16()
            plus#(0(),s(x)) -> c_17(plus#(0(),x))
            plus#(s(x),y) -> c_18(plus#(x,y))
        - Weak TRS:
            div(x,y) -> ify(ge(y,s(0())),x,y)
            div(plus(x,y),z) -> plus(div(x,z),div(y,z))
            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/3,c_3/0,c_4/0,c_5/1,c_6/1,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/1,c_14/1
            ,c_15/1,c_16/0,c_17/1,c_18/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
          {3,4,8,10,12,16}
        by application of
          Pre({3,4,8,10,12,16}) = {1,2,5,6,7,9,11,13,14,15,17,18}.
        Here rules are labelled as follows:
          1: div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
          2: div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
          3: ge#(0(),0()) -> c_3()
          4: ge#(0(),s(0())) -> c_4()
          5: ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x)))
          6: ge#(s(x),0()) -> c_6(ge#(x,0()))
          7: ge#(s(x),s(y)) -> c_7(ge#(x,y))
          8: if#(false(),x,y) -> c_8()
          9: if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
          10: ify#(false(),x,y) -> c_10()
          11: ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
          12: minus#(0(),0()) -> c_12()
          13: minus#(0(),s(x)) -> c_13(minus#(0(),x))
          14: minus#(s(x),0()) -> c_14(minus#(x,0()))
          15: minus#(s(x),s(y)) -> c_15(minus#(x,y))
          16: plus#(0(),0()) -> c_16()
          17: plus#(0(),s(x)) -> c_17(plus#(0(),x))
          18: plus#(s(x),y) -> c_18(plus#(x,y))
* Step 3: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
            div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
            ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x)))
            ge#(s(x),0()) -> c_6(ge#(x,0()))
            ge#(s(x),s(y)) -> c_7(ge#(x,y))
            if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
            ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
            minus#(0(),s(x)) -> c_13(minus#(0(),x))
            minus#(s(x),0()) -> c_14(minus#(x,0()))
            minus#(s(x),s(y)) -> c_15(minus#(x,y))
            plus#(0(),s(x)) -> c_17(plus#(0(),x))
            plus#(s(x),y) -> c_18(plus#(x,y))
        - Weak DPs:
            ge#(0(),0()) -> c_3()
            ge#(0(),s(0())) -> c_4()
            if#(false(),x,y) -> c_8()
            ify#(false(),x,y) -> c_10()
            minus#(0(),0()) -> c_12()
            plus#(0(),0()) -> c_16()
        - Weak TRS:
            div(x,y) -> ify(ge(y,s(0())),x,y)
            div(plus(x,y),z) -> plus(div(x,z),div(y,z))
            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/3,c_3/0,c_4/0,c_5/1,c_6/1,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/1,c_14/1
            ,c_15/1,c_16/0,c_17/1,c_18/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_11(if#(ge(x,y),x,y),ge#(x,y)):7
             -->_2 ge#(s(x),s(y)) -> c_7(ge#(x,y)):5
             -->_1 ify#(false(),x,y) -> c_10():16
             -->_2 ge#(0(),s(0())) -> c_4():14
          
          2:S:div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
             -->_1 plus#(s(x),y) -> c_18(plus#(x,y)):12
             -->_1 plus#(0(),s(x)) -> c_17(plus#(0(),x)):11
             -->_1 plus#(0(),0()) -> c_16():18
             -->_3 div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z)):2
             -->_2 div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z)):2
             -->_3 div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0()))):1
             -->_2 div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0()))):1
          
          3:S:ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x)))
             -->_1 ge#(0(),s(0())) -> c_4():14
             -->_1 ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x))):3
          
          4:S:ge#(s(x),0()) -> c_6(ge#(x,0()))
             -->_1 ge#(0(),0()) -> c_3():13
             -->_1 ge#(s(x),0()) -> c_6(ge#(x,0())):4
          
          5:S:ge#(s(x),s(y)) -> c_7(ge#(x,y))
             -->_1 ge#(0(),s(0())) -> c_4():14
             -->_1 ge#(0(),0()) -> c_3():13
             -->_1 ge#(s(x),s(y)) -> c_7(ge#(x,y)):5
             -->_1 ge#(s(x),0()) -> c_6(ge#(x,0())):4
             -->_1 ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x))):3
          
          6:S:if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
             -->_2 minus#(s(x),s(y)) -> c_15(minus#(x,y)):10
             -->_2 minus#(s(x),0()) -> c_14(minus#(x,0())):9
             -->_2 minus#(0(),s(x)) -> c_13(minus#(0(),x)):8
             -->_2 minus#(0(),0()) -> c_12():17
             -->_1 div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z)):2
             -->_1 div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0()))):1
          
          7:S:ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
             -->_1 if#(false(),x,y) -> c_8():15
             -->_2 ge#(0(),s(0())) -> c_4():14
             -->_2 ge#(0(),0()) -> c_3():13
             -->_1 if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y)):6
             -->_2 ge#(s(x),s(y)) -> c_7(ge#(x,y)):5
             -->_2 ge#(s(x),0()) -> c_6(ge#(x,0())):4
             -->_2 ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x))):3
          
          8:S:minus#(0(),s(x)) -> c_13(minus#(0(),x))
             -->_1 minus#(0(),0()) -> c_12():17
             -->_1 minus#(0(),s(x)) -> c_13(minus#(0(),x)):8
          
          9:S:minus#(s(x),0()) -> c_14(minus#(x,0()))
             -->_1 minus#(0(),0()) -> c_12():17
             -->_1 minus#(s(x),0()) -> c_14(minus#(x,0())):9
          
          10:S:minus#(s(x),s(y)) -> c_15(minus#(x,y))
             -->_1 minus#(0(),0()) -> c_12():17
             -->_1 minus#(s(x),s(y)) -> c_15(minus#(x,y)):10
             -->_1 minus#(s(x),0()) -> c_14(minus#(x,0())):9
             -->_1 minus#(0(),s(x)) -> c_13(minus#(0(),x)):8
          
          11:S:plus#(0(),s(x)) -> c_17(plus#(0(),x))
             -->_1 plus#(0(),0()) -> c_16():18
             -->_1 plus#(0(),s(x)) -> c_17(plus#(0(),x)):11
          
          12:S:plus#(s(x),y) -> c_18(plus#(x,y))
             -->_1 plus#(0(),0()) -> c_16():18
             -->_1 plus#(s(x),y) -> c_18(plus#(x,y)):12
             -->_1 plus#(0(),s(x)) -> c_17(plus#(0(),x)):11
          
          13:W:ge#(0(),0()) -> c_3()
             
          
          14:W:ge#(0(),s(0())) -> c_4()
             
          
          15:W:if#(false(),x,y) -> c_8()
             
          
          16:W:ify#(false(),x,y) -> c_10()
             
          
          17:W:minus#(0(),0()) -> c_12()
             
          
          18:W:plus#(0(),0()) -> c_16()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          16: ify#(false(),x,y) -> c_10()
          18: plus#(0(),0()) -> c_16()
          17: minus#(0(),0()) -> c_12()
          13: ge#(0(),0()) -> c_3()
          14: ge#(0(),s(0())) -> c_4()
          15: if#(false(),x,y) -> c_8()
* Step 4: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
            div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
            ge#(0(),s(s(x))) -> c_5(ge#(0(),s(x)))
            ge#(s(x),0()) -> c_6(ge#(x,0()))
            ge#(s(x),s(y)) -> c_7(ge#(x,y))
            if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
            ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
            minus#(0(),s(x)) -> c_13(minus#(0(),x))
            minus#(s(x),0()) -> c_14(minus#(x,0()))
            minus#(s(x),s(y)) -> c_15(minus#(x,y))
            plus#(0(),s(x)) -> c_17(plus#(0(),x))
            plus#(s(x),y) -> c_18(plus#(x,y))
        - Weak TRS:
            div(x,y) -> ify(ge(y,s(0())),x,y)
            div(plus(x,y),z) -> plus(div(x,z),div(y,z))
            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/3,c_3/0,c_4/0,c_5/1,c_6/1,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/1,c_14/1
            ,c_15/1,c_16/0,c_17/1,c_18/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,ge#,if#,ify#,minus#,plus#} and constructors {0
            ,divByZeroError,false,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_1) = {1,2},
          uargs(c_2) = {1,2,3},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_7) = {1},
          uargs(c_9) = {1,2},
          uargs(c_11) = {1,2},
          uargs(c_13) = {1},
          uargs(c_14) = {1},
          uargs(c_15) = {1},
          uargs(c_17) = {1},
          uargs(c_18) = {1}
        
        Following symbols are considered usable:
          {minus,div#,ge#,if#,ify#,minus#,plus#}
        TcT has computed the following interpretation:
                       p(0) = [0]                           
                     p(div) = [3] x1 + [0]                  
          p(divByZeroError) = [0]                           
                   p(false) = [2]                           
                      p(ge) = [0]                           
                      p(if) = [1] x2 + [0]                  
                     p(ify) = [2] x1 + [1] x2 + [0]         
                   p(minus) = [0]                           
                    p(plus) = [2] x1 + [3] x2 + [1]         
                       p(s) = [0]                           
                    p(true) = [0]                           
                    p(div#) = [4] x1 + [0]                  
                     p(ge#) = [0]                           
                     p(if#) = [0]                           
                    p(ify#) = [0]                           
                  p(minus#) = [0]                           
                   p(plus#) = [0]                           
                     p(c_1) = [1] x1 + [2] x2 + [0]         
                     p(c_2) = [1] x1 + [1] x2 + [2] x3 + [0]
                     p(c_3) = [1]                           
                     p(c_4) = [1]                           
                     p(c_5) = [1] x1 + [0]                  
                     p(c_6) = [1] x1 + [0]                  
                     p(c_7) = [4] x1 + [0]                  
                     p(c_8) = [1]                           
                     p(c_9) = [4] x1 + [1] x2 + [0]         
                    p(c_10) = [1]                           
                    p(c_11) = [2] x1 + [4] x2 + [0]         
                    p(c_12) = [1]                           
                    p(c_13) = [4] x1 + [0]                  
                    p(c_14) = [4] x1 + [0]                  
                    p(c_15) = [2] x1 + [0]                  
                    p(c_16) = [1]                           
                    p(c_17) = [4] x1 + [0]                  
                    p(c_18) = [4] x1 + [0]                  
        
        Following rules are strictly oriented:
        div#(plus(x,y),z) = [8] x + [12] y + [4]                             
                          > [4] x + [8] y + [0]                              
                          = c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
        
        
        Following rules are (at-least) weakly oriented:
                div#(x,y) =  [4] x + [0]                              
                          >= [0]                                      
                          =  c_1(ify#(ge(y,s(0())),x,y),ge#(y,s(0())))
        
         ge#(0(),s(s(x))) =  [0]                                      
                          >= [0]                                      
                          =  c_5(ge#(0(),s(x)))                       
        
            ge#(s(x),0()) =  [0]                                      
                          >= [0]                                      
                          =  c_6(ge#(x,0()))                          
        
           ge#(s(x),s(y)) =  [0]                                      
                          >= [0]                                      
                          =  c_7(ge#(x,y))                            
        
          if#(true(),x,y) =  [0]                                      
                          >= [0]                                      
                          =  c_9(div#(minus(x,y),y),minus#(x,y))      
        
         ify#(true(),x,y) =  [0]                                      
                          >= [0]                                      
                          =  c_11(if#(ge(x,y),x,y),ge#(x,y))          
        
         minus#(0(),s(x)) =  [0]                                      
                          >= [0]                                      
                          =  c_13(minus#(0(),x))                      
        
         minus#(s(x),0()) =  [0]                                      
                          >= [0]                                      
                          =  c_14(minus#(x,0()))                      
        
        minus#(s(x),s(y)) =  [0]                                      
                          >= [0]                                      
                          =  c_15(minus#(x,y))                        
        
          plus#(0(),s(x)) =  [0]                                      
                          >= [0]                                      
                          =  c_17(plus#(0(),x))                       
        
            plus#(s(x),y) =  [0]                                      
                          >= [0]                                      
                          =  c_18(plus#(x,y))                         
        
           minus(0(),0()) =  [0]                                      
                          >= [0]                                      
                          =  0()                                      
        
          minus(0(),s(x)) =  [0]                                      
                          >= [0]                                      
                          =  minus(0(),x)                             
        
          minus(s(x),0()) =  [0]                                      
                          >= [0]                                      
                          =  s(minus(x,0()))                          
        
         minus(s(x),s(y)) =  [0]                                      
                          >= [0]                                      
                          =  minus(x,y)                               
        
* 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_5(ge#(0(),s(x)))
          ge#(s(x),0()) -> c_6(ge#(x,0()))
          ge#(s(x),s(y)) -> c_7(ge#(x,y))
          if#(true(),x,y) -> c_9(div#(minus(x,y),y),minus#(x,y))
          ify#(true(),x,y) -> c_11(if#(ge(x,y),x,y),ge#(x,y))
          minus#(0(),s(x)) -> c_13(minus#(0(),x))
          minus#(s(x),0()) -> c_14(minus#(x,0()))
          minus#(s(x),s(y)) -> c_15(minus#(x,y))
          plus#(0(),s(x)) -> c_17(plus#(0(),x))
          plus#(s(x),y) -> c_18(plus#(x,y))
      - Weak DPs:
          div#(plus(x,y),z) -> c_2(plus#(div(x,z),div(y,z)),div#(x,z),div#(y,z))
      - Weak TRS:
          div(x,y) -> ify(ge(y,s(0())),x,y)
          div(plus(x,y),z) -> plus(div(x,z),div(y,z))
          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/3,c_3/0,c_4/0,c_5/1,c_6/1,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/1,c_14/1
          ,c_15/1,c_16/0,c_17/1,c_18/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