*** 1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
        D(+(x,y)) -> +(D(x),D(y))
        D(-(x,y)) -> -(D(x),D(y))
        D(constant()) -> 0()
        D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
        D(ln(x)) -> div(D(x),x)
        D(minus(x)) -> minus(D(x))
        D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
        D(t()) -> 1()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
      Obligation:
        Full
        basic terms: {D}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
    Applied Processor:
      DependencyPairs {dpKind_ = WIDP}
    Proof:
      We add the following weak dependency pairs:
      
      Strict DPs
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        D#(t()) -> c_9()
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        D#(t()) -> c_9()
      Strict TRS Rules:
        D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
        D(+(x,y)) -> +(D(x),D(y))
        D(-(x,y)) -> -(D(x),D(y))
        D(constant()) -> 0()
        D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
        D(ln(x)) -> div(D(x),x)
        D(minus(x)) -> minus(D(x))
        D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
        D(t()) -> 1()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
      Obligation:
        Full
        basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        D#(t()) -> c_9()
*** 1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        D#(t()) -> c_9()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
      Obligation:
        Full
        basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
    Applied Processor:
      Succeeding
    Proof:
      ()
*** 1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        D#(t()) -> c_9()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
      Obligation:
        Full
        basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {4,9}
      by application of
        Pre({4,9}) = {1,2,3,5,6,7,8}.
      Here rules are labelled as follows:
        1: D#(*(x,y)) -> c_1(y           
                            ,D#(x)       
                            ,x           
                            ,D#(y))      
        2: D#(+(x,y)) -> c_2(D#(x),D#(y))
        3: D#(-(x,y)) -> c_3(D#(x),D#(y))
        4: D#(constant()) -> c_4()       
        5: D#(div(x,y)) -> c_5(D#(x)     
                              ,y         
                              ,x         
                              ,D#(y)     
                              ,y)        
        6: D#(ln(x)) -> c_6(D#(x),x)     
        7: D#(minus(x)) -> c_7(D#(x))    
        8: D#(pow(x,y)) -> c_8(y         
                              ,x         
                              ,y         
                              ,D#(x)     
                              ,x         
                              ,y         
                              ,x         
                              ,D#(y))    
        9: D#(t()) -> c_9()              
