YES

proof:
The input problem is infeasible because

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

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

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