YES exiting with thread! (VAR x ) (RULES +(x,0) -> x s(x) -> x p(x) -> x )