YES

weighted path orer with linear polynomial on natural numbers:

  odd_A(x1) = 3
  s_A(x1) = 1
  false_A = 0
  true_A = 2
  even_A(x1) = 3
  zero_A(x1) = x1 + 1
  0_A = 3


precedence:

  false > 0 > true > zero > even > s > odd


status:
odd: []
s: []
false: []
true: []
even: []
zero: []
0: []

the condition zero(s(x)) ->> true() is unsatisfiable for all substitutions.