YES Input TRS: 1: le(x,0()) -> false() 2: le(0(),s(y)) -> true() 3: le(s(x),s(y)) -> le(x,y) 4: min(cons(x,nil())) -> x 5: min(cons(x,xs)) -> x | min(xs) --> y | le(x,y) --> true() 6: min(cons(x,xs)) -> y | min(xs) --> y | le(x,y) --> false() Infeasibility test: min(nil()) --> x1 le(x2,x1) --> true() Co-Order(NegReal,≥,Sum) ... succeeded. le(x1,x2) weight: (- (/ 37175 2)) + x2 s(x1) weight: 0 false() weight: (- (/ 37175 2)) true() weight: (- (/ 37175 2)) 0() weight: 0 nil() weight: (- (/ 44229 2)) #(x1,x2) weight: x2 + x1 min(x1) weight: x1 cons(x1,x2) weight: 0