MAYBE
Time: 0.001985
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),
  sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l)),
                        plus(0(), y) -> y,
                        plus(s x, y) -> s plus(x, y),
               pred cons(s x, nil()) -> cons(x, nil())}
 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),
    sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(y, l)),
    sum# plus(cons(0(), x), cons(y, l)) -> pred# sum cons(s x, cons(y, l)),
                          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),
   sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l)),
                         plus(0(), y) -> y,
                         plus(s x, y) -> s plus(x, y),
                pred cons(s x, nil()) -> cons(x, nil())}
  EDG:
   {(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))) -> app#(l, sum cons(x, cons(y, k))), app#(cons(x, l), k) -> app#(l, k))
    (sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(y, l)), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(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)) -> 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))
    (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# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (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# 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))) -> sum# app(l, sum cons(x, cons(y, k))), sum# plus(cons(0(), x), cons(y, l)) -> sum# cons(s x, cons(y, l)))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# plus(cons(0(), x), cons(y, l)) -> pred# sum cons(s x, cons(y, l)))}
   STATUS:
    arrows: 0.790123
    SCCS (4):
     Scc:
      {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
     Scc:
      {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     Scc:
      {app#(cons(x, l), k) -> app#(l, k)}
     
     SCC (1):
      Strict:
       {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
      Weak:
      {                     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),
       sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l)),
                             plus(0(), y) -> y,
                             plus(s x, y) -> s plus(x, y),
                    pred cons(s x, nil()) -> cons(x, nil())}
      Open
     
     
     
     SCC (1):
      Strict:
       {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
      Weak:
      {                     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),
       sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l)),
                             plus(0(), y) -> y,
                             plus(s x, y) -> s plus(x, y),
                    pred cons(s x, nil()) -> cons(x, nil())}
      Open
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, y)}
      Weak:
      {                     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),
       sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l)),
                             plus(0(), y) -> y,
                             plus(s x, y) -> s plus(x, y),
                    pred cons(s x, nil()) -> cons(x, nil())}
      Open
     
     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 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),
       sum plus(cons(0(), x), cons(y, l)) -> pred sum cons(s x, cons(y, l)),
                             plus(0(), y) -> y,
                             plus(s x, y) -> s plus(x, y),
                    pred cons(s x, nil()) -> cons(x, nil())}
      Open