MAYBE

Problem:
 app(app(app(fold(),f),nil()),x) -> x
 app(app(app(fold(),f),app(app(cons(),h),t)),x) -> app(app(app(fold(),f),t),app(app(f,x),h))
 app(sum(),l) -> app(app(app(fold(),add()),l),0())
 app(app(app(fold(),mul()),l),1()) -> app(prod(),l)

Proof:
 Uncurry Processor:
  fold3(f,nil(),x) -> x
  fold3(f,cons2(h,t),x) -> fold3(f,t,app(app(f,x),h))
  sum1(l) -> fold3(add(),l,0())
  fold3(mul(),l,1()) -> prod1(l)
  app(fold2(x6,x5),x7) -> fold3(x6,x5,x7)
  app(fold1(x6),x7) -> fold2(x6,x7)
  app(fold(),x7) -> fold1(x7)
  app(cons1(x6),x7) -> cons2(x6,x7)
  app(cons(),x7) -> cons1(x7)
  app(sum(),x7) -> sum1(x7)
  app(prod(),x7) -> prod1(x7)
  DP Processor:
   DPs:
    fold{3,#}(f,cons2(h,t),x) -> app#(f,x)
    fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h)
    fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h))
    sum{1,#}(l) -> fold{3,#}(add(),l,0())
    app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7)
    app#(sum(),x7) -> sum{1,#}(x7)
   TRS:
    fold3(f,nil(),x) -> x
    fold3(f,cons2(h,t),x) -> fold3(f,t,app(app(f,x),h))
    sum1(l) -> fold3(add(),l,0())
    fold3(mul(),l,1()) -> prod1(l)
    app(fold2(x6,x5),x7) -> fold3(x6,x5,x7)
    app(fold1(x6),x7) -> fold2(x6,x7)
    app(fold(),x7) -> fold1(x7)
    app(cons1(x6),x7) -> cons2(x6,x7)
    app(cons(),x7) -> cons1(x7)
    app(sum(),x7) -> sum1(x7)
    app(prod(),x7) -> prod1(x7)
   TDG Processor:
    DPs:
     fold{3,#}(f,cons2(h,t),x) -> app#(f,x)
     fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h)
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h))
     sum{1,#}(l) -> fold{3,#}(add(),l,0())
     app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7)
     app#(sum(),x7) -> sum{1,#}(x7)
    TRS:
     fold3(f,nil(),x) -> x
     fold3(f,cons2(h,t),x) -> fold3(f,t,app(app(f,x),h))
     sum1(l) -> fold3(add(),l,0())
     fold3(mul(),l,1()) -> prod1(l)
     app(fold2(x6,x5),x7) -> fold3(x6,x5,x7)
     app(fold1(x6),x7) -> fold2(x6,x7)
     app(fold(),x7) -> fold1(x7)
     app(cons1(x6),x7) -> cons2(x6,x7)
     app(cons(),x7) -> cons1(x7)
     app(sum(),x7) -> sum1(x7)
     app(prod(),x7) -> prod1(x7)
    graph:
     sum{1,#}(l) -> fold{3,#}(add(),l,0()) ->
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h))
     sum{1,#}(l) -> fold{3,#}(add(),l,0()) ->
     fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h)
     sum{1,#}(l) -> fold{3,#}(add(),l,0()) ->
     fold{3,#}(f,cons2(h,t),x) -> app#(f,x)
     app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7) ->
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h))
     app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7) ->
     fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h)
     app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7) ->
     fold{3,#}(f,cons2(h,t),x) -> app#(f,x)
     app#(sum(),x7) -> sum{1,#}(x7) ->
     sum{1,#}(l) -> fold{3,#}(add(),l,0())
     fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(sum(),x7) -> sum{1,#}(x7)
     fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7)
     fold{3,#}(f,cons2(h,t),x) -> app#(f,x) ->
     app#(sum(),x7) -> sum{1,#}(x7)
     fold{3,#}(f,cons2(h,t),x) -> app#(f,x) ->
     app#(fold2(x6,x5),x7) -> fold{3,#}(x6,x5,x7)
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h)) ->
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h))
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h)) ->
     fold{3,#}(f,cons2(h,t),x) -> app#(app(f,x),h)
     fold{3,#}(f,cons2(h,t),x) -> fold{3,#}(f,t,app(app(f,x),h)) ->
     fold{3,#}(f,cons2(h,t),x) -> app#(f,x)
    Open