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