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()) --> x3 le(x1,x3) --> false() Co-Order(NegReal,≥,Sum) ... succeeded. le(x1,x2) weight: -11797 + x2 s(x1) weight: 0 false() weight: (- (/ 40325 2)) true() weight: -11797 0() weight: (- (/ 16731 2)) nil() weight: -11644 #(x1,x2) weight: x2 + x1 min(x1) weight: x1 cons(x1,x2) weight: 0