YES
exiting with thread!
(VAR x y z )
(RULES 
        +(+(x,y),z) -> +(x,+(y,z))
        +(x,-(x)) -> 0
        f(0,y,z) -> y
        -(0) -> 0
        +(x,0) -> x
        +(0,x) -> x
        -(-(x)) -> x
        +(x,+(-(x),z)) -> z
        +(-(x),x) -> 0
        +(-(x),+(x,z)) -> z
        -(+(y,x)) -> +(-(x),-(y))
        g(y,x) -> f(y,+(y,-(x)),x)
        
)