MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { D(t()) -> 1() , D(constant()) -> 0() , D(+(x, y)) -> +(D(x), D(y)) , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) , D(-(x, y)) -> -(D(x), D(y)) , D(minus(x)) -> minus(D(x)) , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))) , D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))) , D(ln(x)) -> div(D(x), x) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..