MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { rev(nil()) -> nil() , rev(.(x, y)) -> ++(rev(y), .(x, nil())) , ++(nil(), y) -> y , ++(.(x, y), z) -> .(x, ++(y, z)) , car(.(x, y)) -> x , cdr(.(x, y)) -> y , null(nil()) -> true() , null(.(x, y)) -> false() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..