MAYBE
* Step 1: InnermostRuleRemoval MAYBE
    + Considered Problem:
        - Strict TRS:
            div(x,y) -> quot(x,y,y)
            div(0(),y) -> 0()
            div(div(x,y),z) -> div(x,times(y,z))
            divides(y,x) -> eq(x,times(div(x,y),y))
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            if(false(),x,y) -> pr(x,y)
            if(true(),x,y) -> false()
            plus(x,0()) -> x
            plus(0(),y) -> y
            plus(s(x),y) -> s(plus(x,y))
            pr(x,s(0())) -> true()
            pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y))
            prime(s(s(x))) -> pr(s(s(x)),s(x))
            quot(x,0(),s(z)) -> s(div(x,s(z)))
            quot(0(),s(y),z) -> 0()
            quot(s(x),s(y),z) -> quot(x,y,z)
            times(0(),y) -> 0()
            times(s(x),y) -> plus(y,times(x,y))
            times(s(0()),y) -> y
        - Signature:
            {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div,divides,eq,if,plus,pr,prime,quot
            ,times} and constructors {0,false,s,true}
    + Applied Processor:
        InnermostRuleRemoval
    + Details:
        Arguments of following rules are not normal-forms.
          div(div(x,y),z) -> div(x,times(y,z))
        All above mentioned rules can be savely removed.
