MAYBE 1184.32/297.08 MAYBE 1184.32/297.08 1184.32/297.08 We are left with following problem, upon which TcT provides the 1184.32/297.08 certificate MAYBE. 1184.32/297.08 1184.32/297.08 Strict Trs: 1184.32/297.08 { insertionsort#1(nil()) -> nil() 1184.32/297.08 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 1184.32/297.08 , insert(@x, @l) -> insert#1(@l, @x) 1184.32/297.08 , testInsertionsortD(@x) -> insertionsortD(testList(#unit())) 1184.32/297.08 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 1184.32/297.08 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 1184.32/297.08 , insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys)) 1184.32/297.08 , insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 1184.32/297.08 , insertD(@x, @l) -> insertD#1(@l, @x) 1184.32/297.08 , testInsertionsort(@x) -> insertionsort(testList(#unit())) 1184.32/297.08 , insertD#1(nil(), @x) -> ::(@x, nil()) 1184.32/297.08 , insertD#1(::(@y, @ys), @x) -> 1184.32/297.08 insertD#2(#less(@y, @x), @x, @y, @ys) 1184.32/297.08 , insert#1(nil(), @x) -> ::(@x, nil()) 1184.32/297.08 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 1184.32/297.08 , testList(@_) -> 1184.32/297.08 ::(#abs(#0()), 1184.32/297.08 ::(#abs(#pos(#s(#s(#s(#s(#0())))))), 1184.32/297.08 ::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))), 1184.32/297.08 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))), 1184.32/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))), 1184.32/297.09 ::(#abs(#pos(#s(#0()))), 1184.32/297.09 ::(#abs(#pos(#s(#s(#0())))), 1184.32/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))), 1184.32/297.09 ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))), 1184.32/297.09 ::(#abs(#pos(#s(#s(#s(#0()))))), nil())))))))))) 1184.32/297.09 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 1184.32/297.09 , #abs(#pos(@x)) -> #pos(@x) 1184.32/297.09 , #abs(#0()) -> #0() 1184.32/297.09 , #abs(#neg(@x)) -> #pos(@x) 1184.32/297.09 , #abs(#s(@x)) -> #pos(#s(@x)) 1184.32/297.09 , insertionsortD#1(nil()) -> nil() 1184.32/297.09 , insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs)) 1184.32/297.09 , insertionsortD(@l) -> insertionsortD#1(@l) 1184.32/297.09 , insertionsort(@l) -> insertionsort#1(@l) } 1184.32/297.09 Weak Trs: 1184.32/297.09 { #cklt(#EQ()) -> #false() 1184.32/297.09 , #cklt(#LT()) -> #true() 1184.32/297.09 , #cklt(#GT()) -> #false() 1184.32/297.09 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 1184.32/297.09 , #compare(#pos(@x), #0()) -> #GT() 1184.32/297.09 , #compare(#pos(@x), #neg(@y)) -> #GT() 1184.32/297.09 , #compare(#0(), #pos(@y)) -> #LT() 1184.32/297.09 , #compare(#0(), #0()) -> #EQ() 1184.32/297.09 , #compare(#0(), #neg(@y)) -> #GT() 1184.32/297.09 , #compare(#0(), #s(@y)) -> #LT() 1184.32/297.09 , #compare(#neg(@x), #pos(@y)) -> #LT() 1184.32/297.09 , #compare(#neg(@x), #0()) -> #LT() 1184.32/297.09 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 1184.32/297.09 , #compare(#s(@x), #0()) -> #GT() 1184.32/297.09 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) } 1184.32/297.09 Obligation: 1184.32/297.09 innermost runtime complexity 1184.32/297.09 Answer: 1184.32/297.09 MAYBE 1184.32/297.09 1184.32/297.09 None of the processors succeeded. 1184.32/297.09 1184.32/297.09 Details of failed attempt(s): 1184.32/297.09 ----------------------------- 1184.32/297.09 1) 'empty' failed due to the following reason: 1184.32/297.09 1184.32/297.09 Empty strict component of the problem is NOT empty. 1184.32/297.09 1184.32/297.09 2) 'Best' failed due to the following reason: 1184.32/297.09 1184.32/297.09 None of the processors succeeded. 1184.32/297.09 1184.32/297.09 Details of failed attempt(s): 1184.32/297.09 ----------------------------- 1184.32/297.09 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1184.32/297.09 following reason: 1184.32/297.09 1184.32/297.09 Computation stopped due to timeout after 297.0 seconds. 1184.32/297.09 1184.32/297.09 2) 'Best' failed due to the following reason: 1184.32/297.09 1184.32/297.09 None of the processors succeeded. 1184.32/297.09 1184.32/297.09 Details of failed attempt(s): 1184.32/297.09 ----------------------------- 1184.32/297.09 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1184.32/297.09 seconds)' failed due to the following reason: 1184.32/297.09 1184.32/297.09 Computation stopped due to timeout after 148.0 seconds. 1184.32/297.09 1184.32/297.09 2) 'Best' failed due to the following reason: 1184.32/297.09 1184.32/297.09 None of the processors succeeded. 1184.32/297.09 1184.32/297.09 Details of failed attempt(s): 1184.32/297.09 ----------------------------- 1184.32/297.09 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1184.32/297.09 following reason: 1184.32/297.09 1184.32/297.09 The input cannot be shown compatible 1184.32/297.09 1184.32/297.09 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1184.32/297.09 to the following reason: 1184.32/297.09 1184.32/297.09 The input cannot be shown compatible 1184.32/297.09 1184.32/297.09 1184.32/297.09 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1184.32/297.09 failed due to the following reason: 1184.32/297.09 1184.32/297.09 None of the processors succeeded. 1184.32/297.09 1184.32/297.09 Details of failed attempt(s): 1184.32/297.09 ----------------------------- 1184.32/297.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1184.32/297.09 failed due to the following reason: 1184.32/297.09 1184.32/297.09 match-boundness of the problem could not be verified. 1184.32/297.09 1184.32/297.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1184.32/297.09 failed due to the following reason: 1184.32/297.09 1184.32/297.09 match-boundness of the problem could not be verified. 1184.32/297.09 1184.32/297.09 1184.32/297.09 1184.32/297.09 1184.32/297.09 1184.32/297.09 Arrrr.. 1185.06/297.57 EOF