YES
Time: 0.187226
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)-DP-bounded by 3
      Automaton:
       {s1#_3(80) -> 81*
        s1#_2(84) -> 85*
        s1#_2(82) -> 83*
        s1#_2(67) -> 68*
        s1#_2(49) -> 50*
        s1#_2(41) -> 42*
        s1#_2(28) -> 29*
        s1#_1(71) -> 72*
        s1#_1(69) -> 70*
        s1#_1(53) -> 54*
        s1#_1(51) -> 52*
        s1#_1(45) -> 46*
        s1#_1(43) -> 44*
        s1#_1(32) -> 33*
        s1#_1(30) -> 31*
        s1#_1(13) -> 14*
        s1#_0(19) -> 20*
        s1#_0(10) -> 4*
         s1_3(79) -> 80*
         s1_3(78) -> 79*
         s1_2(86) -> 87*
         s1_2(73) -> 74*
         s1_2(66) -> 67*
         s1_2(65) -> 66*
         s1_2(60) -> 61*
         s1_2(55) -> 56*
         s1_2(48) -> 49*
         s1_2(47) -> 48*
         s1_2(40) -> 41*
         s1_2(39) -> 40*
         s1_2(27) -> 28*
         s1_2(26) -> 27*
         s1_1(34) -> 35*
         s1_1(21) -> 22*
         s1_1(17) -> 18*
         s1_1(15) -> 16*
         s1_1(12) -> 13*
         s1_1(11) -> 12*
         s1_0(10) -> 10*
          s1_0(9) -> 10*
          s1_0(7) -> 9*
         s0_2(89) -> 90*
         s0_2(88) -> 89*
         s0_2(87) -> 88*
         s0_2(76) -> 77*
         s0_2(75) -> 76*
         s0_2(74) -> 75*
         s0_2(63) -> 64*
         s0_2(62) -> 63*
         s0_2(61) -> 62*
         s0_2(58) -> 59*
         s0_2(57) -> 58*
         s0_2(56) -> 57*
         s0_1(37) -> 38*
         s0_1(36) -> 37*
         s0_1(35) -> 36*
         s0_1(24) -> 25*
         s0_1(23) -> 24*
         s0_1(22) -> 23*
         s0_0(10) -> 7*
          s0_0(9) -> 7*
          s0_0(7) -> 7*
               90 -> 56*
               85 -> 50*
               83 -> 50*
               81 -> 50*
               80 -> 86*
               79 -> 84*
               77 -> 48*
               75 -> 82 | 78
               72 -> 52*
               70 -> 52*
               68 -> 52*
               67 -> 73*
               66 -> 71*
               64 -> 28*
               62 -> 69 | 65
               59 -> 41*
               54 -> 46*
               52 -> 46*
               50 -> 46*
               49 -> 55*
               48 -> 53*
               46 -> 33*
               44 -> 33*
               42 -> 33*
               41 -> 60*
               40 -> 45*
               38 -> 22*
               37 -> 43 | 39
               35 -> 51 | 47
               33 -> 14*
               31 -> 14*
               29 -> 14*
               28 -> 34*
               27 -> 32*
               25 -> 18 | 16 | 13
               23 -> 30 | 26
               20 -> 4*
               18 -> 12*
               16 -> 12*
               14 -> 20 | 4
               13 -> 21*
               10 -> 17*
                9 -> 19 | 15
                7 -> 11 | 10
                4 -> 20*}
      Strict:
       {s1# s1 s0 s0 x -> s1# x,
        s1# s1 s0 s0 x -> s1# s1 x}
      EDG:
       {(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# x)
        (s1# s1 s0 s0 x -> s1# x, s1# s1 s0 s0 x -> s1# x)
        (s1# s1 s0 s0 x -> s1# x, s1# s1 s0 s0 x -> s1# s1 x)}
       SCCS (1):
        Scc:
         {s1# s1 s0 s0 x -> s1# x,
          s1# s1 s0 s0 x -> s1# s1 x}
        SCC (2):
         Strict:
          {s1# s1 s0 s0 x -> s1# x,
           s1# s1 s0 s0 x -> s1# s1 x}
         Weak:
         {s1 s1 s0 s0 x -> s0 s0 s0 s1 s1 s1 x}
         BOUND:
          Bound: match(-raise)-DP-bounded by 1
          Automaton:
           {s1#_1(18) -> 19*
            s1#_1(16) -> 17*
            s1#_1(10) -> 11*
            s1#_0(14) -> 15*
             s1#_0(8) -> 4*
             s1_1(56) -> 57*
             s1_1(55) -> 56*
             s1_1(54) -> 55*
             s1_1(49) -> 50*
             s1_1(48) -> 49*
             s1_1(47) -> 48*
             s1_1(42) -> 43*
             s1_1(41) -> 42*
             s1_1(40) -> 41*
             s1_1(35) -> 36*
             s1_1(34) -> 35*
             s1_1(33) -> 34*
             s1_1(28) -> 29*
             s1_1(27) -> 28*
             s1_1(26) -> 27*
             s1_1(21) -> 22*
             s1_1(20) -> 21*
             s1_1(12) -> 13*
              s1_1(9) -> 10*
              s1_0(8) -> 8*
              s1_0(6) -> 8*
             s0_1(59) -> 60*
             s0_1(58) -> 59*
             s0_1(57) -> 58*
             s0_1(52) -> 53*
             s0_1(51) -> 52*
             s0_1(50) -> 51*
             s0_1(45) -> 46*
             s0_1(44) -> 45*
             s0_1(43) -> 44*
             s0_1(38) -> 39*
             s0_1(37) -> 38*
             s0_1(36) -> 37*
             s0_1(31) -> 32*
             s0_1(30) -> 31*
             s0_1(29) -> 30*
             s0_1(24) -> 25*
             s0_1(23) -> 24*
             s0_1(22) -> 23*
              s0_0(8) -> 6*
              s0_0(6) -> 6*
                   60 -> 43*
                   53 -> 41*
                   51 -> 54*
                   46 -> 35*
                   39 -> 28*
                   37 -> 47*
                   32 -> 22*
                   31 -> 33*
                   29 -> 40*
                   25 -> 21 | 13
                   23 -> 26*
                   19 -> 11*
                   17 -> 11*
                   15 -> 4*
                   13 -> 10*
                   11 -> 19 | 4
                   10 -> 20*
                    8 -> 18 | 12
                    6 -> 16 | 14 | 9 | 8}
          Strict:
           {s1# s1 s0 s0 x -> s1# x}
          EDG:
           {(s1# s1 s0 s0 x -> s1# x, s1# s1 s0 s0 x -> s1# x)}
           SCCS (1):
            Scc:
             {s1# s1 s0 s0 x -> s1# x}
            SCC (1):
             Strict:
              {s1# s1 s0 s0 x -> s1# x}
             Weak:
             {s1 s1 s0 s0 x -> s0 s0 s0 s1 s1 s1 x}
             SPSC:
              Simple Projection:
               pi(s1#) = 0
              Strict:
               {}
              Qed