YES

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:
 Bounds Processor:
  bound: 1
  enrichment: roof
  automaton:
   final states: {18,17,16,15,14,2,8,7,4,3,1}
   transitions:
    f60() -> 5*
    a__f0(18,5) -> 15*
    a__f0(3,17) -> 14*
    a__f0(15,5) -> 15*
    a__f0(16,2) -> 14*
    a__f0(17,5) -> 15*
    a__f0(3,2) -> 14*,6,4,1
    a__f0(14,5) -> 15*
    a__f0(16,5) -> 15*
    a__f0(6,5) -> 15*,6,4
    a__f0(16,17) -> 14*
    a0() -> 16*,6,7,3
    b0() -> 17*,6,7,2
    mark0(5) -> 6*
    a__b0() -> 18*,6,7
    f0(18,5) -> 15*
    f0(3,17) -> 14*
    f0(15,5) -> 15*
    f0(5,5) -> 8*
    f0(16,2) -> 14*
    f0(17,5) -> 15*
    f0(3,2) -> 14*,6,4,1
    f0(14,5) -> 15*
    f0(16,5) -> 15*
    f0(6,5) -> 15*,6,4
    f0(16,17) -> 14*
    b1() -> 18,2,7,6,17*
    f1(18,5) -> 15*
    f1(3,17) -> 14*
    f1(15,5) -> 15*
    f1(5,5) -> 8*
    f1(16,2) -> 14*
    f1(17,5) -> 15*
    f1(3,2) -> 14*,6,4,1
    f1(14,5) -> 15*
    f1(16,5) -> 15*
    f1(6,5) -> 15*,6,4
    f1(16,17) -> 14*
    a1() -> 18,3,7,6,16*
    4 -> 6*
    7 -> 6*
  problem:
   
  Qed