We consider the following Problem:

  Strict Trs:
    {  f(b(a(), z)) -> z
     , b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))
     , f(f(f(c(z, x, a())))) -> b(f(x), z)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  f(b(a(), z)) -> z
       , b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))
       , f(f(f(c(z, x, a())))) -> b(f(x), z)}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
    
      The weightgap principle does not apply
    
    We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
    
    Strict Trs:
      {  f(b(a(), z)) -> z
       , b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))
       , f(f(f(c(z, x, a())))) -> b(f(x), z)}
    StartTerms: basic terms
    Strategy: innermost
    
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {f(f(f(c(z, x, a())))) -> b(f(x), z)}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(f) = {}, Uargs(b) = {1, 2}, Uargs(c) = {}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         f(x1) = [1 1 0] x1 + [1]
                 [0 0 1]      [1]
                 [0 0 0]      [1]
         b(x1, x2) = [1 0 0] x1 + [1 1 0] x2 + [0]
                     [0 0 0]      [0 0 0]      [0]
                     [0 0 0]      [0 0 0]      [0]
         a() = [0]
               [0]
               [0]
         c(x1, x2, x3) = [1 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0]
                         [0 0 0]      [0 0 0]      [0 0 0]      [0]
                         [0 1 0]      [1 1 0]      [0 0 0]      [0]
      
      The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  f(b(a(), z)) -> z
         , b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
      Weak Trs: {f(f(f(c(z, x, a())))) -> b(f(x), z)}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
      
        The weightgap principle does not apply
      
      We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
      
      Strict Trs:
        {  f(b(a(), z)) -> z
         , b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
      Weak Trs: {f(f(f(c(z, x, a())))) -> b(f(x), z)}
      StartTerms: basic terms
      Strategy: innermost
      
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component:
          {b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(f) = {}, Uargs(b) = {1, 2}, Uargs(c) = {}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           f(x1) = [1 0 1] x1 + [0]
                   [0 0 0]      [0]
                   [0 1 0]      [1]
           b(x1, x2) = [1 0 0] x1 + [1 0 1] x2 + [0]
                       [0 0 0]      [0 0 0]      [0]
                       [0 1 0]      [0 0 0]      [0]
           a() = [0]
                 [1]
                 [0]
           c(x1, x2, x3) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [0]
                           [1 0 1]      [0 0 1]      [0 0 0]      [0]
                           [0 0 0]      [0 0 0]      [0 0 0]      [0]
        
        The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs: {f(b(a(), z)) -> z}
        Weak Trs:
          {  b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))
           , f(f(f(c(z, x, a())))) -> b(f(x), z)}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        We consider the following Problem:
        
          Strict Trs: {f(b(a(), z)) -> z}
          Weak Trs:
            {  b(y, b(a(), z)) -> b(f(c(y, y, a())), b(f(z), a()))
             , f(f(f(c(z, x, a())))) -> b(f(x), z)}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^1))
        
        Proof:
          The following argument positions are usable:
            Uargs(f) = {}, Uargs(b) = {1, 2}, Uargs(c) = {}
          We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           f(x1) = [0 1] x1 + [0]
                   [2 2]      [0]
           b(x1, x2) = [2 0] x1 + [2 1] x2 + [0]
                       [0 0]      [2 2]      [1]
           a() = [0]
                 [0]
           c(x1, x2, x3) = [1 1] x1 + [0 1] x2 + [0 0] x3 + [1]
                           [0 0]      [0 0]      [0 0]      [0]

Hurray, we answered YES(?,O(n^1))