---- Non-confluence check
R:
W(B(x)) -> I(x)
B(S(x)) -> S(x)
W(x) -> I(x)

Unjoinable conversion:
I(___y5()) <->* I(B(___y5()))