WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
            top(mark(X)) -> top(proper(X))
            top(ok(X)) -> top(active(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1} / {mark/1,ok/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active,f,g,proper,top} and constructors {mark,ok}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
          active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
          active#(g(X)) -> c_3(g#(active(X)),active#(X))
          f#(mark(X1),X2) -> c_4(f#(X1,X2))
          f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
          g#(mark(X)) -> c_6(g#(X))
          g#(ok(X)) -> c_7(g#(X))
          proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
          top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
          top#(ok(X)) -> c_11(top#(active(X)),active#(X))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> c_3(g#(active(X)),active#(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
            proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
            top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_11(top#(active(X)),active#(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
            top(mark(X)) -> top(proper(X))
            top(ok(X)) -> top(active(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          active(f(X1,X2)) -> f(active(X1),X2)
          active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
          active(g(X)) -> g(active(X))
          f(mark(X1),X2) -> mark(f(X1,X2))
          f(ok(X1),ok(X2)) -> ok(f(X1,X2))
          g(mark(X)) -> mark(g(X))
          g(ok(X)) -> ok(g(X))
          proper(f(X1,X2)) -> f(proper(X1),proper(X2))
          proper(g(X)) -> g(proper(X))
          active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
          active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
          active#(g(X)) -> c_3(g#(active(X)),active#(X))
          f#(mark(X1),X2) -> c_4(f#(X1,X2))
          f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
          g#(mark(X)) -> c_6(g#(X))
          g#(ok(X)) -> c_7(g#(X))
          proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
          top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
          top#(ok(X)) -> c_11(top#(active(X)),active#(X))
* Step 3: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> c_3(g#(active(X)),active#(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
            proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
            top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_11(top#(active(X)),active#(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
          top#(ok(X)) -> c_11(top#(active(X)),active#(X))
        and a lower component
          active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
          active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
          active#(g(X)) -> c_3(g#(active(X)),active#(X))
          f#(mark(X1),X2) -> c_4(f#(X1,X2))
          f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
          g#(mark(X)) -> c_6(g#(X))
          g#(ok(X)) -> c_7(g#(X))
          proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
        Further, following extension rules are added to the lower component.
          top#(mark(X)) -> proper#(X)
          top#(mark(X)) -> top#(proper(X))
          top#(ok(X)) -> active#(X)
          top#(ok(X)) -> top#(active(X))
** Step 3.a:1: SimplifyRHS WORST_CASE(?,O(1))
    + Considered Problem:
        - Strict DPs:
            top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_11(top#(active(X)),active#(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:top#(mark(X)) -> c_10(top#(proper(X)),proper#(X))
             -->_1 top#(ok(X)) -> c_11(top#(active(X)),active#(X)):2
             -->_1 top#(mark(X)) -> c_10(top#(proper(X)),proper#(X)):1
          
          2:S:top#(ok(X)) -> c_11(top#(active(X)),active#(X))
             -->_1 top#(ok(X)) -> c_11(top#(active(X)),active#(X)):2
             -->_1 top#(mark(X)) -> c_10(top#(proper(X)),proper#(X)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          top#(mark(X)) -> c_10(top#(proper(X)))
          top#(ok(X)) -> c_11(top#(active(X)))
** Step 3.a:2: NaturalMI WORST_CASE(?,O(1))
    + Considered Problem:
        - Strict DPs:
            top#(mark(X)) -> c_10(top#(proper(X)))
            top#(ok(X)) -> c_11(top#(active(X)))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_10) = {1},
          uargs(c_11) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [7]                  
                p(f) = [1] x1 + [0]         
                p(g) = [1] x1 + [0]         
             p(mark) = [4]                  
               p(ok) = [14]                 
           p(proper) = [0]                  
              p(top) = [0]                  
          p(active#) = [2]                  
               p(f#) = [8] x1 + [4] x2 + [2]
               p(g#) = [1]                  
          p(proper#) = [1] x1 + [1]         
             p(top#) = [2] x1 + [0]         
              p(c_1) = [1] x1 + [8] x2 + [2]
              p(c_2) = [1] x1 + [1]         
              p(c_3) = [1] x1 + [1] x2 + [1]
              p(c_4) = [2] x1 + [1]         
              p(c_5) = [8] x1 + [1]         
              p(c_6) = [4]                  
              p(c_7) = [1] x1 + [1]         
              p(c_8) = [2] x2 + [2]         
              p(c_9) = [1] x1 + [2] x2 + [2]
             p(c_10) = [2] x1 + [4]         
             p(c_11) = [2] x1 + [0]         
        
        Following rules are strictly oriented:
        top#(mark(X)) = [8]                  
                      > [4]                  
                      = c_10(top#(proper(X)))
        
        
        Following rules are (at-least) weakly oriented:
              top#(ok(X)) =  [28]                    
                          >= [28]                    
                          =  c_11(top#(active(X)))   
        
         active(f(X1,X2)) =  [7]                     
                          >= [7]                     
                          =  f(active(X1),X2)        
        
        active(f(g(X),Y)) =  [7]                     
                          >= [4]                     
                          =  mark(f(X,f(g(X),Y)))    
        
             active(g(X)) =  [7]                     
                          >= [7]                     
                          =  g(active(X))            
        
           f(mark(X1),X2) =  [4]                     
                          >= [4]                     
                          =  mark(f(X1,X2))          
        
         f(ok(X1),ok(X2)) =  [14]                    
                          >= [14]                    
                          =  ok(f(X1,X2))            
        
               g(mark(X)) =  [4]                     
                          >= [4]                     
                          =  mark(g(X))              
        
                 g(ok(X)) =  [14]                    
                          >= [14]                    
                          =  ok(g(X))                
        
         proper(f(X1,X2)) =  [0]                     
                          >= [0]                     
                          =  f(proper(X1),proper(X2))
        
             proper(g(X)) =  [0]                     
                          >= [0]                     
                          =  g(proper(X))            
        
** Step 3.a:3: NaturalMI WORST_CASE(?,O(1))
    + Considered Problem:
        - Strict DPs:
            top#(ok(X)) -> c_11(top#(active(X)))
        - Weak DPs:
            top#(mark(X)) -> c_10(top#(proper(X)))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_10) = {1},
          uargs(c_11) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [8]         
                p(f) = [1] x1 + [0]
                p(g) = [1] x1 + [0]
             p(mark) = [8]         
               p(ok) = [9]         
           p(proper) = [0]         
              p(top) = [0]         
          p(active#) = [0]         
               p(f#) = [0]         
               p(g#) = [0]         
          p(proper#) = [0]         
             p(top#) = [1] x1 + [1]
              p(c_1) = [0]         
              p(c_2) = [0]         
              p(c_3) = [1]         
              p(c_4) = [0]         
              p(c_5) = [2]         
              p(c_6) = [0]         
              p(c_7) = [4]         
              p(c_8) = [0]         
              p(c_9) = [0]         
             p(c_10) = [8] x1 + [0]
             p(c_11) = [1] x1 + [0]
        
        Following rules are strictly oriented:
        top#(ok(X)) = [10]                 
                    > [9]                  
                    = c_11(top#(active(X)))
        
        
        Following rules are (at-least) weakly oriented:
            top#(mark(X)) =  [9]                     
                          >= [8]                     
                          =  c_10(top#(proper(X)))   
        
         active(f(X1,X2)) =  [8]                     
                          >= [8]                     
                          =  f(active(X1),X2)        
        
        active(f(g(X),Y)) =  [8]                     
                          >= [8]                     
                          =  mark(f(X,f(g(X),Y)))    
        
             active(g(X)) =  [8]                     
                          >= [8]                     
                          =  g(active(X))            
        
           f(mark(X1),X2) =  [8]                     
                          >= [8]                     
                          =  mark(f(X1,X2))          
        
         f(ok(X1),ok(X2)) =  [9]                     
                          >= [9]                     
                          =  ok(f(X1,X2))            
        
               g(mark(X)) =  [8]                     
                          >= [8]                     
                          =  mark(g(X))              
        
                 g(ok(X)) =  [9]                     
                          >= [9]                     
                          =  ok(g(X))                
        
         proper(f(X1,X2)) =  [0]                     
                          >= [0]                     
                          =  f(proper(X1),proper(X2))
        
             proper(g(X)) =  [0]                     
                          >= [0]                     
                          =  g(proper(X))            
        
** Step 3.a:4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            top#(mark(X)) -> c_10(top#(proper(X)))
            top#(ok(X)) -> c_11(top#(active(X)))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 3.b:1: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> c_3(g#(active(X)),active#(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
            proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
        - Weak DPs:
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
          active#(g(X)) -> c_3(g#(active(X)),active#(X))
          proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
          top#(mark(X)) -> proper#(X)
          top#(mark(X)) -> top#(proper(X))
          top#(ok(X)) -> active#(X)
          top#(ok(X)) -> top#(active(X))
        and a lower component
          active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
          f#(mark(X1),X2) -> c_4(f#(X1,X2))
          f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
          g#(mark(X)) -> c_6(g#(X))
          g#(ok(X)) -> c_7(g#(X))
        Further, following extension rules are added to the lower component.
          active#(f(X1,X2)) -> active#(X1)
          active#(f(X1,X2)) -> f#(active(X1),X2)
          active#(g(X)) -> active#(X)
          active#(g(X)) -> g#(active(X))
          proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
          proper#(f(X1,X2)) -> proper#(X1)
          proper#(f(X1,X2)) -> proper#(X2)
          proper#(g(X)) -> g#(proper(X))
          proper#(g(X)) -> proper#(X)
          top#(mark(X)) -> proper#(X)
          top#(mark(X)) -> top#(proper(X))
          top#(ok(X)) -> active#(X)
          top#(ok(X)) -> top#(active(X))
*** Step 3.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
            active#(g(X)) -> c_3(g#(active(X)),active#(X))
            proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
            top#(ok(X)) -> active#(X)
        - Weak DPs:
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1))
             -->_2 active#(g(X)) -> c_3(g#(active(X)),active#(X)):2
             -->_2 active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1)):1
          
          2:S:active#(g(X)) -> c_3(g#(active(X)),active#(X))
             -->_2 active#(g(X)) -> c_3(g#(active(X)),active#(X)):2
             -->_2 active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1)):1
          
          3:S:proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
             -->_3 proper#(g(X)) -> c_9(g#(proper(X)),proper#(X)):4
             -->_2 proper#(g(X)) -> c_9(g#(proper(X)),proper#(X)):4
             -->_3 proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):3
             -->_2 proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):3
          
          4:S:proper#(g(X)) -> c_9(g#(proper(X)),proper#(X))
             -->_2 proper#(g(X)) -> c_9(g#(proper(X)),proper#(X)):4
             -->_2 proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):3
          
          5:S:top#(ok(X)) -> active#(X)
             -->_1 active#(g(X)) -> c_3(g#(active(X)),active#(X)):2
             -->_1 active#(f(X1,X2)) -> c_1(f#(active(X1),X2),active#(X1)):1
          
          6:W:top#(mark(X)) -> proper#(X)
             -->_1 proper#(g(X)) -> c_9(g#(proper(X)),proper#(X)):4
             -->_1 proper#(f(X1,X2)) -> c_8(f#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):3
          
          7:W:top#(mark(X)) -> top#(proper(X))
             -->_1 top#(ok(X)) -> top#(active(X)):8
             -->_1 top#(mark(X)) -> top#(proper(X)):7
             -->_1 top#(mark(X)) -> proper#(X):6
             -->_1 top#(ok(X)) -> active#(X):5
          
          8:W:top#(ok(X)) -> top#(active(X))
             -->_1 top#(ok(X)) -> top#(active(X)):8
             -->_1 top#(mark(X)) -> top#(proper(X)):7
             -->_1 top#(mark(X)) -> proper#(X):6
             -->_1 top#(ok(X)) -> active#(X):5
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          active#(f(X1,X2)) -> c_1(active#(X1))
          active#(g(X)) -> c_3(active#(X))
          proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
          proper#(g(X)) -> c_9(proper#(X))
*** Step 3.b:1.a:2: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(active#(X1))
            active#(g(X)) -> c_3(active#(X))
            proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(proper#(X))
            top#(ok(X)) -> active#(X)
        - Weak DPs:
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/3,c_3/1
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1},
          uargs(c_8) = {1,2},
          uargs(c_9) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [0]                  
                p(f) = [0]                  
                p(g) = [0]                  
             p(mark) = [1] x1 + [0]         
               p(ok) = [1] x1 + [0]         
           p(proper) = [0]                  
              p(top) = [0]                  
          p(active#) = [0]                  
               p(f#) = [0]                  
               p(g#) = [1]                  
          p(proper#) = [0]                  
             p(top#) = [1] x1 + [8]         
              p(c_1) = [1] x1 + [0]         
              p(c_2) = [4] x1 + [0]         
              p(c_3) = [2] x1 + [0]         
              p(c_4) = [0]                  
              p(c_5) = [1] x1 + [0]         
              p(c_6) = [1] x1 + [8]         
              p(c_7) = [1] x1 + [1]         
              p(c_8) = [2] x1 + [1] x2 + [0]
              p(c_9) = [8] x1 + [0]         
             p(c_10) = [1] x1 + [1] x2 + [1]
             p(c_11) = [1] x1 + [1] x2 + [1]
        
        Following rules are strictly oriented:
        top#(ok(X)) = [1] X + [8]
                    > [0]        
                    = active#(X) 
        
        
        Following rules are (at-least) weakly oriented:
        active#(f(X1,X2)) =  [0]                         
                          >= [0]                         
                          =  c_1(active#(X1))            
        
            active#(g(X)) =  [0]                         
                          >= [0]                         
                          =  c_3(active#(X))             
        
        proper#(f(X1,X2)) =  [0]                         
                          >= [0]                         
                          =  c_8(proper#(X1),proper#(X2))
        
            proper#(g(X)) =  [0]                         
                          >= [0]                         
                          =  c_9(proper#(X))             
        
            top#(mark(X)) =  [1] X + [8]                 
                          >= [0]                         
                          =  proper#(X)                  
        
            top#(mark(X)) =  [1] X + [8]                 
                          >= [8]                         
                          =  top#(proper(X))             
        
              top#(ok(X)) =  [1] X + [8]                 
                          >= [8]                         
                          =  top#(active(X))             
        
         active(f(X1,X2)) =  [0]                         
                          >= [0]                         
                          =  f(active(X1),X2)            
        
        active(f(g(X),Y)) =  [0]                         
                          >= [0]                         
                          =  mark(f(X,f(g(X),Y)))        
        
             active(g(X)) =  [0]                         
                          >= [0]                         
                          =  g(active(X))                
        
           f(mark(X1),X2) =  [0]                         
                          >= [0]                         
                          =  mark(f(X1,X2))              
        
         f(ok(X1),ok(X2)) =  [0]                         
                          >= [0]                         
                          =  ok(f(X1,X2))                
        
               g(mark(X)) =  [0]                         
                          >= [0]                         
                          =  mark(g(X))                  
        
                 g(ok(X)) =  [0]                         
                          >= [0]                         
                          =  ok(g(X))                    
        
         proper(f(X1,X2)) =  [0]                         
                          >= [0]                         
                          =  f(proper(X1),proper(X2))    
        
             proper(g(X)) =  [0]                         
                          >= [0]                         
                          =  g(proper(X))                
        
*** Step 3.b:1.a:3: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(active#(X1))
            active#(g(X)) -> c_3(active#(X))
            proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(proper#(X))
        - Weak DPs:
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/3,c_3/1
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1},
          uargs(c_8) = {1,2},
          uargs(c_9) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [0]         
                p(f) = [4] x1 + [0]         
                p(g) = [4] x1 + [1]         
             p(mark) = [1] x1 + [1]         
               p(ok) = [1] x1 + [1]         
           p(proper) = [1] x1 + [0]         
              p(top) = [1] x1 + [2]         
          p(active#) = [4] x1 + [0]         
               p(f#) = [2]                  
               p(g#) = [1]                  
          p(proper#) = [0]                  
             p(top#) = [4] x1 + [0]         
              p(c_1) = [1] x1 + [0]         
              p(c_2) = [1] x1 + [8] x3 + [1]
              p(c_3) = [4] x1 + [3]         
              p(c_4) = [1] x1 + [0]         
              p(c_5) = [2] x1 + [2]         
              p(c_6) = [1] x1 + [2]         
              p(c_7) = [2] x1 + [1]         
              p(c_8) = [2] x1 + [2] x2 + [0]
              p(c_9) = [1] x1 + [0]         
             p(c_10) = [2]                  
             p(c_11) = [1] x1 + [1]         
        
        Following rules are strictly oriented:
        active#(g(X)) = [16] X + [4]   
                      > [16] X + [3]   
                      = c_3(active#(X))
        
        
        Following rules are (at-least) weakly oriented:
        active#(f(X1,X2)) =  [16] X1 + [0]               
                          >= [4] X1 + [0]                
                          =  c_1(active#(X1))            
        
        proper#(f(X1,X2)) =  [0]                         
                          >= [0]                         
                          =  c_8(proper#(X1),proper#(X2))
        
            proper#(g(X)) =  [0]                         
                          >= [0]                         
                          =  c_9(proper#(X))             
        
            top#(mark(X)) =  [4] X + [4]                 
                          >= [0]                         
                          =  proper#(X)                  
        
            top#(mark(X)) =  [4] X + [4]                 
                          >= [4] X + [0]                 
                          =  top#(proper(X))             
        
              top#(ok(X)) =  [4] X + [4]                 
                          >= [4] X + [0]                 
                          =  active#(X)                  
        
              top#(ok(X)) =  [4] X + [4]                 
                          >= [4] X + [0]                 
                          =  top#(active(X))             
        
         active(f(X1,X2)) =  [4] X1 + [0]                
                          >= [4] X1 + [0]                
                          =  f(active(X1),X2)            
        
        active(f(g(X),Y)) =  [16] X + [4]                
                          >= [4] X + [1]                 
                          =  mark(f(X,f(g(X),Y)))        
        
             active(g(X)) =  [4] X + [1]                 
                          >= [4] X + [1]                 
                          =  g(active(X))                
        
           f(mark(X1),X2) =  [4] X1 + [4]                
                          >= [4] X1 + [1]                
                          =  mark(f(X1,X2))              
        
         f(ok(X1),ok(X2)) =  [4] X1 + [4]                
                          >= [4] X1 + [1]                
                          =  ok(f(X1,X2))                
        
               g(mark(X)) =  [4] X + [5]                 
                          >= [4] X + [2]                 
                          =  mark(g(X))                  
        
                 g(ok(X)) =  [4] X + [5]                 
                          >= [4] X + [2]                 
                          =  ok(g(X))                    
        
         proper(f(X1,X2)) =  [4] X1 + [0]                
                          >= [4] X1 + [0]                
                          =  f(proper(X1),proper(X2))    
        
             proper(g(X)) =  [4] X + [1]                 
                          >= [4] X + [1]                 
                          =  g(proper(X))                
        
*** Step 3.b:1.a:4: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            active#(f(X1,X2)) -> c_1(active#(X1))
            proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(proper#(X))
        - Weak DPs:
            active#(g(X)) -> c_3(active#(X))
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/3,c_3/1
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1},
          uargs(c_8) = {1,2},
          uargs(c_9) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [0]         
                p(f) = [8] x1 + [1]         
                p(g) = [2] x1 + [0]         
             p(mark) = [1] x1 + [0]         
               p(ok) = [1] x1 + [0]         
           p(proper) = [1] x1 + [0]         
              p(top) = [8] x1 + [1]         
          p(active#) = [2] x1 + [0]         
               p(f#) = [1] x1 + [0]         
               p(g#) = [0]                  
          p(proper#) = [0]                  
             p(top#) = [8] x1 + [8]         
              p(c_1) = [4] x1 + [1]         
              p(c_2) = [2] x1 + [1]         
              p(c_3) = [2] x1 + [0]         
              p(c_4) = [1]                  
              p(c_5) = [0]                  
              p(c_6) = [1] x1 + [1]         
              p(c_7) = [8] x1 + [0]         
              p(c_8) = [8] x1 + [1] x2 + [0]
              p(c_9) = [1] x1 + [0]         
             p(c_10) = [1] x1 + [1] x2 + [1]
             p(c_11) = [2] x1 + [1]         
        
        Following rules are strictly oriented:
        active#(f(X1,X2)) = [16] X1 + [2]   
                          > [8] X1 + [1]    
                          = c_1(active#(X1))
        
        
        Following rules are (at-least) weakly oriented:
            active#(g(X)) =  [4] X + [0]                 
                          >= [4] X + [0]                 
                          =  c_3(active#(X))             
        
        proper#(f(X1,X2)) =  [0]                         
                          >= [0]                         
                          =  c_8(proper#(X1),proper#(X2))
        
            proper#(g(X)) =  [0]                         
                          >= [0]                         
                          =  c_9(proper#(X))             
        
            top#(mark(X)) =  [8] X + [8]                 
                          >= [0]                         
                          =  proper#(X)                  
        
            top#(mark(X)) =  [8] X + [8]                 
                          >= [8] X + [8]                 
                          =  top#(proper(X))             
        
              top#(ok(X)) =  [8] X + [8]                 
                          >= [2] X + [0]                 
                          =  active#(X)                  
        
              top#(ok(X)) =  [8] X + [8]                 
                          >= [8] X + [8]                 
                          =  top#(active(X))             
        
         active(f(X1,X2)) =  [8] X1 + [1]                
                          >= [8] X1 + [1]                
                          =  f(active(X1),X2)            
        
        active(f(g(X),Y)) =  [16] X + [1]                
                          >= [8] X + [1]                 
                          =  mark(f(X,f(g(X),Y)))        
        
             active(g(X)) =  [2] X + [0]                 
                          >= [2] X + [0]                 
                          =  g(active(X))                
        
           f(mark(X1),X2) =  [8] X1 + [1]                
                          >= [8] X1 + [1]                
                          =  mark(f(X1,X2))              
        
         f(ok(X1),ok(X2)) =  [8] X1 + [1]                
                          >= [8] X1 + [1]                
                          =  ok(f(X1,X2))                
        
               g(mark(X)) =  [2] X + [0]                 
                          >= [2] X + [0]                 
                          =  mark(g(X))                  
        
                 g(ok(X)) =  [2] X + [0]                 
                          >= [2] X + [0]                 
                          =  ok(g(X))                    
        
         proper(f(X1,X2)) =  [8] X1 + [1]                
                          >= [8] X1 + [1]                
                          =  f(proper(X1),proper(X2))    
        
             proper(g(X)) =  [2] X + [0]                 
                          >= [2] X + [0]                 
                          =  g(proper(X))                
        
*** Step 3.b:1.a:5: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(proper#(X))
        - Weak DPs:
            active#(f(X1,X2)) -> c_1(active#(X1))
            active#(g(X)) -> c_3(active#(X))
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/3,c_3/1
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          active :: ["A"(0, 0)] -(0)-> "A"(0, 0)
          f :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0)
          g :: ["A"(0, 0)] -(1)-> "A"(0, 0)
          mark :: ["A"(0, 0)] -(0)-> "A"(0, 0)
          mark :: ["A"(0, 0)] -(0)-> "A"(7, 7)
          mark :: ["A"(0, 0)] -(0)-> "A"(5, 6)
          mark :: ["A"(0, 0)] -(0)-> "A"(0, 8)
          ok :: ["A"(0, 0)] -(0)-> "A"(0, 0)
          ok :: ["A"(0, 0)] -(0)-> "A"(8, 3)
          ok :: ["A"(0, 0)] -(0)-> "A"(9, 3)
          proper :: ["A"(0, 0)] -(0)-> "A"(0, 0)
          active# :: ["A"(0, 0)] -(0)-> "A"(1, 2)
          proper# :: ["A"(0, 0)] -(0)-> "A"(3, 3)
          top# :: ["A"(0, 0)] -(8)-> "A"(0, 1)
          c_1 :: ["A"(0, 0)] -(0)-> "A"(1, 10)
          c_3 :: ["A"(0, 2)] -(0)-> "A"(2, 2)
          c_8 :: ["A"(3, 3) x "A"(3, 3)] -(0)-> "A"(7, 3)
          c_9 :: ["A"(0, 3)] -(0)-> "A"(4, 3)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "c_8_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
          "c_8_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
          "c_9_A" :: ["A"(0)] -(0)-> "A"(1, 0)
          "c_9_A" :: ["A"(0)] -(0)-> "A"(0, 1)
          "mark_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "mark_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
          "ok_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "ok_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          proper#(g(X)) -> c_9(proper#(X))
        2. Weak:
          proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
*** Step 3.b:1.a:6: MI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
        - Weak DPs:
            active#(f(X1,X2)) -> c_1(active#(X1))
            active#(g(X)) -> c_3(active#(X))
            proper#(g(X)) -> c_9(proper#(X))
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/3,c_3/1
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind Automaton Nothing:
        
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_3) = {1},
          uargs(c_8) = {1,2},
          uargs(c_9) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [4 0] x_1 + [0]            
                       [0 1]       [0]            
                p(f) = [1 0] x_1 + [2 0] x_2 + [1]
                       [0 1]       [0 2]       [0]
                p(g) = [2 0] x_1 + [2]            
                       [0 2]       [0]            
             p(mark) = [1 0] x_1 + [0]            
                       [0 0]       [0]            
               p(ok) = [0 0] x_1 + [2]            
                       [1 1]       [2]            
           p(proper) = [1 0] x_1 + [0]            
                       [0 0]       [0]            
              p(top) = [0 0] x_1 + [1]            
                       [0 1]       [4]            
          p(active#) = [0]                        
                       [1]                        
               p(f#) = [0 0] x_1 + [2 0] x_2 + [1]
                       [0 1]       [0 2]       [0]
               p(g#) = [0 0] x_1 + [0]            
                       [0 4]       [1]            
          p(proper#) = [1 0] x_1 + [0]            
                       [0 0]       [0]            
             p(top#) = [1 4] x_1 + [4]            
                       [0 0]       [2]            
              p(c_1) = [1 0] x_1 + [0]            
                       [0 0]       [0]            
              p(c_2) = [1 4] x_2 + [0 1] x_3 + [0]
                       [0 0]       [0 2]       [1]
              p(c_3) = [1 0] x_1 + [0]            
                       [0 0]       [0]            
              p(c_4) = [1 1] x_1 + [2]            
                       [1 4]       [1]            
              p(c_5) = [4 4] x_1 + [0]            
                       [1 2]       [1]            
              p(c_6) = [0]                        
                       [0]                        
              p(c_7) = [1]                        
                       [1]                        
              p(c_8) = [1 0] x_1 + [1 0] x_2 + [0]
                       [0 0]       [0 0]       [0]
              p(c_9) = [2 0] x_1 + [2]            
                       [0 0]       [0]            
             p(c_10) = [2 1] x_1 + [0 1] x_2 + [1]
                       [1 0]       [0 1]       [2]
             p(c_11) = [4 4] x_1 + [0 0] x_2 + [4]
                       [0 0]       [1 1]       [0]
        
        Following rules are strictly oriented:
        proper#(f(X1,X2)) = [1 0] X1 + [2 0] X2 + [1]   
                            [0 0]      [0 0]      [0]   
                          > [1 0] X1 + [1 0] X2 + [0]   
                            [0 0]      [0 0]      [0]   
                          = c_8(proper#(X1),proper#(X2))
        
        
        Following rules are (at-least) weakly oriented:
        active#(f(X1,X2)) =  [0]                      
                             [1]                      
                          >= [0]                      
                             [0]                      
                          =  c_1(active#(X1))         
        
            active#(g(X)) =  [0]                      
                             [1]                      
                          >= [0]                      
                             [0]                      
                          =  c_3(active#(X))          
        
            proper#(g(X)) =  [2 0] X + [2]            
                             [0 0]     [0]            
                          >= [2 0] X + [2]            
                             [0 0]     [0]            
                          =  c_9(proper#(X))          
        
            top#(mark(X)) =  [1 0] X + [4]            
                             [0 0]     [2]            
                          >= [1 0] X + [0]            
                             [0 0]     [0]            
                          =  proper#(X)               
        
            top#(mark(X)) =  [1 0] X + [4]            
                             [0 0]     [2]            
                          >= [1 0] X + [4]            
                             [0 0]     [2]            
                          =  top#(proper(X))          
        
              top#(ok(X)) =  [4 4] X + [14]           
                             [0 0]     [2]            
                          >= [0]                      
                             [1]                      
                          =  active#(X)               
        
              top#(ok(X)) =  [4 4] X + [14]           
                             [0 0]     [2]            
                          >= [4 4] X + [4]            
                             [0 0]     [2]            
                          =  top#(active(X))          
        
         active(f(X1,X2)) =  [4 0] X1 + [8 0] X2 + [4]
                             [0 1]      [0 2]      [0]
                          >= [4 0] X1 + [2 0] X2 + [1]
                             [0 1]      [0 2]      [0]
                          =  f(active(X1),X2)         
        
        active(f(g(X),Y)) =  [8 0] X + [8 0] Y + [12] 
                             [0 2]     [0 2]     [0]  
                          >= [5 0] X + [4 0] Y + [7]  
                             [0 0]     [0 0]     [0]  
                          =  mark(f(X,f(g(X),Y)))     
        
             active(g(X)) =  [8 0] X + [8]            
                             [0 2]     [0]            
                          >= [8 0] X + [2]            
                             [0 2]     [0]            
                          =  g(active(X))             
        
           f(mark(X1),X2) =  [1 0] X1 + [2 0] X2 + [1]
                             [0 0]      [0 2]      [0]
                          >= [1 0] X1 + [2 0] X2 + [1]
                             [0 0]      [0 0]      [0]
                          =  mark(f(X1,X2))           
        
         f(ok(X1),ok(X2)) =  [0 0] X1 + [0 0] X2 + [7]
                             [1 1]      [2 2]      [6]
                          >= [0 0] X1 + [0 0] X2 + [2]
                             [1 1]      [2 2]      [3]
                          =  ok(f(X1,X2))             
        
               g(mark(X)) =  [2 0] X + [2]            
                             [0 0]     [0]            
                          >= [2 0] X + [2]            
                             [0 0]     [0]            
                          =  mark(g(X))               
        
                 g(ok(X)) =  [0 0] X + [6]            
                             [2 2]     [4]            
                          >= [0 0] X + [2]            
                             [2 2]     [4]            
                          =  ok(g(X))                 
        
         proper(f(X1,X2)) =  [1 0] X1 + [2 0] X2 + [1]
                             [0 0]      [0 0]      [0]
                          >= [1 0] X1 + [2 0] X2 + [1]
                             [0 0]      [0 0]      [0]
                          =  f(proper(X1),proper(X2)) 
        
             proper(g(X)) =  [2 0] X + [2]            
                             [0 0]     [0]            
                          >= [2 0] X + [2]            
                             [0 0]     [0]            
                          =  g(proper(X))             
        
*** Step 3.b:1.a:7: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            active#(f(X1,X2)) -> c_1(active#(X1))
            active#(g(X)) -> c_3(active#(X))
            proper#(f(X1,X2)) -> c_8(proper#(X1),proper#(X2))
            proper#(g(X)) -> c_9(proper#(X))
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/3,c_3/1
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

*** Step 3.b:1.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
        - Weak DPs:
            active#(f(X1,X2)) -> active#(X1)
            active#(f(X1,X2)) -> f#(active(X1),X2)
            active#(g(X)) -> active#(X)
            active#(g(X)) -> g#(active(X))
            proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
            proper#(f(X1,X2)) -> proper#(X1)
            proper#(f(X1,X2)) -> proper#(X2)
            proper#(g(X)) -> g#(proper(X))
            proper#(g(X)) -> proper#(X)
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1,3},
          uargs(c_4) = {1},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_7) = {1}
        
        Following symbols are considered usable:
          {active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [3]         
                p(f) = [0]                  
                p(g) = [1] x1 + [5]         
             p(mark) = [0]                  
               p(ok) = [1]                  
           p(proper) = [0]                  
              p(top) = [0]                  
          p(active#) = [6]                  
               p(f#) = [2]                  
               p(g#) = [0]                  
          p(proper#) = [2]                  
             p(top#) = [6]                  
              p(c_1) = [0]                  
              p(c_2) = [2] x1 + [4] x3 + [1]
              p(c_3) = [0]                  
              p(c_4) = [1] x1 + [0]         
              p(c_5) = [1] x1 + [0]         
              p(c_6) = [4] x1 + [0]         
              p(c_7) = [1] x1 + [0]         
              p(c_8) = [0]                  
              p(c_9) = [0]                  
             p(c_10) = [0]                  
             p(c_11) = [0]                  
        
        Following rules are strictly oriented:
        active#(f(g(X),Y)) = [6]                                  
                           > [5]                                  
                           = c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
        
        
        Following rules are (at-least) weakly oriented:
        active#(f(X1,X2)) =  [6]                      
                          >= [6]                      
                          =  active#(X1)              
        
        active#(f(X1,X2)) =  [6]                      
                          >= [2]                      
                          =  f#(active(X1),X2)        
        
            active#(g(X)) =  [6]                      
                          >= [6]                      
                          =  active#(X)               
        
            active#(g(X)) =  [6]                      
                          >= [0]                      
                          =  g#(active(X))            
        
          f#(mark(X1),X2) =  [2]                      
                          >= [2]                      
                          =  c_4(f#(X1,X2))           
        
        f#(ok(X1),ok(X2)) =  [2]                      
                          >= [2]                      
                          =  c_5(f#(X1,X2))           
        
              g#(mark(X)) =  [0]                      
                          >= [0]                      
                          =  c_6(g#(X))               
        
                g#(ok(X)) =  [0]                      
                          >= [0]                      
                          =  c_7(g#(X))               
        
        proper#(f(X1,X2)) =  [2]                      
                          >= [2]                      
                          =  f#(proper(X1),proper(X2))
        
        proper#(f(X1,X2)) =  [2]                      
                          >= [2]                      
                          =  proper#(X1)              
        
        proper#(f(X1,X2)) =  [2]                      
                          >= [2]                      
                          =  proper#(X2)              
        
            proper#(g(X)) =  [2]                      
                          >= [0]                      
                          =  g#(proper(X))            
        
            proper#(g(X)) =  [2]                      
                          >= [2]                      
                          =  proper#(X)               
        
            top#(mark(X)) =  [6]                      
                          >= [2]                      
                          =  proper#(X)               
        
            top#(mark(X)) =  [6]                      
                          >= [6]                      
                          =  top#(proper(X))          
        
              top#(ok(X)) =  [6]                      
                          >= [6]                      
                          =  active#(X)               
        
              top#(ok(X)) =  [6]                      
                          >= [6]                      
                          =  top#(active(X))          
        
*** Step 3.b:1.b:2: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
        - Weak DPs:
            active#(f(X1,X2)) -> active#(X1)
            active#(f(X1,X2)) -> f#(active(X1),X2)
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> active#(X)
            active#(g(X)) -> g#(active(X))
            proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
            proper#(f(X1,X2)) -> proper#(X1)
            proper#(f(X1,X2)) -> proper#(X2)
            proper#(g(X)) -> g#(proper(X))
            proper#(g(X)) -> proper#(X)
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1,3},
          uargs(c_4) = {1},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_7) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [0]         
                p(f) = [4] x1 + [0]         
                p(g) = [1] x1 + [0]         
             p(mark) = [1] x1 + [0]         
               p(ok) = [1] x1 + [2]         
           p(proper) = [0]                  
              p(top) = [1] x1 + [1]         
          p(active#) = [1] x1 + [0]         
               p(f#) = [4] x1 + [0]         
               p(g#) = [0]                  
          p(proper#) = [0]                  
             p(top#) = [1] x1 + [0]         
              p(c_1) = [2] x2 + [0]         
              p(c_2) = [1] x1 + [1] x3 + [0]
              p(c_3) = [4] x2 + [0]         
              p(c_4) = [1] x1 + [0]         
              p(c_5) = [1] x1 + [4]         
              p(c_6) = [1] x1 + [0]         
              p(c_7) = [1] x1 + [0]         
              p(c_8) = [1] x2 + [1] x3 + [0]
              p(c_9) = [4] x1 + [1]         
             p(c_10) = [1] x1 + [1]         
             p(c_11) = [0]                  
        
        Following rules are strictly oriented:
        f#(ok(X1),ok(X2)) = [4] X1 + [8]  
                          > [4] X1 + [4]  
                          = c_5(f#(X1,X2))
        
        
        Following rules are (at-least) weakly oriented:
         active#(f(X1,X2)) =  [4] X1 + [0]                         
                           >= [1] X1 + [0]                         
                           =  active#(X1)                          
        
         active#(f(X1,X2)) =  [4] X1 + [0]                         
                           >= [4] X1 + [0]                         
                           =  f#(active(X1),X2)                    
        
        active#(f(g(X),Y)) =  [4] X + [0]                          
                           >= [4] X + [0]                          
                           =  c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
        
             active#(g(X)) =  [1] X + [0]                          
                           >= [1] X + [0]                          
                           =  active#(X)                           
        
             active#(g(X)) =  [1] X + [0]                          
                           >= [0]                                  
                           =  g#(active(X))                        
        
           f#(mark(X1),X2) =  [4] X1 + [0]                         
                           >= [4] X1 + [0]                         
                           =  c_4(f#(X1,X2))                       
        
               g#(mark(X)) =  [0]                                  
                           >= [0]                                  
                           =  c_6(g#(X))                           
        
                 g#(ok(X)) =  [0]                                  
                           >= [0]                                  
                           =  c_7(g#(X))                           
        
         proper#(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  f#(proper(X1),proper(X2))            
        
         proper#(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  proper#(X1)                          
        
         proper#(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  proper#(X2)                          
        
             proper#(g(X)) =  [0]                                  
                           >= [0]                                  
                           =  g#(proper(X))                        
        
             proper#(g(X)) =  [0]                                  
                           >= [0]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [1] X + [0]                          
                           >= [0]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [1] X + [0]                          
                           >= [0]                                  
                           =  top#(proper(X))                      
        
               top#(ok(X)) =  [1] X + [2]                          
                           >= [1] X + [0]                          
                           =  active#(X)                           
        
               top#(ok(X)) =  [1] X + [2]                          
                           >= [1] X + [0]                          
                           =  top#(active(X))                      
        
          active(f(X1,X2)) =  [4] X1 + [0]                         
                           >= [4] X1 + [0]                         
                           =  f(active(X1),X2)                     
        
         active(f(g(X),Y)) =  [4] X + [0]                          
                           >= [4] X + [0]                          
                           =  mark(f(X,f(g(X),Y)))                 
        
              active(g(X)) =  [1] X + [0]                          
                           >= [1] X + [0]                          
                           =  g(active(X))                         
        
            f(mark(X1),X2) =  [4] X1 + [0]                         
                           >= [4] X1 + [0]                         
                           =  mark(f(X1,X2))                       
        
          f(ok(X1),ok(X2)) =  [4] X1 + [8]                         
                           >= [4] X1 + [2]                         
                           =  ok(f(X1,X2))                         
        
                g(mark(X)) =  [1] X + [0]                          
                           >= [1] X + [0]                          
                           =  mark(g(X))                           
        
                  g(ok(X)) =  [1] X + [2]                          
                           >= [1] X + [2]                          
                           =  ok(g(X))                             
        
          proper(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  f(proper(X1),proper(X2))             
        
              proper(g(X)) =  [0]                                  
                           >= [0]                                  
                           =  g(proper(X))                         
        
*** Step 3.b:1.b:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
        - Weak DPs:
            active#(f(X1,X2)) -> active#(X1)
            active#(f(X1,X2)) -> f#(active(X1),X2)
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> active#(X)
            active#(g(X)) -> g#(active(X))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
            proper#(f(X1,X2)) -> proper#(X1)
            proper#(f(X1,X2)) -> proper#(X2)
            proper#(g(X)) -> g#(proper(X))
            proper#(g(X)) -> proper#(X)
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1,3},
          uargs(c_4) = {1},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_7) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [1]         
                p(f) = [1] x1 + [0]         
                p(g) = [1] x1 + [0]         
             p(mark) = [1] x1 + [1]         
               p(ok) = [1] x1 + [1]         
           p(proper) = [0]                  
              p(top) = [4] x1 + [0]         
          p(active#) = [7] x1 + [4]         
               p(f#) = [4] x1 + [0]         
               p(g#) = [0]                  
          p(proper#) = [2]                  
             p(top#) = [7] x1 + [0]         
              p(c_1) = [4] x1 + [4]         
              p(c_2) = [1] x1 + [1] x3 + [4]
              p(c_3) = [1] x1 + [1] x2 + [1]
              p(c_4) = [1] x1 + [2]         
              p(c_5) = [1] x1 + [0]         
              p(c_6) = [4] x1 + [0]         
              p(c_7) = [4] x1 + [0]         
              p(c_8) = [2] x1 + [1] x2 + [0]
              p(c_9) = [1] x1 + [2] x2 + [1]
             p(c_10) = [0]                  
             p(c_11) = [2]                  
        
        Following rules are strictly oriented:
        f#(mark(X1),X2) = [4] X1 + [4]  
                        > [4] X1 + [2]  
                        = c_4(f#(X1,X2))
        
        
        Following rules are (at-least) weakly oriented:
         active#(f(X1,X2)) =  [7] X1 + [4]                         
                           >= [7] X1 + [4]                         
                           =  active#(X1)                          
        
         active#(f(X1,X2)) =  [7] X1 + [4]                         
                           >= [4] X1 + [4]                         
                           =  f#(active(X1),X2)                    
        
        active#(f(g(X),Y)) =  [7] X + [4]                          
                           >= [4] X + [4]                          
                           =  c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
        
             active#(g(X)) =  [7] X + [4]                          
                           >= [7] X + [4]                          
                           =  active#(X)                           
        
             active#(g(X)) =  [7] X + [4]                          
                           >= [0]                                  
                           =  g#(active(X))                        
        
         f#(ok(X1),ok(X2)) =  [4] X1 + [4]                         
                           >= [4] X1 + [0]                         
                           =  c_5(f#(X1,X2))                       
        
               g#(mark(X)) =  [0]                                  
                           >= [0]                                  
                           =  c_6(g#(X))                           
        
                 g#(ok(X)) =  [0]                                  
                           >= [0]                                  
                           =  c_7(g#(X))                           
        
         proper#(f(X1,X2)) =  [2]                                  
                           >= [0]                                  
                           =  f#(proper(X1),proper(X2))            
        
         proper#(f(X1,X2)) =  [2]                                  
                           >= [2]                                  
                           =  proper#(X1)                          
        
         proper#(f(X1,X2)) =  [2]                                  
                           >= [2]                                  
                           =  proper#(X2)                          
        
             proper#(g(X)) =  [2]                                  
                           >= [0]                                  
                           =  g#(proper(X))                        
        
             proper#(g(X)) =  [2]                                  
                           >= [2]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [7] X + [7]                          
                           >= [2]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [7] X + [7]                          
                           >= [0]                                  
                           =  top#(proper(X))                      
        
               top#(ok(X)) =  [7] X + [7]                          
                           >= [7] X + [4]                          
                           =  active#(X)                           
        
               top#(ok(X)) =  [7] X + [7]                          
                           >= [7] X + [7]                          
                           =  top#(active(X))                      
        
          active(f(X1,X2)) =  [1] X1 + [1]                         
                           >= [1] X1 + [1]                         
                           =  f(active(X1),X2)                     
        
         active(f(g(X),Y)) =  [1] X + [1]                          
                           >= [1] X + [1]                          
                           =  mark(f(X,f(g(X),Y)))                 
        
              active(g(X)) =  [1] X + [1]                          
                           >= [1] X + [1]                          
                           =  g(active(X))                         
        
            f(mark(X1),X2) =  [1] X1 + [1]                         
                           >= [1] X1 + [1]                         
                           =  mark(f(X1,X2))                       
        
          f(ok(X1),ok(X2)) =  [1] X1 + [1]                         
                           >= [1] X1 + [1]                         
                           =  ok(f(X1,X2))                         
        
                g(mark(X)) =  [1] X + [1]                          
                           >= [1] X + [1]                          
                           =  mark(g(X))                           
        
                  g(ok(X)) =  [1] X + [1]                          
                           >= [1] X + [1]                          
                           =  ok(g(X))                             
        
          proper(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  f(proper(X1),proper(X2))             
        
              proper(g(X)) =  [0]                                  
                           >= [0]                                  
                           =  g(proper(X))                         
        
*** Step 3.b:1.b:4: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
        - Weak DPs:
            active#(f(X1,X2)) -> active#(X1)
            active#(f(X1,X2)) -> f#(active(X1),X2)
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> active#(X)
            active#(g(X)) -> g#(active(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
            proper#(f(X1,X2)) -> proper#(X1)
            proper#(f(X1,X2)) -> proper#(X2)
            proper#(g(X)) -> g#(proper(X))
            proper#(g(X)) -> proper#(X)
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1,3},
          uargs(c_4) = {1},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_7) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [0]                  
                p(f) = [2] x1 + [0]                  
                p(g) = [2] x1 + [0]                  
             p(mark) = [1] x1 + [0]                  
               p(ok) = [1] x1 + [1]                  
           p(proper) = [0]                           
              p(top) = [0]                           
          p(active#) = [2] x1 + [5]                  
               p(f#) = [1] x1 + [0]                  
               p(g#) = [1] x1 + [0]                  
          p(proper#) = [4]                           
             p(top#) = [3] x1 + [5]                  
              p(c_1) = [1] x1 + [1]                  
              p(c_2) = [3] x1 + [1] x2 + [3] x3 + [0]
              p(c_3) = [1] x1 + [4]                  
              p(c_4) = [1] x1 + [0]                  
              p(c_5) = [1] x1 + [1]                  
              p(c_6) = [1] x1 + [0]                  
              p(c_7) = [1] x1 + [0]                  
              p(c_8) = [2] x2 + [1] x3 + [4]         
              p(c_9) = [4]                           
             p(c_10) = [1]                           
             p(c_11) = [4]                           
        
        Following rules are strictly oriented:
        g#(ok(X)) = [1] X + [1]
                  > [1] X + [0]
                  = c_7(g#(X)) 
        
        
        Following rules are (at-least) weakly oriented:
         active#(f(X1,X2)) =  [4] X1 + [5]                         
                           >= [2] X1 + [5]                         
                           =  active#(X1)                          
        
         active#(f(X1,X2)) =  [4] X1 + [5]                         
                           >= [1] X1 + [0]                         
                           =  f#(active(X1),X2)                    
        
        active#(f(g(X),Y)) =  [8] X + [5]                          
                           >= [8] X + [0]                          
                           =  c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
        
             active#(g(X)) =  [4] X + [5]                          
                           >= [2] X + [5]                          
                           =  active#(X)                           
        
             active#(g(X)) =  [4] X + [5]                          
                           >= [1] X + [0]                          
                           =  g#(active(X))                        
        
           f#(mark(X1),X2) =  [1] X1 + [0]                         
                           >= [1] X1 + [0]                         
                           =  c_4(f#(X1,X2))                       
        
         f#(ok(X1),ok(X2)) =  [1] X1 + [1]                         
                           >= [1] X1 + [1]                         
                           =  c_5(f#(X1,X2))                       
        
               g#(mark(X)) =  [1] X + [0]                          
                           >= [1] X + [0]                          
                           =  c_6(g#(X))                           
        
         proper#(f(X1,X2)) =  [4]                                  
                           >= [0]                                  
                           =  f#(proper(X1),proper(X2))            
        
         proper#(f(X1,X2)) =  [4]                                  
                           >= [4]                                  
                           =  proper#(X1)                          
        
         proper#(f(X1,X2)) =  [4]                                  
                           >= [4]                                  
                           =  proper#(X2)                          
        
             proper#(g(X)) =  [4]                                  
                           >= [0]                                  
                           =  g#(proper(X))                        
        
             proper#(g(X)) =  [4]                                  
                           >= [4]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [3] X + [5]                          
                           >= [4]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [3] X + [5]                          
                           >= [5]                                  
                           =  top#(proper(X))                      
        
               top#(ok(X)) =  [3] X + [8]                          
                           >= [2] X + [5]                          
                           =  active#(X)                           
        
               top#(ok(X)) =  [3] X + [8]                          
                           >= [3] X + [5]                          
                           =  top#(active(X))                      
        
          active(f(X1,X2)) =  [2] X1 + [0]                         
                           >= [2] X1 + [0]                         
                           =  f(active(X1),X2)                     
        
         active(f(g(X),Y)) =  [4] X + [0]                          
                           >= [2] X + [0]                          
                           =  mark(f(X,f(g(X),Y)))                 
        
              active(g(X)) =  [2] X + [0]                          
                           >= [2] X + [0]                          
                           =  g(active(X))                         
        
            f(mark(X1),X2) =  [2] X1 + [0]                         
                           >= [2] X1 + [0]                         
                           =  mark(f(X1,X2))                       
        
          f(ok(X1),ok(X2)) =  [2] X1 + [2]                         
                           >= [2] X1 + [1]                         
                           =  ok(f(X1,X2))                         
        
                g(mark(X)) =  [2] X + [0]                          
                           >= [2] X + [0]                          
                           =  mark(g(X))                           
        
                  g(ok(X)) =  [2] X + [2]                          
                           >= [2] X + [1]                          
                           =  ok(g(X))                             
        
          proper(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  f(proper(X1),proper(X2))             
        
              proper(g(X)) =  [0]                                  
                           >= [0]                                  
                           =  g(proper(X))                         
        
*** Step 3.b:1.b:5: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            g#(mark(X)) -> c_6(g#(X))
        - Weak DPs:
            active#(f(X1,X2)) -> active#(X1)
            active#(f(X1,X2)) -> f#(active(X1),X2)
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> active#(X)
            active#(g(X)) -> g#(active(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(ok(X)) -> c_7(g#(X))
            proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
            proper#(f(X1,X2)) -> proper#(X1)
            proper#(f(X1,X2)) -> proper#(X2)
            proper#(g(X)) -> g#(proper(X))
            proper#(g(X)) -> proper#(X)
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_2) = {1,3},
          uargs(c_4) = {1},
          uargs(c_5) = {1},
          uargs(c_6) = {1},
          uargs(c_7) = {1}
        
        Following symbols are considered usable:
          {active,f,g,proper,active#,f#,g#,proper#,top#}
        TcT has computed the following interpretation:
           p(active) = [1] x1 + [2]         
                p(f) = [1] x1 + [0]         
                p(g) = [1] x1 + [0]         
             p(mark) = [1] x1 + [2]         
               p(ok) = [1] x1 + [2]         
           p(proper) = [0]                  
              p(top) = [1]                  
          p(active#) = [2] x1 + [4]         
               p(f#) = [2]                  
               p(g#) = [2] x1 + [0]         
          p(proper#) = [5]                  
             p(top#) = [2] x1 + [3]         
              p(c_1) = [4] x2 + [1]         
              p(c_2) = [1] x1 + [1] x3 + [2]
              p(c_3) = [1] x1 + [1]         
              p(c_4) = [1] x1 + [0]         
              p(c_5) = [1] x1 + [0]         
              p(c_6) = [1] x1 + [3]         
              p(c_7) = [1] x1 + [1]         
              p(c_8) = [1] x1 + [2] x3 + [1]
              p(c_9) = [0]                  
             p(c_10) = [4] x1 + [4] x2 + [4]
             p(c_11) = [2] x1 + [4]         
        
        Following rules are strictly oriented:
        g#(mark(X)) = [2] X + [4]
                    > [2] X + [3]
                    = c_6(g#(X)) 
        
        
        Following rules are (at-least) weakly oriented:
         active#(f(X1,X2)) =  [2] X1 + [4]                         
                           >= [2] X1 + [4]                         
                           =  active#(X1)                          
        
         active#(f(X1,X2)) =  [2] X1 + [4]                         
                           >= [2]                                  
                           =  f#(active(X1),X2)                    
        
        active#(f(g(X),Y)) =  [2] X + [4]                          
                           >= [2] X + [4]                          
                           =  c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
        
             active#(g(X)) =  [2] X + [4]                          
                           >= [2] X + [4]                          
                           =  active#(X)                           
        
             active#(g(X)) =  [2] X + [4]                          
                           >= [2] X + [4]                          
                           =  g#(active(X))                        
        
           f#(mark(X1),X2) =  [2]                                  
                           >= [2]                                  
                           =  c_4(f#(X1,X2))                       
        
         f#(ok(X1),ok(X2)) =  [2]                                  
                           >= [2]                                  
                           =  c_5(f#(X1,X2))                       
        
                 g#(ok(X)) =  [2] X + [4]                          
                           >= [2] X + [1]                          
                           =  c_7(g#(X))                           
        
         proper#(f(X1,X2)) =  [5]                                  
                           >= [2]                                  
                           =  f#(proper(X1),proper(X2))            
        
         proper#(f(X1,X2)) =  [5]                                  
                           >= [5]                                  
                           =  proper#(X1)                          
        
         proper#(f(X1,X2)) =  [5]                                  
                           >= [5]                                  
                           =  proper#(X2)                          
        
             proper#(g(X)) =  [5]                                  
                           >= [0]                                  
                           =  g#(proper(X))                        
        
             proper#(g(X)) =  [5]                                  
                           >= [5]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [2] X + [7]                          
                           >= [5]                                  
                           =  proper#(X)                           
        
             top#(mark(X)) =  [2] X + [7]                          
                           >= [3]                                  
                           =  top#(proper(X))                      
        
               top#(ok(X)) =  [2] X + [7]                          
                           >= [2] X + [4]                          
                           =  active#(X)                           
        
               top#(ok(X)) =  [2] X + [7]                          
                           >= [2] X + [7]                          
                           =  top#(active(X))                      
        
          active(f(X1,X2)) =  [1] X1 + [2]                         
                           >= [1] X1 + [2]                         
                           =  f(active(X1),X2)                     
        
         active(f(g(X),Y)) =  [1] X + [2]                          
                           >= [1] X + [2]                          
                           =  mark(f(X,f(g(X),Y)))                 
        
              active(g(X)) =  [1] X + [2]                          
                           >= [1] X + [2]                          
                           =  g(active(X))                         
        
            f(mark(X1),X2) =  [1] X1 + [2]                         
                           >= [1] X1 + [2]                         
                           =  mark(f(X1,X2))                       
        
          f(ok(X1),ok(X2)) =  [1] X1 + [2]                         
                           >= [1] X1 + [2]                         
                           =  ok(f(X1,X2))                         
        
                g(mark(X)) =  [1] X + [2]                          
                           >= [1] X + [2]                          
                           =  mark(g(X))                           
        
                  g(ok(X)) =  [1] X + [2]                          
                           >= [1] X + [2]                          
                           =  ok(g(X))                             
        
          proper(f(X1,X2)) =  [0]                                  
                           >= [0]                                  
                           =  f(proper(X1),proper(X2))             
        
              proper(g(X)) =  [0]                                  
                           >= [0]                                  
                           =  g(proper(X))                         
        
*** Step 3.b:1.b:6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            active#(f(X1,X2)) -> active#(X1)
            active#(f(X1,X2)) -> f#(active(X1),X2)
            active#(f(g(X),Y)) -> c_2(f#(X,f(g(X),Y)),f#(g(X),Y),g#(X))
            active#(g(X)) -> active#(X)
            active#(g(X)) -> g#(active(X))
            f#(mark(X1),X2) -> c_4(f#(X1,X2))
            f#(ok(X1),ok(X2)) -> c_5(f#(X1,X2))
            g#(mark(X)) -> c_6(g#(X))
            g#(ok(X)) -> c_7(g#(X))
            proper#(f(X1,X2)) -> f#(proper(X1),proper(X2))
            proper#(f(X1,X2)) -> proper#(X1)
            proper#(f(X1,X2)) -> proper#(X2)
            proper#(g(X)) -> g#(proper(X))
            proper#(g(X)) -> proper#(X)
            top#(mark(X)) -> proper#(X)
            top#(mark(X)) -> top#(proper(X))
            top#(ok(X)) -> active#(X)
            top#(ok(X)) -> top#(active(X))
        - Weak TRS:
            active(f(X1,X2)) -> f(active(X1),X2)
            active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
            active(g(X)) -> g(active(X))
            f(mark(X1),X2) -> mark(f(X1,X2))
            f(ok(X1),ok(X2)) -> ok(f(X1,X2))
            g(mark(X)) -> mark(g(X))
            g(ok(X)) -> ok(g(X))
            proper(f(X1,X2)) -> f(proper(X1),proper(X2))
            proper(g(X)) -> g(proper(X))
        - Signature:
            {active/1,f/2,g/1,proper/1,top/1,active#/1,f#/2,g#/1,proper#/1,top#/1} / {mark/1,ok/1,c_1/2,c_2/3,c_3/2
            ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/3,c_9/2,c_10/2,c_11/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {active#,f#,g#,proper#,top#} and constructors {mark,ok}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))