YES

proof:
The input problem is infeasible because

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

	c = c
	f(x, b) = b ==> g(x, a) = d
	f(x, a) = a ==> g(a, x) = c
	f(b, x) = b
	f(a, x) = a
	f(a, b) = b & f(a, 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(a, x) = a
	f(b, x) = b
	t1(b, x) = d
	t1(f(x, b), x) = g(x, a)
	t2(a, x) = c
	t2(f(x, a), x) = g(a, x)
	t3(b, a) = false__
	t3(f(a, b), f(a, a)) = true__
	t4(false__) = true__
	t4(true__) = false__
G:
	true__ = false__

This holds because

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

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