TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() , average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y) , if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y) , if(false(), b1, b2, b3, x, y) -> average(p(x), s(y)) , if2(true(), b2, b3, x, y) -> 0() , if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y) , if3(true(), b3, x, y) -> 0() , if3(false(), b3, x, y) -> if4(b3, x, y) , if4(true(), x, y) -> s(0()) , if4(false(), x, y) -> average(s(x), p(p(y))) } Obligation: innermost runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 60.0 seconds. Arrrr..