YES
Time: 0.089483
TRS:
 {  f(X, X) -> c X,
  f(X, c X) -> f(s X, X),
  f(s X, X) -> f(X, a X)}
 BOUND:
  Bound: roof(-raise)-bounded by 3
  Automaton:
   {    c_3(20) -> 1*
        c_3(19) -> 1*
        c_3(18) -> 1*
        c_3(15) -> 1*
        c_3(14) -> 1*
        c_3(13) -> 1*
        c_3(11) -> 1*
        c_3(10) -> 1*
        c_2(20) -> 1*
        c_2(19) -> 1*
        c_2(18) -> 1*
        c_2(15) -> 1*
        c_2(14) -> 1*
        c_2(13) -> 1*
        c_2(12) -> 1*
        c_2(11) -> 1*
        c_2(10) -> 1*
         c_2(5) -> 1*
         c_2(4) -> 1*
        c_1(20) -> 1*
        c_1(19) -> 1*
        c_1(18) -> 1*
        c_1(15) -> 1*
        c_1(14) -> 1*
        c_1(13) -> 1*
        c_1(12) -> 1*
        c_1(11) -> 1*
        c_1(10) -> 1*
         c_1(5) -> 1*
         c_1(4) -> 1*
         c_1(1) -> 1*
        c_0(20) -> 1*
        c_0(19) -> 1*
        c_0(18) -> 1*
        c_0(15) -> 1*
        c_0(14) -> 1*
        c_0(13) -> 1*
        c_0(12) -> 1*
        c_0(11) -> 1*
        c_0(10) -> 1*
         c_0(5) -> 1*
         c_0(4) -> 1*
         c_0(1) -> 1*
        s_2(11) -> 11* | 9 | 4 | 3 | 1
         s_2(4) -> 11* | 9 | 4 | 3 | 1
        s_1(20) -> 4* | 3 | 1
        s_1(19) -> 4* | 3 | 1
        s_1(18) -> 4* | 3 | 1
        s_1(15) -> 4* | 3 | 1
        s_1(14) -> 4* | 3 | 1
        s_1(13) -> 4* | 3 | 1
        s_1(12) -> 4* | 3 | 1
        s_1(11) -> 4* | 3 | 1
        s_1(10) -> 4* | 3 | 1
         s_1(5) -> 4* | 3 | 1
         s_1(4) -> 4* | 3 | 1
         s_1(1) -> 4* | 3 | 1
        s_0(20) -> 1*
        s_0(19) -> 1*
        s_0(18) -> 1*
        s_0(15) -> 1*
        s_0(14) -> 1*
        s_0(13) -> 1*
        s_0(12) -> 1*
        s_0(11) -> 1*
        s_0(10) -> 1*
         s_0(5) -> 1*
         s_0(4) -> 1*
         s_0(1) -> 1*
        a_3(11) -> 20* | 19 | 18 | 17 | 16 | 14 | 12 | 10 | 7 | 6 | 5 | 2 | 1
         a_3(4) -> 18* | 16 | 14 | 12 | 10 | 7 | 6 | 5 | 2 | 1
        a_2(20) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(19) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(18) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(15) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(14) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(13) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(12) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_2(11) -> 14* | 12 | 10 | 7 | 6 | 5 | 2 | 1
        a_2(10) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
         a_2(5) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
         a_2(4) -> 14* | 12 | 10 | 7 | 6 | 5 | 2 | 1
         a_2(1) -> 10* | 6 | 5 | 2 | 1
        a_1(20) -> 5* | 2 | 1
        a_1(19) -> 5* | 2 | 1
        a_1(18) -> 5* | 2 | 1
        a_1(15) -> 5* | 2 | 1
        a_1(14) -> 5* | 2 | 1
        a_1(13) -> 5* | 2 | 1
        a_1(12) -> 5* | 2 | 1
        a_1(11) -> 5* | 2 | 1
        a_1(10) -> 5* | 2 | 1
         a_1(5) -> 5* | 2 | 1
         a_1(4) -> 5* | 2 | 1
         a_1(1) -> 5* | 2 | 1
        a_0(20) -> 1*
        a_0(19) -> 1*
        a_0(18) -> 1*
        a_0(15) -> 1*
        a_0(14) -> 1*
        a_0(13) -> 1*
        a_0(12) -> 1*
        a_0(11) -> 1*
        a_0(10) -> 1*
         a_0(5) -> 1*
         a_0(4) -> 1*
         a_0(1) -> 1*
    f_3(11, 20) -> 1*
    f_3(11, 19) -> 1*
    f_3(11, 18) -> 1*
    f_3(11, 17) -> 1*
    f_3(11, 16) -> 1*
     f_3(4, 20) -> 1*
     f_3(4, 18) -> 1*
     f_3(4, 16) -> 1*
    f_2(20, 20) -> 1*
    f_2(20, 19) -> 1*
    f_2(20, 18) -> 1*
    f_2(20, 15) -> 1*
    f_2(20, 14) -> 1*
    f_2(20, 13) -> 1*
    f_2(20, 10) -> 1*
     f_2(20, 8) -> 1*
     f_2(20, 6) -> 1*
    f_2(19, 20) -> 1*
    f_2(19, 19) -> 1*
    f_2(19, 18) -> 1*
    f_2(19, 15) -> 1*
    f_2(19, 14) -> 1*
    f_2(19, 13) -> 1*
    f_2(19, 10) -> 1*
     f_2(19, 8) -> 1*
     f_2(19, 6) -> 1*
    f_2(18, 20) -> 1*
    f_2(18, 19) -> 1*
    f_2(18, 18) -> 1*
    f_2(18, 15) -> 1*
    f_2(18, 14) -> 1*
    f_2(18, 13) -> 1*
    f_2(18, 10) -> 1*
     f_2(18, 8) -> 1*
     f_2(18, 6) -> 1*
    f_2(15, 20) -> 1*
    f_2(15, 19) -> 1*
    f_2(15, 18) -> 1*
    f_2(15, 15) -> 1*
    f_2(15, 14) -> 1*
    f_2(15, 13) -> 1*
    f_2(15, 10) -> 1*
     f_2(15, 8) -> 1*
     f_2(15, 6) -> 1*
    f_2(14, 20) -> 1*
    f_2(14, 19) -> 1*
    f_2(14, 18) -> 1*
    f_2(14, 15) -> 1*
    f_2(14, 14) -> 1*
    f_2(14, 13) -> 1*
    f_2(14, 10) -> 1*
     f_2(14, 8) -> 1*
     f_2(14, 6) -> 1*
    f_2(13, 20) -> 1*
    f_2(13, 19) -> 1*
    f_2(13, 18) -> 1*
    f_2(13, 15) -> 1*
    f_2(13, 14) -> 1*
    f_2(13, 13) -> 1*
    f_2(13, 10) -> 1*
     f_2(13, 8) -> 1*
     f_2(13, 6) -> 1*
    f_2(12, 20) -> 1*
    f_2(12, 19) -> 1*
    f_2(12, 18) -> 1*
    f_2(12, 15) -> 1*
    f_2(12, 14) -> 1*
    f_2(12, 13) -> 1*
    f_2(12, 10) -> 1*
     f_2(12, 8) -> 1*
     f_2(12, 6) -> 1*
    f_2(11, 20) -> 1*
    f_2(11, 19) -> 1*
    f_2(11, 18) -> 1*
    f_2(11, 15) -> 1*
    f_2(11, 14) -> 1*
    f_2(11, 12) -> 1*
    f_2(11, 11) -> 1*
    f_2(11, 10) -> 1*
     f_2(11, 7) -> 1*
     f_2(11, 6) -> 1*
     f_2(11, 4) -> 1*
    f_2(10, 20) -> 1*
    f_2(10, 19) -> 1*
    f_2(10, 18) -> 1*
    f_2(10, 15) -> 1*
    f_2(10, 14) -> 1*
    f_2(10, 13) -> 1*
    f_2(10, 10) -> 1*
     f_2(10, 8) -> 1*
     f_2(10, 6) -> 1*
     f_2(9, 11) -> 1*
      f_2(9, 4) -> 1*
     f_2(5, 20) -> 1*
     f_2(5, 19) -> 1*
     f_2(5, 18) -> 1*
     f_2(5, 15) -> 1*
     f_2(5, 14) -> 1*
     f_2(5, 13) -> 1*
     f_2(5, 10) -> 1*
      f_2(5, 8) -> 1*
      f_2(5, 6) -> 1*
     f_2(4, 20) -> 1*
     f_2(4, 19) -> 1*
     f_2(4, 18) -> 1*
     f_2(4, 15) -> 1*
     f_2(4, 14) -> 1*
     f_2(4, 12) -> 1*
     f_2(4, 10) -> 1*
      f_2(4, 7) -> 1*
      f_2(4, 6) -> 1*
     f_2(1, 20) -> 1*
     f_2(1, 19) -> 1*
     f_2(1, 18) -> 1*
     f_2(1, 15) -> 1*
     f_2(1, 14) -> 1*
     f_2(1, 10) -> 1*
      f_2(1, 6) -> 1*
    f_1(20, 20) -> 1*
    f_1(20, 19) -> 1*
    f_1(20, 18) -> 1*
    f_1(20, 15) -> 1*
    f_1(20, 14) -> 1*
    f_1(20, 13) -> 1*
    f_1(20, 12) -> 1*
    f_1(20, 10) -> 1*
     f_1(20, 5) -> 1*
     f_1(20, 2) -> 1*
    f_1(19, 20) -> 1*
    f_1(19, 19) -> 1*
    f_1(19, 18) -> 1*
    f_1(19, 15) -> 1*
    f_1(19, 14) -> 1*
    f_1(19, 13) -> 1*
    f_1(19, 12) -> 1*
    f_1(19, 10) -> 1*
     f_1(19, 5) -> 1*
     f_1(19, 2) -> 1*
    f_1(18, 20) -> 1*
    f_1(18, 19) -> 1*
    f_1(18, 18) -> 1*
    f_1(18, 15) -> 1*
    f_1(18, 14) -> 1*
    f_1(18, 13) -> 1*
    f_1(18, 12) -> 1*
    f_1(18, 10) -> 1*
     f_1(18, 5) -> 1*
     f_1(18, 2) -> 1*
    f_1(15, 20) -> 1*
    f_1(15, 19) -> 1*
    f_1(15, 18) -> 1*
    f_1(15, 15) -> 1*
    f_1(15, 14) -> 1*
    f_1(15, 13) -> 1*
    f_1(15, 12) -> 1*
    f_1(15, 10) -> 1*
     f_1(15, 5) -> 1*
     f_1(15, 2) -> 1*
    f_1(14, 20) -> 1*
    f_1(14, 19) -> 1*
    f_1(14, 18) -> 1*
    f_1(14, 15) -> 1*
    f_1(14, 14) -> 1*
    f_1(14, 13) -> 1*
    f_1(14, 12) -> 1*
    f_1(14, 10) -> 1*
     f_1(14, 5) -> 1*
     f_1(14, 2) -> 1*
    f_1(13, 20) -> 1*
    f_1(13, 19) -> 1*
    f_1(13, 18) -> 1*
    f_1(13, 15) -> 1*
    f_1(13, 14) -> 1*
    f_1(13, 13) -> 1*
    f_1(13, 12) -> 1*
    f_1(13, 10) -> 1*
     f_1(13, 5) -> 1*
     f_1(13, 2) -> 1*
    f_1(12, 20) -> 1*
    f_1(12, 19) -> 1*
    f_1(12, 18) -> 1*
    f_1(12, 15) -> 1*
    f_1(12, 14) -> 1*
    f_1(12, 13) -> 1*
    f_1(12, 12) -> 1*
    f_1(12, 10) -> 1*
     f_1(12, 5) -> 1*
     f_1(12, 2) -> 1*
    f_1(11, 20) -> 1*
    f_1(11, 19) -> 1*
    f_1(11, 18) -> 1*
    f_1(11, 15) -> 1*
    f_1(11, 14) -> 1*
    f_1(11, 13) -> 1*
    f_1(11, 12) -> 1*
    f_1(11, 11) -> 1*
    f_1(11, 10) -> 1*
     f_1(11, 5) -> 1*
     f_1(11, 4) -> 1*
     f_1(11, 2) -> 1*
     f_1(11, 1) -> 1*
    f_1(10, 20) -> 1*
    f_1(10, 19) -> 1*
    f_1(10, 18) -> 1*
    f_1(10, 15) -> 1*
    f_1(10, 14) -> 1*
    f_1(10, 13) -> 1*
    f_1(10, 12) -> 1*
    f_1(10, 10) -> 1*
     f_1(10, 5) -> 1*
     f_1(10, 2) -> 1*
     f_1(5, 20) -> 1*
     f_1(5, 19) -> 1*
     f_1(5, 18) -> 1*
     f_1(5, 15) -> 1*
     f_1(5, 14) -> 1*
     f_1(5, 13) -> 1*
     f_1(5, 12) -> 1*
     f_1(5, 10) -> 1*
      f_1(5, 5) -> 1*
      f_1(5, 2) -> 1*
     f_1(4, 20) -> 1*
     f_1(4, 19) -> 1*
     f_1(4, 18) -> 1*
     f_1(4, 15) -> 1*
     f_1(4, 14) -> 1*
     f_1(4, 13) -> 1*
     f_1(4, 12) -> 1*
     f_1(4, 11) -> 1*
     f_1(4, 10) -> 1*
      f_1(4, 5) -> 1*
      f_1(4, 4) -> 1*
      f_1(4, 2) -> 1*
      f_1(4, 1) -> 1*
     f_1(3, 20) -> 1*
     f_1(3, 19) -> 1*
     f_1(3, 18) -> 1*
     f_1(3, 15) -> 1*
     f_1(3, 14) -> 1*
     f_1(3, 13) -> 1*
     f_1(3, 12) -> 1*
     f_1(3, 11) -> 1*
     f_1(3, 10) -> 1*
      f_1(3, 5) -> 1*
      f_1(3, 4) -> 1*
      f_1(3, 1) -> 1*
     f_1(1, 20) -> 1*
     f_1(1, 19) -> 1*
     f_1(1, 18) -> 1*
     f_1(1, 15) -> 1*
     f_1(1, 14) -> 1*
     f_1(1, 13) -> 1*
     f_1(1, 12) -> 1*
     f_1(1, 10) -> 1*
      f_1(1, 5) -> 1*
      f_1(1, 2) -> 1*
    f_0(20, 20) -> 1*
    f_0(20, 19) -> 1*
    f_0(20, 18) -> 1*
    f_0(20, 15) -> 1*
    f_0(20, 14) -> 1*
    f_0(20, 13) -> 1*
    f_0(20, 12) -> 1*
    f_0(20, 11) -> 1*
    f_0(20, 10) -> 1*
     f_0(20, 5) -> 1*
     f_0(20, 4) -> 1*
     f_0(20, 1) -> 1*
    f_0(19, 20) -> 1*
    f_0(19, 19) -> 1*
    f_0(19, 18) -> 1*
    f_0(19, 15) -> 1*
    f_0(19, 14) -> 1*
    f_0(19, 13) -> 1*
    f_0(19, 12) -> 1*
    f_0(19, 11) -> 1*
    f_0(19, 10) -> 1*
     f_0(19, 5) -> 1*
     f_0(19, 4) -> 1*
     f_0(19, 1) -> 1*
    f_0(18, 20) -> 1*
    f_0(18, 19) -> 1*
    f_0(18, 18) -> 1*
    f_0(18, 15) -> 1*
    f_0(18, 14) -> 1*
    f_0(18, 13) -> 1*
    f_0(18, 12) -> 1*
    f_0(18, 11) -> 1*
    f_0(18, 10) -> 1*
     f_0(18, 5) -> 1*
     f_0(18, 4) -> 1*
     f_0(18, 1) -> 1*
    f_0(15, 20) -> 1*
    f_0(15, 19) -> 1*
    f_0(15, 18) -> 1*
    f_0(15, 15) -> 1*
    f_0(15, 14) -> 1*
    f_0(15, 13) -> 1*
    f_0(15, 12) -> 1*
    f_0(15, 11) -> 1*
    f_0(15, 10) -> 1*
     f_0(15, 5) -> 1*
     f_0(15, 4) -> 1*
     f_0(15, 1) -> 1*
    f_0(14, 20) -> 1*
    f_0(14, 19) -> 1*
    f_0(14, 18) -> 1*
    f_0(14, 15) -> 1*
    f_0(14, 14) -> 1*
    f_0(14, 13) -> 1*
    f_0(14, 12) -> 1*
    f_0(14, 11) -> 1*
    f_0(14, 10) -> 1*
     f_0(14, 5) -> 1*
     f_0(14, 4) -> 1*
     f_0(14, 1) -> 1*
    f_0(13, 20) -> 1*
    f_0(13, 19) -> 1*
    f_0(13, 18) -> 1*
    f_0(13, 15) -> 1*
    f_0(13, 14) -> 1*
    f_0(13, 13) -> 1*
    f_0(13, 12) -> 1*
    f_0(13, 11) -> 1*
    f_0(13, 10) -> 1*
     f_0(13, 5) -> 1*
     f_0(13, 4) -> 1*
     f_0(13, 1) -> 1*
    f_0(12, 20) -> 1*
    f_0(12, 19) -> 1*
    f_0(12, 18) -> 1*
    f_0(12, 15) -> 1*
    f_0(12, 14) -> 1*
    f_0(12, 13) -> 1*
    f_0(12, 12) -> 1*
    f_0(12, 11) -> 1*
    f_0(12, 10) -> 1*
     f_0(12, 5) -> 1*
     f_0(12, 4) -> 1*
     f_0(12, 1) -> 1*
    f_0(11, 20) -> 1*
    f_0(11, 19) -> 1*
    f_0(11, 18) -> 1*
    f_0(11, 15) -> 1*
    f_0(11, 14) -> 1*
    f_0(11, 13) -> 1*
    f_0(11, 12) -> 1*
    f_0(11, 11) -> 1*
    f_0(11, 10) -> 1*
     f_0(11, 5) -> 1*
     f_0(11, 4) -> 1*
     f_0(11, 1) -> 1*
    f_0(10, 20) -> 1*
    f_0(10, 19) -> 1*
    f_0(10, 18) -> 1*
    f_0(10, 15) -> 1*
    f_0(10, 14) -> 1*
    f_0(10, 13) -> 1*
    f_0(10, 12) -> 1*
    f_0(10, 11) -> 1*
    f_0(10, 10) -> 1*
     f_0(10, 5) -> 1*
     f_0(10, 4) -> 1*
     f_0(10, 1) -> 1*
     f_0(5, 20) -> 1*
     f_0(5, 19) -> 1*
     f_0(5, 18) -> 1*
     f_0(5, 15) -> 1*
     f_0(5, 14) -> 1*
     f_0(5, 13) -> 1*
     f_0(5, 12) -> 1*
     f_0(5, 11) -> 1*
     f_0(5, 10) -> 1*
      f_0(5, 5) -> 1*
      f_0(5, 4) -> 1*
      f_0(5, 1) -> 1*
     f_0(4, 20) -> 1*
     f_0(4, 19) -> 1*
     f_0(4, 18) -> 1*
     f_0(4, 15) -> 1*
     f_0(4, 14) -> 1*
     f_0(4, 13) -> 1*
     f_0(4, 12) -> 1*
     f_0(4, 11) -> 1*
     f_0(4, 10) -> 1*
      f_0(4, 5) -> 1*
      f_0(4, 4) -> 1*
      f_0(4, 1) -> 1*
     f_0(1, 20) -> 1*
     f_0(1, 19) -> 1*
     f_0(1, 18) -> 1*
     f_0(1, 15) -> 1*
     f_0(1, 14) -> 1*
     f_0(1, 13) -> 1*
     f_0(1, 12) -> 1*
     f_0(1, 11) -> 1*
     f_0(1, 10) -> 1*
      f_0(1, 5) -> 1*
      f_0(1, 4) -> 1*
      f_0(1, 1) -> 1*}
  Strict:
   {}
  Qed