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}

Prove or disprove confluence.

No.

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

t₀	=	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)))
	=	t₃

t₀	=	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)
	=	t₃

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

When applying the cap-function on both terms (where variables may be treated like constants) then the resulting terms do not unify.