YES
Time: 0.024915
TRS:
 {                  app(l, nil()) -> l,
                    app(nil(), k) -> k,
               app(cons(x, l), k) -> cons(x, app(l, k)),
  sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
               sum cons(x, nil()) -> cons(x, nil()),
          sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                     plus(0(), y) -> y,
                     plus(s x, y) -> s plus(x, y)}
 DP:
  DP:
   {             app#(cons(x, l), k) -> app#(l, k),
    sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))),
    sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))),
    sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)),
            sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l),
            sum# cons(x, cons(y, l)) -> plus#(x, y),
                       plus#(s x, y) -> plus#(x, y)}
  TRS:
  {                  app(l, nil()) -> l,
                     app(nil(), k) -> k,
                app(cons(x, l), k) -> cons(x, app(l, k)),
   sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                sum cons(x, nil()) -> cons(x, nil()),
           sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                      plus(0(), y) -> y,
                      plus(s x, y) -> s plus(x, y)}
  EDG:
   {(app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))
    (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))), app#(cons(x, l), k) -> app#(l, k))
    (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> plus#(x, y))}
   EDG:
    {(sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
     (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
     (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> plus#(x, y))}
    EDG:
     {(sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
      (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
      (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
      (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> plus#(x, y))}
     STATUS:
      arrows: 0.918367
      SCCS (0):