MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(x, 0()) -> x , plus(x, s(y)) -> s(plus(x, y)) , d(0()) -> 0() , d(s(x)) -> s(s(d(x))) , q(0()) -> 0() , q(s(x)) -> s(plus(q(x), d(x))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..