MAYBE Input TRS: 1: f(x,x) -> f(a(),b()) Infeasibility test: F(a(),b()) --> F(x,x) Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.