MAYBE Input TRS: 1: s(p(x)) -> x 2: p(s(x)) -> x 3: pos(0()) -> false() 4: pos(s(0())) -> true() 5: pos(s(x)) -> true() | pos(x) --> true() 6: pos(p(x)) -> false() | pos(x) --> false() Infeasibility test: pos(p(x)) --> true() Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.