MAYBE

Problem:
 ap(f(),x) -> x
 ap(ap(ap(g(),x),y),ap(s(),z)) -> ap(ap(ap(g(),x),y),ap(ap(x,y),0()))

Proof:
 Uncurry Processor:
  f1(x) -> x
  g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
  ap(f(),x5) -> f1(x5)
  ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
  ap(g1(x4),x5) -> g2(x4,x5)
  ap(g(),x5) -> g1(x5)
  ap(s(),x5) -> s1(x5)
  DP Processor:
   DPs:
    g{3,#}(x,y,s1(z)) -> ap#(x,y)
    g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
    g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
    ap#(f(),x5) -> f{1,#}(x5)
    ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5)
   TRS:
    f1(x) -> x
    g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
    ap(f(),x5) -> f1(x5)
    ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
    ap(g1(x4),x5) -> g2(x4,x5)
    ap(g(),x5) -> g1(x5)
    ap(s(),x5) -> s1(x5)
   TDG Processor:
    DPs:
     g{3,#}(x,y,s1(z)) -> ap#(x,y)
     g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
     g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
     ap#(f(),x5) -> f{1,#}(x5)
     ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5)
    TRS:
     f1(x) -> x
     g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
     ap(f(),x5) -> f1(x5)
     ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
     ap(g1(x4),x5) -> g2(x4,x5)
     ap(g(),x5) -> g1(x5)
     ap(s(),x5) -> s1(x5)
    graph:
     ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5) ->
     g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
     ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5) ->
     g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
     ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5) ->
     g{3,#}(x,y,s1(z)) -> ap#(x,y)
     g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0()) ->
     ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5)
     g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0()) ->
     ap#(f(),x5) -> f{1,#}(x5)
     g{3,#}(x,y,s1(z)) -> ap#(x,y) ->
     ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5)
     g{3,#}(x,y,s1(z)) -> ap#(x,y) ->
     ap#(f(),x5) -> f{1,#}(x5)
     g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0())) ->
     g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
     g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0())) ->
     g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
     g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0())) -> g{3,#}(x,y,s1(z)) -> ap#(x,y)
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 10/25
     DPs:
      ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5)
      g{3,#}(x,y,s1(z)) -> ap#(x,y)
      g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
      g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
     TRS:
      f1(x) -> x
      g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
      ap(f(),x5) -> f1(x5)
      ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
      ap(g1(x4),x5) -> g2(x4,x5)
      ap(g(),x5) -> g1(x5)
      ap(s(),x5) -> s1(x5)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [ap#](x0, x1) = x0,
       
       [g{3,#}](x0, x1, x2) = 1x0 + x1,
       
       [s1](x0) = 0,
       
       [g1](x0) = x0 + 6,
       
       [g3](x0, x1, x2) = 2x0 + 1x1 + x2,
       
       [g2](x0, x1) = 1x0 + x1,
       
       [f1](x0) = x0 + 5,
       
       [0] = 0,
       
       [s] = 0,
       
       [g] = 5,
       
       [ap](x0, x1) = 1x0 + x1,
       
       [f] = 4
      orientation:
       ap#(g2(x4,x3),x5) = x3 + 1x4 >= x3 + 1x4 = g{3,#}(x4,x3,x5)
       
       g{3,#}(x,y,s1(z)) = 1x + y >= x = ap#(x,y)
       
       g{3,#}(x,y,s1(z)) = 1x + y >= 1x + y = ap#(ap(x,y),0())
       
       g{3,#}(x,y,s1(z)) = 1x + y >= 1x + y = g{3,#}(x,y,ap(ap(x,y),0()))
       
       f1(x) = x + 5 >= x = x
       
       g3(x,y,s1(z)) = 2x + 1y + 0 >= 2x + 1y + 0 = g3(x,y,ap(ap(x,y),0()))
       
       ap(f(),x5) = x5 + 5 >= x5 + 5 = f1(x5)
       
       ap(g2(x4,x3),x5) = 1x3 + 2x4 + x5 >= 1x3 + 2x4 + x5 = g3(x4,x3,x5)
       
       ap(g1(x4),x5) = 1x4 + x5 + 7 >= 1x4 + x5 = g2(x4,x5)
       
       ap(g(),x5) = x5 + 6 >= x5 + 6 = g1(x5)
       
       ap(s(),x5) = x5 + 1 >= 0 = s1(x5)
      problem:
       DPs:
        ap#(g2(x4,x3),x5) -> g{3,#}(x4,x3,x5)
        g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
        g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
       TRS:
        f1(x) -> x
        g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
        ap(f(),x5) -> f1(x5)
        ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
        ap(g1(x4),x5) -> g2(x4,x5)
        ap(g(),x5) -> g1(x5)
        ap(s(),x5) -> s1(x5)
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [ap#](x0, x1) = 1x1 + 1,
        
        [g{3,#}](x0, x1, x2) = x2 + 0,
        
        [s1](x0) = 1x0 + 2,
        
        [g1](x0) = x0,
        
        [g3](x0, x1, x2) = 1x2 + 2,
        
        [g2](x0, x1) = 2,
        
        [f1](x0) = x0,
        
        [0] = 1,
        
        [s] = 1,
        
        [g] = 4,
        
        [ap](x0, x1) = 1x1 + 2,
        
        [f] = 1
       orientation:
        ap#(g2(x4,x3),x5) = 1x5 + 1 >= x5 + 0 = g{3,#}(x4,x3,x5)
        
        g{3,#}(x,y,s1(z)) = 1z + 2 >= 2 = ap#(ap(x,y),0())
        
        g{3,#}(x,y,s1(z)) = 1z + 2 >= 2 = g{3,#}(x,y,ap(ap(x,y),0()))
        
        f1(x) = x >= x = x
        
        g3(x,y,s1(z)) = 2z + 3 >= 3 = g3(x,y,ap(ap(x,y),0()))
        
        ap(f(),x5) = 1x5 + 2 >= x5 = f1(x5)
        
        ap(g2(x4,x3),x5) = 1x5 + 2 >= 1x5 + 2 = g3(x4,x3,x5)
        
        ap(g1(x4),x5) = 1x5 + 2 >= 2 = g2(x4,x5)
        
        ap(g(),x5) = 1x5 + 2 >= x5 = g1(x5)
        
        ap(s(),x5) = 1x5 + 2 >= 1x5 + 2 = s1(x5)
       problem:
        DPs:
         g{3,#}(x,y,s1(z)) -> ap#(ap(x,y),0())
         g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
        TRS:
         f1(x) -> x
         g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
         ap(f(),x5) -> f1(x5)
         ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
         ap(g1(x4),x5) -> g2(x4,x5)
         ap(g(),x5) -> g1(x5)
         ap(s(),x5) -> s1(x5)
       SCC Processor:
        #sccs: 1
        #rules: 1
        #arcs: 8/4
        DPs:
         g{3,#}(x,y,s1(z)) -> g{3,#}(x,y,ap(ap(x,y),0()))
        TRS:
         f1(x) -> x
         g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
         ap(f(),x5) -> f1(x5)
         ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
         ap(g1(x4),x5) -> g2(x4,x5)
         ap(g(),x5) -> g1(x5)
         ap(s(),x5) -> s1(x5)
        Open