YES Input TRS: 1: -(0(),x) -> 0() 2: -(x,0()) -> x 3: -(s(x),s(y)) -> -(x,y) Infeasibility test: -(x,x) --> s(x) Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ... succeeded. s(x1) status: [x1] precedence above: - 0() status: [] precedence above: -(x1,x2) status: [x1] precedence above: #(x1) status: [x1] precedence above: