YES

weighted path orer with linear polynomial on natural numbers:

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


precedence:

  true > false > 0 > s > p > pos


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

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