YES

proof:
The input problem is infeasible because

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

	e(x) = true ==> e(s(x)) = false
	e(x) = false ==> e(s(x)) = true
	e(0) = true
	e(x1) = false & e(x1) = true ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

[2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)):

E:
	e(0) = true
	g1(e(x), x) = e(s(x))
	g1(false, x) = true
	g1(true, x) = false
	t1(e(x1), e(x1)) = true__
	t1(false, true) = 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:

	e(0) -> true
	e(s(X0)) -> g1(e(X0), X0)
	g1(false, X0) -> true
	g1(g2, X0) -> true
	g1(true, X0) -> false
	g2 -> false
	t1(Z1, Z1) -> true__
	t1(false, true) -> false__
	t1(g1(Z1, X0), g1(Z1, X0)) -> true__
	t1(g1(g1(Z1, X0), s(X0)), g1(g1(Z1, X0), s(X0))) -> true__
	t1(g2, e(0)) -> false__
	t1(g2, g2) -> true__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	g2 > e > g1 > t2 > false > true > 0 > s > t1 > true__ > false__