MAYBE

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

Proof:
 DP Processor:
  DPs:
   f#(a()) -> h#(a())
   h#(g(x)) -> f#(x)
   h#(g(x)) -> h#(f(x))
  TRS:
   f(a()) -> g(h(a()))
   h(g(x)) -> g(h(f(x)))
   k(x,h(x),a()) -> h(x)
   k(f(x),y,x) -> f(x)
  Usable Rule Processor:
   DPs:
    f#(a()) -> h#(a())
    h#(g(x)) -> f#(x)
    h#(g(x)) -> h#(f(x))
   TRS:
    f(a()) -> g(h(a()))
   TDG Processor:
    DPs:
     f#(a()) -> h#(a())
     h#(g(x)) -> f#(x)
     h#(g(x)) -> h#(f(x))
    TRS:
     f(a()) -> g(h(a()))
    graph:
     h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x))
     h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x)
     h#(g(x)) -> f#(x) -> f#(a()) -> h#(a())
     f#(a()) -> h#(a()) -> h#(g(x)) -> h#(f(x))
     f#(a()) -> h#(a()) -> h#(g(x)) -> f#(x)
    EDG Processor:
     DPs:
      f#(a()) -> h#(a())
      h#(g(x)) -> f#(x)
      h#(g(x)) -> h#(f(x))
     TRS:
      f(a()) -> g(h(a()))
     graph:
      h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x)
      h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x))
      h#(g(x)) -> f#(x) -> f#(a()) -> h#(a())
     CDG Processor:
      DPs:
       f#(a()) -> h#(a())
       h#(g(x)) -> f#(x)
       h#(g(x)) -> h#(f(x))
      TRS:
       f(a()) -> g(h(a()))
      graph:
       h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x))
       h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x)
      Restore Modifier:
       DPs:
        f#(a()) -> h#(a())
        h#(g(x)) -> f#(x)
        h#(g(x)) -> h#(f(x))
       TRS:
        f(a()) -> g(h(a()))
        h(g(x)) -> g(h(f(x)))
        k(x,h(x),a()) -> h(x)
        k(f(x),y,x) -> f(x)
       SCC Processor:
        #sccs: 1
        #rules: 1
        #arcs: 2/9
        DPs:
         h#(g(x)) -> h#(f(x))
        TRS:
         f(a()) -> g(h(a()))
         h(g(x)) -> g(h(f(x)))
         k(x,h(x),a()) -> h(x)
         k(f(x),y,x) -> f(x)
        Open