Certification Problem

Input (COPS 676)

We consider the TRS containing the following rules:

c → f(f(c)) (1)
h(h(h(b,b),f(f(a))),f(f(f(a)))) → a (2)
b → h(h(f(a),c),f(a)) (3)

The underlying signature is as follows:

{c/0, f/1, h/2, b/0, a/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2020)

1 Non-Joinable Fork

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

t0 = h(h(h(b,b),f(f(a))),f(f(f(a))))
→ h(h(h(h(h(f(a),c),f(a)),b),f(f(a))),f(f(f(a))))
= t1

t0 = h(h(h(b,b),f(f(a))),f(f(f(a))))
→ a
= t1

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