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 , weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0(), x))) , weight(cons(n, nil())) -> n } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..