YES
exiting with thread!
(VAR x y )
(RULES 
        plus(x,z) -> x
        plus(x,s(y)) -> s(plus(x,y))
        
)