Certification Problem

Input (COPS 981)

We consider the TRS containing the following rules:

a(a(x)) a(b(b(c(x)))) (1)
b(a(x)) x (2)
c(b(x)) a(c(x)) (3)

The underlying signature is as follows:

{a/1, b/1, c/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2020)

1 Non-Joinable Fork

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

t0 = b(c(b(b(a(a(c_1))))))
b(a(c(b(a(a(c_1))))))
c(b(a(a(c_1))))
c(a(c_1))
= t3

t0 = b(c(b(b(a(a(c_1))))))
b(c(b(a(c_1))))
b(c(c_1))
= t2

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