YES Input TRS: 1: f(g(h(x))) -> g(f(h(g(x)))) 2: f(x) -> x 3: g(x) -> x 4: h(x) -> x Infeasibility test: f(g(h(x))) --> g(f(g(h(x)))) Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ... succeeded. h(x1) status: [x1] precedence above: f(x1) status: [x1] precedence above: h g #(x1) status: [x1] precedence above: g(x1) status: [x1] precedence above: h