YES

Problem:
 f(b(a(),z)) -> z
 b(y,b(a(),z)) -> b(f(c(y,y,a())),b(f(z),a()))
 f(f(f(c(z,x,a())))) -> b(f(x),z)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: roof
  automaton:
   final states: {5}
   transitions:
    b3(25,23) -> 5,7,12
    b3(22,21) -> 23*
    b1(7,5) -> 5*
    b1(10,8) -> 5*
    b1(7,6) -> 8*
    f3(24) -> 25*
    f3(11) -> 22*
    f1(5) -> 7*
    f1(9) -> 10*
    c3(15,15,21) -> 24*
    c1(5,5,6) -> 9*
    a3() -> 21*
    a1() -> 6*
    b2(15,13) -> 5*
    b2(12,11) -> 13*
    f0(5) -> 5*
    f2(5) -> 12*
    f2(14) -> 15*
    f2(6) -> 12*
    b0(5,5) -> 5*
    c2(10,10,11) -> 14*
    c2(7,7,11) -> 14*
    a0() -> 5*
    a2() -> 11*
    c0(5,5,5) -> 5*
    5 -> 12,7
  problem:
   
  Qed