We consider the following Problem:

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

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

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {f(a(), f(x, a())) -> f(a(), f(f(f(a(), a()), a()), x))}
    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(a(), f(x, a())) -> f(a(), f(f(f(a(), a()), a()), x))}
    StartTerms: basic terms
    Strategy: innermost
    
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component:
        {f(a(), f(x, a())) -> f(a(), f(f(f(a(), a()), a()), x))}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(f) = {}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         f(x1, x2) = [1 0 0] x1 + [0 0 1] x2 + [0]
                     [0 0 0]      [0 0 0]      [0]
                     [0 1 0]      [0 1 0]      [1]
         a() = [1]
               [2]
               [0]
      
      The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Weak Trs: {f(a(), f(x, a())) -> f(a(), f(f(f(a(), a()), a()), x))}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(O(1),O(1))
    
    Proof:
      We consider the following Problem:
      
        Weak Trs: {f(a(), f(x, a())) -> f(a(), f(f(f(a(), a()), a()), x))}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(O(1),O(1))
      
      Proof:
        Empty rules are trivially bounded

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