YES
TRS:
 {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
  f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
 DP:
  Strict:
   {        f#(f(f(a(), x), b()), b()) -> f#(x, b()),
            f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()),
            f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()),
            f#(f(f(a(), x), b()), b()) -> f#(a(), f(f(x, b()), b())),
    f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()),
    f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x),
    f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)),
    f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x)))}
  Weak:
  {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
   f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
  EDG:
   {(f#(f(f(a(), x), b()), b()) -> f#(x, b()), f#(f(f(a(), x), b()), b()) -> f#(a(), f(f(x, b()), b())))
    (f#(f(f(a(), x), b()), b()) -> f#(x, b()), f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()))
    (f#(f(f(a(), x), b()), b()) -> f#(x, b()), f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()))
    (f#(f(f(a(), x), b()), b()) -> f#(x, b()), f#(f(f(a(), x), b()), b()) -> f#(x, b()))
    (f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()), f#(f(f(a(), x), b()), b()) -> f#(a(), f(f(x, b()), b())))
    (f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()), f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()))
    (f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()), f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()))
    (f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()), f#(f(f(a(), x), b()), b()) -> f#(x, b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()), f#(f(f(a(), x), b()), b()) -> f#(x, b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()), f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()), f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()), f#(f(f(a(), x), b()), b()) -> f#(a(), f(f(x, b()), b())))
    (f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()), f#(f(f(a(), x), b()), b()) -> f#(x, b()))
    (f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()), f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()))
    (f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()), f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()))
    (f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()), f#(f(f(a(), x), b()), b()) -> f#(a(), f(f(x, b()), b())))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(f(a(), f(a(), f(a(), x))), b()))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)))
    (f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))))}
   SCCS:
    Scc:
     {f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x),
      f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)),
      f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x)))}
    Scc:
     {f#(f(f(a(), x), b()), b()) -> f#(x, b()),
      f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()),
      f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b())}
    SCC:
     Strict:
      {f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), x),
       f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), x)),
       f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x)))}
     Weak:
     {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
      f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
     POLY:
      Argument Filtering:
       pi(b) = [], pi(a) = [], pi(f#) = 1, pi(f) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [f](x0, x1) = x0 + x1,
       [b] = 0,
       [a] = 1
      Strict:
       {f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x)))}
      Weak:
       {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
        f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
      EDG:
       {(f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))), f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x))))}
       SCCS:
        Scc:
         {f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x)))}
        SCC:
         Strict:
          {f#(a(), f(a(), f(a(), f(x, b())))) -> f#(a(), f(a(), f(a(), x)))}
         Weak:
         {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
          f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
         UR:
          {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
           f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
          BOUND:
           Bound: match(-raise)-DP-bounded by 1
           Automaton:
            {       b_1() -> 12*
                    b_0() -> 10*
                    a_1() -> 13*
                    a_0() -> 9*
             f#_1(13, 15) -> 5*
              f#_0(9, 12) -> 5*
              f_1(15, 12) -> 13*
              f_1(14, 12) -> 13*
              f_1(13, 15) -> 13*
              f_1(13, 14) -> 15*
              f_1(13, 12) -> 15 | 14 | 13
              f_1(13, 11) -> 14*
              f_1(13, 10) -> 14*
               f_1(13, 9) -> 14*
               f_1(13, 8) -> 14*
              f_1(12, 12) -> 13*
              f_1(11, 12) -> 13*
              f_1(10, 12) -> 13*
               f_1(9, 12) -> 13*
               f_1(8, 12) -> 13*
              f_0(12, 12) -> 8*
              f_0(12, 11) -> 8*
              f_0(12, 10) -> 12 | 8
               f_0(12, 9) -> 8*
               f_0(12, 8) -> 8*
              f_0(11, 12) -> 8*
              f_0(11, 11) -> 8*
              f_0(11, 10) -> 12 | 8
               f_0(11, 9) -> 8*
               f_0(11, 8) -> 8*
              f_0(10, 12) -> 8*
              f_0(10, 11) -> 8*
              f_0(10, 10) -> 8*
               f_0(10, 9) -> 8*
               f_0(10, 8) -> 8*
               f_0(9, 12) -> 12*
               f_0(9, 11) -> 12*
               f_0(9, 10) -> 11*
                f_0(9, 9) -> 11*
                f_0(9, 8) -> 11*
               f_0(8, 12) -> 8*
               f_0(8, 11) -> 8*
               f_0(8, 10) -> 8*
                f_0(8, 9) -> 8*
                f_0(8, 8) -> 8*}
           Strict:
            {}
           Qed
    SCC:
     Strict:
      {f#(f(f(a(), x), b()), b()) -> f#(x, b()),
       f#(f(f(a(), x), b()), b()) -> f#(f(x, b()), b()),
       f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b())}
     Weak:
     {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
      f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
     POLY:
      Argument Filtering:
       pi(b) = [], pi(a) = [], pi(f#) = 0, pi(f) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [f](x0, x1) = x0 + x1,
       [b] = 0,
       [a] = 1
      Strict:
       {f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b())}
      Weak:
       {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
        f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
      EDG:
       {(f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()), f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b()))}
       SCCS:
        Scc:
         {f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b())}
        SCC:
         Strict:
          {f#(f(f(a(), x), b()), b()) -> f#(f(a(), f(f(x, b()), b())), b())}
         Weak:
         {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
          f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
         UR:
          {        f(f(f(a(), x), b()), b()) -> f(f(a(), f(f(x, b()), b())), b()),
           f(a(), f(a(), f(a(), f(x, b())))) -> f(f(a(), f(a(), f(a(), x))), b())}
          BOUND:
           Bound: match(-raise)-DP-bounded by 0
           Automaton:
            {       b_0() -> 11*
                    a_0() -> 10*
             f#_0(14, 11) -> 5*
              f_0(14, 14) -> 9*
              f_0(14, 13) -> 9*
              f_0(14, 12) -> 9*
              f_0(14, 11) -> 13 | 12 | 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) -> 13*
              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) -> 13*
              f_0(12, 10) -> 9*
               f_0(12, 9) -> 9*
              f_0(11, 14) -> 9*
              f_0(11, 13) -> 9*
              f_0(11, 12) -> 9*
              f_0(11, 11) -> 12*
              f_0(11, 10) -> 9*
               f_0(11, 9) -> 9*
              f_0(10, 14) -> 9*
              f_0(10, 13) -> 14*
              f_0(10, 12) -> 9*
              f_0(10, 11) -> 12*
              f_0(10, 10) -> 9*
               f_0(10, 9) -> 9*
               f_0(9, 14) -> 9*
               f_0(9, 13) -> 9*
               f_0(9, 12) -> 9*
               f_0(9, 11) -> 12 | 9
               f_0(9, 10) -> 9*
                f_0(9, 9) -> 9*}
           Strict:
            {}
           Qed