YES

proof:
The input problem is infeasible because

[1] the following set of Horn clauses is satisfiable:

	d = x & e = x ==> c = d
	d = x & e = x ==> b = d
	b = x & c = x ==> a = a
	d = x & e = x ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

[2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)):

E:
	g1(d) = b
	g1(d) = c
	g1(e) = d
	t1(b) = a
	t1(c) = a
	t2(d) = false__
	t2(e) = true__
	t3(false__) = true__
	t3(true__) = false__
G:
	true__ = false__

This holds because

[3] the following ground-complete ordered TRS entails E but does not entail G:

	a -> t1(g1(g1(e)))
	a -> t1(g1(g1(e)))
	b -> g1(g1(e))
	c -> g1(g1(e))
	d -> g1(e)
	t2(e) -> true__
	t2(g1(e)) -> false__
	t3(false__) -> true__
	t3(true__) -> false__
with the LPO induced by
	t3 > a > b > c > d > e > g1 > t2 > t1 > false__ > true__