YES

linear polynomial interpretations on negative integers:

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



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