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