YES
Time: 0.175229
TRS:
 {s1 s1 s0 s0 x -> s0 s0 s0 s1 s1 s1 x}
 DP:
  DP:
   {s1# s1 s0 s0 x -> s1# x,
    s1# s1 s0 s0 x -> s1# s1 x,
    s1# s1 s0 s0 x -> s1# s1 s1 x}
  TRS:
  {s1 s1 s0 s0 x -> s0 s0 s0 s1 s1 s1 x}
  EDG:
   {(s1# s1 s0 s0 x -> s1# x, s1# s1 s0 s0 x -> s1# s1 s1 x)
    (s1# s1 s0 s0 x -> s1# x, s1# s1 s0 s0 x -> s1# s1 x)
    (s1# s1 s0 s0 x -> s1# x, s1# s1 s0 s0 x -> s1# x)
    (s1# s1 s0 s0 x -> s1# s1 x, s1# s1 s0 s0 x -> s1# x)
    (s1# s1 s0 s0 x -> s1# s1 x, s1# s1 s0 s0 x -> s1# s1 x)
    (s1# s1 s0 s0 x -> s1# s1 x, s1# s1 s0 s0 x -> s1# s1 s1 x)
    (s1# s1 s0 s0 x -> s1# s1 s1 x, s1# s1 s0 s0 x -> s1# x)
    (s1# s1 s0 s0 x -> s1# s1 s1 x, s1# s1 s0 s0 x -> s1# s1 x)
    (s1# s1 s0 s0 x -> s1# s1 s1 x, s1# s1 s0 s0 x -> s1# s1 s1 x)}
   SCCS (1):
    Scc:
     {s1# s1 s0 s0 x -> s1# x,
      s1# s1 s0 s0 x -> s1# s1 x,
      s1# s1 s0 s0 x -> s1# s1 s1 x}
    SCC (3):
     Strict:
      {s1# s1 s0 s0 x -> s1# x,
       s1# s1 s0 s0 x -> s1# s1 x,
       s1# s1 s0 s0 x -> s1# s1 s1 x}
     Weak:
     {s1 s1 s0 s0 x -> s0 s0 s0 s1 s1 s1 x}
     BOUND:
      Bound: match(-raise)-bounded by 4
      Automaton:
       {s1#_4(134) -> 135*
        s1#_4(132) -> 133*
        s1#_3(130) -> 131*
        s1#_3(110) -> 111*
        s1#_3(108) -> 109*
         s1#_3(91) -> 92*
         s1#_3(57) -> 58*
         s1#_2(89) -> 90*
         s1#_2(55) -> 56*
         s1#_2(53) -> 54*
         s1#_2(51) -> 52*
         s1#_2(40) -> 41*
         s1#_2(17) -> 18*
         s1#_1(15) -> 16*
         s1#_1(13) -> 14*
          s1#_1(2) -> 3*
          s1#_0(1) -> 1*
         s1_4(155) -> 156*
         s1_4(150) -> 151*
         s1_4(146) -> 147*
         s1_4(144) -> 145*
         s1_4(140) -> 141*
         s1_4(138) -> 139*
         s1_3(148) -> 149*
         s1_3(142) -> 143*
         s1_3(136) -> 137*
         s1_3(125) -> 126*
         s1_3(120) -> 121*
         s1_3(118) -> 119*
         s1_3(116) -> 117*
         s1_3(114) -> 115*
         s1_3(112) -> 113*
         s1_3(103) -> 104*
          s1_3(99) -> 100*
          s1_3(95) -> 96*
          s1_3(84) -> 85*
          s1_3(73) -> 74*
          s1_3(65) -> 66*
         s1_2(101) -> 102*
          s1_2(97) -> 98*
          s1_2(93) -> 94*
          s1_2(82) -> 83*
          s1_2(77) -> 78*
          s1_2(75) -> 76*
          s1_2(71) -> 72*
          s1_2(69) -> 70*
          s1_2(67) -> 68*
          s1_2(63) -> 64*
          s1_2(61) -> 62*
          s1_2(59) -> 60*
          s1_2(46) -> 47*
          s1_2(44) -> 45*
          s1_2(42) -> 43*
          s1_2(35) -> 36*
          s1_2(29) -> 30*
          s1_2(23) -> 24*
          s1_1(33) -> 34*
          s1_1(31) -> 32*
          s1_1(27) -> 28*
          s1_1(25) -> 26*
          s1_1(21) -> 22*
          s1_1(19) -> 20*
           s1_1(8) -> 9*
           s1_1(6) -> 7*
           s1_1(4) -> 5*
           s1_0(1) -> 1*
         s0_4(158) -> 159*
         s0_4(157) -> 158*
         s0_4(156) -> 157*
         s0_4(153) -> 154*
         s0_4(152) -> 153*
         s0_4(151) -> 152*
         s0_3(128) -> 129*
         s0_3(127) -> 128*
         s0_3(126) -> 127*
         s0_3(123) -> 124*
         s0_3(122) -> 123*
         s0_3(121) -> 122*
         s0_3(106) -> 107*
         s0_3(105) -> 106*
         s0_3(104) -> 105*
          s0_3(87) -> 88*
          s0_3(86) -> 87*
          s0_3(85) -> 86*
          s0_2(80) -> 81*
          s0_2(79) -> 80*
          s0_2(78) -> 79*
          s0_2(49) -> 50*
          s0_2(48) -> 49*
          s0_2(47) -> 48*
          s0_2(38) -> 39*
          s0_2(37) -> 38*
          s0_2(36) -> 37*
          s0_1(11) -> 12*
          s0_1(10) -> 11*
           s0_1(9) -> 10*
           s0_0(1) -> 1*
               159 -> 104*
               154 -> 119*
               149 -> 121*
               147 -> 155 | 134
               145 -> 150 | 132
               143 -> 148 | 134
               141 -> 146 | 134
               139 -> 144 | 132
               137 -> 142 | 134
               135 -> 92*
               133 -> 111*
               131 -> 92*
               129 -> 72*
               127 -> 136 | 130
               124 -> 96*
               122 -> 140 | 134
               119 -> 125 | 110
               117 -> 120 | 108
               115 -> 118 | 110
               113 -> 116 | 108
               111 -> 58*
               109 -> 92*
               107 -> 70*
               102 -> 36*
               100 -> 103 | 91
                98 -> 101 | 91
                96 -> 99 | 91
                94 -> 97 | 91
                92 -> 58*
                90 -> 41*
                88 -> 47 | 45
                87 -> 114 | 110
                85 -> 138 | 132
                83 -> 36*
                81 -> 30 | 26
                79 -> 112 | 108 | 93 | 89
                76 -> 36*
                74 -> 84 | 57
                72 -> 82 | 57
                70 -> 77 | 57
                68 -> 75 | 57
                66 -> 73 | 57
                64 -> 71 | 57
                62 -> 69 | 57
                60 -> 67 | 57
                58 -> 41*
                56 -> 41*
                54 -> 18*
                52 -> 41*
                50 -> 28*
                48 -> 63 | 55
                45 -> 46 | 40
                43 -> 44 | 40
                41 -> 18*
                39 -> 43 | 9 | 7
                38 -> 61 | 53
                37 -> 65 | 59 | 57 | 51
                36 -> 95 | 91
                34 -> 9*
                32 -> 9*
                30 -> 35 | 17
                28 -> 33 | 17
                26 -> 31 | 17
                24 -> 29 | 17
                22 -> 27 | 17
                20 -> 25 | 17
                18 -> 41 | 3
                16 -> 3 | 1
                14 -> 3 | 1
                12 -> 7 | 5 | 1
                11 -> 21 | 15
                10 -> 23 | 19 | 17 | 13
                 9 -> 42 | 40
                 7 -> 8 | 2
                 5 -> 6 | 2
                 3 -> 1*
                 1 -> 4 | 2}
      Strict:
       {}
      Qed