MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          #equal(@x,@y) -> #eq(@x,@y)
          #less(@x,@y) -> #cklt(#compare(@x,@y))
          and(@x,@y) -> #and(@x,@y)
          insert(@x,@l) -> insert#1(@l,@x)
          insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
          insert#1(nil(),@x) -> ::(@x,nil())
          insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
          insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
          isortlist(@l) -> isortlist#1(@l)
          isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
          isortlist#1(nil()) -> nil()
          leq(@l1,@l2) -> leq#1(@l1,@l2)
          leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
          leq#1(nil(),@l2) -> #true()
          leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
          leq#2(nil(),@x,@xs) -> #false()
          or(@x,@y) -> #or(@x,@y)
      - Weak TRS:
          #and(#false(),#false()) -> #false()
          #and(#false(),#true()) -> #false()
          #and(#true(),#false()) -> #false()
          #and(#true(),#true()) -> #true()
          #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)
          #eq(#0(),#0()) -> #true()
          #eq(#0(),#neg(@y)) -> #false()
          #eq(#0(),#pos(@y)) -> #false()
          #eq(#0(),#s(@y)) -> #false()
          #eq(#neg(@x),#0()) -> #false()
          #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
          #eq(#neg(@x),#pos(@y)) -> #false()
          #eq(#pos(@x),#0()) -> #false()
          #eq(#pos(@x),#neg(@y)) -> #false()
          #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
          #eq(#s(@x),#0()) -> #false()
          #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          #eq(::(@x_1,@x_2),nil()) -> #false()
          #eq(nil(),::(@y_1,@y_2)) -> #false()
          #eq(nil(),nil()) -> #true()
          #or(#false(),#false()) -> #false()
          #or(#false(),#true()) -> #true()
          #or(#true(),#false()) -> #true()
          #or(#true(),#true()) -> #true()
      - Signature:
          {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
          ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0
          ,::/2,nil/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert
          ,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} and constructors {#0,#EQ,#GT,#LT,#false,#neg
          ,#pos,#s,#true,::,nil}
  + Applied Processor:
      MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = NoUArgs, miURules = NoURules, miSelector = Nothing}
  + Details:
      Incompatible
MAYBE