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