WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            log(s(0())) -> 0()
            log(s(s(X))) -> s(log(s(quot(X,s(s(0()))))))
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log,min,quot} and constructors {0,s}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          log#(s(0())) -> c_1()
          log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
          min#(X,0()) -> c_3()
          min#(s(X),s(Y)) -> c_4(min#(X,Y))
          quot#(0(),s(Y)) -> c_5()
          quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            log#(s(0())) -> c_1()
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(X,0()) -> c_3()
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(0(),s(Y)) -> c_5()
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak TRS:
            log(s(0())) -> 0()
            log(s(s(X))) -> s(log(s(quot(X,s(s(0()))))))
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          min(X,0()) -> X
          min(s(X),s(Y)) -> min(X,Y)
          quot(0(),s(Y)) -> 0()
          quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
          log#(s(0())) -> c_1()
          log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
          min#(X,0()) -> c_3()
          min#(s(X),s(Y)) -> c_4(min#(X,Y))
          quot#(0(),s(Y)) -> c_5()
          quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            log#(s(0())) -> c_1()
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(X,0()) -> c_3()
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(0(),s(Y)) -> c_5()
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,5}
        by application of
          Pre({1,3,5}) = {2,4,6}.
        Here rules are labelled as follows:
          1: log#(s(0())) -> c_1()
          2: log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
          3: min#(X,0()) -> c_3()
          4: min#(s(X),s(Y)) -> c_4(min#(X,Y))
          5: quot#(0(),s(Y)) -> c_5()
          6: quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak DPs:
            log#(s(0())) -> c_1()
            min#(X,0()) -> c_3()
            quot#(0(),s(Y)) -> c_5()
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
             -->_2 quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y)):3
             -->_2 quot#(0(),s(Y)) -> c_5():6
             -->_1 log#(s(0())) -> c_1():4
             -->_1 log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0())))):1
          
          2:S:min#(s(X),s(Y)) -> c_4(min#(X,Y))
             -->_1 min#(X,0()) -> c_3():5
             -->_1 min#(s(X),s(Y)) -> c_4(min#(X,Y)):2
          
          3:S:quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
             -->_1 quot#(0(),s(Y)) -> c_5():6
             -->_2 min#(X,0()) -> c_3():5
             -->_1 quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y)):3
             -->_2 min#(s(X),s(Y)) -> c_4(min#(X,Y)):2
          
          4:W:log#(s(0())) -> c_1()
             
          
          5:W:min#(X,0()) -> c_3()
             
          
          6:W:quot#(0(),s(Y)) -> c_5()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: log#(s(0())) -> c_1()
          5: min#(X,0()) -> c_3()
          6: quot#(0(),s(Y)) -> c_5()
* Step 5: PredecessorEstimationCP WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
          2: min#(s(X),s(Y)) -> c_4(min#(X,Y))
          3: quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
          
        The strictly oriented rules are moved into the weak component.
** Step 5.a:1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(c_2) = {1,2},
          uargs(c_4) = {1},
          uargs(c_6) = {1,2}
        
        Following symbols are considered usable:
          {min,quot,log#,min#,quot#}
        TcT has computed the following interpretation:
              p(0) = 0          
            p(log) = 0          
            p(min) = x1         
           p(quot) = x1         
              p(s) = 1 + x1     
           p(log#) = 3*x1^2     
           p(min#) = 1 + 2*x2   
          p(quot#) = 1 + 2*x1*x2
            p(c_1) = 0          
            p(c_2) = x1 + x2    
            p(c_3) = 2          
            p(c_4) = x1         
            p(c_5) = 0          
            p(c_6) = x1 + x2    
        
        Following rules are strictly oriented:
           log#(s(s(X))) = 12 + 12*X + 3*X^2                                 
                         > 4 + 10*X + 3*X^2                                  
                         = c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
        
         min#(s(X),s(Y)) = 3 + 2*Y                                           
                         > 1 + 2*Y                                           
                         = c_4(min#(X,Y))                                    
        
        quot#(s(X),s(Y)) = 3 + 2*X + 2*X*Y + 2*Y                             
                         > 2 + 2*X + 2*X*Y + 2*Y                             
                         = c_6(quot#(min(X,Y),s(Y)),min#(X,Y))               
        
        
        Following rules are (at-least) weakly oriented:
             min(X,0()) =  X                     
                        >= X                     
                        =  X                     
        
         min(s(X),s(Y)) =  1 + X                 
                        >= X                     
                        =  min(X,Y)              
        
         quot(0(),s(Y)) =  0                     
                        >= 0                     
                        =  0()                   
        
        quot(s(X),s(Y)) =  1 + X                 
                        >= 1 + X                 
                        =  s(quot(min(X,Y),s(Y)))
        
** Step 5.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

** Step 5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
            min#(s(X),s(Y)) -> c_4(min#(X,Y))
            quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
             -->_2 quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y)):3
             -->_1 log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0())))):1
          
          2:W:min#(s(X),s(Y)) -> c_4(min#(X,Y))
             -->_1 min#(s(X),s(Y)) -> c_4(min#(X,Y)):2
          
          3:W:quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
             -->_1 quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y)):3
             -->_2 min#(s(X),s(Y)) -> c_4(min#(X,Y)):2
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          1: log#(s(s(X))) -> c_2(log#(s(quot(X,s(s(0()))))),quot#(X,s(s(0()))))
          3: quot#(s(X),s(Y)) -> c_6(quot#(min(X,Y),s(Y)),min#(X,Y))
          2: min#(s(X),s(Y)) -> c_4(min#(X,Y))
** Step 5.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            min(X,0()) -> X
            min(s(X),s(Y)) -> min(X,Y)
            quot(0(),s(Y)) -> 0()
            quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
        - Signature:
            {log/1,min/2,quot/2,log#/1,min#/2,quot#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {log#,min#,quot#} and constructors {0,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))