YES(?,O(n^1))
TRS:
 {a a x -> a b a x}
 DUP: We consider a non-duplicating system.
  Trs:
   {a a x -> a b a x}
  BOUND:
   Bound: match(-raise)-bounded by 2
   Automaton:
    {
     b_2(7) -> 8*
     b_1(3) -> 4*
     b_0(1) -> 1*
     a_2(8) -> 9*
     a_2(6) -> 7*
     a_1(4) -> 5*
     a_1(2) -> 3*
     a_0(1) -> 1*
        9 -> 3*
        5 -> 3 | 1
        4 -> 6*
        1 -> 2*
    }
   Strict:
    {}
   Qed