YES

proof:
The input problem is infeasible because

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

	h(x, x) = g(a)
	g(g(a)) = f(b)
	f(a) = g(h(a, b))
	G(h(a, b)) = G(g(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(a) = g(h(a, b))
	g(g(a)) = f(b)
	h(x, x) = g(a)
	t1(G(g(a))) = false__
	t1(G(h(a, b))) = true__
	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:

	g(g(a)) -> f(b)
	g(h(a, b)) -> f(a)
	h(x, x) -> g(a)
	t1(G(g(a))) -> false__
	t1(G(h(a, b))) -> true__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	t2 > G > t1 > h > g > f > b > a > false__ > true__