MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          #add(#0(),y) -> y
          #add(#neg(#s(#0())),y) -> #pred(y)
          #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y))
          #add(#pos(#s(#0())),y) -> #succ(y)
          #add(#pos(#s(#s(x))),y) -> #succ(#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(#neg(#s(x))) -> #neg(#s(#s(x)))
          #pred(#pos(#s(#0()))) -> #0()
          #pred(#pos(#s(#s(x)))) -> #pos(#s(x))
          #succ(#0()) -> #pos(#s(#0()))
          #succ(#neg(#s(#0()))) -> #0()
          #succ(#neg(#s(#s(x)))) -> #neg(#s(x))
          #succ(#pos(#s(x))) -> #pos(#s(#s(x)))
          add(x,y) -> #add(x,y)
          and(x,y) -> #and(x,y)
          append(l,ys) -> append#1(l,ys)
          append#1(dd(x,xs),ys) -> append#2(append(xs,ys),x)
          append#1(nil(),ys) -> ys
          append#2(l',x) -> dd(x,l')
          bitonicMerge(l,direction) -> bitonicMerge#1(l,direction,l)
          bitonicMerge#1(dd(x,xs),direction,l) -> bitonicMerge#2(xs,direction,l)
          bitonicMerge#1(nil(),direction,l) -> nil()
          bitonicMerge#10(#false(),hi,low) -> tuple#2(low,hi)
          bitonicMerge#10(#true(),hi,low) -> tuple#2(hi,low)
          bitonicMerge#2(dd(y,ys),direction,l) -> bitonicMerge#3(div2(length(l)),direction,l)
          bitonicMerge#2(nil(),direction,l) -> l
          bitonicMerge#3(h,direction,l) -> bitonicMerge#4(splitAt(h,l),direction)
          bitonicMerge#4(s,direction) -> bitonicMerge#5(bitonicMerge#6(s),direction,s)
          bitonicMerge#5(hi,direction,s) -> bitonicMerge#7(bitonicMerge#8(s),direction,hi)
          bitonicMerge#6(tuple#2(zipWithOr1,zipWithOr2)) -> zipWithOr(zipWithOr1,zipWithOr2)
          bitonicMerge#7(low,direction,hi) -> bitonicMerge#9(bitonicMerge#10(direction,hi,low),direction)
          bitonicMerge#8(tuple#2(zipWithAnd3,zipWithAnd4)) -> zipWithAnd(zipWithAnd3,zipWithAnd4)
          bitonicMerge#9(tuple#2(hi,low),direction) -> append(bitonicMerge(low,direction),bitonicMerge(hi,direction))
          bitonicSort(l,dir) -> bitonicSort#1(l,dir,l)
          bitonicSort#1(dd(x,xs),dir,l) -> bitonicSort#2(split(l),dir)
          bitonicSort#1(nil(),dir,l) -> nil()
          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(n) -> div2#1(n)
          div2#1(#0()) -> #0()
          div2#1(#s(n)) -> div2#2(n)
          div2#2(#0()) -> #0()
          div2#2(#s(n)) -> add(#pos(#s(#0())),div2(n))
          length(l) -> length#1(l)
          length#1(dd(x,xs)) -> add(#pos(#s(#0())),length(xs))
          length#1(nil()) -> #0()
          or(x,y) -> #or(x,y)
          split(l) -> split#1(l)
          split#1(dd(x1,xs)) -> split#2(xs,x1)
          split#1(nil()) -> tuple#2(nil(),nil())
          split#2(dd(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(dd(x1,l1),dd(x2,l2))
          splitAt(n,l) -> splitAt#1(n,l)
          splitAt#1(#0(),l) -> tuple#2(nil(),l)
          splitAt#1(#s(n'),l) -> splitAt#2(l,n')
          splitAt#2(dd(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(dd(x,l1),l2)
          zipWithAnd(l1,l2) -> zipWithAnd#1(l1,l2)
          zipWithAnd#1(dd(x,xs),l2) -> zipWithAnd#2(l2,x,xs)
          zipWithAnd#1(nil(),l2) -> nil()
          zipWithAnd#2(dd(y,ys),x,xs) -> dd(and(x,y),zipWithAnd(xs,ys))
          zipWithAnd#2(nil(),x,xs) -> nil()
          zipWithOr(l1,l2) -> zipWithOr#1(l1,l2)
          zipWithOr#1(dd(x,xs),l2) -> zipWithOr#2(l2,x,xs)
          zipWithOr#1(nil(),l2) -> nil()
          zipWithOr#2(dd(y,ys),x,xs) -> dd(or(x,y),zipWithOr(xs,ys))
          zipWithOr#2(nil(),x,xs) -> nil()
      - Signature:
          {#add/2,#and/2,#or/2,#pred/1,#succ/1,add/2,and/2,append/2,append#1/2,append#2/2,bitonicMerge/2
          ,bitonicMerge#1/3,bitonicMerge#10/3,bitonicMerge#2/3,bitonicMerge#3/3,bitonicMerge#4/2,bitonicMerge#5/3
          ,bitonicMerge#6/1,bitonicMerge#7/3,bitonicMerge#8/1,bitonicMerge#9/2,bitonicSort/2,bitonicSort#1/3
          ,bitonicSort#2/2,bitonicSort#3/4,bitonicSort#4/4,div2/1,div2#1/1,div2#2/1,length/1,length#1/1,or/2,split/1
          ,split#1/1,split#2/2,split#3/3,splitAt/2,splitAt#1/2,splitAt#2/2,splitAt#3/2,zipWithAnd/2,zipWithAnd#1/2
          ,zipWithAnd#2/3,zipWithOr/2,zipWithOr#1/2,zipWithOr#2/3} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
          ,nil/0,tuple#2/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {#add,#and,#or,#pred,#succ,add,and,append,append#1
          ,append#2,bitonicMerge,bitonicMerge#1,bitonicMerge#10,bitonicMerge#2,bitonicMerge#3,bitonicMerge#4
          ,bitonicMerge#5,bitonicMerge#6,bitonicMerge#7,bitonicMerge#8,bitonicMerge#9,bitonicSort,bitonicSort#1
          ,bitonicSort#2,bitonicSort#3,bitonicSort#4,div2,div2#1,div2#2,length,length#1,or,split,split#1,split#2
          ,split#3,splitAt,splitAt#1,splitAt#2,splitAt#3,zipWithAnd,zipWithAnd#1,zipWithAnd#2,zipWithOr,zipWithOr#1
          ,zipWithOr#2} and constructors {#0,#false,#neg,#pos,#s,#true,dd,nil,tuple#2}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE