MAYBE

Problem:
 f(a(x),y,s(z),u) -> f(a(b()),y,z,g(x,y,s(z),u))
 g(x,y,z,u) -> h(x,y,z,u)
 h(b(),y,z,u) -> f(y,y,z,u)
 a(b()) -> c()

Proof:
 DP Processor:
  DPs:
   f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
   f#(a(x),y,s(z),u) -> a#(b())
   f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u))
   g#(x,y,z,u) -> h#(x,y,z,u)
   h#(b(),y,z,u) -> f#(y,y,z,u)
  TRS:
   f(a(x),y,s(z),u) -> f(a(b()),y,z,g(x,y,s(z),u))
   g(x,y,z,u) -> h(x,y,z,u)
   h(b(),y,z,u) -> f(y,y,z,u)
   a(b()) -> c()
  TDG Processor:
   DPs:
    f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
    f#(a(x),y,s(z),u) -> a#(b())
    f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u))
    g#(x,y,z,u) -> h#(x,y,z,u)
    h#(b(),y,z,u) -> f#(y,y,z,u)
   TRS:
    f(a(x),y,s(z),u) -> f(a(b()),y,z,g(x,y,s(z),u))
    g(x,y,z,u) -> h(x,y,z,u)
    h(b(),y,z,u) -> f(y,y,z,u)
    a(b()) -> c()
   graph:
    h#(b(),y,z,u) -> f#(y,y,z,u) ->
    f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u))
    h#(b(),y,z,u) -> f#(y,y,z,u) -> f#(a(x),y,s(z),u) -> a#(b())
    h#(b(),y,z,u) -> f#(y,y,z,u) -> f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
    g#(x,y,z,u) -> h#(x,y,z,u) -> h#(b(),y,z,u) -> f#(y,y,z,u)
    f#(a(x),y,s(z),u) -> g#(x,y,s(z),u) ->
    g#(x,y,z,u) -> h#(x,y,z,u)
    f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u)) ->
    f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u))
    f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u)) ->
    f#(a(x),y,s(z),u) -> a#(b())
    f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u)) -> f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
   Restore Modifier:
    DPs:
     f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
     f#(a(x),y,s(z),u) -> a#(b())
     f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u))
     g#(x,y,z,u) -> h#(x,y,z,u)
     h#(b(),y,z,u) -> f#(y,y,z,u)
    TRS:
     f(a(x),y,s(z),u) -> f(a(b()),y,z,g(x,y,s(z),u))
     g(x,y,z,u) -> h(x,y,z,u)
     h(b(),y,z,u) -> f(y,y,z,u)
     a(b()) -> c()
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 8/25
     DPs:
      h#(b(),y,z,u) -> f#(y,y,z,u)
      f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
      g#(x,y,z,u) -> h#(x,y,z,u)
      f#(a(x),y,s(z),u) -> f#(a(b()),y,z,g(x,y,s(z),u))
     TRS:
      f(a(x),y,s(z),u) -> f(a(b()),y,z,g(x,y,s(z),u))
      g(x,y,z,u) -> h(x,y,z,u)
      h(b(),y,z,u) -> f(y,y,z,u)
      a(b()) -> c()
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [h#](x0, x1, x2, x3) = x2,
       
       [g#](x0, x1, x2, x3) = x2,
       
       [f#](x0, x1, x2, x3) = x2,
       
       [c] = 0,
       
       [h](x0, x1, x2, x3) = x0 + x3,
       
       [g](x0, x1, x2, x3) = x0 + x3,
       
       [b] = 1,
       
       [f](x0, x1, x2, x3) = 1,
       
       [s](x0) = x0 + 1,
       
       [a](x0) = 0
      orientation:
       h#(b(),y,z,u) = z >= z = f#(y,y,z,u)
       
       f#(a(x),y,s(z),u) = z + 1 >= z + 1 = g#(x,y,s(z),u)
       
       g#(x,y,z,u) = z >= z = h#(x,y,z,u)
       
       f#(a(x),y,s(z),u) = z + 1 >= z = f#(a(b()),y,z,g(x,y,s(z),u))
       
       f(a(x),y,s(z),u) = 1 >= 1 = f(a(b()),y,z,g(x,y,s(z),u))
       
       g(x,y,z,u) = u + x >= u + x = h(x,y,z,u)
       
       h(b(),y,z,u) = u + 1 >= 1 = f(y,y,z,u)
       
       a(b()) = 0 >= 0 = c()
      problem:
       DPs:
        h#(b(),y,z,u) -> f#(y,y,z,u)
        f#(a(x),y,s(z),u) -> g#(x,y,s(z),u)
        g#(x,y,z,u) -> h#(x,y,z,u)
       TRS:
        f(a(x),y,s(z),u) -> f(a(b()),y,z,g(x,y,s(z),u))
        g(x,y,z,u) -> h(x,y,z,u)
        h(b(),y,z,u) -> f(y,y,z,u)
        a(b()) -> c()
      Open