Certification Problem

Input (COPS 680)

We consider the TRS containing the following rules:

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

The underlying signature is as follows:

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

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(c,f(f(f(a))))
h(c,f(f(f(c))))
= t1

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

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