MAYBE Input TRS: 1: f(x) -> A() | s(x) --> t() 2: f(x) -> B() | s(x) --> t() 3: s(a()) -> t() 4: s(b()) -> t() 5: a() -> c() 6: b() -> c() 7: g(x,x) -> h(x,x) Infeasibility test: s(x1) --> t() Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.