MAYBE
Time: 0.017789
TRS:
 {           +(x, 0()) -> x,
         +(+(x, y), z) -> +(x, +(y, z)),
             +(0(), x) -> x,
           +(s x, s y) -> s s +(x, y),
             *(x, 0()) -> 0(),
             *(0(), x) -> 0(),
           *(s x, s y) -> s +(*(x, y), +(x, y)),
         *(*(x, y), z) -> *(x, *(y, z)),
         app(nil(), l) -> l,
  app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
       sum app(l1, l2) -> +(sum l1, sum l2),
             sum nil() -> 0(),
        sum cons(x, l) -> +(x, sum l),
      prod app(l1, l2) -> *(prod l1, prod l2),
            prod nil() -> s 0(),
       prod cons(x, l) -> *(x, prod l)}
 DP:
  DP:
   {       +#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z),
             +#(s x, s y) -> +#(x, y),
             *#(s x, s y) -> +#(x, y),
             *#(s x, s y) -> +#(*(x, y), +(x, y)),
             *#(s x, s y) -> *#(x, y),
           *#(*(x, y), z) -> *#(x, *(y, z)),
           *#(*(x, y), z) -> *#(y, z),
    app#(cons(x, l1), l2) -> app#(l1, l2),
         sum# app(l1, l2) -> +#(sum l1, sum l2),
         sum# app(l1, l2) -> sum# l1,
         sum# app(l1, l2) -> sum# l2,
          sum# cons(x, l) -> +#(x, sum l),
          sum# cons(x, l) -> sum# l,
        prod# app(l1, l2) -> *#(prod l1, prod l2),
        prod# app(l1, l2) -> prod# l1,
        prod# app(l1, l2) -> prod# l2,
         prod# cons(x, l) -> *#(x, prod l),
         prod# cons(x, l) -> prod# l}
  TRS:
  {           +(x, 0()) -> x,
          +(+(x, y), z) -> +(x, +(y, z)),
              +(0(), x) -> x,
            +(s x, s y) -> s s +(x, y),
              *(x, 0()) -> 0(),
              *(0(), x) -> 0(),
            *(s x, s y) -> s +(*(x, y), +(x, y)),
          *(*(x, y), z) -> *(x, *(y, z)),
          app(nil(), l) -> l,
   app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
        sum app(l1, l2) -> +(sum l1, sum l2),
              sum nil() -> 0(),
         sum cons(x, l) -> +(x, sum l),
       prod app(l1, l2) -> *(prod l1, prod l2),
             prod nil() -> s 0(),
        prod cons(x, l) -> *(x, prod l)}
  EDG:
   {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
    (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> +#(*(x, y), +(x, y)))
    (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> +#(x, y))
    (sum# cons(x, l) -> +#(x, sum l), +#(s x, s y) -> +#(x, y))
    (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(y, z))
    (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(x, +(y, z)))
    (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(y, z))
    (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(x, *(y, z)))
    (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> *#(x, y))
    (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> +#(*(x, y), +(x, y)))
    (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> +#(x, y))
    (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> prod# l)
    (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> *#(x, prod l))
    (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l2)
    (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l1)
    (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> *#(prod l1, prod l2))
    (*#(s x, s y) -> +#(*(x, y), +(x, y)), +#(s x, s y) -> +#(x, y))
    (*#(s x, s y) -> +#(*(x, y), +(x, y)), +#(+(x, y), z) -> +#(y, z))
    (*#(s x, s y) -> +#(*(x, y), +(x, y)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
    (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (*#(s x, s y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (*#(s x, s y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> *#(x, y))
    (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(*(x, y), +(x, y)))
    (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(x, y))
    (sum# app(l1, l2) -> sum# l2, sum# cons(x, l) -> sum# l)
    (sum# app(l1, l2) -> sum# l2, sum# cons(x, l) -> +#(x, sum l))
    (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> sum# l2)
    (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> sum# l1)
    (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> +#(sum l1, sum l2))
    (prod# app(l1, l2) -> prod# l2, prod# cons(x, l) -> prod# l)
    (prod# app(l1, l2) -> prod# l2, prod# cons(x, l) -> *#(x, prod l))
    (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> prod# l2)
    (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> prod# l1)
    (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> *#(prod l1, prod l2))
    (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> *#(prod l1, prod l2))
    (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> prod# l1)
    (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> prod# l2)
    (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> *#(x, prod l))
    (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> prod# l)
    (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> +#(sum l1, sum l2))
    (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> sum# l1)
    (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> sum# l2)
    (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> +#(x, sum l))
    (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> sum# l)
    (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))
    (*#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (*#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (*#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> +#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> +#(*(x, y), +(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y))
    (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> +#(sum l1, sum l2))
    (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> sum# l1)
    (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> sum# l2)
    (sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> +#(x, sum l))
    (sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> sum# l)
    (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> +#(x, y))
    (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> +#(*(x, y), +(x, y)))
    (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> *#(x, y))
    (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(*(x, y), z) -> *#(x, *(y, z)))
    (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(*(x, y), z) -> *#(y, z))
    (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(+(x, y), z) -> +#(x, +(y, z)))
    (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(+(x, y), z) -> +#(y, z))
    (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(s x, s y) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y))}
   EDG:
    {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
     (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> +#(*(x, y), +(x, y)))
     (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> +#(x, y))
     (sum# cons(x, l) -> +#(x, sum l), +#(s x, s y) -> +#(x, y))
     (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(y, z))
     (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(x, +(y, z)))
     (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(y, z))
     (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(x, *(y, z)))
     (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> *#(x, y))
     (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> +#(*(x, y), +(x, y)))
     (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> +#(x, y))
     (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> prod# l)
     (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> *#(x, prod l))
     (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l2)
     (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l1)
     (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> *#(prod l1, prod l2))
     (*#(s x, s y) -> +#(*(x, y), +(x, y)), +#(s x, s y) -> +#(x, y))
     (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
     (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (*#(s x, s y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
     (*#(s x, s y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> *#(x, y))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(*(x, y), +(x, y)))
     (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(x, y))
     (sum# app(l1, l2) -> sum# l2, sum# cons(x, l) -> sum# l)
     (sum# app(l1, l2) -> sum# l2, sum# cons(x, l) -> +#(x, sum l))
     (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> sum# l2)
     (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> sum# l1)
     (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> +#(sum l1, sum l2))
     (prod# app(l1, l2) -> prod# l2, prod# cons(x, l) -> prod# l)
     (prod# app(l1, l2) -> prod# l2, prod# cons(x, l) -> *#(x, prod l))
     (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> prod# l2)
     (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> prod# l1)
     (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> *#(prod l1, prod l2))
     (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> *#(prod l1, prod l2))
     (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> prod# l1)
     (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> prod# l2)
     (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> *#(x, prod l))
     (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> prod# l)
     (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> +#(sum l1, sum l2))
     (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> sum# l1)
     (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> sum# l2)
     (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> +#(x, sum l))
     (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> sum# l)
     (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))
     (*#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (*#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (*#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> +#(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> +#(*(x, y), +(x, y)))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y))
     (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> +#(sum l1, sum l2))
     (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> sum# l1)
     (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> sum# l2)
     (sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> +#(x, sum l))
     (sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> sum# l)
     (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> +#(x, y))
     (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> +#(*(x, y), +(x, y)))
     (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> *#(x, y))
     (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(*(x, y), z) -> *#(x, *(y, z)))
     (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(*(x, y), z) -> *#(y, z))
     (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(+(x, y), z) -> +#(x, +(y, z)))
     (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(+(x, y), z) -> +#(y, z))
     (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(s x, s y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y))}
    EDG:
     {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
      (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
      (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> *#(x, y))
      (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> +#(*(x, y), +(x, y)))
      (*#(*(x, y), z) -> *#(y, z), *#(s x, s y) -> +#(x, y))
      (sum# cons(x, l) -> +#(x, sum l), +#(s x, s y) -> +#(x, y))
      (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(y, z))
      (sum# cons(x, l) -> +#(x, sum l), +#(+(x, y), z) -> +#(x, +(y, z)))
      (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(y, z))
      (prod# cons(x, l) -> *#(x, prod l), *#(*(x, y), z) -> *#(x, *(y, z)))
      (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> *#(x, y))
      (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> +#(*(x, y), +(x, y)))
      (prod# cons(x, l) -> *#(x, prod l), *#(s x, s y) -> +#(x, y))
      (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> prod# l)
      (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> *#(x, prod l))
      (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l2)
      (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l1)
      (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> *#(prod l1, prod l2))
      (*#(s x, s y) -> +#(*(x, y), +(x, y)), +#(s x, s y) -> +#(x, y))
      (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
      (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
      (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
      (*#(s x, s y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
      (*#(s x, s y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
      (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> *#(x, y))
      (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(*(x, y), +(x, y)))
      (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(x, y))
      (sum# app(l1, l2) -> sum# l2, sum# cons(x, l) -> sum# l)
      (sum# app(l1, l2) -> sum# l2, sum# cons(x, l) -> +#(x, sum l))
      (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> sum# l2)
      (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> sum# l1)
      (sum# app(l1, l2) -> sum# l2, sum# app(l1, l2) -> +#(sum l1, sum l2))
      (prod# app(l1, l2) -> prod# l2, prod# cons(x, l) -> prod# l)
      (prod# app(l1, l2) -> prod# l2, prod# cons(x, l) -> *#(x, prod l))
      (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> prod# l2)
      (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> prod# l1)
      (prod# app(l1, l2) -> prod# l2, prod# app(l1, l2) -> *#(prod l1, prod l2))
      (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> *#(prod l1, prod l2))
      (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> prod# l1)
      (prod# cons(x, l) -> prod# l, prod# app(l1, l2) -> prod# l2)
      (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> *#(x, prod l))
      (prod# cons(x, l) -> prod# l, prod# cons(x, l) -> prod# l)
      (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> +#(sum l1, sum l2))
      (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> sum# l1)
      (sum# cons(x, l) -> sum# l, sum# app(l1, l2) -> sum# l2)
      (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> +#(x, sum l))
      (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> sum# l)
      (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))
      (*#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
      (*#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
      (*#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
      (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> +#(x, y))
      (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> +#(*(x, y), +(x, y)))
      (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s x, s y) -> *#(x, y))
      (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
      (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
      (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
      (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
      (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y))
      (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> +#(sum l1, sum l2))
      (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> sum# l1)
      (sum# app(l1, l2) -> sum# l1, sum# app(l1, l2) -> sum# l2)
      (sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> +#(x, sum l))
      (sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> sum# l)
      (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> +#(x, y))
      (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> +#(*(x, y), +(x, y)))
      (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(s x, s y) -> *#(x, y))
      (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(*(x, y), z) -> *#(x, *(y, z)))
      (prod# app(l1, l2) -> *#(prod l1, prod l2), *#(*(x, y), z) -> *#(y, z))
      (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(+(x, y), z) -> +#(x, +(y, z)))
      (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(+(x, y), z) -> +#(y, z))
      (sum# app(l1, l2) -> +#(sum l1, sum l2), +#(s x, s y) -> +#(x, y))
      (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
      (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
      (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y))}
     STATUS:
      arrows: 0.792244
      SCCS (5):
       Scc:
        {app#(cons(x, l1), l2) -> app#(l1, l2)}
       Scc:
        {prod# app(l1, l2) -> prod# l1,
         prod# app(l1, l2) -> prod# l2,
          prod# cons(x, l) -> prod# l}
       Scc:
        {sum# app(l1, l2) -> sum# l1,
         sum# app(l1, l2) -> sum# l2,
          sum# cons(x, l) -> sum# l}
       Scc:
        {  *#(s x, s y) -> *#(x, y),
         *#(*(x, y), z) -> *#(x, *(y, z)),
         *#(*(x, y), z) -> *#(y, z)}
       Scc:
        {+#(+(x, y), z) -> +#(x, +(y, z)),
         +#(+(x, y), z) -> +#(y, z),
           +#(s x, s y) -> +#(x, y)}
       
       SCC (1):
        Strict:
         {app#(cons(x, l1), l2) -> app#(l1, l2)}
        Weak:
        {           +(x, 0()) -> x,
                +(+(x, y), z) -> +(x, +(y, z)),
                    +(0(), x) -> x,
                  +(s x, s y) -> s s +(x, y),
                    *(x, 0()) -> 0(),
                    *(0(), x) -> 0(),
                  *(s x, s y) -> s +(*(x, y), +(x, y)),
                *(*(x, y), z) -> *(x, *(y, z)),
                app(nil(), l) -> l,
         app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum app(l1, l2) -> +(sum l1, sum l2),
                    sum nil() -> 0(),
               sum cons(x, l) -> +(x, sum l),
             prod app(l1, l2) -> *(prod l1, prod l2),
                   prod nil() -> s 0(),
              prod cons(x, l) -> *(x, prod l)}
        Open
       SCC (3):
        Strict:
         {prod# app(l1, l2) -> prod# l1,
          prod# app(l1, l2) -> prod# l2,
           prod# cons(x, l) -> prod# l}
        Weak:
        {           +(x, 0()) -> x,
                +(+(x, y), z) -> +(x, +(y, z)),
                    +(0(), x) -> x,
                  +(s x, s y) -> s s +(x, y),
                    *(x, 0()) -> 0(),
                    *(0(), x) -> 0(),
                  *(s x, s y) -> s +(*(x, y), +(x, y)),
                *(*(x, y), z) -> *(x, *(y, z)),
                app(nil(), l) -> l,
         app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum app(l1, l2) -> +(sum l1, sum l2),
                    sum nil() -> 0(),
               sum cons(x, l) -> +(x, sum l),
             prod app(l1, l2) -> *(prod l1, prod l2),
                   prod nil() -> s 0(),
              prod cons(x, l) -> *(x, prod l)}
        Open
       SCC (3):
        Strict:
         {sum# app(l1, l2) -> sum# l1,
          sum# app(l1, l2) -> sum# l2,
           sum# cons(x, l) -> sum# l}
        Weak:
        {           +(x, 0()) -> x,
                +(+(x, y), z) -> +(x, +(y, z)),
                    +(0(), x) -> x,
                  +(s x, s y) -> s s +(x, y),
                    *(x, 0()) -> 0(),
                    *(0(), x) -> 0(),
                  *(s x, s y) -> s +(*(x, y), +(x, y)),
                *(*(x, y), z) -> *(x, *(y, z)),
                app(nil(), l) -> l,
         app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum app(l1, l2) -> +(sum l1, sum l2),
                    sum nil() -> 0(),
               sum cons(x, l) -> +(x, sum l),
             prod app(l1, l2) -> *(prod l1, prod l2),
                   prod nil() -> s 0(),
              prod cons(x, l) -> *(x, prod l)}
        Open
       
       
       
       
       SCC (3):
        Strict:
         {  *#(s x, s y) -> *#(x, y),
          *#(*(x, y), z) -> *#(x, *(y, z)),
          *#(*(x, y), z) -> *#(y, z)}
        Weak:
        {           +(x, 0()) -> x,
                +(+(x, y), z) -> +(x, +(y, z)),
                    +(0(), x) -> x,
                  +(s x, s y) -> s s +(x, y),
                    *(x, 0()) -> 0(),
                    *(0(), x) -> 0(),
                  *(s x, s y) -> s +(*(x, y), +(x, y)),
                *(*(x, y), z) -> *(x, *(y, z)),
                app(nil(), l) -> l,
         app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum app(l1, l2) -> +(sum l1, sum l2),
                    sum nil() -> 0(),
               sum cons(x, l) -> +(x, sum l),
             prod app(l1, l2) -> *(prod l1, prod l2),
                   prod nil() -> s 0(),
              prod cons(x, l) -> *(x, prod l)}
        Open
       
       
       SCC (3):
        Strict:
         {+#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z),
            +#(s x, s y) -> +#(x, y)}
        Weak:
        {           +(x, 0()) -> x,
                +(+(x, y), z) -> +(x, +(y, z)),
                    +(0(), x) -> x,
                  +(s x, s y) -> s s +(x, y),
                    *(x, 0()) -> 0(),
                    *(0(), x) -> 0(),
                  *(s x, s y) -> s +(*(x, y), +(x, y)),
                *(*(x, y), z) -> *(x, *(y, z)),
                app(nil(), l) -> l,
         app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum app(l1, l2) -> +(sum l1, sum l2),
                    sum nil() -> 0(),
               sum cons(x, l) -> +(x, sum l),
             prod app(l1, l2) -> *(prod l1, prod l2),
                   prod nil() -> s 0(),
              prod cons(x, l) -> *(x, prod l)}
        Open