---- Non-confluence check
R:
H(H(x)) -> K(x)

Unjoinable conversion:
K(H(___y1())) <->* H(K(___y1()))