YES(?,O(n^2))
TRS:
 {f(x, f(y, a())) -> f(f(f(f(a(), x), y), a()), h a())}
 DUP: We consider a non-duplicating system.
  Trs:
   {f(x, f(y, a())) -> f(f(f(f(a(), x), y), a()), h a())}
  RLAB:
   Strict:
    {
     f([a,f])(x, f([f,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,f])(f([a,a])(a(), x), y), a()), h(a) a()),
     f([a,f])(x, f([h,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,h])(f([a,a])(a(), x), y), a()), h(a) a()),
     f([a,f])(x, f([a,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,a])(f([a,a])(a(), x), y), a()), h(a) a()),
     f([f,f])(x, f([f,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,f])(f([a,f])(a(), x), y), a()), h(a) a()),
     f([f,f])(x, f([h,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,h])(f([a,f])(a(), x), y), a()), h(a) a()),
     f([f,f])(x, f([a,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,a])(f([a,f])(a(), x), y), a()), h(a) a()),
     f([h,f])(x, f([f,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,f])(f([a,h])(a(), x), y), a()), h(a) a()),
     f([h,f])(x, f([h,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,h])(f([a,h])(a(), x), y), a()), h(a) a()),
     f([h,f])(x, f([a,a])(y, a())) ->
     f([f,h])(f([f,a])(f([f,a])(f([a,h])(a(), x), y), a()), h(a) a())
    }
   Weak:
    {}
   Matrix Interpretation:
    Interpretation class: triangular
          [0]
    [a] = [1]
    
           [X1]    [1 0][X1]   [0]
    [h(3)]([X0]) = [0 0][X0] + [0]
    
           [X3]  [X1]    [1 3][X3]   [1 3][X1]   [2]
    [f(8)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [2]
    
           [X3]  [X1]    [1 0][X3]   [1 3][X1]   [0]
    [f(7)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [1]
    
           [X3]  [X1]    [1 0][X3]   [1 1][X1]   [0]
    [f(6)]([X2], [X0]) = [0 1][X2] + [0 0][X0] + [0]
    
           [X3]  [X1]    [1 0][X3]   [1 0][X1]   [2]
    [f(5)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0]
    
           [X3]  [X1]    [1 0][X3]   [1 0][X1]   [0]
    [f(4)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0]
    
           [X3]  [X1]    [1 0][X3]   [1 1][X1]   [0]
    [f(2)]([X2], [X0]) = [0 1][X2] + [0 0][X0] + [3]
    
           [X3]  [X1]    [1 2][X3]   [1 1][X1]   [3]
    [f(1)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [2]
    
           [X3]  [X1]    [1 1][X3]   [1 2][X1]   [1]
    [f(0)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0]
    
    
    Qed