*** 1.1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
      Strict TRS Rules:
        
      Weak DP Rules:
        D#(constant()) -> c_4()
        D#(t()) -> c_9()
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
      Obligation:
        Full
        basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
           -->_4 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_3 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_4 D#(minus(x)) -> c_7(D#(x)):6
           -->_3 D#(minus(x)) -> c_7(D#(x)):6
           -->_2 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_4 D#(ln(x)) -> c_6(D#(x),x):5
           -->_3 D#(ln(x)) -> c_6(D#(x),x):5
           -->_2 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_4 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_3 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_4 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_3 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_4 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_3 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_4 D#(t()) -> c_9():9
           -->_3 D#(t()) -> c_9():9
           -->_2 D#(t()) -> c_9():9
           -->_1 D#(t()) -> c_9():9
           -->_4 D#(constant()) -> c_4():8
           -->_3 D#(constant()) -> c_4():8
           -->_2 D#(constant()) -> c_4():8
           -->_1 D#(constant()) -> c_4():8
           -->_4 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_3 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        2:S:D#(+(x,y)) -> c_2(D#(x),D#(y))
           -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_2 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_2 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(t()) -> c_9():9
           -->_1 D#(t()) -> c_9():9
           -->_2 D#(constant()) -> c_4():8
           -->_1 D#(constant()) -> c_4():8
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        3:S:D#(-(x,y)) -> c_3(D#(x),D#(y))
           -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_2 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_2 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_2 D#(t()) -> c_9():9
           -->_1 D#(t()) -> c_9():9
           -->_2 D#(constant()) -> c_4():8
           -->_1 D#(constant()) -> c_4():8
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        4:S:D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
           -->_5 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_4 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_3 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_5 D#(minus(x)) -> c_7(D#(x)):6
           -->_4 D#(minus(x)) -> c_7(D#(x)):6
           -->_3 D#(minus(x)) -> c_7(D#(x)):6
           -->_2 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_5 D#(ln(x)) -> c_6(D#(x),x):5
           -->_4 D#(ln(x)) -> c_6(D#(x),x):5
           -->_3 D#(ln(x)) -> c_6(D#(x),x):5
           -->_2 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_5 D#(t()) -> c_9():9
           -->_4 D#(t()) -> c_9():9
           -->_3 D#(t()) -> c_9():9
           -->_2 D#(t()) -> c_9():9
           -->_1 D#(t()) -> c_9():9
           -->_5 D#(constant()) -> c_4():8
           -->_4 D#(constant()) -> c_4():8
           -->_3 D#(constant()) -> c_4():8
           -->_2 D#(constant()) -> c_4():8
           -->_1 D#(constant()) -> c_4():8
           -->_5 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_4 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_3 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_5 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_4 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_3 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_5 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_4 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_3 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_5 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_4 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_3 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        5:S:D#(ln(x)) -> c_6(D#(x),x)
           -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_2 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_2 D#(t()) -> c_9():9
           -->_1 D#(t()) -> c_9():9
           -->_2 D#(constant()) -> c_4():8
           -->_1 D#(constant()) -> c_4():8
           -->_2 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        6:S:D#(minus(x)) -> c_7(D#(x))
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(t()) -> c_9():9
           -->_1 D#(constant()) -> c_4():8
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        7:S:D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
           -->_8 D#(t()) -> c_9():9
           -->_7 D#(t()) -> c_9():9
           -->_6 D#(t()) -> c_9():9
           -->_5 D#(t()) -> c_9():9
           -->_4 D#(t()) -> c_9():9
           -->_3 D#(t()) -> c_9():9
           -->_2 D#(t()) -> c_9():9
           -->_1 D#(t()) -> c_9():9
           -->_8 D#(constant()) -> c_4():8
           -->_7 D#(constant()) -> c_4():8
           -->_6 D#(constant()) -> c_4():8
           -->_5 D#(constant()) -> c_4():8
           -->_4 D#(constant()) -> c_4():8
           -->_3 D#(constant()) -> c_4():8
           -->_2 D#(constant()) -> c_4():8
           -->_1 D#(constant()) -> c_4():8
           -->_8 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_7 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_6 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_5 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_4 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_3 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
           -->_8 D#(minus(x)) -> c_7(D#(x)):6
           -->_7 D#(minus(x)) -> c_7(D#(x)):6
           -->_6 D#(minus(x)) -> c_7(D#(x)):6
           -->_5 D#(minus(x)) -> c_7(D#(x)):6
           -->_4 D#(minus(x)) -> c_7(D#(x)):6
           -->_3 D#(minus(x)) -> c_7(D#(x)):6
           -->_2 D#(minus(x)) -> c_7(D#(x)):6
           -->_1 D#(minus(x)) -> c_7(D#(x)):6
           -->_8 D#(ln(x)) -> c_6(D#(x),x):5
           -->_7 D#(ln(x)) -> c_6(D#(x),x):5
           -->_6 D#(ln(x)) -> c_6(D#(x),x):5
           -->_5 D#(ln(x)) -> c_6(D#(x),x):5
           -->_4 D#(ln(x)) -> c_6(D#(x),x):5
           -->_3 D#(ln(x)) -> c_6(D#(x),x):5
           -->_2 D#(ln(x)) -> c_6(D#(x),x):5
           -->_1 D#(ln(x)) -> c_6(D#(x),x):5
           -->_8 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_7 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_6 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_5 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_4 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_3 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
           -->_8 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_7 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_6 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_5 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_4 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_3 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_8 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_7 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_6 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_5 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_4 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_3 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_8 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_7 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_6 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_5 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_4 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_3 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
        
        8:W:D#(constant()) -> c_4()
           
        
        9:W:D#(t()) -> c_9()
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        8: D#(constant()) -> c_4()
        9: D#(t()) -> c_9()       
