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