MAYBE
Time: 0.012159
TRS:
 {                  minus(x, 0()) -> x,
            minus(minus(x, y), z) -> minus(x, plus(y, z)),
                  minus(s x, s y) -> minus(x, y),
                   quot(0(), s y) -> 0(),
                   quot(s x, s y) -> s quot(minus(x, y), s y),
                     plus(0(), y) -> y,
                     plus(s x, y) -> s plus(x, y),
                    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)}
 DP:
  DP:
   {          minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(minus(x, y), z) -> plus#(y, z),
                    minus#(s x, s y) -> minus#(x, y),
                     quot#(s x, s y) -> minus#(x, y),
                     quot#(s x, s y) -> quot#(minus(x, y), s y),
                       plus#(s x, y) -> plus#(x, y),
                 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)) -> plus#(x, y),
            sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
  TRS:
  {                  minus(x, 0()) -> x,
             minus(minus(x, y), z) -> minus(x, plus(y, z)),
                   minus(s x, s y) -> minus(x, y),
                    quot(0(), s y) -> 0(),
                    quot(s x, s y) -> s quot(minus(x, y), s y),
                      plus(0(), y) -> y,
                      plus(s x, y) -> s plus(x, y),
                     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)}
  EDG:
   {(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))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(s x, s y) -> minus#(x, y))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> plus#(y, z))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
    (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (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# 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# 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# 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))) -> app#(l, sum cons(x, cons(y, k))))
    (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (minus#(minus(x, y), z) -> plus#(y, z), 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# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
   STATUS:
    arrows: 0.826389
    SCCS (6):
     Scc:
      {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
     Scc:
      {app#(cons(x, l), k) -> app#(l, k)}
     Scc:
      {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
     Scc:
      {quot#(s x, s y) -> quot#(minus(x, y), s y)}
     Scc:
      {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
             minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     SCC (1):
      Strict:
       {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
      Weak:
      {                  minus(x, 0()) -> x,
                 minus(minus(x, y), z) -> minus(x, plus(y, z)),
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                          plus(0(), y) -> y,
                          plus(s x, y) -> s plus(x, y),
                         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)}
      Open
     
     SCC (1):
      Strict:
       {app#(cons(x, l), k) -> app#(l, k)}
      Weak:
      {                  minus(x, 0()) -> x,
                 minus(minus(x, y), z) -> minus(x, plus(y, z)),
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                          plus(0(), y) -> y,
                          plus(s x, y) -> s plus(x, y),
                         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)}
      Open
     
     SCC (1):
      Strict:
       {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
      Weak:
      {                  minus(x, 0()) -> x,
                 minus(minus(x, y), z) -> minus(x, plus(y, z)),
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                          plus(0(), y) -> y,
                          plus(s x, y) -> s plus(x, y),
                         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)}
      Open
     
     SCC (1):
      Strict:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Weak:
      {                  minus(x, 0()) -> x,
                 minus(minus(x, y), z) -> minus(x, plus(y, z)),
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                          plus(0(), y) -> y,
                          plus(s x, y) -> s plus(x, y),
                         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)}
      Open
     
     SCC (2):
      Strict:
       {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {                  minus(x, 0()) -> x,
                 minus(minus(x, y), z) -> minus(x, plus(y, z)),
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                          plus(0(), y) -> y,
                          plus(s x, y) -> s plus(x, y),
                         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)}
      Open
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, y)}
      Weak:
      {                  minus(x, 0()) -> x,
                 minus(minus(x, y), z) -> minus(x, plus(y, z)),
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                          plus(0(), y) -> y,
                          plus(s x, y) -> s plus(x, y),
                         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)}
      Open