---- Non-confluence check R: F(x,x) -> A() F(x,G(x)) -> B() C() -> G(C()) Unjoinable conversion: A() <->* B()