YES weighted path orer with linear polynomial on natural numbers: h_A(x1) = x1 + 1 g_A(x1) = x1 f_A(x1) = x1 + 1 precedence: f > g > h status: h: [1] g: [1] f: [1] the condition f(g(h(x))) ->> g(f(g(h(x)))) is unsatisfiable for all substitutions.