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
	b = x & c = 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:
	f1(d) = c
	f1(e) = d
	f2(d) = b
	f2(e) = d
	f3(b) = a
	f3(c) = a
	f4(b) = true__
	f4(c) = false__
	f5(false__) = false__
	f5(true__) = true__
G:
	true__ = false__

This holds because

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

	a -> f3(f1(f1(e)))
	b -> f2(f1(e))
	c -> f1(f1(e))
	d -> f1(e)
	f2(e) -> f1(e)
	f3(f2(f1(e))) -> f3(f1(f1(e)))
	f4(f1(f1(e))) -> false__
	f4(f2(f1(e))) -> true__
	f5(false__) -> false__
	f5(true__) -> true__
with the LPO induced by
	f5 > f4 > c > a > b > f2 > d > f1 > e > f3 > false__ > true__