MAYBE

Problem:
 app(app(add(),0()),y) -> y
 app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y))
 app(app(mult(),0()),y) -> 0()
 app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y)
 app(app(app(rec(),f),x),0()) -> x
 app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y))
 fact() -> app(app(rec(),mult()),app(s(),0()))

Proof:
 Uncurry Processor:
  add2(0(),y) -> y
  add2(s1(x),y) -> s1(add2(x,y))
  mult2(0(),y) -> 0()
  mult2(s1(x),y) -> add2(mult2(x,y),y)
  rec3(f,x,0()) -> x
  rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
  fact() -> rec2(mult(),s1(0()))
  app(add1(x4),x5) -> add2(x4,x5)
  app(add(),x5) -> add1(x5)
  app(s(),x5) -> s1(x5)
  app(mult1(x4),x5) -> mult2(x4,x5)
  app(mult(),x5) -> mult1(x5)
  app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
  app(rec1(x4),x5) -> rec2(x4,x5)
  app(rec(),x5) -> rec1(x5)
  DP Processor:
   DPs:
    add{2,#}(s1(x),y) -> add{2,#}(x,y)
    mult{2,#}(s1(x),y) -> mult{2,#}(x,y)
    mult{2,#}(s1(x),y) -> add{2,#}(mult2(x,y),y)
    rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
    rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
    rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
    app#(add1(x4),x5) -> add{2,#}(x4,x5)
    app#(mult1(x4),x5) -> mult{2,#}(x4,x5)
    app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
   TRS:
    add2(0(),y) -> y
    add2(s1(x),y) -> s1(add2(x,y))
    mult2(0(),y) -> 0()
    mult2(s1(x),y) -> add2(mult2(x,y),y)
    rec3(f,x,0()) -> x
    rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
    fact() -> rec2(mult(),s1(0()))
    app(add1(x4),x5) -> add2(x4,x5)
    app(add(),x5) -> add1(x5)
    app(s(),x5) -> s1(x5)
    app(mult1(x4),x5) -> mult2(x4,x5)
    app(mult(),x5) -> mult1(x5)
    app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
    app(rec1(x4),x5) -> rec2(x4,x5)
    app(rec(),x5) -> rec1(x5)
   TDG Processor:
    DPs:
     add{2,#}(s1(x),y) -> add{2,#}(x,y)
     mult{2,#}(s1(x),y) -> mult{2,#}(x,y)
     mult{2,#}(s1(x),y) -> add{2,#}(mult2(x,y),y)
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     app#(add1(x4),x5) -> add{2,#}(x4,x5)
     app#(mult1(x4),x5) -> mult{2,#}(x4,x5)
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
    TRS:
     add2(0(),y) -> y
     add2(s1(x),y) -> s1(add2(x,y))
     mult2(0(),y) -> 0()
     mult2(s1(x),y) -> add2(mult2(x,y),y)
     rec3(f,x,0()) -> x
     rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
     fact() -> rec2(mult(),s1(0()))
     app(add1(x4),x5) -> add2(x4,x5)
     app(add(),x5) -> add1(x5)
     app(s(),x5) -> s1(x5)
     app(mult1(x4),x5) -> mult2(x4,x5)
     app(mult(),x5) -> mult1(x5)
     app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
     app(rec1(x4),x5) -> rec2(x4,x5)
     app(rec(),x5) -> rec1(x5)
    graph:
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5) ->
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5) ->
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5) ->
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
     app#(mult1(x4),x5) -> mult{2,#}(x4,x5) ->
     mult{2,#}(s1(x),y) -> add{2,#}(mult2(x,y),y)
     app#(mult1(x4),x5) -> mult{2,#}(x4,x5) ->
     mult{2,#}(s1(x),y) -> mult{2,#}(x,y)
     app#(add1(x4),x5) -> add{2,#}(x4,x5) ->
     add{2,#}(s1(x),y) -> add{2,#}(x,y)
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y)) ->
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y)) ->
     app#(mult1(x4),x5) -> mult{2,#}(x4,x5)
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y)) ->
     app#(add1(x4),x5) -> add{2,#}(x4,x5)
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y)) ->
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y)) ->
     app#(mult1(x4),x5) -> mult{2,#}(x4,x5)
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y)) ->
     app#(add1(x4),x5) -> add{2,#}(x4,x5)
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y) ->
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y) ->
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y) ->
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
     mult{2,#}(s1(x),y) -> mult{2,#}(x,y) ->
     mult{2,#}(s1(x),y) -> add{2,#}(mult2(x,y),y)
     mult{2,#}(s1(x),y) -> mult{2,#}(x,y) ->
     mult{2,#}(s1(x),y) -> mult{2,#}(x,y)
     mult{2,#}(s1(x),y) -> add{2,#}(mult2(x,y),y) ->
     add{2,#}(s1(x),y) -> add{2,#}(x,y)
     add{2,#}(s1(x),y) -> add{2,#}(x,y) -> add{2,#}(s1(x),y) -> add{2,#}(x,y)
    SCC Processor:
     #sccs: 3
     #rules: 6
     #arcs: 19/81
     DPs:
      app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
      rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
      rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
      rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     TRS:
      add2(0(),y) -> y
      add2(s1(x),y) -> s1(add2(x,y))
      mult2(0(),y) -> 0()
      mult2(s1(x),y) -> add2(mult2(x,y),y)
      rec3(f,x,0()) -> x
      rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
      fact() -> rec2(mult(),s1(0()))
      app(add1(x4),x5) -> add2(x4,x5)
      app(add(),x5) -> add1(x5)
      app(s(),x5) -> s1(x5)
      app(mult1(x4),x5) -> mult2(x4,x5)
      app(mult(),x5) -> mult1(x5)
      app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
      app(rec1(x4),x5) -> rec2(x4,x5)
      app(rec(),x5) -> rec1(x5)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [app#](x0, x1) = 1x0 + x1 + 0,
       
       [rec{3,#}](x0, x1, x2) = 2x0 + 1x1 + 1,
       
       [rec1](x0) = x0 + 0,
       
       [rec3](x0, x1, x2) = 2x0 + 1x1 + 1,
       
       [rec2](x0, x1) = 1x0 + x1 + 1,
       
       [mult2](x0, x1) = x0 + x1,
       
       [mult1](x0) = x0,
       
       [s1](x0) = 0,
       
       [add2](x0, x1) = x1 + 0,
       
       [add1](x0) = x0,
       
       [fact] = 5,
       
       [rec] = 1,
       
       [mult] = 3,
       
       [s] = 3,
       
       [app](x0, x1) = 1x0 + x1 + 0,
       
       [0] = 0,
       
       [add] = 2
      orientation:
       app#(rec2(x4,x3),x5) = 1x3 + 2x4 + x5 + 2 >= 1x3 + 2x4 + 1 = rec{3,#}(x4,x3,x5)
       
       rec{3,#}(f,x,s1(y)) = 2f + 1x + 1 >= 2f + 1x + 1 = rec{3,#}(f,x,y)
       
       rec{3,#}(f,x,s1(y)) = 2f + 1x + 1 >= 1f + 0 = app#(f,s1(y))
       
       rec{3,#}(f,x,s1(y)) = 2f + 1x + 1 >= 2f + 1x + 1 = app#(app(f,s1(y)),rec3(f,x,y))
       
       add2(0(),y) = y + 0 >= y = y
       
       add2(s1(x),y) = y + 0 >= 0 = s1(add2(x,y))
       
       mult2(0(),y) = y + 0 >= 0 = 0()
       
       mult2(s1(x),y) = y + 0 >= y + 0 = add2(mult2(x,y),y)
       
       rec3(f,x,0()) = 2f + 1x + 1 >= x = x
       
       rec3(f,x,s1(y)) = 2f + 1x + 1 >= 2f + 1x + 1 = app(app(f,s1(y)),rec3(f,x,y))
       
       fact() = 5 >= 4 = rec2(mult(),s1(0()))
       
       app(add1(x4),x5) = 1x4 + x5 + 0 >= x5 + 0 = add2(x4,x5)
       
       app(add(),x5) = x5 + 3 >= x5 = add1(x5)
       
       app(s(),x5) = x5 + 4 >= 0 = s1(x5)
       
       app(mult1(x4),x5) = 1x4 + x5 + 0 >= x4 + x5 = mult2(x4,x5)
       
       app(mult(),x5) = x5 + 4 >= x5 = mult1(x5)
       
       app(rec2(x4,x3),x5) = 1x3 + 2x4 + x5 + 2 >= 1x3 + 2x4 + 1 = rec3(x4,x3,x5)
       
       app(rec1(x4),x5) = 1x4 + x5 + 1 >= 1x4 + x5 + 1 = rec2(x4,x5)
       
       app(rec(),x5) = x5 + 2 >= x5 + 0 = rec1(x5)
      problem:
       DPs:
        app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
        rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
        rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
       TRS:
        add2(0(),y) -> y
        add2(s1(x),y) -> s1(add2(x,y))
        mult2(0(),y) -> 0()
        mult2(s1(x),y) -> add2(mult2(x,y),y)
        rec3(f,x,0()) -> x
        rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
        fact() -> rec2(mult(),s1(0()))
        app(add1(x4),x5) -> add2(x4,x5)
        app(add(),x5) -> add1(x5)
        app(s(),x5) -> s1(x5)
        app(mult1(x4),x5) -> mult2(x4,x5)
        app(mult(),x5) -> mult1(x5)
        app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
        app(rec1(x4),x5) -> rec2(x4,x5)
        app(rec(),x5) -> rec1(x5)
      Open
     
     DPs:
      mult{2,#}(s1(x),y) -> mult{2,#}(x,y)
     TRS:
      add2(0(),y) -> y
      add2(s1(x),y) -> s1(add2(x,y))
      mult2(0(),y) -> 0()
      mult2(s1(x),y) -> add2(mult2(x,y),y)
      rec3(f,x,0()) -> x
      rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
      fact() -> rec2(mult(),s1(0()))
      app(add1(x4),x5) -> add2(x4,x5)
      app(add(),x5) -> add1(x5)
      app(s(),x5) -> s1(x5)
      app(mult1(x4),x5) -> mult2(x4,x5)
      app(mult(),x5) -> mult1(x5)
      app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
      app(rec1(x4),x5) -> rec2(x4,x5)
      app(rec(),x5) -> rec1(x5)
     Subterm Criterion Processor:
      simple projection:
       pi(mult{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        add2(0(),y) -> y
        add2(s1(x),y) -> s1(add2(x,y))
        mult2(0(),y) -> 0()
        mult2(s1(x),y) -> add2(mult2(x,y),y)
        rec3(f,x,0()) -> x
        rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
        fact() -> rec2(mult(),s1(0()))
        app(add1(x4),x5) -> add2(x4,x5)
        app(add(),x5) -> add1(x5)
        app(s(),x5) -> s1(x5)
        app(mult1(x4),x5) -> mult2(x4,x5)
        app(mult(),x5) -> mult1(x5)
        app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
        app(rec1(x4),x5) -> rec2(x4,x5)
        app(rec(),x5) -> rec1(x5)
      Qed
     
     DPs:
      add{2,#}(s1(x),y) -> add{2,#}(x,y)
     TRS:
      add2(0(),y) -> y
      add2(s1(x),y) -> s1(add2(x,y))
      mult2(0(),y) -> 0()
      mult2(s1(x),y) -> add2(mult2(x,y),y)
      rec3(f,x,0()) -> x
      rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
      fact() -> rec2(mult(),s1(0()))
      app(add1(x4),x5) -> add2(x4,x5)
      app(add(),x5) -> add1(x5)
      app(s(),x5) -> s1(x5)
      app(mult1(x4),x5) -> mult2(x4,x5)
      app(mult(),x5) -> mult1(x5)
      app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
      app(rec1(x4),x5) -> rec2(x4,x5)
      app(rec(),x5) -> rec1(x5)
     Subterm Criterion Processor:
      simple projection:
       pi(add{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        add2(0(),y) -> y
        add2(s1(x),y) -> s1(add2(x,y))
        mult2(0(),y) -> 0()
        mult2(s1(x),y) -> add2(mult2(x,y),y)
        rec3(f,x,0()) -> x
        rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
        fact() -> rec2(mult(),s1(0()))
        app(add1(x4),x5) -> add2(x4,x5)
        app(add(),x5) -> add1(x5)
        app(s(),x5) -> s1(x5)
        app(mult1(x4),x5) -> mult2(x4,x5)
        app(mult(),x5) -> mult1(x5)
        app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
        app(rec1(x4),x5) -> rec2(x4,x5)
        app(rec(),x5) -> rec1(x5)
      Qed