YES
exiting with thread!
(VAR x )
(RULES 
        b(a(b(x))) -> b(x)
        a(a(x)) -> c(b(a(x)))
        c(b(a(c(x)))) -> c(a(c(x)))
        b(c(b(a(x)))) -> b(c(c(x)))
        a(b(c(b(x)))) -> c(c(b(x)))
        a(b(c(c(x)))) -> c(c(x))
        b(c(a(c(x)))) -> b(c(c(c(x))))
        b(c(c(b(x)))) -> b(c(b(x)))
        c(c(b(a(x)))) -> c(c(x))
        a(c(c(x))) -> c(c(c(x)))
        c(b(c(b(x)))) -> c(c(c(b(x))))
        c(b(c(c(x)))) -> c(c(c(x)))
        c(c(a(x))) -> c(c(c(x)))
        a(c(a(x))) -> c(c(c(x)))
        c(c(c(c(x)))) -> c(c(c(x)))
        a(c(b(x))) -> c(c(c(b(x))))
        
)