MAYBE
MAYBE
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(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
                  plus(s(x), s(y)) ->
  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
                 plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
                   plus(zero(), y) -> y,
                  if(true(), x, y) -> x,
                 if(false(), x, y) -> y,
                    gt(s(x), s(y)) -> gt(x, y),
                  gt(s(x), zero()) -> true(),
                     gt(zero(), y) -> false(),
                            not(x) -> if(x, false(), true()),
                             id(x) -> x
 }
 DUP: We consider a duplicating system.
  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(s(x), x) ->
    plus(if(gt(x, x), id(x), id(x)), s(x)),
                    plus(s(x), s(y)) ->
    s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
                   plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
                     plus(zero(), y) -> y,
                    if(true(), x, y) -> x,
                   if(false(), x, y) -> y,
                      gt(s(x), s(y)) -> gt(x, y),
                    gt(s(x), zero()) -> true(),
                       gt(zero(), y) -> false(),
                              not(x) -> if(x, false(), true()),
                               id(x) -> x
   }
  Fail