MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { admit(x, nil()) -> nil() , admit(x, .(u, .(v, .(w(), z)))) -> cond(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z))))) , cond(true(), y) -> y } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..