MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) , sum(cons(0(), x), y) -> sum(x, y) , sum(nil(), y) -> y , empty(cons(n, x)) -> false() , empty(nil()) -> true() , tail(cons(n, x)) -> x , tail(nil()) -> nil() , head(cons(n, x)) -> n , weight(x) -> if(empty(x), empty(tail(x)), x) , if(true(), b, x) -> weight_undefined_error() , if(false(), b, x) -> if2(b, x) , if2(true(), x) -> head(x) , if2(false(), x) -> weight(sum(x, cons(0(), tail(tail(x))))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..