MAYBE
Time: 0.006817
TRS:
 {            h(x, c(y, z), t w) -> h(c(s y, x), z, t c(t w, w)),
      h(c(x, y), c(s z, z), t w) -> h(z, c(y, x), t t c(x, c(y, t w))),
  h(c(s x, c(s 0(), y)), z, t x) -> h(y, c(s 0(), c(x, z)), t t c(x, s x)),
                             t x -> x,
                             t x -> c(0(), c(0(), c(0(), c(0(), c(0(), x))))),
                           t t x -> t c(t x, x)}
 DP:
  DP:
   {            h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)),
                h#(x, c(y, z), t w) -> t# c(t w, w),
        h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))),
        h#(c(x, y), c(s z, z), t w) -> t# c(x, c(y, t w)),
        h#(c(x, y), c(s z, z), t w) -> t# t c(x, c(y, t w)),
    h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)),
    h#(c(s x, c(s 0(), y)), z, t x) -> t# c(x, s x),
    h#(c(s x, c(s 0(), y)), z, t x) -> t# t c(x, s x),
                             t# t x -> t# c(t x, x)}
  TRS:
  {            h(x, c(y, z), t w) -> h(c(s y, x), z, t c(t w, w)),
       h(c(x, y), c(s z, z), t w) -> h(z, c(y, x), t t c(x, c(y, t w))),
   h(c(s x, c(s 0(), y)), z, t x) -> h(y, c(s 0(), c(x, z)), t t c(x, s x)),
                              t x -> x,
                              t x -> c(0(), c(0(), c(0(), c(0(), c(0(), x))))),
                            t t x -> t c(t x, x)}
  EDG:
   {(h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(c(s x, c(s 0(), y)), z, t x) -> t# t c(x, s x))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(c(s x, c(s 0(), y)), z, t x) -> t# c(x, s x))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(c(x, y), c(s z, z), t w) -> t# t c(x, c(y, t w)))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(c(x, y), c(s z, z), t w) -> t# c(x, c(y, t w)))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(x, c(y, z), t w) -> t# c(t w, w))
    (h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))), h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)))
    (h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)), h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)))
    (h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)), h#(x, c(y, z), t w) -> t# c(t w, w))
    (h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)), h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)))
    (h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)), h#(c(s x, c(s 0(), y)), z, t x) -> t# c(x, s x))
    (h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)), h#(c(s x, c(s 0(), y)), z, t x) -> t# t c(x, s x))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(x, c(y, z), t w) -> t# c(t w, w))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(c(x, y), c(s z, z), t w) -> t# c(x, c(y, t w)))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(c(x, y), c(s z, z), t w) -> t# t c(x, c(y, t w)))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x)))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(c(s x, c(s 0(), y)), z, t x) -> t# c(x, s x))
    (h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)), h#(c(s x, c(s 0(), y)), z, t x) -> t# t c(x, s x))
    (h#(c(s x, c(s 0(), y)), z, t x) -> t# t c(x, s x), t# t x -> t# c(t x, x))
    (h#(c(x, y), c(s z, z), t w) -> t# t c(x, c(y, t w)), t# t x -> t# c(t x, x))}
   STATUS:
    arrows: 0.716049
    SCCS (1):
     Scc:
      {            h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)),
           h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))),
       h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x))}
     
     SCC (3):
      Strict:
       {            h#(x, c(y, z), t w) -> h#(c(s y, x), z, t c(t w, w)),
            h#(c(x, y), c(s z, z), t w) -> h#(z, c(y, x), t t c(x, c(y, t w))),
        h#(c(s x, c(s 0(), y)), z, t x) -> h#(y, c(s 0(), c(x, z)), t t c(x, s x))}
      Weak:
      {            h(x, c(y, z), t w) -> h(c(s y, x), z, t c(t w, w)),
           h(c(x, y), c(s z, z), t w) -> h(z, c(y, x), t t c(x, c(y, t w))),
       h(c(s x, c(s 0(), y)), z, t x) -> h(y, c(s 0(), c(x, z)), t t c(x, s x)),
                                  t x -> x,
                                  t x -> c(0(), c(0(), c(0(), c(0(), c(0(), x))))),
                                t t x -> t c(t x, x)}
      Open