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