MAYBE

Problem:
 a__f(X,X) -> a__f(a(),b())
 a__b() -> a()
 mark(f(X1,X2)) -> a__f(mark(X1),X2)
 mark(b()) -> a__b()
 mark(a()) -> a()
 a__f(X1,X2) -> f(X1,X2)
 a__b() -> b()

Proof:
 DP Processor:
  DPs:
   a__f#(X,X) -> a__f#(a(),b())
   mark#(f(X1,X2)) -> mark#(X1)
   mark#(f(X1,X2)) -> a__f#(mark(X1),X2)
   mark#(b()) -> a__b#()
  TRS:
   a__f(X,X) -> a__f(a(),b())
   a__b() -> a()
   mark(f(X1,X2)) -> a__f(mark(X1),X2)
   mark(b()) -> a__b()
   mark(a()) -> a()
   a__f(X1,X2) -> f(X1,X2)
   a__b() -> b()
  Open