YES

proof:
The input problem is infeasible because

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

	h(x) = b ==> h(a(a(x))) = a(b)
	h(b) = b
	c(f(c(x), c(c(y)))) = c(a(a(b))) ==> f(c(c(c(x))), y) = a(y)
	c(f(x, y)) = c(a(b)) ==> f(c(x), c(c(y))) = a(a(x))
	c(f(c(c(x1)), y)) = c(a(b)) & c(f(c(x1), c(c(c(c(y)))))) = c(a(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:
	f1(b, x) = h(a(a(x)))
	f1(h(x), x) = a(b)
	f2(c(a(a(b))), x, y) = f(c(c(c(x))), y)
	f2(c(f(c(x), c(c(y)))), x, y) = a(y)
	f3(c(a(b)), x, y) = f(c(x), c(c(y)))
	f3(c(f(x, y)), x, y) = a(a(x))
	f4(c(a(b))) = true__
	f5(c(a(a(b))), x1, y) = f4(c(f(c(c(x1)), y)))
	f5(c(f(c(x1), c(c(c(c(y)))))), x1, y) = false__
	f6(false__) = false__
	f6(true__) = true__
	h(b) = b
G:
	true__ = false__

This holds because

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

	f1(a(b), a(a(b))) -> a(b)
	f1(b, x) -> h(a(a(x)))
	f1(h(x), x) -> a(b)
	f2(c(a(a(b))), x, y) -> f(c(c(c(x))), y)
	f2(c(f(c(x), c(c(y)))), x, y) -> a(y)
	f3(c(a(b)), x, y) -> f(c(x), c(c(y)))
	f3(c(f(x, y)), x, y) -> a(a(x))
	f4(c(a(b))) -> true__
	f4(c(f(c(c(x1)), y))) -> f5(c(a(a(b))), x1, y)
	f5(c(f(c(x1), c(c(c(c(y)))))), x1, y) -> false__
	f6(false__) -> false__
	f6(true__) -> true__
	h(a(a(b))) -> a(b)
	h(b) -> b
with the LPO induced by
	f2 > f4 > f5 > f3 > f1 > a > f6 > h > b > c > f > true__ > false__