TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict Trs: { min(0(), y) -> 0() , min(s(x), 0()) -> 0() , min(s(x), s(y)) -> min(x, y) , len(nil()) -> 0() , len(cons(x, xs)) -> s(len(xs)) , sum(x, 0()) -> x , sum(x, s(y)) -> s(sum(x, y)) , le(0(), x) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , take(0(), cons(y, ys)) -> y , take(s(x), cons(y, ys)) -> take(x, ys) , addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil()) , if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)) , if(false(), c, x, y, z) -> z } Obligation: innermost runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 60.0 seconds. Arrrr..