YES

proof:
The input problem is infeasible because

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

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

	t1(F(x, b), y) -> true__
	t1(F(y, a), y) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	t2 > b > F > t1 > a > g > h > false__ > true__
with the following interpretations:
	g returns 2nd variable
	h returns 1st variable