YES
Time: 0.018772
TRS:
 {f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))),
  f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x))}
 DP:
  DP:
   {f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))),
    f#(a(), f(b(), f(a(), x))) -> f#(b(), f(b(), f(a(), x)))}
  TRS:
  {f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))),
   f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x))}
  EDG:
   {(f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))), f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))))
    (f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))), f#(a(), f(b(), f(a(), x))) -> f#(b(), f(b(), f(a(), x))))}
   SCCS (1):
    Scc:
     {f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x))))}
    SCC (1):
     Strict:
      {f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x))))}
     Weak:
     {f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))),
      f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {       b_0() -> 11*
               a_0() -> 10*
        f#_0(10, 14) -> 5*
         f_0(14, 14) -> 9*
         f_0(14, 13) -> 9*
         f_0(14, 12) -> 9*
         f_0(14, 11) -> 9*
         f_0(14, 10) -> 9*
          f_0(14, 9) -> 9*
         f_0(13, 14) -> 9*
         f_0(13, 13) -> 9*
         f_0(13, 12) -> 9*
         f_0(13, 11) -> 9*
         f_0(13, 10) -> 9*
          f_0(13, 9) -> 9*
         f_0(12, 14) -> 9*
         f_0(12, 13) -> 9*
         f_0(12, 12) -> 9*
         f_0(12, 11) -> 9*
         f_0(12, 10) -> 9*
          f_0(12, 9) -> 9*
         f_0(11, 14) -> 9*
         f_0(11, 13) -> 14 | 9
         f_0(11, 12) -> 13*
         f_0(11, 11) -> 9*
         f_0(11, 10) -> 9*
          f_0(11, 9) -> 9*
         f_0(10, 14) -> 12*
         f_0(10, 13) -> 12*
         f_0(10, 12) -> 12*
         f_0(10, 11) -> 12*
         f_0(10, 10) -> 12*
          f_0(10, 9) -> 12*
          f_0(9, 14) -> 9*
          f_0(9, 13) -> 9*
          f_0(9, 12) -> 9*
          f_0(9, 11) -> 9*
          f_0(9, 10) -> 9*
           f_0(9, 9) -> 9*}
      Strict:
       {}
      Qed