MAYBE

Problem:
 a__h(X) -> a__g(mark(X),X)
 a__g(a(),X) -> a__f(b(),X)
 a__f(X,X) -> a__h(a__a())
 a__a() -> b()
 mark(h(X)) -> a__h(mark(X))
 mark(g(X1,X2)) -> a__g(mark(X1),X2)
 mark(a()) -> a__a()
 mark(f(X1,X2)) -> a__f(mark(X1),X2)
 mark(b()) -> b()
 a__h(X) -> h(X)
 a__g(X1,X2) -> g(X1,X2)
 a__a() -> a()
 a__f(X1,X2) -> f(X1,X2)

Proof:
 DP Processor:
  DPs:
   a__h#(X) -> mark#(X)
   a__h#(X) -> a__g#(mark(X),X)
   a__g#(a(),X) -> a__f#(b(),X)
   a__f#(X,X) -> a__a#()
   a__f#(X,X) -> a__h#(a__a())
   mark#(h(X)) -> mark#(X)
   mark#(h(X)) -> a__h#(mark(X))
   mark#(g(X1,X2)) -> mark#(X1)
   mark#(g(X1,X2)) -> a__g#(mark(X1),X2)
   mark#(a()) -> a__a#()
   mark#(f(X1,X2)) -> mark#(X1)
   mark#(f(X1,X2)) -> a__f#(mark(X1),X2)
  TRS:
   a__h(X) -> a__g(mark(X),X)
   a__g(a(),X) -> a__f(b(),X)
   a__f(X,X) -> a__h(a__a())
   a__a() -> b()
   mark(h(X)) -> a__h(mark(X))
   mark(g(X1,X2)) -> a__g(mark(X1),X2)
   mark(a()) -> a__a()
   mark(f(X1,X2)) -> a__f(mark(X1),X2)
   mark(b()) -> b()
   a__h(X) -> h(X)
   a__g(X1,X2) -> g(X1,X2)
   a__a() -> a()
   a__f(X1,X2) -> f(X1,X2)
  Open