YES

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {9,1}
   transitions:
    f90() -> 2*
    f0(3,7) -> 15*
    f0(4,2) -> 4*
    f0(14,4) -> 8*
    f0(15,5) -> 21*
    f0(5,3) -> 11*
    f0(15,11) -> 20*
    f0(21,4) -> 1*
    f0(11,2) -> 6*
    f0(6,2) -> 6*
    f0(1,2) -> 1,10
    f0(7,5) -> 14*
    f0(7,11) -> 18*
    f0(18,2) -> 8*
    f0(8,2) -> 8*
    f0(3,2) -> 4*
    f0(3,8) -> 1*
    f0(3,14) -> 21*
    f0(3,18) -> 20*
    f0(14,3) -> 18*
    f0(20,2) -> 1*
    f0(10,2) -> 9*
    f0(15,6) -> 1*
    f0(5,4) -> 6*
    f0(21,3) -> 20*
    f0(2,2) -> 10*
    f0(7,6) -> 8*
    b0() -> 3*
    a0() -> 7*
    c0() -> 5*
    f1(28,3) -> 26,20
    f1(23,5) -> 28,21
    f1(23,11) -> 26,20
    f1(3,7) -> 23*
    f1(49,2) -> 1*
    f1(34,2) -> 34,6
    f1(29,2) -> 29,8
    f1(14,4) -> 29*
    f1(3,29) -> 26*
    f1(3,31) -> 28*
    f1(5,3) -> 34*
    f1(15,5) -> 28*
    f1(15,11) -> 26*
    f1(36,2) -> 8*
    f1(26,2) -> 26,1
    f1(31,4) -> 29,8
    f1(21,4) -> 1,26
    f1(1,2) -> 1*
    f1(7,5) -> 31*
    f1(7,11) -> 29*
    f1(28,4) -> 26,1
    f1(23,6) -> 26,1
    f1(3,8) -> 26*
    f1(3,14) -> 28*
    f1(3,18) -> 26*
    f1(14,3) -> 29*
    f1(20,2) -> 1*
    f1(5,4) -> 34*
    f1(15,6) -> 26*
    f1(31,3) -> 29,18
    f1(21,3) -> 20,26
    f1(15,34) -> 26*
    f1(7,6) -> 29*
    f2(43,5) -> 28,42
    f2(28,3) -> 38*
    f2(23,5) -> 50*
    f2(43,11) -> 26,39
    f2(3,7) -> 43*
    f2(49,2) -> 26*
    f2(7,34) -> 36*
    f2(39,2) -> 39,26
    f2(3,29) -> 39*
    f2(3,31) -> 42*
    f2(50,3) -> 38*
    f2(15,5) -> 46*
    f2(46,4) -> 26,39
    f2(36,2) -> 36,29
    f2(52,3) -> 36*
    f2(42,3) -> 39,26
    f2(7,5) -> 52*
    f2(38,2) -> 39,38,26,1
    f2(43,6) -> 26,39
    f2(28,4) -> 38*
    f2(3,14) -> 42*
    f2(43,34) -> 38*
    f2(23,34) -> 38*
    f2(50,4) -> 38*
    f2(46,3) -> 26,39
    f2(15,34) -> 39*
    f2(52,4) -> 36*
    f2(42,4) -> 39,26
    f3(53,5) -> 55*
    f3(3,7) -> 53*
    f3(49,2) -> 49,39
    f3(55,3) -> 49*
    f3(53,34) -> 49*
    f3(55,4) -> 49*
    f3(3,36) -> 49*
    f3(3,52) -> 55*
    1 -> 10,9
    9 -> 10*
  problem:
   
  Qed