We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { decrease(Cons(x, xs)) -> decrease(xs) , decrease(Nil()) -> number42(Nil()) , number42(x) -> Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Cons(Nil(), Nil())))))))))))))))))))))))))))))))))))))))))) , goal(x) -> decrease(x) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(decrease) = {}, safe(Cons) = {1, 2}, safe(Nil) = {}, safe(number42) = {1}, safe(goal) = {} and precedence decrease > number42, goal > decrease . Following symbols are considered recursive: {decrease} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: decrease(Cons(; x, xs);) > decrease(xs;) decrease(Nil();) > number42(; Nil()) number42(; x) > Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Cons(; Nil(), Nil())))))))))))))))))))))))))))))))))))))))))) goal(x;) > decrease(x;) Hurray, we answered YES(?,O(n^1))