YES

proof:
The input problem is infeasible because

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

	a = b
	y' = y & y'' = y ==> f(g(y'), y'') = h(y, f(g(y), a))
	x' = x & x'' = x ==> f(x', x'') = h(x, f(x, b))
	g(x1) = x & x2 = x & x1 = x3 & x2 = x3 ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	a = b
	f(g(y), y) = h(y, f(g(y), a))
	f(x, x) = h(x, f(x, b))
	t1(g(x3), x3) = true__
	t1(x3, x3) = false__
	t2(false__) = true__
	t2(true__) = false__
G:
	true__ = false__

This holds because

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

	b -> a
	h(Y0, f(Y0, a)) -> f(Y0, Y0)
	h(y, f(g(y), a)) -> f(g(y), y)
	t1(g(x3), x3) -> true__
	t1(x3, x3) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	h > f > g > t1 > t2 > b > a > false__ > true__