YES Input TRS: 1: f(y,a()) -> g(x,x) | h(z) --> x | y --> k(z) 2: k(x) -> h(x) 3: k(x) -> b() 4: k(x) -> a() 5: a() -> b() Infeasibility test: f(k(b()),x) --> g(h(a()),y) Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ... succeeded. a() weight: (/ 7 32) status: [] precedence above: h(x1) weight: (/ 1 8) + x1 status: [] precedence above: b() weight: 0 status: [] precedence above: a k(x1) weight: (/ 9 32) + x1 status: [] precedence above: h f(x1,x2) weight: (/ 5 32) + x1 status: [] precedence above: #(x1) weight: x1 status: [] precedence above: g(x1,x2) weight: (/ 1 8) + x1 status: [] precedence above: