MAYBE
Time: 0.001678
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)}
  UR:
   {      +(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),
            a(z, w) -> z,
            a(z, w) -> w}
   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