MAYBE 1080.62/297.09 MAYBE 1080.62/297.09 1080.62/297.09 We are left with following problem, upon which TcT provides the 1080.62/297.09 certificate MAYBE. 1080.62/297.09 1080.62/297.09 Strict Trs: 1080.62/297.09 { splitD(@pivot, @l) -> splitD#1(@l, @pivot) 1080.62/297.09 , quicksort#2(tuple#2(@xs, @ys), @z) -> 1080.62/297.09 append(quicksort(@xs), ::(@z, quicksort(@ys))) 1080.62/297.09 , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) 1080.62/297.09 , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) 1080.62/297.09 , append(@l, @ys) -> append#1(@l, @ys) 1080.62/297.09 , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) 1080.62/297.09 , split#1(::(@x, @xs), @pivot) -> 1080.62/297.09 split#2(split(@pivot, @xs), @pivot, @x) 1080.62/297.09 , split(@pivot, @l) -> split#1(@l, @pivot) 1080.62/297.09 , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) 1080.62/297.09 , splitD#1(::(@x, @xs), @pivot) -> 1080.62/297.09 splitD#2(splitD(@pivot, @xs), @pivot, @x) 1080.62/297.09 , quicksortD#2(tuple#2(@xs, @ys), @z) -> 1080.62/297.09 appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) 1080.62/297.09 , quicksortD(@l) -> quicksortD#1(@l) 1080.62/297.09 , appendD#1(nil(), @ys) -> @ys 1080.62/297.09 , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) 1080.62/297.09 , split#2(tuple#2(@ls, @rs), @pivot, @x) -> 1080.62/297.09 split#3(#greater(@x, @pivot), @ls, @rs, @x) 1080.62/297.09 , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) 1080.62/297.09 , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> 1080.62/297.09 splitD#3(#greater(@x, @pivot), @ls, @rs, @x) 1080.62/297.09 , quicksort#1(nil()) -> nil() 1080.62/297.09 , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) 1080.62/297.09 , append#1(nil(), @ys) -> @ys 1080.62/297.09 , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) 1080.62/297.09 , testQuicksort2(@x) -> quicksort(testList(#unit())) 1080.62/297.09 , quicksort(@l) -> quicksort#1(@l) 1080.62/297.09 , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) 1080.62/297.09 , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) 1080.62/297.09 , testQuicksort(@x) -> quicksort(testList(#unit())) 1080.62/297.09 , testList(@x) -> 1080.62/297.09 ::(#abs(#0()), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#s(#0())))))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))), 1080.62/297.09 ::(#abs(#pos(#s(#0()))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#0())))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))), 1080.62/297.09 ::(#abs(#pos(#s(#s(#s(#0()))))), nil())))))))))) 1080.62/297.09 , quicksortD#1(nil()) -> nil() 1080.62/297.09 , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) 1080.62/297.09 , #abs(#pos(@x)) -> #pos(@x) 1080.62/297.09 , #abs(#0()) -> #0() 1080.62/297.09 , #abs(#neg(@x)) -> #pos(@x) 1080.62/297.09 , #abs(#s(@x)) -> #pos(#s(@x)) 1080.62/297.09 , appendD(@l, @ys) -> appendD#1(@l, @ys) } 1080.62/297.09 Weak Trs: 1080.62/297.09 { #ckgt(#EQ()) -> #false() 1080.62/297.09 , #ckgt(#LT()) -> #false() 1080.62/297.09 , #ckgt(#GT()) -> #true() 1080.62/297.09 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 1080.62/297.09 , #compare(#pos(@x), #0()) -> #GT() 1080.62/297.09 , #compare(#pos(@x), #neg(@y)) -> #GT() 1080.62/297.09 , #compare(#0(), #pos(@y)) -> #LT() 1080.62/297.09 , #compare(#0(), #0()) -> #EQ() 1080.62/297.09 , #compare(#0(), #neg(@y)) -> #GT() 1080.62/297.09 , #compare(#0(), #s(@y)) -> #LT() 1080.62/297.09 , #compare(#neg(@x), #pos(@y)) -> #LT() 1080.62/297.09 , #compare(#neg(@x), #0()) -> #LT() 1080.62/297.09 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 1080.62/297.09 , #compare(#s(@x), #0()) -> #GT() 1080.62/297.09 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) } 1080.62/297.09 Obligation: 1080.62/297.09 innermost runtime complexity 1080.62/297.09 Answer: 1080.62/297.09 MAYBE 1080.62/297.09 1080.62/297.09 None of the processors succeeded. 1080.62/297.09 1080.62/297.09 Details of failed attempt(s): 1080.62/297.09 ----------------------------- 1080.62/297.09 1) 'empty' failed due to the following reason: 1080.62/297.09 1080.62/297.09 Empty strict component of the problem is NOT empty. 1080.62/297.09 1080.62/297.09 2) 'Best' failed due to the following reason: 1080.62/297.09 1080.62/297.09 None of the processors succeeded. 1080.62/297.09 1080.62/297.09 Details of failed attempt(s): 1080.62/297.09 ----------------------------- 1080.62/297.09 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1080.62/297.09 following reason: 1080.62/297.09 1080.62/297.09 Computation stopped due to timeout after 297.0 seconds. 1080.62/297.09 1080.62/297.09 2) 'Best' failed due to the following reason: 1080.62/297.09 1080.62/297.09 None of the processors succeeded. 1080.62/297.09 1080.62/297.09 Details of failed attempt(s): 1080.62/297.09 ----------------------------- 1080.62/297.09 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1080.62/297.09 seconds)' failed due to the following reason: 1080.62/297.09 1080.62/297.09 Computation stopped due to timeout after 148.0 seconds. 1080.62/297.09 1080.62/297.09 2) 'Best' failed due to the following reason: 1080.62/297.09 1080.62/297.09 None of the processors succeeded. 1080.62/297.09 1080.62/297.09 Details of failed attempt(s): 1080.62/297.09 ----------------------------- 1080.62/297.09 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1080.62/297.09 to the following reason: 1080.62/297.09 1080.62/297.09 The input cannot be shown compatible 1080.62/297.09 1080.62/297.09 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1080.62/297.09 following reason: 1080.62/297.09 1080.62/297.09 The input cannot be shown compatible 1080.62/297.09 1080.62/297.09 1080.62/297.09 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1080.62/297.09 failed due to the following reason: 1080.62/297.09 1080.62/297.09 None of the processors succeeded. 1080.62/297.09 1080.62/297.09 Details of failed attempt(s): 1080.62/297.09 ----------------------------- 1080.62/297.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1080.62/297.09 failed due to the following reason: 1080.62/297.09 1080.62/297.09 match-boundness of the problem could not be verified. 1080.62/297.09 1080.62/297.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1080.62/297.09 failed due to the following reason: 1080.62/297.09 1080.62/297.09 match-boundness of the problem could not be verified. 1080.62/297.09 1080.62/297.09 1080.62/297.09 1080.62/297.09 1080.62/297.09 1080.62/297.09 Arrrr.. 1081.17/297.39 EOF