YES

weighted path orer with linear polynomial on natural numbers:

  pos_A(x1) = x1 + 2
  p_A(x1) = 1
  false_A = 2
  s_A(x1) = 5
  true_A = 4
  0_A = 1


precedence:

  true > false > 0 > s > p > pos


status:
pos: [1]
p: []
false: []
s: []
true: []
0: []

the condition pos(0()) ->> true() is unsatisfiable for all substitutions.