MAYBE

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   +#(0(x),0(y)) -> +#(x,y)
   +#(0(x),0(y)) -> 0#(+(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(#()))
   +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
   *#(0(x),y) -> *#(x,y)
   *#(0(x),y) -> 0#(*(x,y))
   *#(1(x),y) -> *#(x,y)
   *#(1(x),y) -> 0#(*(x,y))
   *#(1(x),y) -> +#(0(*(x,y)),y)
   sum#(nil()) -> 0#(#())
   sum#(cons(x,l)) -> sum#(l)
   sum#(cons(x,l)) -> +#(x,sum(l))
   prod#(cons(x,l)) -> prod#(l)
   prod#(cons(x,l)) -> *#(x,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))
  TDG Processor:
   DPs:
    +#(0(x),0(y)) -> +#(x,y)
    +#(0(x),0(y)) -> 0#(+(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(#()))
    +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    *#(0(x),y) -> *#(x,y)
    *#(0(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> *#(x,y)
    *#(1(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> +#(0(*(x,y)),y)
    sum#(nil()) -> 0#(#())
    sum#(cons(x,l)) -> sum#(l)
    sum#(cons(x,l)) -> +#(x,sum(l))
    prod#(cons(x,l)) -> prod#(l)
    prod#(cons(x,l)) -> *#(x,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))
   graph:
    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)) ->
    *#(1(x),y) -> +#(0(*(x,y)),y)
    prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(1(x),y) -> 0#(*(x,y))
    prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(1(x),y) -> *#(x,y)
    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)
    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)
    sum#(cons(x,l)) -> sum#(l) -> sum#(nil()) -> 0#(#())
    sum#(cons(x,l)) -> +#(x,sum(l)) ->
    +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    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),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)) -> 0#(+(x,y))
    sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),0(y)) -> +#(x,y)
    *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> +#(0(*(x,y)),y)
    *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> *#(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) -> +#(0(*(x,y)),y) ->
    +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    *#(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),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)) -> 0#(+(x,y))
    *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),0(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) -> *#(1(x),y) -> *#(x,y)
    *#(0(x),y) -> *#(x,y) -> *#(0(x),y) -> 0#(*(x,y))
    *#(0(x),y) -> *#(x,y) -> *#(0(x),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(#()))
    +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
    +#(1(x),1(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
    +#(1(x),0(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
    +#(0(x),1(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
    +#(0(x),0(y)) -> 0#(+(x,y))
    +#(1(x),1(y)) -> +#(+(x,y),1(#())) -> +#(0(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(#()))
    +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(x,y) -> +#(0(x),1(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),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(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),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)) -> 0#(+(x,y))
    +#(1(x),0(y)) -> +#(x,y) -> +#(0(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),1(#()))
    +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(x,y)
    +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
    +#(0(x),1(y)) -> +#(x,y) -> +#(0(x),1(y)) -> +#(x,y)
    +#(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),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(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),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)) -> 0#(+(x,y))
    +#(0(x),0(y)) -> +#(x,y) -> +#(0(x),0(y)) -> +#(x,y)
   EDG Processor:
    DPs:
     +#(0(x),0(y)) -> +#(x,y)
     +#(0(x),0(y)) -> 0#(+(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(#()))
     +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     *#(0(x),y) -> *#(x,y)
     *#(0(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> *#(x,y)
     *#(1(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> +#(0(*(x,y)),y)
     sum#(nil()) -> 0#(#())
     sum#(cons(x,l)) -> sum#(l)
     sum#(cons(x,l)) -> +#(x,sum(l))
     prod#(cons(x,l)) -> prod#(l)
     prod#(cons(x,l)) -> *#(x,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))
    graph:
     prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> prod#(l)
     prod#(cons(x,l)) -> prod#(l) ->
     prod#(cons(x,l)) -> *#(x,prod(l))
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(0(x),y) -> *#(x,y)
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(0(x),y) -> 0#(*(x,y))
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(1(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)
     sum#(cons(x,l)) -> sum#(l) -> sum#(nil()) -> 0#(#())
     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)) -> +#(x,sum(l)) -> +#(0(x),0(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),0(y)) -> 0#(+(x,y))
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),1(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(1(x),0(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(1(x),1(y)) -> +#(x,y)
     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)) -> 0#(+(+(x,y),1(#())))
     *#(1(x),y) -> *#(x,y) -> *#(0(x),y) -> *#(x,y)
     *#(1(x),y) -> *#(x,y) -> *#(0(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> *#(x,y) -> *#(1(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) -> +#(0(*(x,y)),y) -> +#(0(x),0(y)) -> +#(x,y)
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),0(y)) -> 0#(+(x,y))
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),1(y)) -> +#(x,y)
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(1(x),0(y)) -> +#(x,y)
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(1(x),1(y)) -> +#(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)) -> 0#(+(+(x,y),1(#())))
     *#(0(x),y) -> *#(x,y) -> *#(0(x),y) -> *#(x,y)
     *#(0(x),y) -> *#(x,y) -> *#(0(x),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))
     *#(0(x),y) -> *#(x,y) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
     +#(0(x),1(y)) -> +#(x,y)
     +#(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(#()))
     +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
     +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     +#(1(x),1(y)) -> +#(x,y) -> +#(0(x),0(y)) -> +#(x,y)
     +#(1(x),1(y)) -> +#(x,y) -> +#(0(x),0(y)) -> 0#(+(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)) -> +#(x,y)
     +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     +#(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))
     +#(1(x),0(y)) -> +#(x,y) -> +#(0(x),1(y)) -> +#(x,y)
     +#(1(x),0(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
     +#(1(x),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(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)) -> 0#(+(+(x,y),1(#())))
     +#(0(x),1(y)) -> +#(x,y) -> +#(0(x),0(y)) -> +#(x,y)
     +#(0(x),1(y)) -> +#(x,y) -> +#(0(x),0(y)) -> 0#(+(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)) -> +#(x,y)
     +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     +#(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))
     +#(0(x),0(y)) -> +#(x,y) -> +#(0(x),1(y)) -> +#(x,y)
     +#(0(x),0(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
     +#(0(x),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(x,y)
     +#(0(x),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     +#(0(x),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    CDG Processor:
     DPs:
      +#(0(x),0(y)) -> +#(x,y)
      +#(0(x),0(y)) -> 0#(+(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(#()))
      +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
      *#(0(x),y) -> *#(x,y)
      *#(0(x),y) -> 0#(*(x,y))
      *#(1(x),y) -> *#(x,y)
      *#(1(x),y) -> 0#(*(x,y))
      *#(1(x),y) -> +#(0(*(x,y)),y)
      sum#(nil()) -> 0#(#())
      sum#(cons(x,l)) -> sum#(l)
      sum#(cons(x,l)) -> +#(x,sum(l))
      prod#(cons(x,l)) -> prod#(l)
      prod#(cons(x,l)) -> *#(x,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))
     graph:
      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)) ->
      *#(1(x),y) -> +#(0(*(x,y)),y)
      prod#(cons(x,l)) -> *#(x,prod(l)) ->
      *#(1(x),y) -> 0#(*(x,y))
      prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(1(x),y) -> *#(x,y)
      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)
      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)
      sum#(cons(x,l)) -> sum#(l) -> sum#(nil()) -> 0#(#())
      sum#(cons(x,l)) -> +#(x,sum(l)) ->
      +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
      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),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)) -> 0#(+(x,y))
      sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),0(y)) -> +#(x,y)
      *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> +#(0(*(x,y)),y)
      *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> 0#(*(x,y))
      *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> *#(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) -> +#(0(*(x,y)),y) -> +#(0(x),1(y)) -> +#(x,y)
      *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),0(y)) -> 0#(+(x,y))
      *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),0(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) -> *#(1(x),y) -> *#(x,y)
      *#(0(x),y) -> *#(x,y) -> *#(0(x),y) -> 0#(*(x,y))
      *#(0(x),y) -> *#(x,y) -> *#(0(x),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(#()))
      +#(1(x),1(y)) -> +#(+(x,y),1(#())) ->
      +#(1(x),1(y)) -> +#(x,y)
      +#(1(x),1(y)) -> +#(+(x,y),1(#())) -> +#(0(x),1(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(#()))
      +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(x,y)
      +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
      +#(1(x),1(y)) -> +#(x,y) -> +#(0(x),1(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),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
      +#(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),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)) -> 0#(+(x,y))
      +#(1(x),0(y)) -> +#(x,y) -> +#(0(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),1(#()))
      +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> +#(x,y)
      +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
      +#(0(x),1(y)) -> +#(x,y) -> +#(0(x),1(y)) -> +#(x,y)
      +#(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),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
      +#(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),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)) -> 0#(+(x,y))
      +#(0(x),0(y)) -> +#(x,y) -> +#(0(x),0(y)) -> +#(x,y)
     SCC Processor:
      #sccs: 4
      #rules: 9
      #arcs: 62/289
      DPs:
       sum#(cons(x,l)) -> sum#(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))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [sum#](x0) = 2x0,
        
        [prod](x0) = x0 + 0,
        
        [cons](x0, x1) = 7x0 + 3x1 + 4,
        
        [sum](x0) = x0 + 0,
        
        [nil] = 4,
        
        [*](x0, x1) = 3x0 + 2x1 + 3,
        
        [1](x0) = 2,
        
        [+](x0, x1) = 1x0 + 1x1,
        
        [0](x0) = 2,
        
        [#] = 0
       orientation:
        sum#(cons(x,l)) = 5l + 9x + 6 >= 2l = sum#(l)
        
        0(#()) = 2 >= 0 = #()
        
        +(x,#()) = 1x + 1 >= x = x
        
        +(#(),x) = 1x + 1 >= x = x
        
        +(0(x),0(y)) = 3 >= 2 = 0(+(x,y))
        
        +(0(x),1(y)) = 3 >= 2 = 1(+(x,y))
        
        +(1(x),0(y)) = 3 >= 2 = 1(+(x,y))
        
        +(1(x),1(y)) = 3 >= 2 = 0(+(+(x,y),1(#())))
        
        *(#(),x) = 2x + 3 >= 0 = #()
        
        *(0(x),y) = 2y + 5 >= 2 = 0(*(x,y))
        
        *(1(x),y) = 2y + 5 >= 1y + 3 = +(0(*(x,y)),y)
        
        sum(nil()) = 4 >= 2 = 0(#())
        
        sum(cons(x,l)) = 3l + 7x + 4 >= 1l + 1x + 1 = +(x,sum(l))
        
        prod(nil()) = 4 >= 2 = 1(#())
        
        prod(cons(x,l)) = 3l + 7x + 4 >= 2l + 3x + 3 = *(x,prod(l))
       problem:
        DPs:
         
        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))
       Qed
      
      DPs:
       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))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [prod#](x0) = 2x0,
        
        [prod](x0) = x0 + 0,
        
        [cons](x0, x1) = 7x0 + 3x1 + 4,
        
        [sum](x0) = x0 + 0,
        
        [nil] = 4,
        
        [*](x0, x1) = 3x0 + 2x1 + 3,
        
        [1](x0) = 2,
        
        [+](x0, x1) = 1x0 + 1x1,
        
        [0](x0) = 2,
        
        [#] = 0
       orientation:
        prod#(cons(x,l)) = 5l + 9x + 6 >= 2l = prod#(l)
        
        0(#()) = 2 >= 0 = #()
        
        +(x,#()) = 1x + 1 >= x = x
        
        +(#(),x) = 1x + 1 >= x = x
        
        +(0(x),0(y)) = 3 >= 2 = 0(+(x,y))
        
        +(0(x),1(y)) = 3 >= 2 = 1(+(x,y))
        
        +(1(x),0(y)) = 3 >= 2 = 1(+(x,y))
        
        +(1(x),1(y)) = 3 >= 2 = 0(+(+(x,y),1(#())))
        
        *(#(),x) = 2x + 3 >= 0 = #()
        
        *(0(x),y) = 2y + 5 >= 2 = 0(*(x,y))
        
        *(1(x),y) = 2y + 5 >= 1y + 3 = +(0(*(x,y)),y)
        
        sum(nil()) = 4 >= 2 = 0(#())
        
        sum(cons(x,l)) = 3l + 7x + 4 >= 1l + 1x + 1 = +(x,sum(l))
        
        prod(nil()) = 4 >= 2 = 1(#())
        
        prod(cons(x,l)) = 3l + 7x + 4 >= 2l + 3x + 3 = *(x,prod(l))
       problem:
        DPs:
         
        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))
       Qed
      
      DPs:
       *#(0(x),y) -> *#(x,y)
       *#(1(x),y) -> *#(x,y)
      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))
      Open
      
      DPs:
       +#(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(#()))
      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))
      Open