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