MAYBE
Trs:
 {          sum(nil()) -> 0(),
       sum(cons(x, l)) -> +(x, sum(l)),
      sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
         +(+(x, y), z) -> +(x, +(y, z)),
             +(0(), x) -> x,
         +(s(x), s(y)) -> s(s(+(x, y))),
             +(x, 0()) -> x,
         app(nil(), l) -> l,
  app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
           prod(nil()) -> s(0()),
      prod(cons(x, l)) -> *(x, prod(l)),
     prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
             *(0(), x) -> 0(),
         *(s(x), s(y)) -> s(+(*(x, y), +(x, y))),
         *(*(x, y), z) -> *(x, *(y, z)),
             *(x, 0()) -> 0()}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open