WORST_CASE(?,O(n^2))

Solution:
---------

  "0" :: [] -(0)-> "nat"(0, 0)
  "0" :: [] -(0)-> "nat"(1, 0)
  "Cons" :: ["__ANY_TYPE__"(5, 9) x "list"(14, 9)] -(5)-> "list"(5, 9)
  "Cons" :: ["__ANY_TYPE__"(4, 0) x "list"(4, 0)] -(4)-> "list"(4, 0)
  "Cons" :: ["__ANY_TYPE__"(1, 0) x "list"(1, 0)] -(1)-> "list"(1, 0)
  "Cons" :: ["__ANY_TYPE__"(2, 0) x "list"(2, 0)] -(2)-> "list"(2, 0)
  "Cons" :: ["__ANY_TYPE__"(1, 1) x "list"(2, 1)] -(1)-> "list"(1, 1)
  "False" :: [] -(0)-> "bool"(3, 3)
  "False" :: [] -(0)-> "bool"(13, 13)
  "Nil" :: [] -(0)-> "list"(5, 9)
  "Nil" :: [] -(0)-> "list"(4, 0)
  "Nil" :: [] -(0)-> "list"(8, 8)
  "Nil" :: [] -(0)-> "list"(12, 2)
  "S" :: ["nat"(0, 0)] -(0)-> "nat"(0, 0)
  "S" :: ["nat"(1, 0)] -(1)-> "nat"(1, 0)
  "True" :: [] -(0)-> "bool"(3, 3)
  "True" :: [] -(0)-> "bool"(13, 13)
  "cond_insert_ord_x_ys_1" :: ["bool"(3, 3) x "nat"(4, 8) x "nat"(2, 0) x "list"(4, 0)] -(4)-> "list"(1, 0)
  "insert#3" :: ["nat"(4, 8) x "list"(4, 0)] -(2)-> "list"(1, 0)
  "leq#2" :: ["nat"(0, 0) x "nat"(1, 0)] -(1)-> "bool"(13, 13)
  "main" :: ["list"(11, 15)] -(16)-> "list"(0, 0)
  "sort#2" :: ["list"(5, 9)] -(9)-> "list"(0, 0)


Cost Free Signatures:
---------------------

  "0" :: [] -(0)-> "nat"_cf(0, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(9, 0) x "list"_cf(9, 0)] -(9)-> "list"_cf(9, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(4, 0) x "list"_cf(4, 0)] -(4)-> "list"_cf(4, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(0, 0) x "list"_cf(0, 0)] -(0)-> "list"_cf(0, 0)
  "False" :: [] -(0)-> "bool"_cf(0, 0)
  "Nil" :: [] -(0)-> "list"_cf(9, 0)
  "Nil" :: [] -(0)-> "list"_cf(10, 8)
  "Nil" :: [] -(0)-> "list"_cf(4, 0)
  "Nil" :: [] -(0)-> "list"_cf(15, 12)
  "Nil" :: [] -(0)-> "list"_cf(0, 0)
  "S" :: ["nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "True" :: [] -(0)-> "bool"_cf(0, 0)
  "cond_insert_ord_x_ys_1" :: ["bool"_cf(0, 0) x "nat"_cf(9, 0) x "nat"_cf(4, 0) x "list"_cf(4, 0)] -(13)-> "list"_cf(4, 0)
  "cond_insert_ord_x_ys_1" :: ["bool"_cf(0, 0) x "nat"_cf(0, 0) x "nat"_cf(0, 0) x "list"_cf(0, 0)] -(0)-> "list"_cf(0, 0)
  "insert#3" :: ["nat"_cf(9, 0) x "list"_cf(4, 0)] -(9)-> "list"_cf(4, 0)
  "insert#3" :: ["nat"_cf(0, 0) x "list"_cf(0, 0)] -(0)-> "list"_cf(0, 0)
  "leq#2" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(0)-> "bool"_cf(0, 0)
  "sort#2" :: ["list"_cf(9, 0)] -(0)-> "list"_cf(4, 0)


Base Constructors:
------------------
  "\"0\"_nat" :: [] -(0)-> "nat"(1, 0)
  "\"0\"_nat" :: [] -(0)-> "nat"(0, 1)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(1, 0) x "list"(1, 0)] -(1)-> "list"(1, 0)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(0, 1) x "list"(1, 1)] -(0)-> "list"(0, 1)
  "\"False\"_bool" :: [] -(0)-> "bool"(1, 0)
  "\"False\"_bool" :: [] -(0)-> "bool"(0, 1)
  "\"Nil\"_list" :: [] -(0)-> "list"(1, 0)
  "\"Nil\"_list" :: [] -(0)-> "list"(0, 1)
  "\"S\"_nat" :: ["nat"(1, 0)] -(1)-> "nat"(1, 0)
  "\"S\"_nat" :: ["nat"(0, 0)] -(0)-> "nat"(0, 1)
  "\"True\"_bool" :: [] -(0)-> "bool"(1, 0)
  "\"True\"_bool" :: [] -(0)-> "bool"(0, 1)



Parsed Typed Term Rewrite System:
---------------------------------

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v2" "v3" "v1" "v6" "v8" "v12")
(DATATYPES
   "bool" = < "True", "False" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >)
(SIGNATURES
   "sort#2" :: ["list"] --> "list"
   "cond_insert_ord_x_ys_1" :: ["bool" x "nat" x "nat" x "list"] --> "list"
   "insert#3" :: ["nat" x "list"] --> "list"
   "leq#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "sort#2"("Nil"()) -> "Nil"()
 "sort#2"("Cons"("v4","v2")) -> "insert#3"("v4","sort#2"("v2"))
 "cond_insert_ord_x_ys_1"("True"(),"v3","v2","v1") -> "Cons"("v3","Cons"("v2","v1"))
 "cond_insert_ord_x_ys_1"("False"(),"v3","v2","v1") -> "Cons"("v2","insert#3"("v3","v1"))
 "insert#3"("v2","Nil"()) -> "Cons"("v2","Nil"())
 "insert#3"("v6","Cons"("v4","v2")) -> "cond_insert_ord_x_ys_1"("leq#2"("v6","v4"),"v6","v4","v2")
 "leq#2"("0"(),"v8") -> "True"()
 "leq#2"("S"("v12"),"0"()) -> "False"()
 "leq#2"("S"("v4"),"S"("v2")) -> "leq#2"("v4","v2")
 "main"("v1") -> "sort#2"("v1"))


WORST_CASE(?,O(n^2))