Certification Problem

Input (COPS 956)

We consider the TRS containing the following rules:

r(e(x)) w(r(x)) (1)
i(t(x)) e(r(x)) (2)
e(w(x)) r(i(x)) (3)
t(e(x)) r(e(x)) (4)
w(r(x)) i(t(x)) (5)
e(r(x)) e(w(x)) (6)
r(i(t(e(r(x))))) e(w(r(i(t(e(x)))))) (7)

The underlying signature is as follows:

{r/1, e/1, w/1, i/1, t/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2023)

1 Non-Joinable Fork

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

t0 = e(r(e(x355)))
e(w(r(x355)))
r(i(r(x355)))
= t2

t0 = e(r(e(x355)))
e(w(e(x355)))
r(i(e(x355)))
= t2

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