*** 1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
        D#(ln(x)) -> c_6(D#(x),x)
        D#(minus(x)) -> c_7(D#(x))
        D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
      Obligation:
        Full
        basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
    Applied Processor:
      PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
    Proof:
      We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
        3: D#(-(x,y)) -> c_3(D#(x),D#(y))
        
      The strictly oriented rules are moved into the weak component.
  *** 1.1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
          D#(+(x,y)) -> c_2(D#(x),D#(y))
          D#(-(x,y)) -> c_3(D#(x),D#(y))
          D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
          D#(ln(x)) -> c_6(D#(x),x)
          D#(minus(x)) -> c_7(D#(x))
          D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          
        Signature:
          {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
        Obligation:
          Full
          basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
      Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
      Proof:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {2,4},
          uargs(c_2) = {1,2},
          uargs(c_3) = {1,2},
          uargs(c_5) = {1,4},
          uargs(c_6) = {1},
          uargs(c_7) = {1},
          uargs(c_8) = {4,8}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(*) = [1] x1 + [1] x2 + [0]
                 p(+) = [1] x1 + [1] x2 + [0]
                 p(-) = [1] x1 + [1] x2 + [1]
                 p(0) = [0]                  
                 p(1) = [2]                  
                 p(2) = [8]                  
                 p(D) = [2] x1 + [2]         
          p(constant) = [4]                  
               p(div) = [1] x1 + [1] x2 + [0]
                p(ln) = [1] x1 + [0]         
             p(minus) = [1] x1 + [0]         
               p(pow) = [1] x1 + [1] x2 + [0]
                 p(t) = [0]                  
                p(D#) = [8] x1 + [0]         
               p(c_1) = [1] x2 + [1] x4 + [0]
               p(c_2) = [1] x1 + [1] x2 + [0]
               p(c_3) = [1] x1 + [1] x2 + [7]
               p(c_4) = [2]                  
               p(c_5) = [1] x1 + [1] x4 + [0]
               p(c_6) = [1] x1 + [0]         
               p(c_7) = [1] x1 + [0]         
               p(c_8) = [1] x4 + [1] x8 + [0]
               p(c_9) = [8]                  
        
        Following rules are strictly oriented:
        D#(-(x,y)) = [8] x + [8] y + [8]
                   > [8] x + [8] y + [7]
                   = c_3(D#(x),D#(y))   
        
        
        Following rules are (at-least) weakly oriented:
          D#(*(x,y)) =  [8] x + [8] y + [0]         
                     >= [8] x + [8] y + [0]         
                     =  c_1(y,D#(x),x,D#(y))        
        
          D#(+(x,y)) =  [8] x + [8] y + [0]         
                     >= [8] x + [8] y + [0]         
                     =  c_2(D#(x),D#(y))            
        
        D#(div(x,y)) =  [8] x + [8] y + [0]         
                     >= [8] x + [8] y + [0]         
                     =  c_5(D#(x),y,x,D#(y),y)      
        
           D#(ln(x)) =  [8] x + [0]                 
                     >= [8] x + [0]                 
                     =  c_6(D#(x),x)                
        
        D#(minus(x)) =  [8] x + [0]                 
                     >= [8] x + [0]                 
                     =  c_7(D#(x))                  
        
        D#(pow(x,y)) =  [8] x + [8] y + [0]         
                     >= [8] x + [8] y + [0]         
                     =  c_8(y,x,y,D#(x),x,y,x,D#(y))
        
  *** 1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
          D#(+(x,y)) -> c_2(D#(x),D#(y))
          D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
          D#(ln(x)) -> c_6(D#(x),x)
          D#(minus(x)) -> c_7(D#(x))
          D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          D#(-(x,y)) -> c_3(D#(x),D#(y))
        Weak TRS Rules:
          
        Signature:
          {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
        Obligation:
          Full
          basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
      Applied Processor:
        Assumption
      Proof:
        ()
  
  *** 1.1.1.1.1.1.2 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
          D#(+(x,y)) -> c_2(D#(x),D#(y))
          D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
          D#(ln(x)) -> c_6(D#(x),x)
          D#(minus(x)) -> c_7(D#(x))
          D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          D#(-(x,y)) -> c_3(D#(x),D#(y))
        Weak TRS Rules:
          
        Signature:
          {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
        Obligation:
          Full
          basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
      Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
      Proof:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
          1: D#(*(x,y)) -> c_1(y     
                              ,D#(x) 
                              ,x     
                              ,D#(y))
          
        The strictly oriented rules are moved into the weak component.
    *** 1.1.1.1.1.1.2.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
            D#(+(x,y)) -> c_2(D#(x),D#(y))
            D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
            D#(ln(x)) -> c_6(D#(x),x)
            D#(minus(x)) -> c_7(D#(x))
            D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            D#(-(x,y)) -> c_3(D#(x),D#(y))
          Weak TRS Rules:
            
          Signature:
            {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
          Obligation:
            Full
            basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
        Applied Processor:
          NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
        Proof:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_1) = {2,4},
            uargs(c_2) = {1,2},
            uargs(c_3) = {1,2},
            uargs(c_5) = {1,4},
            uargs(c_6) = {1},
            uargs(c_7) = {1},
            uargs(c_8) = {4,8}
          
          Following symbols are considered usable:
            {}
          TcT has computed the following interpretation:
                   p(*) = [1] x1 + [1] x2 + [2] 
                   p(+) = [1] x1 + [1] x2 + [0] 
                   p(-) = [1] x1 + [1] x2 + [0] 
                   p(0) = [0]                   
                   p(1) = [0]                   
                   p(2) = [2]                   
                   p(D) = [0]                   
            p(constant) = [0]                   
                 p(div) = [1] x1 + [1] x2 + [0] 
                  p(ln) = [1] x1 + [0]          
               p(minus) = [1] x1 + [0]          
                 p(pow) = [1] x1 + [1] x2 + [0] 
                   p(t) = [0]                   
                  p(D#) = [8] x1 + [0]          
                 p(c_1) = [1] x2 + [1] x4 + [15]
                 p(c_2) = [1] x1 + [1] x2 + [0] 
                 p(c_3) = [1] x1 + [1] x2 + [0] 
                 p(c_4) = [0]                   
                 p(c_5) = [1] x1 + [1] x4 + [0] 
                 p(c_6) = [1] x1 + [0]          
                 p(c_7) = [1] x1 + [0]          
                 p(c_8) = [1] x4 + [1] x8 + [0] 
                 p(c_9) = [1]                   
          
          Following rules are strictly oriented:
          D#(*(x,y)) = [8] x + [8] y + [16]
                     > [8] x + [8] y + [15]
                     = c_1(y,D#(x),x,D#(y))
          
          
          Following rules are (at-least) weakly oriented:
            D#(+(x,y)) =  [8] x + [8] y + [0]         
                       >= [8] x + [8] y + [0]         
                       =  c_2(D#(x),D#(y))            
          
            D#(-(x,y)) =  [8] x + [8] y + [0]         
                       >= [8] x + [8] y + [0]         
                       =  c_3(D#(x),D#(y))            
          
          D#(div(x,y)) =  [8] x + [8] y + [0]         
                       >= [8] x + [8] y + [0]         
                       =  c_5(D#(x),y,x,D#(y),y)      
          
             D#(ln(x)) =  [8] x + [0]                 
                       >= [8] x + [0]                 
                       =  c_6(D#(x),x)                
          
          D#(minus(x)) =  [8] x + [0]                 
                       >= [8] x + [0]                 
                       =  c_7(D#(x))                  
          
          D#(pow(x,y)) =  [8] x + [8] y + [0]         
                       >= [8] x + [8] y + [0]         
                       =  c_8(y,x,y,D#(x),x,y,x,D#(y))
          
    *** 1.1.1.1.1.1.2.1.1 Progress [(?,O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            D#(+(x,y)) -> c_2(D#(x),D#(y))
            D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
            D#(ln(x)) -> c_6(D#(x),x)
            D#(minus(x)) -> c_7(D#(x))
            D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
            D#(-(x,y)) -> c_3(D#(x),D#(y))
          Weak TRS Rules:
            
          Signature:
            {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
          Obligation:
            Full
            basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
        Applied Processor:
          Assumption
        Proof:
          ()
    
    *** 1.1.1.1.1.1.2.2 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            D#(+(x,y)) -> c_2(D#(x),D#(y))
            D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
            D#(ln(x)) -> c_6(D#(x),x)
            D#(minus(x)) -> c_7(D#(x))
            D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
            D#(-(x,y)) -> c_3(D#(x),D#(y))
          Weak TRS Rules:
            
          Signature:
            {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
          Obligation:
            Full
            basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            4: D#(minus(x)) -> c_7(D#(x))
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.2.2.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              D#(+(x,y)) -> c_2(D#(x),D#(y))
              D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
              D#(ln(x)) -> c_6(D#(x),x)
              D#(minus(x)) -> c_7(D#(x))
              D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
            Strict TRS Rules:
              
            Weak DP Rules:
              D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
              D#(-(x,y)) -> c_3(D#(x),D#(y))
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
            Obligation:
              Full
              basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_1) = {2,4},
              uargs(c_2) = {1,2},
              uargs(c_3) = {1,2},
              uargs(c_5) = {1,4},
              uargs(c_6) = {1},
              uargs(c_7) = {1},
              uargs(c_8) = {4,8}
            
            Following symbols are considered usable:
              {}
            TcT has computed the following interpretation:
                     p(*) = [1] x1 + [1] x2 + [3] 
                     p(+) = [1] x1 + [1] x2 + [2] 
                     p(-) = [1] x1 + [1] x2 + [2] 
                     p(0) = [4]                   
                     p(1) = [2]                   
                     p(2) = [2]                   
                     p(D) = [2] x1 + [1]          
              p(constant) = [1]                   
                   p(div) = [1] x1 + [1] x2 + [1] 
                    p(ln) = [1] x1 + [0]          
                 p(minus) = [1] x1 + [2]          
                   p(pow) = [1] x1 + [1] x2 + [1] 
                     p(t) = [8]                   
                    p(D#) = [8] x1 + [1]          
                   p(c_1) = [1] x2 + [1] x4 + [14]
                   p(c_2) = [1] x1 + [1] x2 + [15]
                   p(c_3) = [1] x1 + [1] x2 + [15]
                   p(c_4) = [8]                   
                   p(c_5) = [1] x1 + [1] x4 + [7] 
                   p(c_6) = [1] x1 + [0]          
                   p(c_7) = [1] x1 + [8]          
                   p(c_8) = [1] x4 + [1] x8 + [7] 
                   p(c_9) = [1]                   
            
            Following rules are strictly oriented:
            D#(minus(x)) = [8] x + [17]
                         > [8] x + [9] 
                         = c_7(D#(x))  
            
            
            Following rules are (at-least) weakly oriented:
              D#(*(x,y)) =  [8] x + [8] y + [25]        
                         >= [8] x + [8] y + [16]        
                         =  c_1(y,D#(x),x,D#(y))        
            
              D#(+(x,y)) =  [8] x + [8] y + [17]        
                         >= [8] x + [8] y + [17]        
                         =  c_2(D#(x),D#(y))            
            
              D#(-(x,y)) =  [8] x + [8] y + [17]        
                         >= [8] x + [8] y + [17]        
                         =  c_3(D#(x),D#(y))            
            
            D#(div(x,y)) =  [8] x + [8] y + [9]         
                         >= [8] x + [8] y + [9]         
                         =  c_5(D#(x),y,x,D#(y),y)      
            
               D#(ln(x)) =  [8] x + [1]                 
                         >= [8] x + [1]                 
                         =  c_6(D#(x),x)                
            
            D#(pow(x,y)) =  [8] x + [8] y + [9]         
                         >= [8] x + [8] y + [9]         
                         =  c_8(y,x,y,D#(x),x,y,x,D#(y))
            
      *** 1.1.1.1.1.1.2.2.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              D#(+(x,y)) -> c_2(D#(x),D#(y))
              D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
              D#(ln(x)) -> c_6(D#(x),x)
              D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
            Strict TRS Rules:
              
            Weak DP Rules:
              D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
              D#(-(x,y)) -> c_3(D#(x),D#(y))
              D#(minus(x)) -> c_7(D#(x))
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
            Obligation:
              Full
              basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.2.2.2 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              D#(+(x,y)) -> c_2(D#(x),D#(y))
              D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
              D#(ln(x)) -> c_6(D#(x),x)
              D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
            Strict TRS Rules:
              
            Weak DP Rules:
              D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
              D#(-(x,y)) -> c_3(D#(x),D#(y))
              D#(minus(x)) -> c_7(D#(x))
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
            Obligation:
              Full
              basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
          Applied Processor:
            PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
          Proof:
            We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
              1: D#(+(x,y)) -> c_2(D#(x),D#(y))
              2: D#(div(x,y)) -> c_5(D#(x)     
                                    ,y         
                                    ,x         
                                    ,D#(y)     
                                    ,y)        
              3: D#(ln(x)) -> c_6(D#(x),x)     
              4: D#(pow(x,y)) -> c_8(y         
                                    ,x         
                                    ,y         
                                    ,D#(x)     
                                    ,x         
                                    ,y         
                                    ,x         
                                    ,D#(y))    
              
            The strictly oriented rules are moved into the weak component.
        *** 1.1.1.1.1.1.2.2.2.1 Progress [(?,O(n^1))]  ***
            Considered Problem:
              Strict DP Rules:
                D#(+(x,y)) -> c_2(D#(x),D#(y))
                D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
                D#(ln(x)) -> c_6(D#(x),x)
                D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
              Strict TRS Rules:
                
              Weak DP Rules:
                D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
                D#(-(x,y)) -> c_3(D#(x),D#(y))
                D#(minus(x)) -> c_7(D#(x))
              Weak TRS Rules:
                
              Signature:
                {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
              Obligation:
                Full
                basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
            Applied Processor:
              NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
            Proof:
              We apply a matrix interpretation of kind constructor based matrix interpretation:
              The following argument positions are considered usable:
                uargs(c_1) = {2,4},
                uargs(c_2) = {1,2},
                uargs(c_3) = {1,2},
                uargs(c_5) = {1,4},
                uargs(c_6) = {1},
                uargs(c_7) = {1},
                uargs(c_8) = {4,8}
              
              Following symbols are considered usable:
                {}
              TcT has computed the following interpretation:
                       p(*) = [1] x1 + [1] x2 + [3]
                       p(+) = [1] x1 + [1] x2 + [2]
                       p(-) = [1] x1 + [1] x2 + [0]
                       p(0) = [0]                  
                       p(1) = [1]                  
                       p(2) = [0]                  
                       p(D) = [1] x1 + [0]         
                p(constant) = [4]                  
                     p(div) = [1] x1 + [1] x2 + [2]
                      p(ln) = [1] x1 + [1]         
                   p(minus) = [1] x1 + [2]         
                     p(pow) = [1] x1 + [1] x2 + [2]
                       p(t) = [1]                  
                      p(D#) = [8] x1 + [0]         
                     p(c_1) = [1] x2 + [1] x4 + [3]
                     p(c_2) = [1] x1 + [1] x2 + [2]
                     p(c_3) = [1] x1 + [1] x2 + [0]
                     p(c_4) = [1]                  
                     p(c_5) = [1] x1 + [1] x4 + [1]
                     p(c_6) = [1] x1 + [5]         
                     p(c_7) = [1] x1 + [0]         
                     p(c_8) = [1] x4 + [1] x8 + [0]
                     p(c_9) = [0]                  
              
              Following rules are strictly oriented:
                D#(+(x,y)) = [8] x + [8] y + [16]        
                           > [8] x + [8] y + [2]         
                           = c_2(D#(x),D#(y))            
              
              D#(div(x,y)) = [8] x + [8] y + [16]        
                           > [8] x + [8] y + [1]         
                           = c_5(D#(x),y,x,D#(y),y)      
              
                 D#(ln(x)) = [8] x + [8]                 
                           > [8] x + [5]                 
                           = c_6(D#(x),x)                
              
              D#(pow(x,y)) = [8] x + [8] y + [16]        
                           > [8] x + [8] y + [0]         
                           = c_8(y,x,y,D#(x),x,y,x,D#(y))
              
              
              Following rules are (at-least) weakly oriented:
                D#(*(x,y)) =  [8] x + [8] y + [24]
                           >= [8] x + [8] y + [3] 
                           =  c_1(y,D#(x),x,D#(y))
              
                D#(-(x,y)) =  [8] x + [8] y + [0] 
                           >= [8] x + [8] y + [0] 
                           =  c_3(D#(x),D#(y))    
              
              D#(minus(x)) =  [8] x + [16]        
                           >= [8] x + [0]         
                           =  c_7(D#(x))          
              
        *** 1.1.1.1.1.1.2.2.2.1.1 Progress [(?,O(1))]  ***
            Considered Problem:
              Strict DP Rules:
                
              Strict TRS Rules:
                
              Weak DP Rules:
                D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
                D#(+(x,y)) -> c_2(D#(x),D#(y))
                D#(-(x,y)) -> c_3(D#(x),D#(y))
                D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
                D#(ln(x)) -> c_6(D#(x),x)
                D#(minus(x)) -> c_7(D#(x))
                D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
              Weak TRS Rules:
                
              Signature:
                {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
              Obligation:
                Full
                basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
            Applied Processor:
              Assumption
            Proof:
              ()
        
        *** 1.1.1.1.1.1.2.2.2.2 Progress [(O(1),O(1))]  ***
            Considered Problem:
              Strict DP Rules:
                
              Strict TRS Rules:
                
              Weak DP Rules:
                D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
                D#(+(x,y)) -> c_2(D#(x),D#(y))
                D#(-(x,y)) -> c_3(D#(x),D#(y))
                D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
                D#(ln(x)) -> c_6(D#(x),x)
                D#(minus(x)) -> c_7(D#(x))
                D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
              Weak TRS Rules:
                
              Signature:
                {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
              Obligation:
                Full
                basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
            Applied Processor:
              RemoveWeakSuffixes
            Proof:
              Consider the dependency graph
                1:W:D#(*(x,y)) -> c_1(y,D#(x),x,D#(y))
                   -->_4 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_3 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_4 D#(minus(x)) -> c_7(D#(x)):6
                   -->_3 D#(minus(x)) -> c_7(D#(x)):6
                   -->_2 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_4 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_3 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_2 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_4 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_3 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_4 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_3 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_4 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_3 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_4 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_3 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
                2:W:D#(+(x,y)) -> c_2(D#(x),D#(y))
                   -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_2 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_2 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
                3:W:D#(-(x,y)) -> c_3(D#(x),D#(y))
                   -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_2 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_2 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
                4:W:D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y)
                   -->_5 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_4 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_3 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_5 D#(minus(x)) -> c_7(D#(x)):6
                   -->_4 D#(minus(x)) -> c_7(D#(x)):6
                   -->_3 D#(minus(x)) -> c_7(D#(x)):6
                   -->_2 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_5 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_4 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_3 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_2 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_5 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_4 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_3 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_5 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_4 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_3 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_5 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_4 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_3 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_5 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_4 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_3 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
                5:W:D#(ln(x)) -> c_6(D#(x),x)
                   -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_2 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_2 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
                6:W:D#(minus(x)) -> c_7(D#(x))
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
                7:W:D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y))
                   -->_8 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_7 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_6 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_5 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_4 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_3 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_2 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_1 D#(pow(x,y)) -> c_8(y,x,y,D#(x),x,y,x,D#(y)):7
                   -->_8 D#(minus(x)) -> c_7(D#(x)):6
                   -->_7 D#(minus(x)) -> c_7(D#(x)):6
                   -->_6 D#(minus(x)) -> c_7(D#(x)):6
                   -->_5 D#(minus(x)) -> c_7(D#(x)):6
                   -->_4 D#(minus(x)) -> c_7(D#(x)):6
                   -->_3 D#(minus(x)) -> c_7(D#(x)):6
                   -->_2 D#(minus(x)) -> c_7(D#(x)):6
                   -->_1 D#(minus(x)) -> c_7(D#(x)):6
                   -->_8 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_7 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_6 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_5 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_4 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_3 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_2 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_1 D#(ln(x)) -> c_6(D#(x),x):5
                   -->_8 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_7 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_6 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_5 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_4 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_3 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_2 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_1 D#(div(x,y)) -> c_5(D#(x),y,x,D#(y),y):4
                   -->_8 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_7 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_6 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_5 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_4 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_3 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                   -->_8 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_7 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_6 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_5 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_4 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_3 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                   -->_8 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_7 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_6 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_5 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_4 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_3 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_2 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                   -->_1 D#(*(x,y)) -> c_1(y,D#(x),x,D#(y)):1
                
              The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
                1: D#(*(x,y)) -> c_1(y           
                                    ,D#(x)       
                                    ,x           
                                    ,D#(y))      
                7: D#(pow(x,y)) -> c_8(y         
                                      ,x         
                                      ,y         
                                      ,D#(x)     
                                      ,x         
                                      ,y         
                                      ,x         
                                      ,D#(y))    
                6: D#(minus(x)) -> c_7(D#(x))    
                5: D#(ln(x)) -> c_6(D#(x),x)     
                4: D#(div(x,y)) -> c_5(D#(x)     
                                      ,y         
                                      ,x         
                                      ,D#(y)     
                                      ,y)        
                3: D#(-(x,y)) -> c_3(D#(x),D#(y))
                2: D#(+(x,y)) -> c_2(D#(x),D#(y))
        *** 1.1.1.1.1.1.2.2.2.2.1 Progress [(O(1),O(1))]  ***
            Considered Problem:
              Strict DP Rules:
                
              Strict TRS Rules:
                
              Weak DP Rules:
                
              Weak TRS Rules:
                
              Signature:
                {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0,c_1/4,c_2/2,c_3/2,c_4/0,c_5/5,c_6/2,c_7/1,c_8/8,c_9/0}
              Obligation:
                Full
                basic terms: {D#}/{*,+,-,0,1,2,constant,div,ln,minus,pow,t}
            Applied Processor:
              EmptyProcessor
            Proof:
              The problem is already closed. The intended complexity is O(1).