MAYBE
Time: 0.003029
TRS:
 {      +(x, 0()) -> x,
        +(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)),
        sum nil() -> 0(),
   sum cons(x, l) -> +(x, sum l),
       prod nil() -> s 0(),
  prod cons(x, l) -> *(x, prod l)}
 DP:
  DP:
   {    +#(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),
     sum# cons(x, l) -> +#(x, sum l),
     sum# cons(x, l) -> sum# l,
    prod# cons(x, l) -> *#(x, prod l),
    prod# cons(x, l) -> prod# l}
  TRS:
  {      +(x, 0()) -> x,
         +(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)),
         sum nil() -> 0(),
    sum cons(x, l) -> +(x, sum l),
        prod nil() -> s 0(),
   prod cons(x, l) -> *(x, prod l)}
  EDG:
   {(sum# cons(x, l) -> sum# l, sum# cons(x, l) -> sum# l)
    (sum# cons(x, l) -> sum# l, sum# cons(x, l) -> +#(x, sum l))
    (+#(s x, s 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), *#(s x, s y) -> +#(*(x, y), +(x, y)))
    (*#(s x, s y) -> *#(x, y), *#(s x, s y) -> +#(x, y))
    (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))
    (sum# cons(x, l) -> +#(x, sum l), +#(s x, s y) -> +#(x, y))
    (*#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y))
    (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)
    (*#(s x, s y) -> +#(*(x, y), +(x, y)), +#(s x, s y) -> +#(x, y))}
   STATUS:
    arrows: 0.781250
    SCCS (4):
     Scc:
      {prod# cons(x, l) -> prod# l}
     Scc:
      {*#(s x, s y) -> *#(x, y)}
     Scc:
      {sum# cons(x, l) -> sum# l}
     Scc:
      {+#(s x, s y) -> +#(x, y)}
     
     SCC (1):
      Strict:
       {prod# cons(x, l) -> prod# l}
      Weak:
      {      +(x, 0()) -> x,
             +(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)),
             sum nil() -> 0(),
        sum cons(x, l) -> +(x, sum l),
            prod nil() -> s 0(),
       prod cons(x, l) -> *(x, prod l)}
      Open
     
     SCC (1):
      Strict:
       {*#(s x, s y) -> *#(x, y)}
      Weak:
      {      +(x, 0()) -> x,
             +(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)),
             sum nil() -> 0(),
        sum cons(x, l) -> +(x, sum l),
            prod nil() -> s 0(),
       prod cons(x, l) -> *(x, prod l)}
      Open
     
     SCC (1):
      Strict:
       {sum# cons(x, l) -> sum# l}
      Weak:
      {      +(x, 0()) -> x,
             +(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)),
             sum nil() -> 0(),
        sum cons(x, l) -> +(x, sum l),
            prod nil() -> s 0(),
       prod cons(x, l) -> *(x, prod l)}
      Open
     
     
     SCC (1):
      Strict:
       {+#(s x, s y) -> +#(x, y)}
      Weak:
      {      +(x, 0()) -> x,
             +(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)),
             sum nil() -> 0(),
        sum cons(x, l) -> +(x, sum l),
            prod nil() -> s 0(),
       prod cons(x, l) -> *(x, prod l)}
      Open