YES

linear polynomial interpretations on negative integers:

  tc_A(x1) = 0
  pin_A(x1) = x1 + -1
  b_A = -1
  pout_A(x1) = x1
  c_A = -2
  a_A = 0
  z_A = 0



the condition pin(x1) ->> pout(z()) is unsatisfiable for all substitutions.