MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(@x, @y) -> #add(@x, @y) , and(@x, @y) -> #and(@x, @y) , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> append#2(append(@xs, @ys), @x) , append#1(nil(), @ys) -> @ys , append#2(@l', @x) -> ::(@x, @l') , bitonicMerge(@l, @direction) -> bitonicMerge#1(@l, @direction, @l) , bitonicMerge#1(::(@x, @xs), @direction, @l) -> bitonicMerge#2(@xs, @direction, @l) , bitonicMerge#1(nil(), @direction, @l) -> nil() , bitonicMerge#2(::(@y, @ys), @direction, @l) -> bitonicMerge#3(div2(length(@l)), @direction, @l) , bitonicMerge#2(nil(), @direction, @l) -> @l , bitonicMerge#10(#false(), @hi, @low) -> tuple#2(@low, @hi) , bitonicMerge#10(#true(), @hi, @low) -> tuple#2(@hi, @low) , length(@l) -> length#1(@l) , div2(@n) -> div2#1(@n) , bitonicMerge#3(@h, @direction, @l) -> bitonicMerge#4(splitAt(@h, @l), @direction) , splitAt(@n, @l) -> splitAt#1(@n, @l) , bitonicMerge#4(@s, @direction) -> bitonicMerge#5(bitonicMerge#6(@s), @direction, @s) , bitonicMerge#6(tuple#2(@zipWithOr@1, @zipWithOr@2)) -> zipWithOr(@zipWithOr@1, @zipWithOr@2) , bitonicMerge#5(@hi, @direction, @s) -> bitonicMerge#7(bitonicMerge#8(@s), @direction, @hi) , bitonicMerge#8(tuple#2(@zipWithAnd@3, @zipWithAnd@4)) -> zipWithAnd(@zipWithAnd@3, @zipWithAnd@4) , bitonicMerge#7(@low, @direction, @hi) -> bitonicMerge#9(bitonicMerge#10(@direction, @hi, @low), @direction) , zipWithOr(@l1, @l2) -> zipWithOr#1(@l1, @l2) , bitonicMerge#9(tuple#2(@hi, @low), @direction) -> append(bitonicMerge(@low, @direction), bitonicMerge(@hi, @direction)) , zipWithAnd(@l1, @l2) -> zipWithAnd#1(@l1, @l2) , bitonicSort(@l, @dir) -> bitonicSort#1(@l, @dir, @l) , bitonicSort#1(::(@x, @xs), @dir, @l) -> bitonicSort#2(split(@l), @dir) , bitonicSort#1(nil(), @dir, @l) -> nil() , split(@l) -> split#1(@l) , bitonicSort#2(tuple#2(@l1, @l2), @dir) -> bitonicSort#3(bitonicSort(@l1, #true()), @dir, @l1, @l2) , bitonicSort#3(@s1, @dir, @l1, @l2) -> bitonicSort#4(bitonicSort(@l2, #false()), @dir, @l1, @l2) , bitonicSort#4(@s2, @dir, @l1, @l2) -> bitonicMerge(append(@l1, @l2), @dir) , div2#1(#0()) -> #0() , div2#1(#s(@n)) -> div2#2(@n) , div2#2(#0()) -> #0() , div2#2(#s(@n)) -> +(#pos(#s(#0())), div2(@n)) , length#1(::(@x, @xs)) -> +(#pos(#s(#0())), length(@xs)) , length#1(nil()) -> #0() , or(@x, @y) -> #or(@x, @y) , split#1(::(@x1, @xs)) -> split#2(@xs, @x1) , split#1(nil()) -> tuple#2(nil(), nil()) , split#2(::(@x2, @xs'), @x1) -> split#3(split(@xs'), @x1, @x2) , split#2(nil(), @x1) -> tuple#2(nil(), nil()) , split#3(tuple#2(@l1, @l2), @x1, @x2) -> tuple#2(::(@x1, @l1), ::(@x2, @l2)) , splitAt#1(#0(), @l) -> tuple#2(nil(), @l) , splitAt#1(#s(@n'), @l) -> splitAt#2(@l, @n') , splitAt#2(::(@x, @xs), @n') -> splitAt#3(splitAt(@n', @xs), @x) , splitAt#2(nil(), @n') -> tuple#2(nil(), nil()) , splitAt#3(tuple#2(@l1, @l2), @x) -> tuple#2(::(@x, @l1), @l2) , zipWithAnd#1(::(@x, @xs), @l2) -> zipWithAnd#2(@l2, @x, @xs) , zipWithAnd#1(nil(), @l2) -> nil() , zipWithAnd#2(::(@y, @ys), @x, @xs) -> ::(and(@x, @y), zipWithAnd(@xs, @ys)) , zipWithAnd#2(nil(), @x, @xs) -> nil() , zipWithOr#1(::(@x, @xs), @l2) -> zipWithOr#2(@l2, @x, @xs) , zipWithOr#1(nil(), @l2) -> nil() , zipWithOr#2(::(@y, @ys), @x, @xs) -> ::(or(@x, @y), zipWithOr(@xs, @ys)) , zipWithOr#2(nil(), @x, @xs) -> nil() } Weak Trs: { #add(#0(), @y) -> @y , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #or(#false(), #false()) -> #false() , #or(#false(), #true()) -> #true() , #or(#true(), #false()) -> #true() , #or(#true(), #true()) -> #true() , #pred(#0()) -> #neg(#s(#0())) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..