YES

linear polynomial interpretations on negative integers:

  power_A(x1,x2) = 0
  mult_A(x1,x2) = x1
  s_A(x1) = 0
  0_A = -1
  div_A(x1,x2) = x1
  mod_A(x1,x2) = x1
  minus_A(x1,x2) = x1
  lte_A(x1,x2) = x1
  false_A = 0
  true_A = -1
  add_A(x1,x2) = 0



the condition mod(0(),s(s(0()))) ->> s(x1) is unsatisfiable for all substitutions.