YES
O(n)
TRS:
 {f(x, f(a(), a())) -> f(f(f(a(), a()), a()), f(a(), x))}
 DUP: We consider a non-duplicating system.
  Trs:
   {f(x, f(a(), a())) -> f(f(f(a(), a()), a()), f(a(), x))}
  BOUND:
   Automaton:
    {
           a_2() -> 11,
           a_1() -> 3,
           a_0() -> 2,
     f_2(13, 14) -> 6,
     f_2(12, 11) -> 13,
     f_2(11, 11) -> 12,
      f_2(11, 5) -> 14,
       f_1(5, 6) -> 2,
       f_1(5, 4) -> 6,
       f_1(4, 3) -> 5,
       f_1(3, 5) -> 6,
       f_1(3, 3) -> 4,
       f_1(3, 2) -> 6,
       f_0(2, 2) -> 2
    }
   Strict:
    {}
   Qed