YES
Time: 0.049047
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:
  DP:
   {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)))}
  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)))}
  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 (2):
    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 (3):
     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)))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {      b_0() -> 9*
              a_0() -> 8*
        f#_0(9, 10) -> 5*
        f_0(10, 10) -> 7*
         f_0(10, 9) -> 7*
         f_0(10, 8) -> 7*
         f_0(10, 7) -> 7*
         f_0(9, 10) -> 10*
          f_0(9, 9) -> 10*
          f_0(9, 8) -> 10*
          f_0(9, 7) -> 10*
         f_0(8, 10) -> 7*
          f_0(8, 9) -> 7*
          f_0(8, 8) -> 7*
          f_0(8, 7) -> 7*
         f_0(7, 10) -> 7*
          f_0(7, 9) -> 7*
          f_0(7, 8) -> 7*
          f_0(7, 7) -> 7*}
      Strict:
       {f#(b(), f(a(), x)) -> f#(b(), x),
        f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
      EDG:
       {(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(), 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(), f(b(), x))), f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x))))}
       SCCS (1):
        Scc:
         {f#(b(), f(a(), x)) -> f#(b(), x),
          f#(b(), f(a(), x)) -> f#(b(), f(b(), f(b(), x)))}
        SCC (2):
         Strict:
          {f#(b(), f(a(), x)) -> 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)))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 0
          Automaton:
           {       b_0() -> 10*
                   a_0() -> 9*
            f#_0(10, 12) -> 5*
             f_0(12, 12) -> 8*
             f_0(12, 11) -> 8*
             f_0(12, 10) -> 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) -> 8*
              f_0(11, 9) -> 8*
              f_0(11, 8) -> 8*
             f_0(10, 12) -> 12 | 11
             f_0(10, 11) -> 12*
             f_0(10, 10) -> 11*
              f_0(10, 9) -> 11*
              f_0(10, 8) -> 11*
              f_0(9, 12) -> 8*
              f_0(9, 11) -> 8*
              f_0(9, 10) -> 8*
               f_0(9, 9) -> 8*
               f_0(9, 8) -> 8*
              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:
           {f#(b(), f(a(), x)) -> f#(b(), x)}
          EDG:
           {(f#(b(), f(a(), x)) -> f#(b(), x), f#(b(), f(a(), x)) -> f#(b(), x))}
           SCCS (1):
            Scc:
             {f#(b(), f(a(), x)) -> f#(b(), x)}
            SCC (1):
             Strict:
              {f#(b(), f(a(), x)) -> 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)))}
             SPSC:
              Simple Projection:
               pi(f#) = 1
              Strict:
               {}
              Qed
    SCC (3):
     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)))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {      b_0() -> 9*
              a_0() -> 8*
        f#_0(8, 10) -> 5*
        f_0(10, 10) -> 7*
         f_0(10, 9) -> 7*
         f_0(10, 8) -> 7*
         f_0(10, 7) -> 7*
         f_0(9, 10) -> 7*
          f_0(9, 9) -> 7*
          f_0(9, 8) -> 7*
          f_0(9, 7) -> 7*
         f_0(8, 10) -> 10*
          f_0(8, 9) -> 10*
          f_0(8, 8) -> 10*
          f_0(8, 7) -> 10*
         f_0(7, 10) -> 7*
          f_0(7, 9) -> 7*
          f_0(7, 8) -> 7*
          f_0(7, 7) -> 7*}
      Strict:
       {f#(a(), f(b(), x)) -> f#(a(), x),
        f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
      EDG:
       {(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(), 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(), 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))))}
       SCCS (1):
        Scc:
         {f#(a(), f(b(), x)) -> f#(a(), x),
          f#(a(), f(b(), x)) -> f#(a(), f(a(), f(a(), x)))}
        SCC (2):
         Strict:
          {f#(a(), f(b(), x)) -> 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)))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 0
          Automaton:
           {      b_0() -> 10*
                  a_0() -> 9*
            f#_0(9, 12) -> 5*
            f_0(12, 12) -> 8*
            f_0(12, 11) -> 8*
            f_0(12, 10) -> 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) -> 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 | 11
             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:
           {f#(a(), f(b(), x)) -> f#(a(), x)}
          EDG:
           {(f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x))}
           SCCS (1):
            Scc:
             {f#(a(), f(b(), x)) -> f#(a(), x)}
            SCC (1):
             Strict:
              {f#(a(), f(b(), x)) -> 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)))}
             SPSC:
              Simple Projection:
               pi(f#) = 1
              Strict:
               {}
              Qed