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