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