MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , plus(0(), y) -> y , plus(s(x), y) -> plus(x, s(y)) , zero(0()) -> true() , zero(s(x)) -> false() , p(s(x)) -> x , div(x, y) -> quot(x, y, 0()) , quot(x, y, z) -> if(zero(x), x, y, plus(z, s(0()))) , if(false(), x, s(y), z) -> quot(minus(x, s(y)), s(y), z) , if(true(), x, y, z) -> p(z) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..