YES
(VAR x y u)
(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(+(x,y),u) -> if(eq(y,u),tt(),has(x,u))
subset(empty(),x) -> tt()
subset(+(x,y),u) -> if(has(u,y),subset(x,u),ff())
)