Certification Problem

Input (COPS 686)

We consider the TRS containing the following rules:

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

The underlying signature is as follows:

{b/0, h/2, c/0, f/1, 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(f(a),a),a),f(f(f(h(h(f(b),b),b)))))
h(h(h(f(a),a),a),f(f(f(h(h(f(h(c,f(b))),b),b)))))
h(h(h(f(a),a),a),f(f(f(h(h(f(h(h(f(h(c,f(f(c)))),f(b)),f(b))),b),b)))))
h(h(h(f(a),a),a),f(f(f(h(h(f(h(h(f(h(h(f(h(c,f(f(c)))),f(b)),f(f(c)))),f(b)),f(b))),b),b)))))
= t3

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

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