MAYBE
Time: 1.115723
TRS:
 {          0 #() -> #(),
        +(x, #()) -> x,
        +(#(), x) -> x,
      +(0 x, 0 y) -> 0 +(x, y),
      +(0 x, 1 y) -> 1 +(x, y),
      +(1 x, 0 y) -> 1 +(x, y),
      +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
        *(#(), x) -> #(),
        *(0 x, y) -> 0 *(x, y),
        *(1 x, y) -> +(0 *(x, y), y),
        sum nil() -> 0 #(),
   sum cons(x, l) -> +(x, sum l),
       prod nil() -> 1 #(),
  prod cons(x, l) -> *(x, prod l)}
 DP:
  DP:
   {    +#(0 x, 0 y) -> 0# +(x, y),
        +#(0 x, 0 y) -> +#(x, y),
        +#(0 x, 1 y) -> +#(x, y),
        +#(1 x, 0 y) -> +#(x, y),
        +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()),
        +#(1 x, 1 y) -> +#(x, y),
        +#(1 x, 1 y) -> +#(+(x, y), 1 #()),
          *#(0 x, y) -> 0# *(x, y),
          *#(0 x, y) -> *#(x, y),
          *#(1 x, y) -> 0# *(x, y),
          *#(1 x, y) -> +#(0 *(x, y), y),
          *#(1 x, y) -> *#(x, y),
          sum# nil() -> 0# #(),
     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:
  {          0 #() -> #(),
         +(x, #()) -> x,
         +(#(), x) -> x,
       +(0 x, 0 y) -> 0 +(x, y),
       +(0 x, 1 y) -> 1 +(x, y),
       +(1 x, 0 y) -> 1 +(x, y),
       +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
         *(#(), x) -> #(),
         *(0 x, y) -> 0 *(x, y),
         *(1 x, y) -> +(0 *(x, y), y),
         sum nil() -> 0 #(),
    sum cons(x, l) -> +(x, sum l),
        prod nil() -> 1 #(),
   prod cons(x, l) -> *(x, prod l)}
  UR:
   {          0 #() -> #(),
          +(x, #()) -> x,
          +(#(), x) -> x,
        +(0 x, 0 y) -> 0 +(x, y),
        +(0 x, 1 y) -> 1 +(x, y),
        +(1 x, 0 y) -> 1 +(x, y),
        +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
          *(#(), x) -> #(),
          *(0 x, y) -> 0 *(x, y),
          *(1 x, y) -> +(0 *(x, y), y),
          sum nil() -> 0 #(),
     sum cons(x, l) -> +(x, sum l),
         prod nil() -> 1 #(),
    prod cons(x, l) -> *(x, prod l),
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(sum# cons(x, l) -> +#(x, sum l), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 1 y) -> +#(x, y))
     (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (sum# cons(x, l) -> +#(x, sum l), +#(1 x, 0 y) -> +#(x, y))
     (sum# cons(x, l) -> +#(x, sum l), +#(0 x, 1 y) -> +#(x, y))
     (sum# cons(x, l) -> +#(x, sum l), +#(0 x, 0 y) -> +#(x, y))
     (sum# cons(x, l) -> +#(x, sum l), +#(0 x, 0 y) -> 0# +(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 0 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 1 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> 0# +(x, y))
     (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))
     (sum# cons(x, l) -> sum# l, sum# nil() -> 0# #())
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y))
     (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y))
     (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y))
     (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y))
     (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y))
     (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y))
     (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y))
     (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (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)
     (prod# cons(x, l) -> *#(x, prod l), *#(0 x, y) -> 0# *(x, y))
     (prod# cons(x, l) -> *#(x, prod l), *#(0 x, y) -> *#(x, y))
     (prod# cons(x, l) -> *#(x, prod l), *#(1 x, y) -> 0# *(x, y))
     (prod# cons(x, l) -> *#(x, prod l), *#(1 x, y) -> +#(0 *(x, y), y))
     (prod# cons(x, l) -> *#(x, prod l), *#(1 x, y) -> *#(x, y))}
    STATUS:
     arrows: 0.771626
     SCCS (4):
      Scc:
       {prod# cons(x, l) -> prod# l}
      Scc:
       {sum# cons(x, l) -> sum# l}
      Scc:
       {*#(0 x, y) -> *#(x, y),
        *#(1 x, y) -> *#(x, y)}
      Scc:
       {+#(0 x, 0 y) -> +#(x, y),
        +#(0 x, 1 y) -> +#(x, y),
        +#(1 x, 0 y) -> +#(x, y),
        +#(1 x, 1 y) -> +#(x, y),
        +#(1 x, 1 y) -> +#(+(x, y), 1 #())}
      
      SCC (1):
       Strict:
        {prod# cons(x, l) -> prod# l}
       Weak:
       {          0 #() -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
            +(0 x, 0 y) -> 0 +(x, y),
            +(0 x, 1 y) -> 1 +(x, y),
            +(1 x, 0 y) -> 1 +(x, y),
            +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
              *(#(), x) -> #(),
              *(0 x, y) -> 0 *(x, y),
              *(1 x, y) -> +(0 *(x, y), y),
              sum nil() -> 0 #(),
         sum cons(x, l) -> +(x, sum l),
             prod nil() -> 1 #(),
        prod cons(x, l) -> *(x, prod l)}
       Open
      SCC (1):
       Strict:
        {sum# cons(x, l) -> sum# l}
       Weak:
       {          0 #() -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
            +(0 x, 0 y) -> 0 +(x, y),
            +(0 x, 1 y) -> 1 +(x, y),
            +(1 x, 0 y) -> 1 +(x, y),
            +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
              *(#(), x) -> #(),
              *(0 x, y) -> 0 *(x, y),
              *(1 x, y) -> +(0 *(x, y), y),
              sum nil() -> 0 #(),
         sum cons(x, l) -> +(x, sum l),
             prod nil() -> 1 #(),
        prod cons(x, l) -> *(x, prod l)}
       Open
      
      SCC (2):
       Strict:
        {*#(0 x, y) -> *#(x, y),
         *#(1 x, y) -> *#(x, y)}
       Weak:
       {          0 #() -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
            +(0 x, 0 y) -> 0 +(x, y),
            +(0 x, 1 y) -> 1 +(x, y),
            +(1 x, 0 y) -> 1 +(x, y),
            +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
              *(#(), x) -> #(),
              *(0 x, y) -> 0 *(x, y),
              *(1 x, y) -> +(0 *(x, y), y),
              sum nil() -> 0 #(),
         sum cons(x, l) -> +(x, sum l),
             prod nil() -> 1 #(),
        prod cons(x, l) -> *(x, prod l)}
       Open
      
      
      
      
      SCC (5):
       Strict:
        {+#(0 x, 0 y) -> +#(x, y),
         +#(0 x, 1 y) -> +#(x, y),
         +#(1 x, 0 y) -> +#(x, y),
         +#(1 x, 1 y) -> +#(x, y),
         +#(1 x, 1 y) -> +#(+(x, y), 1 #())}
       Weak:
       {          0 #() -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
            +(0 x, 0 y) -> 0 +(x, y),
            +(0 x, 1 y) -> 1 +(x, y),
            +(1 x, 0 y) -> 1 +(x, y),
            +(1 x, 1 y) -> 0 +(+(x, y), 1 #()),
              *(#(), x) -> #(),
              *(0 x, y) -> 0 *(x, y),
              *(1 x, y) -> +(0 *(x, y), y),
              sum nil() -> 0 #(),
         sum cons(x, l) -> +(x, sum l),
             prod nil() -> 1 #(),
        prod cons(x, l) -> *(x, prod l)}
       Open