Certification Problem

Input (COPS 98)

We consider the TRS containing the following rules:

I(x) I(B(x)) (1)
F(E(x),x) G(x) (2)
E(x) x (3)

The underlying signature is as follows:

{I/1, B/1, F/2, E/1, G/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2022)

1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.

t0 = F(E(E(E(c_1))),E(E(c_1)))
F(E(E(c_1)),E(E(c_1)))
F(E(c_1),E(E(c_1)))
F(c_1,E(E(c_1)))
F(c_1,E(c_1))
F(c_1,c_1)
= t5

t0 = F(E(E(E(c_1))),E(E(c_1)))
G(E(E(c_1)))
G(E(c_1))
G(c_1)
= t3

The two resulting terms cannot be joined for the following reason: