MAYBE Input TRS: 1: lt(x,0()) -> false() 2: lt(0(),s(x)) -> true() 3: lt(s(x),s(y)) -> lt(x,y) 4: m(0(),s(y)) -> 0() 5: m(x,0()) -> x 6: m(s(x),s(y)) -> m(x,y) 7: gcd(x,x) -> x 8: gcd(s(x),0()) -> s(x) 9: gcd(0(),s(y)) -> s(y) 10: gcd(s(x),s(y)) -> gcd(m(x,y),s(y)) | lt(y,x) --> true() 11: gcd(s(x),s(y)) -> gcd(s(x),m(y,x)) | lt(x,y) --> true() Infeasibility test: lt(x2,x2) --> true() Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.