YES exiting with thread! (VAR x y ) (RULES h(x) -> a f(g(x),y) -> a k(a,a) -> a )