Certification Problem

Input (COPS 699)

We consider the TRS containing the following rules:

h(h(b,h(h(c,h(a,f(h(f(c),c)))),h(h(h(h(a,c),h(f(a),b)),b),f(f(a))))),f(h(a,c))) c (1)
c h(f(h(f(h(b,h(c,b))),f(a))),h(c,h(f(h(b,h(a,h(h(h(c,c),a),b)))),c))) (2)
c h(h(c,h(a,f(h(c,c)))),a) (3)
a c (4)
b h(c,h(a,c)) (5)

The underlying signature is as follows:

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

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2022)

1 Non-Joinable Fork

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

t0 = h(h(b,h(h(c,h(a,f(h(f(c),c)))),h(h(h(h(a,c),h(f(a),b)),b),f(f(a))))),f(h(a,c)))
h(h(b,h(h(h(f(h(f(h(b,h(c,b))),f(a))),h(c,h(f(h(b,h(a,h(h(h(c,c),a),b)))),c))),h(a,f(h(f(c),c)))),h(h(h(h(a,c),h(f(a),b)),b),f(f(a))))),f(h(a,c)))
h(h(h(c,h(a,c)),h(h(h(f(h(f(h(b,h(c,b))),f(a))),h(c,h(f(h(b,h(a,h(h(h(c,c),a),b)))),c))),h(a,f(h(f(c),c)))),h(h(h(h(a,c),h(f(a),b)),b),f(f(a))))),f(h(a,c)))
h(h(h(c,h(a,c)),h(h(h(f(h(f(h(h(c,h(a,c)),h(c,b))),f(a))),h(c,h(f(h(b,h(a,h(h(h(c,c),a),b)))),c))),h(a,f(h(f(c),c)))),h(h(h(h(a,c),h(f(a),b)),b),f(f(a))))),f(h(a,c)))
= t3

t0 = h(h(b,h(h(c,h(a,f(h(f(c),c)))),h(h(h(h(a,c),h(f(a),b)),b),f(f(a))))),f(h(a,c)))
c
h(h(c,h(a,f(h(c,c)))),a)
h(h(c,h(a,f(h(h(f(h(f(h(b,h(c,b))),f(a))),h(c,h(f(h(b,h(a,h(h(h(c,c),a),b)))),c))),c)))),a)
= t3

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