YES

weighted path orer with linear polynomial on natural numbers:

  g_A(x1,x2) = x2 + 1
  h_A(x1) = 0
  f_A(x1,x2) = x1 + 2
  a_A = 3
  b_A = 0
  F_A(x1,x2) = x2


precedence:

  g > f > b > F > a > h


status:
g: []
h: []
f: []
a: []
b: []
F: [2]

the condition F(x,g(x,b())) ->> F(y,a()) is unsatisfiable for all substitutions.