YES
Time: 2.555746
TRS:
 {            h(x, c(y, z)) -> h(c(s y, x), z),
  h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
 DP:
  DP:
   {            h#(x, c(y, z)) -> h#(c(s y, x), z),
    h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
  TRS:
  {            h(x, c(y, z)) -> h(c(s y, x), z),
   h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
  EDG:
   {(h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))
    (h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(x, c(y, z)) -> h#(c(s y, x), z))
    (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(x, c(y, z)) -> h#(c(s y, x), z))
    (h#(x, c(y, z)) -> h#(c(s y, x), z), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))}
   SCCS (1):
    Scc:
     {            h#(x, c(y, z)) -> h#(c(s y, x), z),
      h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
    SCC (2):
     Strict:
      {            h#(x, c(y, z)) -> h#(c(s y, x), z),
       h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
     Weak:
     {            h(x, c(y, z)) -> h(c(s y, x), z),
      h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
     BOUND:
      Bound: match(-raise)-DP-bounded by 2
      Automaton:
       {       0_1() -> 17*
               0_0() -> 12*
             s_2(18) -> 21*
             s_2(14) -> 23*
             s_2(13) -> 23*
             s_2(12) -> 23*
             s_2(10) -> 23*
              s_2(9) -> 23*
             s_1(17) -> 18*
             s_1(14) -> 15*
             s_1(13) -> 15*
             s_1(12) -> 15*
             s_1(10) -> 15*
              s_1(9) -> 15*
             s_0(14) -> 13*
             s_0(13) -> 13*
             s_0(12) -> 13*
             s_0(10) -> 13*
              s_0(9) -> 13*
         c_2(23, 22) -> 24*
         c_2(21, 24) -> 22*
         c_2(21, 22) -> 22*
         c_2(21, 16) -> 22*
         c_2(21, 14) -> 22*
         c_2(21, 13) -> 22*
         c_2(21, 12) -> 22*
         c_2(21, 10) -> 22*
          c_2(21, 9) -> 22*
         c_1(18, 20) -> 20*
         c_1(18, 19) -> 20*
         c_1(15, 24) -> 24*
         c_1(15, 16) -> 16*
         c_1(15, 14) -> 16*
         c_1(15, 13) -> 16*
         c_1(15, 12) -> 16*
         c_1(15, 10) -> 16*
          c_1(15, 9) -> 16*
         c_1(14, 20) -> 19*
         c_1(14, 14) -> 19*
         c_1(14, 13) -> 19*
         c_1(14, 12) -> 19*
         c_1(14, 10) -> 19*
          c_1(14, 9) -> 19*
         c_1(13, 20) -> 19*
         c_1(13, 14) -> 19*
         c_1(13, 13) -> 19*
         c_1(13, 12) -> 19*
         c_1(13, 10) -> 19*
          c_1(13, 9) -> 19*
         c_1(12, 20) -> 19*
         c_1(12, 14) -> 19*
         c_1(12, 13) -> 19*
         c_1(12, 12) -> 19*
         c_1(12, 10) -> 19*
          c_1(12, 9) -> 19*
         c_1(10, 20) -> 19*
         c_1(10, 14) -> 19*
         c_1(10, 13) -> 19*
         c_1(10, 12) -> 19*
         c_1(10, 10) -> 19*
          c_1(10, 9) -> 19*
          c_1(9, 20) -> 19*
          c_1(9, 14) -> 19*
          c_1(9, 13) -> 19*
          c_1(9, 12) -> 19*
          c_1(9, 10) -> 19*
           c_1(9, 9) -> 19*
         c_0(14, 14) -> 10*
         c_0(14, 13) -> 10*
         c_0(14, 12) -> 10*
         c_0(14, 10) -> 10*
          c_0(14, 9) -> 10*
         c_0(13, 14) -> 14*
         c_0(13, 13) -> 14*
         c_0(13, 12) -> 14*
         c_0(13, 10) -> 14*
          c_0(13, 9) -> 14*
         c_0(12, 14) -> 10*
         c_0(12, 13) -> 10*
         c_0(12, 12) -> 10*
         c_0(12, 10) -> 10*
          c_0(12, 9) -> 10*
         c_0(10, 14) -> 10*
         c_0(10, 13) -> 10*
         c_0(10, 12) -> 10*
         c_0(10, 10) -> 10*
          c_0(10, 9) -> 10*
          c_0(9, 14) -> 10*
          c_0(9, 13) -> 10*
          c_0(9, 12) -> 10*
          c_0(9, 10) -> 10*
           c_0(9, 9) -> 10*
        h#_2(24, 20) -> 6*
        h#_2(24, 14) -> 6*
        h#_2(24, 13) -> 6*
        h#_2(24, 12) -> 6*
        h#_2(24, 10) -> 6*
         h#_2(24, 9) -> 6*
        h#_2(22, 20) -> 6*
        h#_2(22, 19) -> 6*
        h#_1(24, 14) -> 6*
        h#_1(24, 13) -> 6*
        h#_1(24, 12) -> 6*
        h#_1(16, 20) -> 6*
        h#_1(16, 14) -> 6*
        h#_1(16, 13) -> 6*
        h#_1(16, 12) -> 6*
        h#_1(16, 10) -> 6*
         h#_1(16, 9) -> 6*
        h#_1(14, 20) -> 6*
        h#_1(13, 20) -> 6*
        h#_1(12, 20) -> 6*
        h#_1(10, 20) -> 6*
         h#_1(9, 20) -> 6*
        h#_0(14, 14) -> 6*
        h#_0(14, 13) -> 6*
        h#_0(14, 12) -> 6*
        h#_0(14, 10) -> 6*
         h#_0(14, 9) -> 6*
        h#_0(13, 14) -> 6*
        h#_0(12, 14) -> 6*
        h#_0(10, 14) -> 6*
         h#_0(9, 14) -> 6*
         h_0(14, 14) -> 9*
         h_0(14, 13) -> 9*
         h_0(14, 12) -> 9*
         h_0(14, 10) -> 9*
          h_0(14, 9) -> 9*
         h_0(13, 14) -> 9*
         h_0(13, 13) -> 9*
         h_0(13, 12) -> 9*
         h_0(13, 10) -> 9*
          h_0(13, 9) -> 9*
         h_0(12, 14) -> 9*
         h_0(12, 13) -> 9*
         h_0(12, 12) -> 9*
         h_0(12, 10) -> 9*
          h_0(12, 9) -> 9*
         h_0(10, 14) -> 9*
         h_0(10, 13) -> 9*
         h_0(10, 12) -> 9*
         h_0(10, 10) -> 9*
          h_0(10, 9) -> 9*
          h_0(9, 14) -> 9*
          h_0(9, 13) -> 9*
          h_0(9, 12) -> 9*
          h_0(9, 10) -> 9*
           h_0(9, 9) -> 9*}
      Strict:
       {h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
      EDG:
       {(h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))), h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z))))}
       SCCS (1):
        Scc:
         {h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
        SCC (1):
         Strict:
          {h#(c(s x, c(s 0(), y)), z) -> h#(y, c(s 0(), c(x, z)))}
         Weak:
         {            h(x, c(y, z)) -> h(c(s y, x), z),
          h(c(s x, c(s 0(), y)), z) -> h(y, c(s 0(), c(x, z)))}
         SPSC:
          Simple Projection:
           pi(h#) = 0
          Strict:
           {}
          Qed