YES
Time: 1.531975
TRS:
 {f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
 DP:
  DP:
   {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), x)),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), x),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(a(), f(b(), x))))),
    f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))}
  TRS:
  {f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
  EDG:
   {(f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(a(), f(b(), x))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), x))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), x)))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), x)))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), x))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(a(), f(b(), x))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), x)))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), x))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(a(), f(b(), x))))))
    (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
   SCCS (1):
    Scc:
     {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))),
      f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))),
      f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))}
    SCC (3):
     Strict:
      {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))),
       f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))),
       f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))}
     Weak:
     {f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 2
      Automaton:
       {       b_2() -> 31*
               b_1() -> 22*
               b_0() -> 14*
               a_2() -> 30*
               a_1() -> 21*
               a_0() -> 13*
        f#_2(30, 37) -> 5*
        f#_1(21, 34) -> 5*
        f#_1(21, 33) -> 5*
        f#_1(21, 28) -> 5*
        f#_0(13, 20) -> 5*
        f#_0(13, 17) -> 5*
        f#_0(13, 16) -> 5*
         f_2(31, 35) -> 36*
         f_2(31, 28) -> 32*
         f_2(30, 36) -> 37*
         f_2(30, 34) -> 35*
         f_2(30, 33) -> 34*
         f_2(30, 32) -> 33*
         f_1(22, 45) -> 28*
         f_1(22, 44) -> 25*
         f_1(22, 41) -> 42*
         f_1(22, 29) -> 24*
         f_1(22, 26) -> 27*
         f_1(22, 25) -> 38*
         f_1(22, 20) -> 23*
         f_1(22, 19) -> 23*
         f_1(22, 18) -> 23*
         f_1(22, 17) -> 23*
         f_1(22, 16) -> 23*
         f_1(22, 15) -> 23*
         f_1(22, 14) -> 23*
         f_1(22, 13) -> 23*
         f_1(22, 12) -> 23*
         f_1(21, 43) -> 44*
         f_1(21, 42) -> 43*
         f_1(21, 40) -> 41*
         f_1(21, 39) -> 40*
         f_1(21, 38) -> 39*
         f_1(21, 37) -> 45*
         f_1(21, 28) -> 44 | 29
         f_1(21, 27) -> 28*
         f_1(21, 25) -> 41 | 26
         f_1(21, 24) -> 40 | 25
         f_1(21, 23) -> 24*
         f_0(20, 20) -> 12*
         f_0(20, 19) -> 12*
         f_0(20, 18) -> 12*
         f_0(20, 17) -> 12*
         f_0(20, 16) -> 12*
         f_0(20, 15) -> 12*
         f_0(20, 14) -> 12*
         f_0(20, 13) -> 12*
         f_0(20, 12) -> 12*
         f_0(19, 20) -> 12*
         f_0(19, 19) -> 12*
         f_0(19, 18) -> 12*
         f_0(19, 17) -> 12*
         f_0(19, 16) -> 12*
         f_0(19, 15) -> 12*
         f_0(19, 14) -> 12*
         f_0(19, 13) -> 12*
         f_0(19, 12) -> 12*
         f_0(18, 20) -> 12*
         f_0(18, 19) -> 12*
         f_0(18, 18) -> 12*
         f_0(18, 17) -> 12*
         f_0(18, 16) -> 12*
         f_0(18, 15) -> 12*
         f_0(18, 14) -> 12*
         f_0(18, 13) -> 12*
         f_0(18, 12) -> 12*
         f_0(17, 20) -> 12*
         f_0(17, 19) -> 12*
         f_0(17, 18) -> 12*
         f_0(17, 17) -> 12*
         f_0(17, 16) -> 12*
         f_0(17, 15) -> 12*
         f_0(17, 14) -> 12*
         f_0(17, 13) -> 12*
         f_0(17, 12) -> 12*
         f_0(16, 20) -> 12*
         f_0(16, 19) -> 12*
         f_0(16, 18) -> 12*
         f_0(16, 17) -> 12*
         f_0(16, 16) -> 12*
         f_0(16, 15) -> 12*
         f_0(16, 14) -> 12*
         f_0(16, 13) -> 12*
         f_0(16, 12) -> 12*
         f_0(15, 20) -> 12*
         f_0(15, 19) -> 12*
         f_0(15, 18) -> 12*
         f_0(15, 17) -> 12*
         f_0(15, 16) -> 12*
         f_0(15, 15) -> 12*
         f_0(15, 14) -> 12*
         f_0(15, 13) -> 12*
         f_0(15, 12) -> 12*
         f_0(14, 20) -> 15*
         f_0(14, 19) -> 15*
         f_0(14, 18) -> 19*
         f_0(14, 17) -> 15*
         f_0(14, 16) -> 15*
         f_0(14, 15) -> 15*
         f_0(14, 14) -> 15*
         f_0(14, 13) -> 15*
         f_0(14, 12) -> 15*
         f_0(13, 20) -> 17*
         f_0(13, 19) -> 20*
         f_0(13, 18) -> 12*
         f_0(13, 17) -> 18*
         f_0(13, 16) -> 17*
         f_0(13, 15) -> 18 | 17 | 16 | 12
         f_0(13, 14) -> 12*
         f_0(13, 13) -> 12*
         f_0(13, 12) -> 12*
         f_0(12, 20) -> 12*
         f_0(12, 19) -> 12*
         f_0(12, 18) -> 12*
         f_0(12, 17) -> 12*
         f_0(12, 16) -> 12*
         f_0(12, 15) -> 12*
         f_0(12, 14) -> 12*
         f_0(12, 13) -> 12*
         f_0(12, 12) -> 12*}
      Strict:
       {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))),
        f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x)))}
      EDG:
       {(f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))))
        (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))))
        (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))))
        (f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))))}
       SCCS (1):
        Scc:
         {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))),
          f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x)))}
        SCC (2):
         Strict:
          {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(a(), f(b(), x)))),
           f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x)))}
         Weak:
         {f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 2
          Automaton:
           {       b_2() -> 25*
                   b_1() -> 16*
                   b_0() -> 11*
                   a_2() -> 24*
                   a_1() -> 15*
                   a_0() -> 10*
            f#_2(24, 28) -> 5*
            f#_2(24, 27) -> 5*
            f#_1(15, 27) -> 5*
            f#_1(15, 19) -> 5*
            f#_1(15, 18) -> 5*
            f#_0(10, 14) -> 5*
             f_2(25, 19) -> 26*
             f_2(24, 27) -> 28*
             f_2(24, 26) -> 27*
             f_1(16, 39) -> 22*
             f_1(16, 36) -> 37*
             f_1(16, 32) -> 19*
             f_1(16, 29) -> 30*
             f_1(16, 23) -> 18*
             f_1(16, 22) -> 33*
             f_1(16, 20) -> 21*
             f_1(16, 14) -> 17*
             f_1(16, 13) -> 17*
             f_1(16, 12) -> 17*
             f_1(16, 11) -> 17*
             f_1(16, 10) -> 17*
              f_1(16, 9) -> 17*
             f_1(15, 38) -> 39*
             f_1(15, 37) -> 38*
             f_1(15, 35) -> 36*
             f_1(15, 34) -> 35*
             f_1(15, 33) -> 34*
             f_1(15, 31) -> 32*
             f_1(15, 30) -> 31*
             f_1(15, 28) -> 29*
             f_1(15, 22) -> 32 | 23
             f_1(15, 21) -> 22*
             f_1(15, 19) -> 29 | 20
             f_1(15, 18) -> 28 | 19
             f_1(15, 17) -> 18*
             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) -> 12*
             f_0(11, 13) -> 12*
             f_0(11, 12) -> 12*
             f_0(11, 11) -> 12*
             f_0(11, 10) -> 12*
              f_0(11, 9) -> 12*
             f_0(10, 14) -> 9*
             f_0(10, 13) -> 14*
             f_0(10, 12) -> 14 | 13 | 9
             f_0(10, 11) -> 9*
             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) -> 9*
              f_0(9, 10) -> 9*
               f_0(9, 9) -> 9*}
          Strict:
           {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x)))}
          EDG:
           {(f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))), f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x))))}
           SCCS (1):
            Scc:
             {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x)))}
            SCC (1):
             Strict:
              {f#(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f#(a(), f(a(), f(b(), x)))}
             Weak:
             {f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) -> f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
             BOUND:
              Bound: match(-raise)-DP-bounded by 1
              Automaton:
               {       b_1() -> 14*
                       b_0() -> 10*
                       a_1() -> 13*
                       a_0() -> 9*
                f#_1(13, 16) -> 5*
                 f#_0(9, 12) -> 5*
                 f_1(14, 12) -> 15*
                 f_1(14, 11) -> 15*
                 f_1(14, 10) -> 15*
                  f_1(14, 9) -> 15*
                  f_1(14, 8) -> 15*
                 f_1(13, 15) -> 16*
                 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) -> 11*
                 f_0(10, 11) -> 11*
                 f_0(10, 10) -> 11*
                  f_0(10, 9) -> 11*
                  f_0(10, 8) -> 11*
                  f_0(9, 12) -> 8*
                  f_0(9, 11) -> 12 | 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:
               {}
              Qed