MAYBE
Time: 0.008108
TRS:
 {                  s h() -> 1(),
        a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
        a(l, x, s y, h()) -> a(l, x, y, s h()),
        a(l, s x, h(), z) -> a(l, x, z, z),
      a(s l, h(), h(), z) -> a(l, z, h(), z),
      a(h(), h(), h(), x) -> s x,
                +(x, h()) -> x,
              +(s x, s y) -> s s +(x, y),
                +(h(), x) -> x,
            +(+(x, y), z) -> +(x, +(y, z)),
            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(), h()), l)}
 DP:
  DP:
   {      a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)),
          a#(l, x, s y, s z) -> a#(l, x, s y, z),
          a#(l, x, s y, h()) -> s# h(),
          a#(l, x, s y, h()) -> a#(l, x, y, s h()),
          a#(l, s x, h(), z) -> a#(l, x, z, z),
        a#(s l, h(), h(), z) -> a#(l, z, h(), z),
        a#(h(), h(), h(), x) -> s# x,
                +#(s x, s y) -> s# s +(x, y),
                +#(s x, s y) -> s# +(x, y),
                +#(s x, s y) -> +#(x, y),
              +#(+(x, y), z) -> +#(x, +(y, z)),
              +#(+(x, y), z) -> +#(y, z),
         app#(cons(x, l), k) -> app#(l, k),
    sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()),
    sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)}
  TRS:
  {                  s h() -> 1(),
         a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
         a(l, x, s y, h()) -> a(l, x, y, s h()),
         a(l, s x, h(), z) -> a(l, x, z, z),
       a(s l, h(), h(), z) -> a(l, z, h(), z),
       a(h(), h(), h(), x) -> s x,
                 +(x, h()) -> x,
               +(s x, s y) -> s s +(x, y),
                 +(h(), x) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
             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(), h()), l)}
  UR:
   {              s h() -> 1(),
      a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
      a(l, x, s y, h()) -> a(l, x, y, s h()),
      a(l, s x, h(), z) -> a(l, x, z, z),
    a(s l, h(), h(), z) -> a(l, z, h(), z),
    a(h(), h(), h(), x) -> s x,
              +(x, h()) -> x,
            +(s x, s y) -> s s +(x, y),
              +(h(), x) -> x,
          +(+(x, y), z) -> +(x, +(y, z)),
                b(w, v) -> w,
                b(w, v) -> v}
   EDG:
    {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# s +(x, y))
     (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(h(), h(), h(), x) -> s# x)
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> s# h())
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# s +(x, y))
     (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# +(x, y))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# s +(x, y))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(h(), h(), h(), x) -> s# x)
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(h(), h(), h(), x) -> s# x)
     (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()))
     (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l))
     (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x)
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h())
     (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, s x, h(), z) -> a#(l, x, z, z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(s l, h(), h(), z) -> a#(l, z, h(), z))
     (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(h(), h(), h(), x) -> s# x)}
    STATUS:
     arrows: 0.800000
     SCCS (4):
      Scc:
       {sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)}
      Scc:
       {app#(cons(x, l), k) -> app#(l, k)}
      Scc:
       {  +#(s x, s y) -> +#(x, y),
        +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z)}
      Scc:
       {  a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)),
          a#(l, x, s y, s z) -> a#(l, x, s y, z),
          a#(l, x, s y, h()) -> a#(l, x, y, s h()),
          a#(l, s x, h(), z) -> a#(l, x, z, z),
        a#(s l, h(), h(), z) -> a#(l, z, h(), z)}
      
      SCC (1):
       Strict:
        {sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)}
       Weak:
       {                  s h() -> 1(),
              a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
              a(l, x, s y, h()) -> a(l, x, y, s h()),
              a(l, s x, h(), z) -> a(l, x, z, z),
            a(s l, h(), h(), z) -> a(l, z, h(), z),
            a(h(), h(), h(), x) -> s x,
                      +(x, h()) -> x,
                    +(s x, s y) -> s s +(x, y),
                      +(h(), x) -> x,
                  +(+(x, y), z) -> +(x, +(y, z)),
                  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(), h()), l)}
       Open
      
      SCC (1):
       Strict:
        {app#(cons(x, l), k) -> app#(l, k)}
       Weak:
       {                  s h() -> 1(),
              a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
              a(l, x, s y, h()) -> a(l, x, y, s h()),
              a(l, s x, h(), z) -> a(l, x, z, z),
            a(s l, h(), h(), z) -> a(l, z, h(), z),
            a(h(), h(), h(), x) -> s x,
                      +(x, h()) -> x,
                    +(s x, s y) -> s s +(x, y),
                      +(h(), x) -> x,
                  +(+(x, y), z) -> +(x, +(y, z)),
                  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(), h()), l)}
       Open
      SCC (3):
       Strict:
        {  +#(s x, s y) -> +#(x, y),
         +#(+(x, y), z) -> +#(x, +(y, z)),
         +#(+(x, y), z) -> +#(y, z)}
       Weak:
       {                  s h() -> 1(),
              a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
              a(l, x, s y, h()) -> a(l, x, y, s h()),
              a(l, s x, h(), z) -> a(l, x, z, z),
            a(s l, h(), h(), z) -> a(l, z, h(), z),
            a(h(), h(), h(), x) -> s x,
                      +(x, h()) -> x,
                    +(s x, s y) -> s s +(x, y),
                      +(h(), x) -> x,
                  +(+(x, y), z) -> +(x, +(y, z)),
                  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(), h()), l)}
       Open
      
      
      SCC (5):
       Strict:
        {  a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)),
           a#(l, x, s y, s z) -> a#(l, x, s y, z),
           a#(l, x, s y, h()) -> a#(l, x, y, s h()),
           a#(l, s x, h(), z) -> a#(l, x, z, z),
         a#(s l, h(), h(), z) -> a#(l, z, h(), z)}
       Weak:
       {                  s h() -> 1(),
              a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)),
              a(l, x, s y, h()) -> a(l, x, y, s h()),
              a(l, s x, h(), z) -> a(l, x, z, z),
            a(s l, h(), h(), z) -> a(l, z, h(), z),
            a(h(), h(), h(), x) -> s x,
                      +(x, h()) -> x,
                    +(s x, s y) -> s s +(x, y),
                      +(h(), x) -> x,
                  +(+(x, y), z) -> +(x, +(y, z)),
                  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(), h()), l)}
       Open