MAYBE

Problem:
 f(a(),g(y)) -> g(g(y))
 f(g(x),a()) -> f(x,g(a()))
 f(g(x),g(y)) -> h(g(y),x,g(y))
 h(g(x),y,z) -> f(y,h(x,y,z))
 h(a(),y,z) -> z

Proof:
 DP Processor:
  DPs:
   f#(g(x),a()) -> f#(x,g(a()))
   f#(g(x),g(y)) -> h#(g(y),x,g(y))
   h#(g(x),y,z) -> h#(x,y,z)
   h#(g(x),y,z) -> f#(y,h(x,y,z))
  TRS:
   f(a(),g(y)) -> g(g(y))
   f(g(x),a()) -> f(x,g(a()))
   f(g(x),g(y)) -> h(g(y),x,g(y))
   h(g(x),y,z) -> f(y,h(x,y,z))
   h(a(),y,z) -> z
  CDG Processor:
   DPs:
    f#(g(x),a()) -> f#(x,g(a()))
    f#(g(x),g(y)) -> h#(g(y),x,g(y))
    h#(g(x),y,z) -> h#(x,y,z)
    h#(g(x),y,z) -> f#(y,h(x,y,z))
   TRS:
    f(a(),g(y)) -> g(g(y))
    f(g(x),a()) -> f(x,g(a()))
    f(g(x),g(y)) -> h(g(y),x,g(y))
    h(g(x),y,z) -> f(y,h(x,y,z))
    h(a(),y,z) -> z
   graph:
    h#(g(x),y,z) -> h#(x,y,z) -> h#(g(x),y,z) -> h#(x,y,z)
    h#(g(x),y,z) -> h#(x,y,z) -> h#(g(x),y,z) -> f#(y,h(x,y,z))
    h#(g(x),y,z) -> f#(y,h(x,y,z)) -> f#(g(x),a()) -> f#(x,g(a()))
    h#(g(x),y,z) -> f#(y,h(x,y,z)) ->
    f#(g(x),g(y)) -> h#(g(y),x,g(y))
    f#(g(x),g(y)) -> h#(g(y),x,g(y)) -> h#(g(x),y,z) -> h#(x,y,z)
    f#(g(x),g(y)) -> h#(g(y),x,g(y)) -> h#(g(x),y,z) -> f#(y,h(x,y,z))
    f#(g(x),a()) -> f#(x,g(a())) -> f#(g(x),g(y)) -> h#(g(y),x,g(y))
   Restore Modifier:
    DPs:
     f#(g(x),a()) -> f#(x,g(a()))
     f#(g(x),g(y)) -> h#(g(y),x,g(y))
     h#(g(x),y,z) -> h#(x,y,z)
     h#(g(x),y,z) -> f#(y,h(x,y,z))
    TRS:
     f(a(),g(y)) -> g(g(y))
     f(g(x),a()) -> f(x,g(a()))
     f(g(x),g(y)) -> h(g(y),x,g(y))
     h(g(x),y,z) -> f(y,h(x,y,z))
     h(a(),y,z) -> z
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 7/16
     DPs:
      h#(g(x),y,z) -> h#(x,y,z)
      h#(g(x),y,z) -> f#(y,h(x,y,z))
      f#(g(x),g(y)) -> h#(g(y),x,g(y))
      f#(g(x),a()) -> f#(x,g(a()))
     TRS:
      f(a(),g(y)) -> g(g(y))
      f(g(x),a()) -> f(x,g(a()))
      f(g(x),g(y)) -> h(g(y),x,g(y))
      h(g(x),y,z) -> f(y,h(x,y,z))
      h(a(),y,z) -> z
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [h#](x0, x1, x2) = x2,
       
       [f#](x0, x1) = x1,
       
       [h](x0, x1, x2) = x2,
       
       [f](x0, x1) = x1,
       
       [g](x0) = 0,
       
       [a] = 1
      orientation:
       h#(g(x),y,z) = z >= z = h#(x,y,z)
       
       h#(g(x),y,z) = z >= z = f#(y,h(x,y,z))
       
       f#(g(x),g(y)) = 0 >= 0 = h#(g(y),x,g(y))
       
       f#(g(x),a()) = 1 >= 0 = f#(x,g(a()))
       
       f(a(),g(y)) = 0 >= 0 = g(g(y))
       
       f(g(x),a()) = 1 >= 0 = f(x,g(a()))
       
       f(g(x),g(y)) = 0 >= 0 = h(g(y),x,g(y))
       
       h(g(x),y,z) = z >= z = f(y,h(x,y,z))
       
       h(a(),y,z) = z >= z = z
      problem:
       DPs:
        h#(g(x),y,z) -> h#(x,y,z)
        h#(g(x),y,z) -> f#(y,h(x,y,z))
        f#(g(x),g(y)) -> h#(g(y),x,g(y))
       TRS:
        f(a(),g(y)) -> g(g(y))
        f(g(x),a()) -> f(x,g(a()))
        f(g(x),g(y)) -> h(g(y),x,g(y))
        h(g(x),y,z) -> f(y,h(x,y,z))
        h(a(),y,z) -> z
      Open