YES

proof:
The input problem is infeasible because

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

	div(s(x), s(y)) = pair(s(q), r)
	div(s(x), s(y)) = pair(0, s(x))
	div(0, s(x)) = pair(0, 0)
	m(s(x), s(y)) = m(x, y)
	m(x, 0) = x
	m(0, s(y)) = 0
	lt(s(x), s(y)) = lt(x, y)
	lt(0, s(x)) = true
	lt(x, 0) = false
	lt(x1, x2) = true & lt(x1, x2) = false & div(m(x1, x2), s(x2)) = pair(x3, x4) ==> 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(0, s(x)) = pair(0, 0)
	div(s(x), s(y)) = pair(0, s(x))
	div(s(x), s(y)) = pair(s(q), r)
	lt(0, s(x)) = true
	lt(s(x), s(y)) = lt(x, y)
	lt(x, 0) = false
	m(0, s(y)) = 0
	m(s(x), s(y)) = m(x, y)
	m(x, 0) = x
	t1(lt(x1, x2), lt(x1, x2), div(m(x1, x2), s(x2)), x3, x4) = true__
	t1(true, false, pair(x3, x4), x3, x4) = 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:
	pair(0, s(X0)) = pair(0, s(X1))
	pair(0, s(X0)) = pair(s(X1), X2)
	pair(s(X0), X1) = pair(s(X2), X3)
	div(0, s(X0)) -> pair(0, 0)
	div(s(X0), s(X1)) -> pair(0, s(X0))
	lt(0, s(X0)) -> true
	lt(X0, 0) -> false
	lt(s(X0), s(X1)) -> lt(X0, X1)
	m(0, s(X0)) -> 0
	m(X0, 0) -> X0
	m(s(X0), s(X1)) -> m(X0, X1)
	t1(X0, X0, Z1, X2, X3) -> true__
	t1(X0, X0, div(Z1, s(X2)), X3, X4) -> true__
	t1(X0, X0, div(Z1, s(s(X2))), X3, X4) -> true__
	t1(X0, X0, pair(0, 0), X1, X2) -> true__
	t1(true, false, Z1, 0, s(X2)) -> false__
	t1(true, false, Z1, X0, X1) -> false__
	t1(true, false, Z1, s(X1), X2) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	t1 > div > pair > 0 > true > s > false > lt > m > t2 > false__ > true__