YES weighted path orer with linear polynomial on natural numbers: c_A = 0 g_A(x1) = x1 + 1 a_A = 0 h_A(x1) = 1 b_A = 2 precedence: h > b > a > g > c status: c: [] g: [1] a: [] h: [] b: [] the condition h(x) ->> b() is unsatisfiable for all substitutions.