* Step 2: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            div(x,y) -> quot(x,y,y)
            div(0(),y) -> 0()
            divides(y,x) -> eq(x,times(div(x,y),y))
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            if(false(),x,y) -> pr(x,y)
            if(true(),x,y) -> false()
            plus(x,0()) -> x
            plus(0(),y) -> y
            plus(s(x),y) -> s(plus(x,y))
            pr(x,s(0())) -> true()
            pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y))
            prime(s(s(x))) -> pr(s(s(x)),s(x))
            quot(x,0(),s(z)) -> s(div(x,s(z)))
            quot(0(),s(y),z) -> 0()
            quot(s(x),s(y),z) -> quot(x,y,z)
            times(0(),y) -> 0()
            times(s(x),y) -> plus(y,times(x,y))
            times(s(0()),y) -> y
        - Signature:
            {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div,divides,eq,if,plus,pr,prime,quot
            ,times} and constructors {0,false,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          div#(x,y) -> c_1(quot#(x,y,y))
          div#(0(),y) -> c_2()
          divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
          eq#(0(),0()) -> c_4()
          eq#(0(),s(y)) -> c_5()
          eq#(s(x),0()) -> c_6()
          eq#(s(x),s(y)) -> c_7(eq#(x,y))
          if#(false(),x,y) -> c_8(pr#(x,y))
          if#(true(),x,y) -> c_9()
          plus#(x,0()) -> c_10()
          plus#(0(),y) -> c_11()
          plus#(s(x),y) -> c_12(plus#(x,y))
          pr#(x,s(0())) -> c_13()
          pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
          prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
          quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
          quot#(0(),s(y),z) -> c_17()
          quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
          times#(0(),y) -> c_19()
          times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
          times#(s(0()),y) -> c_21()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 3: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(quot#(x,y,y))
            div#(0(),y) -> c_2()
            divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
            eq#(0(),0()) -> c_4()
            eq#(0(),s(y)) -> c_5()
            eq#(s(x),0()) -> c_6()
            eq#(s(x),s(y)) -> c_7(eq#(x,y))
            if#(false(),x,y) -> c_8(pr#(x,y))
            if#(true(),x,y) -> c_9()
            plus#(x,0()) -> c_10()
            plus#(0(),y) -> c_11()
            plus#(s(x),y) -> c_12(plus#(x,y))
            pr#(x,s(0())) -> c_13()
            pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
            prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
            quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
            quot#(0(),s(y),z) -> c_17()
            quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
            times#(0(),y) -> c_19()
            times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
            times#(s(0()),y) -> c_21()
        - Weak TRS:
            div(x,y) -> quot(x,y,y)
            div(0(),y) -> 0()
            divides(y,x) -> eq(x,times(div(x,y),y))
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            if(false(),x,y) -> pr(x,y)
            if(true(),x,y) -> false()
            plus(x,0()) -> x
            plus(0(),y) -> y
            plus(s(x),y) -> s(plus(x,y))
            pr(x,s(0())) -> true()
            pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y))
            prime(s(s(x))) -> pr(s(s(x)),s(x))
            quot(x,0(),s(z)) -> s(div(x,s(z)))
            quot(0(),s(y),z) -> 0()
            quot(s(x),s(y),z) -> quot(x,y,z)
            times(0(),y) -> 0()
            times(s(x),y) -> plus(y,times(x,y))
            times(s(0()),y) -> y
        - Signature:
            {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,plus#/2,pr#/2
            ,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0
            ,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/2,c_21/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,plus#,pr#,prime#,quot#
            ,times#} and constructors {0,false,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          div(x,y) -> quot(x,y,y)
          div(0(),y) -> 0()
          divides(y,x) -> eq(x,times(div(x,y),y))
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          plus(x,0()) -> x
          plus(0(),y) -> y
          plus(s(x),y) -> s(plus(x,y))
          quot(x,0(),s(z)) -> s(div(x,s(z)))
          quot(0(),s(y),z) -> 0()
          quot(s(x),s(y),z) -> quot(x,y,z)
          times(0(),y) -> 0()
          times(s(x),y) -> plus(y,times(x,y))
          times(s(0()),y) -> y
          div#(x,y) -> c_1(quot#(x,y,y))
          div#(0(),y) -> c_2()
          divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
          eq#(0(),0()) -> c_4()
          eq#(0(),s(y)) -> c_5()
          eq#(s(x),0()) -> c_6()
          eq#(s(x),s(y)) -> c_7(eq#(x,y))
          if#(false(),x,y) -> c_8(pr#(x,y))
          if#(true(),x,y) -> c_9()
          plus#(x,0()) -> c_10()
          plus#(0(),y) -> c_11()
          plus#(s(x),y) -> c_12(plus#(x,y))
          pr#(x,s(0())) -> c_13()
          pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
          prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
          quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
          quot#(0(),s(y),z) -> c_17()
          quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
          times#(0(),y) -> c_19()
          times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
          times#(s(0()),y) -> c_21()
* Step 4: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(quot#(x,y,y))
            div#(0(),y) -> c_2()
            divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
            eq#(0(),0()) -> c_4()
            eq#(0(),s(y)) -> c_5()
            eq#(s(x),0()) -> c_6()
            eq#(s(x),s(y)) -> c_7(eq#(x,y))
            if#(false(),x,y) -> c_8(pr#(x,y))
            if#(true(),x,y) -> c_9()
            plus#(x,0()) -> c_10()
            plus#(0(),y) -> c_11()
            plus#(s(x),y) -> c_12(plus#(x,y))
            pr#(x,s(0())) -> c_13()
            pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
            prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
            quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
            quot#(0(),s(y),z) -> c_17()
            quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
            times#(0(),y) -> c_19()
            times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
            times#(s(0()),y) -> c_21()
        - Weak TRS:
            div(x,y) -> quot(x,y,y)
            div(0(),y) -> 0()
            divides(y,x) -> eq(x,times(div(x,y),y))
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            plus(x,0()) -> x
            plus(0(),y) -> y
            plus(s(x),y) -> s(plus(x,y))
            quot(x,0(),s(z)) -> s(div(x,s(z)))
            quot(0(),s(y),z) -> 0()
            quot(s(x),s(y),z) -> quot(x,y,z)
            times(0(),y) -> 0()
            times(s(x),y) -> plus(y,times(x,y))
            times(s(0()),y) -> y
        - Signature:
            {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,plus#/2,pr#/2
            ,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0
            ,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/2,c_21/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,plus#,pr#,prime#,quot#
            ,times#} and constructors {0,false,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,5,6,9,10,11,13,17,19,21}
        by application of
          Pre({2,4,5,6,9,10,11,13,17,19,21}) = {1,3,7,8,12,14,15,16,18,20}.
        Here rules are labelled as follows:
          1: div#(x,y) -> c_1(quot#(x,y,y))
          2: div#(0(),y) -> c_2()
          3: divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
          4: eq#(0(),0()) -> c_4()
          5: eq#(0(),s(y)) -> c_5()
          6: eq#(s(x),0()) -> c_6()
          7: eq#(s(x),s(y)) -> c_7(eq#(x,y))
          8: if#(false(),x,y) -> c_8(pr#(x,y))
          9: if#(true(),x,y) -> c_9()
          10: plus#(x,0()) -> c_10()
          11: plus#(0(),y) -> c_11()
          12: plus#(s(x),y) -> c_12(plus#(x,y))
          13: pr#(x,s(0())) -> c_13()
          14: pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
          15: prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
          16: quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
          17: quot#(0(),s(y),z) -> c_17()
          18: quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
          19: times#(0(),y) -> c_19()
          20: times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
          21: times#(s(0()),y) -> c_21()
* Step 5: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(quot#(x,y,y))
            divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
            eq#(s(x),s(y)) -> c_7(eq#(x,y))
            if#(false(),x,y) -> c_8(pr#(x,y))
            plus#(s(x),y) -> c_12(plus#(x,y))
            pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
            prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
            quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
            quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
            times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
        - Weak DPs:
            div#(0(),y) -> c_2()
            eq#(0(),0()) -> c_4()
            eq#(0(),s(y)) -> c_5()
            eq#(s(x),0()) -> c_6()
            if#(true(),x,y) -> c_9()
            plus#(x,0()) -> c_10()
            plus#(0(),y) -> c_11()
            pr#(x,s(0())) -> c_13()
            quot#(0(),s(y),z) -> c_17()
            times#(0(),y) -> c_19()
            times#(s(0()),y) -> c_21()
        - Weak TRS:
            div(x,y) -> quot(x,y,y)
            div(0(),y) -> 0()
            divides(y,x) -> eq(x,times(div(x,y),y))
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            plus(x,0()) -> x
            plus(0(),y) -> y
            plus(s(x),y) -> s(plus(x,y))
            quot(x,0(),s(z)) -> s(div(x,s(z)))
            quot(0(),s(y),z) -> 0()
            quot(s(x),s(y),z) -> quot(x,y,z)
            times(0(),y) -> 0()
            times(s(x),y) -> plus(y,times(x,y))
            times(s(0()),y) -> y
        - Signature:
            {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,plus#/2,pr#/2
            ,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0
            ,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/2,c_21/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,plus#,pr#,prime#,quot#
            ,times#} and constructors {0,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:div#(x,y) -> c_1(quot#(x,y,y))
             -->_1 quot#(s(x),s(y),z) -> c_18(quot#(x,y,z)):9
             -->_1 quot#(0(),s(y),z) -> c_17():19
          
          2:S:divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
             -->_2 times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y)):10
             -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
             -->_2 times#(s(0()),y) -> c_21():21
             -->_2 times#(0(),y) -> c_19():20
             -->_1 eq#(s(x),0()) -> c_6():14
             -->_1 eq#(0(),s(y)) -> c_5():13
             -->_1 eq#(0(),0()) -> c_4():12
             -->_3 div#(0(),y) -> c_2():11
             -->_3 div#(x,y) -> c_1(quot#(x,y,y)):1
          
          3:S:eq#(s(x),s(y)) -> c_7(eq#(x,y))
             -->_1 eq#(s(x),0()) -> c_6():14
             -->_1 eq#(0(),s(y)) -> c_5():13
             -->_1 eq#(0(),0()) -> c_4():12
             -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
          
          4:S:if#(false(),x,y) -> c_8(pr#(x,y))
             -->_1 pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):6
             -->_1 pr#(x,s(0())) -> c_13():18
          
          5:S:plus#(s(x),y) -> c_12(plus#(x,y))
             -->_1 plus#(0(),y) -> c_11():17
             -->_1 plus#(x,0()) -> c_10():16
             -->_1 plus#(s(x),y) -> c_12(plus#(x,y)):5
          
          6:S:pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
             -->_1 if#(true(),x,y) -> c_9():15
             -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4
             -->_2 divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)):2
          
          7:S:prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
             -->_1 pr#(x,s(0())) -> c_13():18
             -->_1 pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):6
          
          8:S:quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
             -->_1 div#(0(),y) -> c_2():11
             -->_1 div#(x,y) -> c_1(quot#(x,y,y)):1
          
          9:S:quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
             -->_1 quot#(0(),s(y),z) -> c_17():19
             -->_1 quot#(s(x),s(y),z) -> c_18(quot#(x,y,z)):9
             -->_1 quot#(x,0(),s(z)) -> c_16(div#(x,s(z))):8
          
          10:S:times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
             -->_2 times#(s(0()),y) -> c_21():21
             -->_2 times#(0(),y) -> c_19():20
             -->_1 plus#(0(),y) -> c_11():17
             -->_1 plus#(x,0()) -> c_10():16
             -->_2 times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y)):10
             -->_1 plus#(s(x),y) -> c_12(plus#(x,y)):5
          
          11:W:div#(0(),y) -> c_2()
             
          
          12:W:eq#(0(),0()) -> c_4()
             
          
          13:W:eq#(0(),s(y)) -> c_5()
             
          
          14:W:eq#(s(x),0()) -> c_6()
             
          
          15:W:if#(true(),x,y) -> c_9()
             
          
          16:W:plus#(x,0()) -> c_10()
             
          
          17:W:plus#(0(),y) -> c_11()
             
          
          18:W:pr#(x,s(0())) -> c_13()
             
          
          19:W:quot#(0(),s(y),z) -> c_17()
             
          
          20:W:times#(0(),y) -> c_19()
             
          
          21:W:times#(s(0()),y) -> c_21()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          18: pr#(x,s(0())) -> c_13()
          15: if#(true(),x,y) -> c_9()
          12: eq#(0(),0()) -> c_4()
          13: eq#(0(),s(y)) -> c_5()
          14: eq#(s(x),0()) -> c_6()
          16: plus#(x,0()) -> c_10()
          17: plus#(0(),y) -> c_11()
          20: times#(0(),y) -> c_19()
          21: times#(s(0()),y) -> c_21()
          11: div#(0(),y) -> c_2()
          19: quot#(0(),s(y),z) -> c_17()
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            div#(x,y) -> c_1(quot#(x,y,y))
            divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
            eq#(s(x),s(y)) -> c_7(eq#(x,y))
            if#(false(),x,y) -> c_8(pr#(x,y))
            plus#(s(x),y) -> c_12(plus#(x,y))
            pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
            prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
            quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
            quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
            times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
        - Weak TRS:
            div(x,y) -> quot(x,y,y)
            div(0(),y) -> 0()
            divides(y,x) -> eq(x,times(div(x,y),y))
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            plus(x,0()) -> x
            plus(0(),y) -> y
            plus(s(x),y) -> s(plus(x,y))
            quot(x,0(),s(z)) -> s(div(x,s(z)))
            quot(0(),s(y),z) -> 0()
            quot(s(x),s(y),z) -> quot(x,y,z)
            times(0(),y) -> 0()
            times(s(x),y) -> plus(y,times(x,y))
            times(s(0()),y) -> y
        - Signature:
            {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,plus#/2,pr#/2
            ,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0
            ,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/2,c_21/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,plus#,pr#,prime#,quot#
            ,times#} and constructors {0,false,s,true}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:div#(x,y) -> c_1(quot#(x,y,y))
           -->_1 quot#(s(x),s(y),z) -> c_18(quot#(x,y,z)):9
        
        2:S:divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
           -->_2 times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y)):10
           -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
           -->_3 div#(x,y) -> c_1(quot#(x,y,y)):1
        
        3:S:eq#(s(x),s(y)) -> c_7(eq#(x,y))
           -->_1 eq#(s(x),s(y)) -> c_7(eq#(x,y)):3
        
        4:S:if#(false(),x,y) -> c_8(pr#(x,y))
           -->_1 pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):6
        
        5:S:plus#(s(x),y) -> c_12(plus#(x,y))
           -->_1 plus#(s(x),y) -> c_12(plus#(x,y)):5
        
        6:S:pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
           -->_1 if#(false(),x,y) -> c_8(pr#(x,y)):4
           -->_2 divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y)):2
        
        7:S:prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x)))
           -->_1 pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x)):6
        
        8:S:quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
           -->_1 div#(x,y) -> c_1(quot#(x,y,y)):1
        
        9:S:quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
           -->_1 quot#(s(x),s(y),z) -> c_18(quot#(x,y,z)):9
           -->_1 quot#(x,0(),s(z)) -> c_16(div#(x,s(z))):8
        
        10:S:times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
           -->_2 times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y)):10
           -->_1 plus#(s(x),y) -> c_12(plus#(x,y)):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).
        
        [(7,prime#(s(s(x))) -> c_15(pr#(s(s(x)),s(x))))]
* Step 7: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          div#(x,y) -> c_1(quot#(x,y,y))
          divides#(y,x) -> c_3(eq#(x,times(div(x,y),y)),times#(div(x,y),y),div#(x,y))
          eq#(s(x),s(y)) -> c_7(eq#(x,y))
          if#(false(),x,y) -> c_8(pr#(x,y))
          plus#(s(x),y) -> c_12(plus#(x,y))
          pr#(x,s(s(y))) -> c_14(if#(divides(s(s(y)),x),x,s(y)),divides#(s(s(y)),x))
          quot#(x,0(),s(z)) -> c_16(div#(x,s(z)))
          quot#(s(x),s(y),z) -> c_18(quot#(x,y,z))
          times#(s(x),y) -> c_20(plus#(y,times(x,y)),times#(x,y))
      - Weak TRS:
          div(x,y) -> quot(x,y,y)
          div(0(),y) -> 0()
          divides(y,x) -> eq(x,times(div(x,y),y))
          eq(0(),0()) -> true()
          eq(0(),s(y)) -> false()
          eq(s(x),0()) -> false()
          eq(s(x),s(y)) -> eq(x,y)
          plus(x,0()) -> x
          plus(0(),y) -> y
          plus(s(x),y) -> s(plus(x,y))
          quot(x,0(),s(z)) -> s(div(x,s(z)))
          quot(0(),s(y),z) -> 0()
          quot(s(x),s(y),z) -> quot(x,y,z)
          times(0(),y) -> 0()
          times(s(x),y) -> plus(y,times(x,y))
          times(s(0()),y) -> y
      - Signature:
          {div/2,divides/2,eq/2,if/3,plus/2,pr/2,prime/1,quot/3,times/2,div#/2,divides#/2,eq#/2,if#/3,plus#/2,pr#/2
          ,prime#/1,quot#/3,times#/2} / {0/0,false/0,s/1,true/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0
          ,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/2,c_21/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {div#,divides#,eq#,if#,plus#,pr#,prime#,quot#
          ,times#} and constructors {0,false,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE