* Step 1: Sum WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            b(y,z) -> f(c(c(y,z,z),a(),a()))
            b(b(z,y),a()) -> z
            c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
        - Signature:
            {b/2,c/3} / {a/0,f/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {b,c} and constructors {a,f}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: InnermostRuleRemoval WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            b(y,z) -> f(c(c(y,z,z),a(),a()))
            b(b(z,y),a()) -> z
            c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
        - Signature:
            {b/2,c/3} / {a/0,f/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {b,c} and constructors {a,f}
    + Applied Processor:
        InnermostRuleRemoval
    + Details:
        Arguments of following rules are not normal-forms.
          b(b(z,y),a()) -> z
        All above mentioned rules can be savely removed.
* Step 3: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            b(y,z) -> f(c(c(y,z,z),a(),a()))
            c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
        - Signature:
            {b/2,c/3} / {a/0,f/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {b,c} and constructors {a,f}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
          c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 4: MI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
            c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
        - Weak TRS:
            b(y,z) -> f(c(c(y,z,z),a(),a()))
            c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
        - Signature:
            {b/2,c/3,b#/2,c#/3} / {a/0,f/1,c_1/2,c_2/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {b#,c#} and constructors {a,f}
    + Applied Processor:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
        
        The following argument positions are considered usable:
          uargs(c_1) = {1,2},
          uargs(c_2) = {1,2,3}
        
        Following symbols are considered usable:
          {b,c,b#,c#}
        TcT has computed the following interpretation:
            p(a) = [1]                                          
                   [0]                                          
                   [0]                                          
            p(b) = [0 0 0]       [0]                            
                   [0 0 0] x_1 + [2]                            
                   [3 2 0]       [2]                            
            p(c) = [0 0 0]       [0 0 0]       [0 0 0]       [0]
                   [0 0 0] x_1 + [0 0 0] x_2 + [0 1 2] x_3 + [0]
                   [3 0 0]       [1 1 0]       [0 0 0]       [0]
            p(f) = [1 1 0]       [0]                            
                   [0 1 2] x_1 + [0]                            
                   [0 0 0]       [0]                            
           p(b#) = [2 0 0]       [0 2 0]       [1]              
                   [2 0 0] x_1 + [0 0 0] x_2 + [0]              
                   [0 0 0]       [2 0 2]       [1]              
           p(c#) = [2 0 0]       [0 1 0]       [0 1 0]       [0]
                   [0 0 0] x_1 + [0 0 0] x_2 + [0 2 0] x_3 + [1]
                   [0 0 0]       [1 1 2]       [0 0 3]       [0]
          p(c_1) = [2 0 0]       [1 0 0]       [0]              
                   [0 0 0] x_1 + [0 0 0] x_2 + [0]              
                   [0 0 0]       [0 0 0]       [1]              
          p(c_2) = [1 0 0]       [1 0 0]       [1 1 0]       [0]
                   [0 0 0] x_1 + [0 0 0] x_2 + [0 0 0] x_3 + [1]
                   [1 0 0]       [0 1 0]       [0 2 0]       [0]
        
        Following rules are strictly oriented:
        b#(y,z) = [2 0 0]     [0 2 0]     [1]        
                  [2 0 0] y + [0 0 0] z + [0]        
                  [0 0 0]     [2 0 2]     [1]        
                > [2 0 0]     [0 2 0]     [0]        
                  [0 0 0] y + [0 0 0] z + [0]        
                  [0 0 0]     [0 0 0]     [1]        
                = c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
        
        
        Following rules are (at-least) weakly oriented:
        c#(f(z),f(c(a(),x,a())),y) =  [2 2 0]     [0 1 0]     [2 2 0]     [6]              
                                      [0 0 0] x + [0 2 0] y + [0 0 0] z + [1]              
                                      [2 2 0]     [0 0 3]     [0 0 0]     [6]              
                                   >= [2 0 0]     [0 1 0]     [2 2 0]     [6]              
                                      [0 0 0] x + [0 0 0] y + [0 0 0] z + [1]              
                                      [2 0 0]     [0 0 0]     [0 0 0]     [6]              
                                   =  c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
        
                            b(y,z) =  [0 0 0]     [0]                                      
                                      [0 0 0] y + [2]                                      
                                      [3 2 0]     [2]                                      
                                   >= [0]                                                  
                                      [2]                                                  
                                      [0]                                                  
                                   =  f(c(c(y,z,z),a(),a()))                               
        
         c(f(z),f(c(a(),x,a())),y) =  [0 0 0]     [0 0 0]     [0 0 0]     [0]              
                                      [0 0 0] x + [0 1 2] y + [0 0 0] z + [0]              
                                      [2 2 0]     [0 0 0]     [3 3 0]     [6]              
                                   >= [0]                                                  
                                      [0]                                                  
                                      [6]                                                  
                                   =  c(f(b(x,z)),c(z,y,a()),a())                          
        
* Step 5: MI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
        - Weak DPs:
            b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
        - Weak TRS:
            b(y,z) -> f(c(c(y,z,z),a(),a()))
            c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
        - Signature:
            {b/2,c/3,b#/2,c#/3} / {a/0,f/1,c_1/2,c_2/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {b#,c#} and constructors {a,f}
    + Applied Processor:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
        
        The following argument positions are considered usable:
          uargs(c_1) = {1,2},
          uargs(c_2) = {1,2,3}
        
        Following symbols are considered usable:
          {b,c,b#,c#}
        TcT has computed the following interpretation:
            p(a) = [0]                                          
                   [1]                                          
                   [1]                                          
            p(b) = [0]                                          
                   [0]                                          
                   [0]                                          
            p(c) = [0 0 0]       [0 0 0]       [0]              
                   [0 0 0] x_1 + [0 0 0] x_2 + [0]              
                   [0 3 0]       [2 0 0]       [0]              
            p(f) = [1 2 1]       [0]                            
                   [0 0 2] x_1 + [0]                            
                   [0 0 1]       [0]                            
           p(b#) = [3 0 0]       [0 2 1]       [2]              
                   [1 0 0] x_1 + [0 0 0] x_2 + [0]              
                   [0 0 0]       [1 0 0]       [0]              
           p(c#) = [1 0 0]       [0 1 0]       [0 1 0]       [0]
                   [2 0 0] x_1 + [0 0 1] x_2 + [2 0 0] x_3 + [2]
                   [2 0 0]       [0 0 0]       [0 0 1]       [0]
          p(c_1) = [1 0 0]       [1 0 1]       [0]              
                   [0 0 0] x_1 + [0 0 0] x_2 + [0]              
                   [0 0 0]       [0 0 0]       [0]              
          p(c_2) = [2 0 0]       [1 1 0]       [1 0 0]       [0]
                   [1 0 3] x_1 + [0 0 2] x_2 + [0 0 0] x_3 + [1]
                   [0 0 0]       [0 0 1]       [0 0 0]       [0]
        
        Following rules are strictly oriented:
        c#(f(z),f(c(a(),x,a())),y) = [4 0 0]     [0 1 0]     [1 2 1]     [6]              
                                     [2 0 0] x + [2 0 0] y + [2 4 2] z + [5]              
                                     [0 0 0]     [0 0 1]     [2 4 2]     [0]              
                                   > [4 0 0]     [0 1 0]     [1 2 1]     [5]              
                                     [0 0 0] x + [0 0 0] y + [2 0 0] z + [5]              
                                     [0 0 0]     [0 0 0]     [1 0 0]     [0]              
                                   = c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
        
        
        Following rules are (at-least) weakly oriented:
                          b#(y,z) =  [3 0 0]     [0 2 1]     [2]        
                                     [1 0 0] y + [0 0 0] z + [0]        
                                     [0 0 0]     [1 0 0]     [0]        
                                  >= [3 0 0]     [0 2 1]     [2]        
                                     [0 0 0] y + [0 0 0] z + [0]        
                                     [0 0 0]     [0 0 0]     [0]        
                                  =  c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
        
                           b(y,z) =  [0]                                
                                     [0]                                
                                     [0]                                
                                  >= [0]                                
                                     [0]                                
                                     [0]                                
                                  =  f(c(c(y,z,z),a(),a()))             
        
        c(f(z),f(c(a(),x,a())),y) =  [0 0 0]     [0 0 0]     [0]        
                                     [0 0 0] x + [0 0 0] z + [0]        
                                     [4 0 0]     [0 0 6]     [6]        
                                  >= [0]                                
                                     [0]                                
                                     [0]                                
                                  =  c(f(b(x,z)),c(z,y,a()),a())        
        
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
            c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
        - Weak TRS:
            b(y,z) -> f(c(c(y,z,z),a(),a()))
            c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
        - Signature:
            {b/2,c/3,b#/2,c#/3} / {a/0,f/1,c_1/2,c_2/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {b#,c#} and constructors {a,f}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))