TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , merge(@l1, @l2) -> merge#1(@l1, @l2) , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs) , merge#1(nil(), @l2) -> @l2 , merge#2(::(@y, @ys), @x, @xs) -> merge#3(#less(@x, @y), @x, @xs, @y, @ys) , merge#2(nil(), @x, @xs) -> ::(@x, @xs) , merge#3(#false(), @x, @xs, @y, @ys) -> ::(@y, merge(::(@x, @xs), @ys)) , merge#3(#true(), @x, @xs, @y, @ys) -> ::(@x, merge(@xs, ::(@y, @ys))) , mergesort(@l) -> mergesort#1(@l) , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1) , mergesort#1(nil()) -> nil() , mergesort#2(::(@x2, @xs'), @x1) -> mergesort#3(msplit(::(@x1, ::(@x2, @xs')))) , mergesort#2(nil(), @x1) -> ::(@x1, nil()) , msplit(@l) -> msplit#1(@l) , mergesort#3(tuple#2(@l1, @l2)) -> merge(mergesort(@l1), mergesort(@l2)) , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1) , msplit#1(nil()) -> tuple#2(nil(), nil()) , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2) , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil()) , msplit#3(tuple#2(@l1, @l2), @x1, @x2) -> tuple#2(::(@x1, @l1), ::(@x2, @l2)) } Weak Trs: { #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() } Obligation: innermost runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 300.0 seconds. Arrrr..