YES

(VAR x0 x)
(RULES
  b(a(a(c(x0)))) -> b(a(a(a(x0))))
  c(a(b(a(a(x0))))) -> a(a(a(x0)))
  a(a(a(c(x0)))) -> a(a(a(x0)))
  a(a(a(a(x0)))) -> a(a(a(x0)))
  c(a(a(x0))) -> a(b(a(a(x0))))
  a(a(b(a(x)))) -> a(a(x))
  c(b(x0)) -> a(a(b(x0)))
  c(a(c(x))) -> a(a(c(x)))
  a(c(a(x))) -> a(a(a(x)))
  a(b(a(a(a(x))))) -> a(a(a(x)))
  c(c(x)) -> a(b(a(a(x))))
  b(a(b(x))) -> b(x)
)

(COMMENT
Termination is shown by EKBO with interpretations on natural numbers

  a_A(x1) = 1
  c_A(x1) = 1
  b_A(x1) = 1

weights

  w0 = 1
  w(a) = 1
  w(c) = 3
  w(b) = 0

and precedence:

b > a > c
)