MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { g(X) -> u(h(X), h(X), X) , u(d(), c(Y), X) -> k(Y) , h(d()) -> c(a()) , h(d()) -> c(b()) , f(k(a()), k(b()), X) -> f(X, X, X) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..