MAYBE
Time: 0.003279
TRS:
 {          app(l, nil()) -> l,
            app(nil(), k) -> k,
       app(cons(x, l), k) -> cons(x, app(l, k)),
       sum cons(x, nil()) -> cons(x, nil()),
  sum cons(x, cons(y, l)) -> sum cons(a(x, y, h()), l),
           a(x, s y, h()) -> a(x, y, s h()),
           a(x, s y, s z) -> a(x, y, a(x, s y, z)),
           a(h(), h(), x) -> s x,
           a(s x, h(), z) -> a(x, z, z)}
 DP:
  DP:
   {     app#(cons(x, l), k) -> app#(l, k),
    sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h()), l),
    sum# cons(x, cons(y, l)) -> a#(x, y, h()),
             a#(x, s y, h()) -> a#(x, y, s h()),
             a#(x, s y, s z) -> a#(x, y, a(x, s y, z)),
             a#(x, s y, s z) -> a#(x, s y, z),
             a#(s x, h(), z) -> a#(x, z, z)}
  TRS:
  {          app(l, nil()) -> l,
             app(nil(), k) -> k,
        app(cons(x, l), k) -> cons(x, app(l, k)),
        sum cons(x, nil()) -> cons(x, nil()),
   sum cons(x, cons(y, l)) -> sum cons(a(x, y, h()), l),
            a(x, s y, h()) -> a(x, y, s h()),
            a(x, s y, s z) -> a(x, y, a(x, s y, z)),
            a(h(), h(), x) -> s x,
            a(s x, h(), z) -> a(x, z, z)}
  UR:
   {a(x, s y, h()) -> a(x, y, s h()),
    a(x, s y, s z) -> a(x, y, a(x, s y, z)),
    a(h(), h(), x) -> s x,
    a(s x, h(), z) -> a(x, z, z),
           b(w, v) -> w,
           b(w, v) -> v}
   EDG:
    {(sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h()), l), sum# cons(x, cons(y, l)) -> a#(x, y, h()))
     (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h()), l), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h()), l))
     (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))
     (sum# cons(x, cons(y, l)) -> a#(x, y, h()), a#(s x, h(), z) -> a#(x, z, z))
     (sum# cons(x, cons(y, l)) -> a#(x, y, h()), a#(x, s y, h()) -> a#(x, y, s h()))
     (a#(x, s y, s z) -> a#(x, y, a(x, s y, z)), a#(x, s y, s z) -> a#(x, y, a(x, s y, z)))
     (a#(x, s y, s z) -> a#(x, y, a(x, s y, z)), a#(x, s y, s z) -> a#(x, s y, z))
     (a#(x, s y, s z) -> a#(x, y, a(x, s y, z)), a#(s x, h(), z) -> a#(x, z, z))
     (a#(s x, h(), z) -> a#(x, z, z), a#(x, s y, h()) -> a#(x, y, s h()))
     (a#(s x, h(), z) -> a#(x, z, z), a#(x, s y, s z) -> a#(x, y, a(x, s y, z)))
     (a#(s x, h(), z) -> a#(x, z, z), a#(x, s y, s z) -> a#(x, s y, z))
     (a#(s x, h(), z) -> a#(x, z, z), a#(s x, h(), z) -> a#(x, z, z))
     (a#(x, s y, s z) -> a#(x, s y, z), a#(x, s y, h()) -> a#(x, y, s h()))
     (a#(x, s y, s z) -> a#(x, s y, z), a#(x, s y, s z) -> a#(x, y, a(x, s y, z)))
     (a#(x, s y, s z) -> a#(x, s y, z), a#(x, s y, s z) -> a#(x, s y, z))
     (a#(x, s y, h()) -> a#(x, y, s h()), a#(x, s y, s z) -> a#(x, y, a(x, s y, z)))
     (a#(x, s y, h()) -> a#(x, y, s h()), a#(x, s y, s z) -> a#(x, s y, z))
     (a#(x, s y, h()) -> a#(x, y, s h()), a#(s x, h(), z) -> a#(x, z, z))}
    STATUS:
     arrows: 0.632653
     SCCS (3):
      Scc:
       {app#(cons(x, l), k) -> app#(l, k)}
      Scc:
       {sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h()), l)}
      Scc:
       {a#(x, s y, h()) -> a#(x, y, s h()),
        a#(x, s y, s z) -> a#(x, y, a(x, s y, z)),
        a#(x, s y, s z) -> a#(x, s y, z),
        a#(s x, h(), z) -> a#(x, z, z)}
      
      SCC (1):
       Strict:
        {app#(cons(x, l), k) -> app#(l, k)}
       Weak:
       {          app(l, nil()) -> l,
                  app(nil(), k) -> k,
             app(cons(x, l), k) -> cons(x, app(l, k)),
             sum cons(x, nil()) -> cons(x, nil()),
        sum cons(x, cons(y, l)) -> sum cons(a(x, y, h()), l),
                 a(x, s y, h()) -> a(x, y, s h()),
                 a(x, s y, s z) -> a(x, y, a(x, s y, z)),
                 a(h(), h(), x) -> s x,
                 a(s x, h(), z) -> a(x, z, z)}
       Open
      SCC (1):
       Strict:
        {sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h()), l)}
       Weak:
       {          app(l, nil()) -> l,
                  app(nil(), k) -> k,
             app(cons(x, l), k) -> cons(x, app(l, k)),
             sum cons(x, nil()) -> cons(x, nil()),
        sum cons(x, cons(y, l)) -> sum cons(a(x, y, h()), l),
                 a(x, s y, h()) -> a(x, y, s h()),
                 a(x, s y, s z) -> a(x, y, a(x, s y, z)),
                 a(h(), h(), x) -> s x,
                 a(s x, h(), z) -> a(x, z, z)}
       Open
      
      SCC (4):
       Strict:
        {a#(x, s y, h()) -> a#(x, y, s h()),
         a#(x, s y, s z) -> a#(x, y, a(x, s y, z)),
         a#(x, s y, s z) -> a#(x, s y, z),
         a#(s x, h(), z) -> a#(x, z, z)}
       Weak:
       {          app(l, nil()) -> l,
                  app(nil(), k) -> k,
             app(cons(x, l), k) -> cons(x, app(l, k)),
             sum cons(x, nil()) -> cons(x, nil()),
        sum cons(x, cons(y, l)) -> sum cons(a(x, y, h()), l),
                 a(x, s y, h()) -> a(x, y, s h()),
                 a(x, s y, s z) -> a(x, y, a(x, s y, z)),
                 a(h(), h(), x) -> s x,
                 a(s x, h(), z) -> a(x, z, z)}
       Open