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