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)
  TDG 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)
   graph:
    a__f#(X,X) -> a__h#(a__a()) -> a__h#(X) -> a__g#(mark(X),X)
    a__f#(X,X) -> a__h#(a__a()) -> a__h#(X) -> mark#(X)
    a__g#(a(),X) -> a__f#(b(),X) -> a__f#(X,X) -> a__h#(a__a())
    a__g#(a(),X) -> a__f#(b(),X) -> a__f#(X,X) -> a__a#()
    mark#(f(X1,X2)) -> a__f#(mark(X1),X2) ->
    a__f#(X,X) -> a__h#(a__a())
    mark#(f(X1,X2)) -> a__f#(mark(X1),X2) -> a__f#(X,X) -> a__a#()
    mark#(f(X1,X2)) -> mark#(X1) ->
    mark#(f(X1,X2)) -> a__f#(mark(X1),X2)
    mark#(f(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1)
    mark#(f(X1,X2)) -> mark#(X1) -> mark#(a()) -> a__a#()
    mark#(f(X1,X2)) -> mark#(X1) ->
    mark#(g(X1,X2)) -> a__g#(mark(X1),X2)
    mark#(f(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1)
    mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> a__h#(mark(X))
    mark#(f(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X)
    mark#(g(X1,X2)) -> a__g#(mark(X1),X2) ->
    a__g#(a(),X) -> a__f#(b(),X)
    mark#(g(X1,X2)) -> mark#(X1) ->
    mark#(f(X1,X2)) -> a__f#(mark(X1),X2)
    mark#(g(X1,X2)) -> mark#(X1) -> mark#(f(X1,X2)) -> mark#(X1)
    mark#(g(X1,X2)) -> mark#(X1) -> mark#(a()) -> a__a#()
    mark#(g(X1,X2)) -> mark#(X1) ->
    mark#(g(X1,X2)) -> a__g#(mark(X1),X2)
    mark#(g(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2)) -> mark#(X1)
    mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> a__h#(mark(X))
    mark#(g(X1,X2)) -> mark#(X1) -> mark#(h(X)) -> mark#(X)
    mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> a__f#(mark(X1),X2)
    mark#(h(X)) -> mark#(X) -> mark#(f(X1,X2)) -> mark#(X1)
    mark#(h(X)) -> mark#(X) -> mark#(a()) -> a__a#()
    mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> a__g#(mark(X1),X2)
    mark#(h(X)) -> mark#(X) -> mark#(g(X1,X2)) -> mark#(X1)
    mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> a__h#(mark(X))
    mark#(h(X)) -> mark#(X) -> mark#(h(X)) -> mark#(X)
    mark#(h(X)) -> a__h#(mark(X)) -> a__h#(X) -> a__g#(mark(X),X)
    mark#(h(X)) -> a__h#(mark(X)) -> a__h#(X) -> mark#(X)
    a__h#(X) -> a__g#(mark(X),X) -> a__g#(a(),X) -> a__f#(b(),X)
    a__h#(X) -> mark#(X) -> mark#(f(X1,X2)) -> a__f#(mark(X1),X2)
    a__h#(X) -> mark#(X) -> mark#(f(X1,X2)) -> mark#(X1)
    a__h#(X) -> mark#(X) -> mark#(a()) -> a__a#()
    a__h#(X) -> mark#(X) -> mark#(g(X1,X2)) -> a__g#(mark(X1),X2)
    a__h#(X) -> mark#(X) -> mark#(g(X1,X2)) -> mark#(X1)
    a__h#(X) -> mark#(X) -> mark#(h(X)) -> a__h#(mark(X))
    a__h#(X) -> mark#(X) -> mark#(h(X)) -> mark#(X)
   SCC Processor:
    #sccs: 1
    #rules: 10
    #arcs: 38/144
    DPs:
     a__f#(X,X) -> a__h#(a__a())
     a__h#(X) -> mark#(X)
     mark#(h(X)) -> mark#(X)
     mark#(h(X)) -> a__h#(mark(X))
     a__h#(X) -> a__g#(mark(X),X)
     a__g#(a(),X) -> a__f#(b(),X)
     mark#(g(X1,X2)) -> mark#(X1)
     mark#(g(X1,X2)) -> a__g#(mark(X1),X2)
     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