YES

proof:
The input problem is infeasible because

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

	-(s(x), s(y)) = -(x, y)
	-(x, 0) = x
	-(0, x) = 0
	-(x, x) = s(x) ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	-(0, x) = 0
	-(s(x), s(y)) = -(x, y)
	-(x, 0) = x
	f1(-(x, x), x) = false__
	f1(s(x), x) = true__
	f2(false__) = false__
	f2(true__) = true__
G:
	true__ = false__

This holds because

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

	-(0, x) -> 0
	-(s(x), s(y)) -> -(x, y)
	-(x, 0) -> x
	f1(-(X0, X0), s(W1)) -> f1(-(X0, X0), W1)
	f1(-(x, x), x) -> false__
	f1(0, 0) -> false__
	f1(0, s(Y1)) -> f1(0, Y1)
	f1(s(x), x) -> true__
	f2(false__) -> false__
	f2(true__) -> true__
with the LPO induced by
	s > f1 > 0 > - > f2 > true__ > false__