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