YES

proof:
The input problem is infeasible because

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

	add(s(x), y) = s(add(x, y))
	add(0, y) = y
	gcd(x, y) = gcd(y, x)
	gcd(0, x) = x
	gcd(x, 0) = x
	gcd(y, add(x, y)) = gcd(x, y)
	gcd(add(x, y), y) = gcd(x, y)
	leq(0, x1) = false ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	add(0, y) = y
	add(s(x), y) = s(add(x, y))
	f1(false) = true__
	f1(leq(0, x1)) = false__
	f2(false__) = false__
	f2(true__) = true__
	gcd(0, x) = x
	gcd(add(x, y), y) = gcd(x, y)
	gcd(x, 0) = x
	gcd(x, y) = gcd(y, x)
	gcd(y, add(x, y)) = gcd(x, y)
G:
	true__ = false__

This holds because

[3] the following ground-complete ordered TRS entails E but does not entail G:
	gcd(x, y) = gcd(y, x)
	add(0, y) -> y
	add(Y1, 0) -> Y1
	false -> true__
	gcd(0, x) -> x
	gcd(Y0, Y0) -> Y0
	gcd(add(x, y), y) -> gcd(x, y)
	gcd(x, 0) -> x
	gcd(y, add(x, y)) -> gcd(x, y)
	leq(0, x1) -> false__
with the LPO induced by
	leq > add > gcd > s > 0 > f2 > false > f1 > false__ > true__
with the following interpretations:
	f1 returns 1st variable
	f2 returns 1st variable
	s returns 1st variable