MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { inc(s(x)) -> s(inc(x)) , inc(0()) -> s(0()) , plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s(0())), x, inc(x)) , ifPlus(false(), x, y, z) -> plus(x, z) , ifPlus(true(), x, y, z) -> y , eq(x, x) -> true() , eq(s(x), s(y)) -> eq(x, y) , eq(s(x), 0()) -> false() , eq(0(), s(x)) -> false() , eq(0(), 0()) -> true() , minus(x, x) -> 0() , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , minus(0(), x) -> 0() , times(x, y) -> timesIter(x, y, 0()) , timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s(0())), y, z, plus(y, z)) , ifTimes(false(), x, y, z, u) -> timesIter(x, y, u) , ifTimes(true(), x, y, z, u) -> z , f() -> g() , f() -> h() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..