MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          cond_insert_ord_x_ys_1(False(),x3,x2,x1) -> Cons(x2,insert#3(x3,x1))
          cond_insert_ord_x_ys_1(True(),x3,x2,x1) -> Cons(x3,Cons(x2,x1))
          insert#3(x2,Nil()) -> Cons(x2,Nil())
          insert#3(x6,Cons(x4,x2)) -> cond_insert_ord_x_ys_1(leq#2(x6,x4),x6,x4,x2)
          leq#2(0(),x8) -> True()
          leq#2(S(x12),0()) -> False()
          leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
          main(x1) -> sort#2(x1)
          sort#2(Cons(x4,x2)) -> insert#3(x4,sort#2(x2))
          sort#2(Nil()) -> Nil()
      - Signature:
          {cond_insert_ord_x_ys_1/4,insert#3/2,leq#2/2,main/1,sort#2/1} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {cond_insert_ord_x_ys_1,insert#3,leq#2,main
          ,sort#2} and constructors {0,Cons,False,Nil,S,True}
  + Applied Processor:
      MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = NoUArgs, miURules = NoURules, miSelector = Nothing}
  + Details:
      Incompatible
MAYBE