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)
   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