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