YES

proof:
The input problem is infeasible because

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

	x = b ==> f(x) = a
	f(a) = a ==> a = a
	f(a) = a ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	f(b) = a
	t1(a) = a
	t1(f(a)) = a
	t2(a) = false__
	t2(f(a)) = 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 -> f(b)
	t1(f(b)) -> f(b)
	t1(f(f(b))) -> f(b)
	t2(f(b)) -> false__
	t2(f(f(b))) -> true__
	t3(false__) -> true__
	t3(true__) -> false__
with the LPO induced by
	t3 > t2 > a > f > b > t1 > true__ > false__