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