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