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