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