MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { ite(tt(), x, y) -> x , ite(ff(), x, y) -> y , lt(x, 0()) -> ff() , lt(0(), s(y)) -> tt() , lt(s(x), s(y)) -> lt(x, y) , insert(a, nil()) -> cons(a, nil()) , insert(a, cons(b, l)) -> ite(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))) , sort(nil()) -> nil() , sort(cons(a, l)) -> insert(a, sort(l)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..