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