YES
exiting with thread!
(VAR u v x y )
(RULES 
        if(tt,x,y) -> x
        if(ff,x,y) -> y
        if(x,y,y) -> y
        if(x,tt,ff) -> x
        eq(0,0) -> tt
        eq(0,s(x)) -> ff
        eq(s(x),0) -> ff
        eq(s(x),s(y)) -> eq(x,y)
        has(empty,x) -> ff
        has(+(u,x),y) -> if(eq(x,y),tt,has(u,y))
        subset(empty,v) -> tt
        subset(+(u,x),v) -> if(has(v,x),subset(u,v),ff)
        
)