YES

weighted path orer with linear polynomial on natural numbers:

  +_A(x1,x2) = x2 + 2
  s_A(x1) = 1
  0_A = 3
  a_A = 0


precedence:

  a > + > 0 > s


status:
+: [2]
s: []
0: []
a: []

the condition +(x,a()) ->> 0() is unsatisfiable for all substitutions.