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