MAYBE

Problem:
 h(X) -> g(X)
 g(a()) -> f(b())
 f(X) -> h(a())
 a() -> b()

Proof:
 DP Processor:
  DPs:
   h#(X) -> g#(X)
   g#(a()) -> f#(b())
   f#(X) -> a#()
   f#(X) -> h#(a())
  TRS:
   h(X) -> g(X)
   g(a()) -> f(b())
   f(X) -> h(a())
   a() -> b()
  CDG Processor:
   DPs:
    h#(X) -> g#(X)
    g#(a()) -> f#(b())
    f#(X) -> a#()
    f#(X) -> h#(a())
   TRS:
    h(X) -> g(X)
    g(a()) -> f(b())
    f(X) -> h(a())
    a() -> b()
   graph:
    f#(X) -> h#(a()) -> h#(X) -> g#(X)
    g#(a()) -> f#(b()) -> f#(X) -> a#()
    g#(a()) -> f#(b()) -> f#(X) -> h#(a())
    h#(X) -> g#(X) -> g#(a()) -> f#(b())
   SCC Processor:
    #sccs: 1
    #rules: 3
    #arcs: 4/16
    DPs:
     f#(X) -> h#(a())
     h#(X) -> g#(X)
     g#(a()) -> f#(b())
    TRS:
     h(X) -> g(X)
     g(a()) -> f(b())
     f(X) -> h(a())
     a() -> b()
    Open