YES

proof:
The input problem is infeasible because

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

	leq(0, x) = true
	leq(s(x), s(y)) = leq(x, y)
	greater(s(x), 0) = true
	greater(s(x), s(y)) = greater(x, y)
	m(s(x), s(y)) = m(x, y)
	m(0, y) = 0
	m(x, 0) = x
	div(x, y) = pair(s(q), r)
	div(x, y) = pair(0, y)
	leq(x, w) = true & div(m(w, x), x) = pair(y, z) & greater(x, w) = 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:
	div(x, y) = pair(0, y)
	div(x, y) = pair(s(q), r)
	greater(s(x), 0) = true
	greater(s(x), s(y)) = greater(x, y)
	leq(0, x) = true
	leq(s(x), s(y)) = leq(x, y)
	m(0, y) = 0
	m(s(x), s(y)) = m(x, y)
	m(x, 0) = x
	t1(leq(x, w), div(m(w, x), x), greater(x, w), y, z) = true__
	t1(true, pair(y, z), true, y, z) = 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:
	g2 = g1
	div(x, y) -> g2
	greater(s(x), 0) -> true
	greater(s(x), s(y)) -> greater(x, y)
	leq(0, x) -> true
	leq(s(x), s(y)) -> leq(x, y)
	m(0, y) -> 0
	m(s(x), s(y)) -> m(x, y)
	m(x, 0) -> x
	pair(0, X0) -> g2
	pair(s(X1), X2) -> g1
	t1(leq(Y0, 0), pair(0, Y0), greater(Y0, 0), Y2, Y3) -> true__
	t1(leq(Y0, Y1), g1, greater(Y0, Y1), Y2, Y3) -> true__
	t1(leq(s(Y0), 0), g1, true, Y1, Y2) -> true__
	t1(leq(s(Y0), 0), pair(0, true__), true, Y1, Y2) -> true__
	t1(leq(x, w), div(m(w, x), x), greater(x, w), y, z) -> true__
	t1(true, g1, greater(0, Y0), Y1, Y2) -> true__
	t1(true, g1, true, 0, Y1) -> false__
	t1(true, g1, true, s(X0), Y1) -> false__
	t1(true, pair(0, 0), greater(0, Y1), Y2, Y3) -> true__
	t1(true, pair(0, true__), greater(0, Y0), Y1, Y2) -> true__
	t1(true, pair(0, true__), true, 0, Y1) -> false__
	t1(true, pair(0, true__), true, s(X0), Y1) -> false__
	t1(true, pair(y, z), true, y, z) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	t1 > div > 0 > g2 > true > s > g1 > greater > pair > m > leq > t2 > false__ > true__