MAYBE
Time: 1.002190
TRS:
 {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
           sum(cons(0(), x), y) -> sum(x, y),
                  sum(nil(), y) -> y,
     weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
          weight cons(n, nil()) -> n}
 DP:
  DP:
   {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
             sum#(cons(0(), x), y) -> sum#(x, y),
       weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)),
       weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))}
  TRS:
  {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
            sum(cons(0(), x), y) -> sum(x, y),
                   sum(nil(), y) -> y,
      weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
           weight cons(n, nil()) -> n}
  UR:
   {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
             sum(cons(0(), x), y) -> sum(x, y),
                    sum(nil(), y) -> y}
   EDG:
    {(sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)), sum#(cons(0(), x), y) -> sum#(x, y))
     (sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
     (weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)), weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)))
     (weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)), weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)))
     (weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
     (weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)), sum#(cons(0(), x), y) -> sum#(x, y))
     (sum#(cons(0(), x), y) -> sum#(x, y), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
     (sum#(cons(0(), x), y) -> sum#(x, y), sum#(cons(0(), x), y) -> sum#(x, y))}
    EDG:
     {(sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)), sum#(cons(0(), x), y) -> sum#(x, y))
      (sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
      (weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)), weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)))
      (weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)), weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)))
      (weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
      (weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)), sum#(cons(0(), x), y) -> sum#(x, y))
      (sum#(cons(0(), x), y) -> sum#(x, y), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
      (sum#(cons(0(), x), y) -> sum#(x, y), sum#(cons(0(), x), y) -> sum#(x, y))}
     STATUS:
      arrows: 0.500000
      SCCS (2):
       Scc:
        {weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))}
       Scc:
        {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
                  sum#(cons(0(), x), y) -> sum#(x, y)}
       
       SCC (1):
        Strict:
         {weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))}
        Weak:
        {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
                  sum(cons(0(), x), y) -> sum(x, y),
                         sum(nil(), y) -> y,
            weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
                 weight cons(n, nil()) -> n}
        Open
       
       SCC (2):
        Strict:
         {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
                   sum#(cons(0(), x), y) -> sum#(x, y)}
        Weak:
        {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
                  sum(cons(0(), x), y) -> sum(x, y),
                         sum(nil(), y) -> y,
            weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
                 weight cons(n, nil()) -> n}
        Open