YES
TRS:
 {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
  f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
 DP:
  Strict:
   {f#(a(), f(b(), x)) -> f#(a(), x),
    f#(a(), f(b(), x)) -> f#(a(), f(a(), x)),
    f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))),
    f#(b(), f(a(), x)) -> f#(b(), x),
    f#(b(), f(a(), x)) -> f#(b(), f(b(), x)),
    f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
  Weak:
  {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
   f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
  EDG:
   {(f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))
    (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)))
    (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), x))
    (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))
    (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)))
    (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), x))
    (f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))
    (f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)))
    (f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), x))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))))
    (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), x))
    (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)))
    (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))))
    (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), x))
    (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)))
    (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))))}
   SCCS:
    Scc:
     {f#(b(), f(a(), x)) -> f#(b(), x),
      f#(b(), f(a(), x)) -> f#(b(), f(b(), x)),
      f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
    Scc:
     {f#(a(), f(b(), x)) -> f#(a(), x),
      f#(a(), f(b(), x)) -> f#(a(), f(a(), x)),
      f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
    SCC:
     Strict:
      {f#(b(), f(a(), x)) -> f#(b(), x),
       f#(b(), f(a(), x)) -> f#(b(), f(b(), x)),
       f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
     Weak:
     {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
      f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
     UR:
      {f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
      BOUND:
       Bound: match(-raise)-DP-bounded by 0
       Automaton:
        {     c_0() -> 3*
              b_0() -> 2*
         f#_0(2, 3) -> 1*
          f_0(2, 3) -> 3*}
       Strict:
        {f#(b(), f(a(), x)) -> f#(b(), f(b(), x)),
         f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
       EDG:
        {(f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))
         (f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)))
         (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), x)))
         (f#(b(), f(a(), x)) -> f#(b(), f(b(), x)), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))}
        SCCS:
         Scc:
          {f#(b(), f(a(), x)) -> f#(b(), f(b(), x)),
           f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
         SCC:
          Strict:
           {f#(b(), f(a(), x)) -> f#(b(), f(b(), x)),
            f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
          Weak:
          {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
           f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
          POLY:
           Argument Filtering:
            pi(b) = [], pi(a) = [], pi(f#) = 1, pi(f) = 0
           Usable Rules:
            {}
           Interpretation:
            [b] = 0,
            [a] = 1
           Strict:
            {}
           Weak:
            {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
             f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
           Qed
    SCC:
     Strict:
      {f#(a(), f(b(), x)) -> f#(a(), x),
       f#(a(), f(b(), x)) -> f#(a(), f(a(), x)),
       f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
     Weak:
     {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
      f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
     UR:
      {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x)))}
      BOUND:
       Bound: match(-raise)-DP-bounded by 0
       Automaton:
        {     d_0() -> 3*
              a_0() -> 2*
         f#_0(2, 3) -> 1*
          f_0(2, 3) -> 3*}
       Strict:
        {f#(a(), f(b(), x)) -> f#(a(), f(a(), x)),
         f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
       EDG:
        {(f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))))
         (f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)))
         (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), x)))
         (f#(a(), f(b(), x)) -> f#(a(), f(a(), x)), f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x))))}
        SCCS:
         Scc:
          {f#(a(), f(b(), x)) -> f#(a(), f(a(), x)),
           f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
         SCC:
          Strict:
           {f#(a(), f(b(), x)) -> f#(a(), f(a(), x)),
            f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
          Weak:
          {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
           f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
          POLY:
           Argument Filtering:
            pi(b) = [], pi(a) = [], pi(f#) = 1, pi(f) = [0]
           Usable Rules:
            {}
           Interpretation:
            [f](x0) = x0 + 1,
            [b] = 1,
            [a] = 0
           Strict:
            {}
           Weak:
            {f(a(), f(b(), x)) -> f(a(), f(a(), f(a(), x))),
             f(b(), f(a(), x)) -> f(b(), f(b(), f(b(), x)))}
           Qed