MAYBE

Problem:
 app(app(app(fold(),f),x),nil()) -> x
 app(app(app(fold(),f),x),app(app(cons(),y),z)) -> app(app(f,y),app(app(app(fold(),f),x),z))
 app(app(plus(),0()),y) -> y
 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
 app(app(times(),0()),y) -> 0()
 app(app(times(),app(s(),x)),y) -> app(app(plus(),app(app(times(),x),y)),y)
 sum() -> app(app(fold(),add()),0())
 prod() -> app(app(fold(),mul()),app(s(),0()))

Proof:
 Uncurry Processor:
  fold3(f,x,nil()) -> x
  fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
  plus2(0(),y) -> y
  plus2(s1(x),y) -> s1(plus2(x,y))
  times2(0(),y) -> 0()
  times2(s1(x),y) -> plus2(times2(x,y),y)
  sum() -> fold2(add(),0())
  prod() -> fold2(mul(),s1(0()))
  app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
  app(fold1(x5),x6) -> fold2(x5,x6)
  app(fold(),x6) -> fold1(x6)
  app(cons1(x5),x6) -> cons2(x5,x6)
  app(cons(),x6) -> cons1(x6)
  app(plus1(x5),x6) -> plus2(x5,x6)
  app(plus(),x6) -> plus1(x6)
  app(s(),x6) -> s1(x6)
  app(times1(x5),x6) -> times2(x5,x6)
  app(times(),x6) -> times1(x6)
  DP Processor:
   DPs:
    fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z)
    fold{3,#}(f,x,cons2(y,z)) -> app#(f,y)
    fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z))
    plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
    times{2,#}(s1(x),y) -> times{2,#}(x,y)
    times{2,#}(s1(x),y) -> plus{2,#}(times2(x,y),y)
    app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6)
    app#(plus1(x5),x6) -> plus{2,#}(x5,x6)
    app#(times1(x5),x6) -> times{2,#}(x5,x6)
   TRS:
    fold3(f,x,nil()) -> x
    fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
    plus2(0(),y) -> y
    plus2(s1(x),y) -> s1(plus2(x,y))
    times2(0(),y) -> 0()
    times2(s1(x),y) -> plus2(times2(x,y),y)
    sum() -> fold2(add(),0())
    prod() -> fold2(mul(),s1(0()))
    app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
    app(fold1(x5),x6) -> fold2(x5,x6)
    app(fold(),x6) -> fold1(x6)
    app(cons1(x5),x6) -> cons2(x5,x6)
    app(cons(),x6) -> cons1(x6)
    app(plus1(x5),x6) -> plus2(x5,x6)
    app(plus(),x6) -> plus1(x6)
    app(s(),x6) -> s1(x6)
    app(times1(x5),x6) -> times2(x5,x6)
    app(times(),x6) -> times1(x6)
   TDG Processor:
    DPs:
     fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z)
     fold{3,#}(f,x,cons2(y,z)) -> app#(f,y)
     fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z))
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     times{2,#}(s1(x),y) -> times{2,#}(x,y)
     times{2,#}(s1(x),y) -> plus{2,#}(times2(x,y),y)
     app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6)
     app#(plus1(x5),x6) -> plus{2,#}(x5,x6)
     app#(times1(x5),x6) -> times{2,#}(x5,x6)
    TRS:
     fold3(f,x,nil()) -> x
     fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
     plus2(0(),y) -> y
     plus2(s1(x),y) -> s1(plus2(x,y))
     times2(0(),y) -> 0()
     times2(s1(x),y) -> plus2(times2(x,y),y)
     sum() -> fold2(add(),0())
     prod() -> fold2(mul(),s1(0()))
     app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
     app(fold1(x5),x6) -> fold2(x5,x6)
     app(fold(),x6) -> fold1(x6)
     app(cons1(x5),x6) -> cons2(x5,x6)
     app(cons(),x6) -> cons1(x6)
     app(plus1(x5),x6) -> plus2(x5,x6)
     app(plus(),x6) -> plus1(x6)
     app(s(),x6) -> s1(x6)
     app(times1(x5),x6) -> times2(x5,x6)
     app(times(),x6) -> times1(x6)
    graph:
     times{2,#}(s1(x),y) -> times{2,#}(x,y) ->
     times{2,#}(s1(x),y) -> plus{2,#}(times2(x,y),y)
     times{2,#}(s1(x),y) -> times{2,#}(x,y) ->
     times{2,#}(s1(x),y) -> times{2,#}(x,y)
     times{2,#}(s1(x),y) -> plus{2,#}(times2(x,y),y) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     app#(times1(x5),x6) -> times{2,#}(x5,x6) ->
     times{2,#}(s1(x),y) -> plus{2,#}(times2(x,y),y)
     app#(times1(x5),x6) -> times{2,#}(x5,x6) ->
     times{2,#}(s1(x),y) -> times{2,#}(x,y)
     app#(plus1(x5),x6) -> plus{2,#}(x5,x6) ->
     plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6) ->
     fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z))
     app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6) ->
     fold{3,#}(f,x,cons2(y,z)) -> app#(f,y)
     app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6) ->
     fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z)
     fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z)) ->
     app#(times1(x5),x6) -> times{2,#}(x5,x6)
     fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z)) ->
     app#(plus1(x5),x6) -> plus{2,#}(x5,x6)
     fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z)) ->
     app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6)
     fold{3,#}(f,x,cons2(y,z)) -> app#(f,y) ->
     app#(times1(x5),x6) -> times{2,#}(x5,x6)
     fold{3,#}(f,x,cons2(y,z)) -> app#(f,y) ->
     app#(plus1(x5),x6) -> plus{2,#}(x5,x6)
     fold{3,#}(f,x,cons2(y,z)) -> app#(f,y) ->
     app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6)
     fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z) ->
     fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z))
     fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z) ->
     fold{3,#}(f,x,cons2(y,z)) -> app#(f,y)
     fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z) -> fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z)
    SCC Processor:
     #sccs: 3
     #rules: 6
     #arcs: 19/81
     DPs:
      app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6)
      fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z)
      fold{3,#}(f,x,cons2(y,z)) -> app#(f,y)
      fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z))
     TRS:
      fold3(f,x,nil()) -> x
      fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      times2(0(),y) -> 0()
      times2(s1(x),y) -> plus2(times2(x,y),y)
      sum() -> fold2(add(),0())
      prod() -> fold2(mul(),s1(0()))
      app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
      app(fold1(x5),x6) -> fold2(x5,x6)
      app(fold(),x6) -> fold1(x6)
      app(cons1(x5),x6) -> cons2(x5,x6)
      app(cons(),x6) -> cons1(x6)
      app(plus1(x5),x6) -> plus2(x5,x6)
      app(plus(),x6) -> plus1(x6)
      app(s(),x6) -> s1(x6)
      app(times1(x5),x6) -> times2(x5,x6)
      app(times(),x6) -> times1(x6)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [app#](x0, x1) = 1x0 + x1,
       
       [fold{3,#}](x0, x1, x2) = 2x0 + 1x1 + x2,
       
       [times2](x0, x1) = x1 + 4,
       
       [times1](x0) = 4,
       
       [s1](x0) = x0,
       
       [plus2](x0, x1) = x1,
       
       [plus1](x0) = x0,
       
       [cons2](x0, x1) = 1x0 + x1 + 0,
       
       [cons1](x0) = x0 + 4,
       
       [fold1](x0) = x0,
       
       [fold3](x0, x1, x2) = 2x0 + 1x1 + x2,
       
       [fold2](x0, x1) = 1x0 + x1,
       
       [mul] = 2,
       
       [prod] = 5,
       
       [add] = 3,
       
       [sum] = 4,
       
       [times] = 5,
       
       [s] = 1,
       
       [0] = 4,
       
       [plus] = 1,
       
       [cons] = 4,
       
       [nil] = 0,
       
       [app](x0, x1) = 1x0 + x1,
       
       [fold] = 6
      orientation:
       app#(fold2(x5,x4),x6) = 1x4 + 2x5 + x6 >= 1x4 + 2x5 + x6 = fold{3,#}(x5,x4,x6)
       
       fold{3,#}(f,x,cons2(y,z)) = 2f + 1x + 1y + z + 0 >= 2f + 1x + z = fold{3,#}(f,x,z)
       
       fold{3,#}(f,x,cons2(y,z)) = 2f + 1x + 1y + z + 0 >= 1f + y = app#(f,y)
       
       fold{3,#}(f,x,cons2(y,z)) = 2f + 1x + 1y + z + 0 >= 2f + 1x + 1y + z = app#(app(f,y),fold3(f,x,z))
       
       fold3(f,x,nil()) = 2f + 1x + 0 >= x = x
       
       fold3(f,x,cons2(y,z)) = 2f + 1x + 1y + z + 0 >= 2f + 1x + 1y + z = app(app(f,y),fold3(f,x,z))
       
       plus2(0(),y) = y >= y = y
       
       plus2(s1(x),y) = y >= y = s1(plus2(x,y))
       
       times2(0(),y) = y + 4 >= 4 = 0()
       
       times2(s1(x),y) = y + 4 >= y = plus2(times2(x,y),y)
       
       sum() = 4 >= 4 = fold2(add(),0())
       
       prod() = 5 >= 4 = fold2(mul(),s1(0()))
       
       app(fold2(x5,x4),x6) = 1x4 + 2x5 + x6 >= 1x4 + 2x5 + x6 = fold3(x5,x4,x6)
       
       app(fold1(x5),x6) = 1x5 + x6 >= 1x5 + x6 = fold2(x5,x6)
       
       app(fold(),x6) = x6 + 7 >= x6 = fold1(x6)
       
       app(cons1(x5),x6) = 1x5 + x6 + 5 >= 1x5 + x6 + 0 = cons2(x5,x6)
       
       app(cons(),x6) = x6 + 5 >= x6 + 4 = cons1(x6)
       
       app(plus1(x5),x6) = 1x5 + x6 >= x6 = plus2(x5,x6)
       
       app(plus(),x6) = x6 + 2 >= x6 = plus1(x6)
       
       app(s(),x6) = x6 + 2 >= x6 = s1(x6)
       
       app(times1(x5),x6) = x6 + 5 >= x6 + 4 = times2(x5,x6)
       
       app(times(),x6) = x6 + 6 >= 4 = times1(x6)
      problem:
       DPs:
        app#(fold2(x5,x4),x6) -> fold{3,#}(x5,x4,x6)
        fold{3,#}(f,x,cons2(y,z)) -> fold{3,#}(f,x,z)
        fold{3,#}(f,x,cons2(y,z)) -> app#(app(f,y),fold3(f,x,z))
       TRS:
        fold3(f,x,nil()) -> x
        fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        times2(0(),y) -> 0()
        times2(s1(x),y) -> plus2(times2(x,y),y)
        sum() -> fold2(add(),0())
        prod() -> fold2(mul(),s1(0()))
        app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
        app(fold1(x5),x6) -> fold2(x5,x6)
        app(fold(),x6) -> fold1(x6)
        app(cons1(x5),x6) -> cons2(x5,x6)
        app(cons(),x6) -> cons1(x6)
        app(plus1(x5),x6) -> plus2(x5,x6)
        app(plus(),x6) -> plus1(x6)
        app(s(),x6) -> s1(x6)
        app(times1(x5),x6) -> times2(x5,x6)
        app(times(),x6) -> times1(x6)
      Open
     
     DPs:
      times{2,#}(s1(x),y) -> times{2,#}(x,y)
     TRS:
      fold3(f,x,nil()) -> x
      fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      times2(0(),y) -> 0()
      times2(s1(x),y) -> plus2(times2(x,y),y)
      sum() -> fold2(add(),0())
      prod() -> fold2(mul(),s1(0()))
      app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
      app(fold1(x5),x6) -> fold2(x5,x6)
      app(fold(),x6) -> fold1(x6)
      app(cons1(x5),x6) -> cons2(x5,x6)
      app(cons(),x6) -> cons1(x6)
      app(plus1(x5),x6) -> plus2(x5,x6)
      app(plus(),x6) -> plus1(x6)
      app(s(),x6) -> s1(x6)
      app(times1(x5),x6) -> times2(x5,x6)
      app(times(),x6) -> times1(x6)
     Subterm Criterion Processor:
      simple projection:
       pi(times{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        fold3(f,x,nil()) -> x
        fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        times2(0(),y) -> 0()
        times2(s1(x),y) -> plus2(times2(x,y),y)
        sum() -> fold2(add(),0())
        prod() -> fold2(mul(),s1(0()))
        app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
        app(fold1(x5),x6) -> fold2(x5,x6)
        app(fold(),x6) -> fold1(x6)
        app(cons1(x5),x6) -> cons2(x5,x6)
        app(cons(),x6) -> cons1(x6)
        app(plus1(x5),x6) -> plus2(x5,x6)
        app(plus(),x6) -> plus1(x6)
        app(s(),x6) -> s1(x6)
        app(times1(x5),x6) -> times2(x5,x6)
        app(times(),x6) -> times1(x6)
      Qed
     
     DPs:
      plus{2,#}(s1(x),y) -> plus{2,#}(x,y)
     TRS:
      fold3(f,x,nil()) -> x
      fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
      plus2(0(),y) -> y
      plus2(s1(x),y) -> s1(plus2(x,y))
      times2(0(),y) -> 0()
      times2(s1(x),y) -> plus2(times2(x,y),y)
      sum() -> fold2(add(),0())
      prod() -> fold2(mul(),s1(0()))
      app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
      app(fold1(x5),x6) -> fold2(x5,x6)
      app(fold(),x6) -> fold1(x6)
      app(cons1(x5),x6) -> cons2(x5,x6)
      app(cons(),x6) -> cons1(x6)
      app(plus1(x5),x6) -> plus2(x5,x6)
      app(plus(),x6) -> plus1(x6)
      app(s(),x6) -> s1(x6)
      app(times1(x5),x6) -> times2(x5,x6)
      app(times(),x6) -> times1(x6)
     Subterm Criterion Processor:
      simple projection:
       pi(plus{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        fold3(f,x,nil()) -> x
        fold3(f,x,cons2(y,z)) -> app(app(f,y),fold3(f,x,z))
        plus2(0(),y) -> y
        plus2(s1(x),y) -> s1(plus2(x,y))
        times2(0(),y) -> 0()
        times2(s1(x),y) -> plus2(times2(x,y),y)
        sum() -> fold2(add(),0())
        prod() -> fold2(mul(),s1(0()))
        app(fold2(x5,x4),x6) -> fold3(x5,x4,x6)
        app(fold1(x5),x6) -> fold2(x5,x6)
        app(fold(),x6) -> fold1(x6)
        app(cons1(x5),x6) -> cons2(x5,x6)
        app(cons(),x6) -> cons1(x6)
        app(plus1(x5),x6) -> plus2(x5,x6)
        app(plus(),x6) -> plus1(x6)
        app(s(),x6) -> s1(x6)
        app(times1(x5),x6) -> times2(x5,x6)
        app(times(),x6) -> times1(x6)
      Qed