WORST_CASE(?,O(n^2))

Solution:
---------

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


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

  "0" :: [] -(0)-> "nat"_cf(0, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(8, 0) x "list"_cf(8, 0)] -(8)-> "list"_cf(8, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(7, 0) x "list"_cf(7, 0)] -(7)-> "list"_cf(7, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(7, 0) x "list"_cf(14, 7)] -(7)-> "list"_cf(7, 7)
  "Cons" :: ["__ANY_TYPE__"_cf(0, 0) x "list"_cf(0, 0)] -(0)-> "list"_cf(0, 0)
  "Cons" :: ["__ANY_TYPE__"_cf(0, 0) x "list"_cf(8, 8)] -(0)-> "list"_cf(0, 8)
  "False" :: [] -(0)-> "bool"_cf(0, 0)
  "False" :: [] -(0)-> "bool"_cf(0, 1)
  "False" :: [] -(0)-> "bool"_cf(4, 4)
  "Nil" :: [] -(0)-> "list"_cf(8, 0)
  "Nil" :: [] -(0)-> "list"_cf(8, 8)
  "Nil" :: [] -(0)-> "list"_cf(7, 0)
  "Nil" :: [] -(0)-> "list"_cf(15, 7)
  "Nil" :: [] -(0)-> "list"_cf(0, 0)
  "S" :: ["nat"_cf(0, 0)] -(0)-> "nat"_cf(0, 0)
  "True" :: [] -(0)-> "bool"_cf(0, 0)
  "True" :: [] -(0)-> "bool"_cf(0, 1)
  "True" :: [] -(0)-> "bool"_cf(0, 8)
  "cond_insert_ord_x_ys_1" :: ["bool"_cf(0, 0) x "nat"_cf(8, 0) x "nat"_cf(7, 0) x "list"_cf(7, 0)] -(15)-> "list"_cf(7, 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)] -(1)-> "list"_cf(0, 0)
  "cond_insert_ord_x_ys_1" :: ["bool"_cf(0, 1) x "nat"_cf(0, 0) x "nat"_cf(0, 0) x "list"_cf(0, 0)] -(0)-> "list"_cf(0, 0)
  "fold#3" :: ["list"_cf(8, 0)] -(0)-> "list"_cf(7, 0)
  "insert_ord#2" :: ["nat"_cf(8, 0) x "list"_cf(7, 0)] -(8)-> "list"_cf(7, 0)
  "insert_ord#2" :: ["nat"_cf(0, 0) x "list"_cf(0, 0)] -(1)-> "list"_cf(0, 0)
  "insert_ord#2" :: ["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)
  "leq#2" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(0)-> "bool"_cf(0, 2)
  "leq#2" :: ["nat"_cf(0, 0) x "nat"_cf(0, 0)] -(1)-> "bool"_cf(0, 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, 0) 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
 "v2" "v1" "v3" "v0" "v5" "v6" "v4" "v8" "v12")
(DATATYPES
   "bool" = < "True", "False" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >)
(SIGNATURES
   "fold#3" :: ["list"] --> "list"
   "cond_insert_ord_x_ys_1" :: ["bool" x "nat" x "nat" x "list"] --> "list"
   "insert_ord#2" :: ["nat" x "list"] --> "list"
   "leq#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "fold#3"("Nil"()) -> "Nil"()
 "fold#3"("Cons"("v2","v1")) -> "insert_ord#2"("v2","fold#3"("v1"))
 "cond_insert_ord_x_ys_1"("True"(),"v3","v2","v1") -> "Cons"("v3","Cons"("v2","v1"))
 "cond_insert_ord_x_ys_1"("False"(),"v0","v5","v2") -> "Cons"("v5","insert_ord#2"("v0","v2"))
 "insert_ord#2"("v2","Nil"()) -> "Cons"("v2","Nil"())
 "insert_ord#2"("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"("v3") -> "fold#3"("v3"))


WORST_CASE(?,O(n^2))