MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          #abs(#0()) -> #0()
          #abs(#neg(@x)) -> #pos(@x)
          #abs(#pos(@x)) -> #pos(@x)
          #abs(#s(@x)) -> #pos(#s(@x))
          #less(@x,@y) -> #cklt(#compare(@x,@y))
          insert(@x,@l) -> insert#1(@l,@x)
          insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
          insert#1(nil(),@x) -> ::(@x,nil())
          insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
          insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
          insertD(@x,@l) -> insertD#1(@l,@x)
          insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys)
          insertD#1(nil(),@x) -> ::(@x,nil())
          insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
          insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys))
          insertionsort(@l) -> insertionsort#1(@l)
          insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
          insertionsort#1(nil()) -> nil()
          insertionsortD(@l) -> insertionsortD#1(@l)
          insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs))
          insertionsortD#1(nil()) -> nil()
          testInsertionsort(@x) -> insertionsort(testList(#unit()))
          testInsertionsortD(@x) -> insertionsortD(testList(#unit()))
          testList(@_) -> ::(#abs(#0())
                            ,::(#abs(#pos(#s(#s(#s(#s(#0()))))))
                               ,::(#abs(#pos(#s(#s(#s(#s(#s(#0())))))))
                                  ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))))
                                     ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0())))))))))
                                        ,::(#abs(#pos(#s(#0())))
                                           ,::(#abs(#pos(#s(#s(#0()))))
                                              ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))
                                                 ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0()))))))))
                                                    ,::(#abs(#pos(#s(#s(#s(#0()))))),nil()))))))))))
      - Weak TRS:
          #cklt(#EQ()) -> #false()
          #cklt(#GT()) -> #false()
          #cklt(#LT()) -> #true()
          #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)
      - Signature:
          {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
          ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1
          ,testInsertionsortD/1,testList/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2
          ,nil/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {#abs,#cklt,#compare,#less,insert,insert#1,insert#2
          ,insertD,insertD#1,insertD#2,insertionsort,insertionsort#1,insertionsortD,insertionsortD#1,testInsertionsort
          ,testInsertionsortD,testList} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,#unit,::,nil}
  + Applied Processor:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
  + Details:
      The input can not be schown compatible.
MAYBE