BEST_CASE(Omega(1),?)
UNSAT
"/tmp/SMTS3560-9" (line 1, column 6):
The smt problem could not be solved (was unsat).


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

(STRATEGY
 INNERMOST)
(VAR
 "v451" "v63" "v79" "v112" "v128" "v44" "v7" "v8" "v5" "v6" "v4"
 "v3" "v2" "v1" "v229" "v10" "v56" "v64" "v22" "v14" "v16" "v20"
 "v113")
(DATATYPES
   "bool" = < "True", "False" >
   "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil", "bot[1]" >
   "nat" = µX.< "S"(X), "0", "bot[0]" >)
(SIGNATURES
   "divide_ys#1" :: ["list" x "nat"] --> "list"
   "cond_merge_ys_zs_2" :: ["bool" x "list" x "list" x "nat" x "list" x "nat" x "list"] --> "list"
   "merge#2" :: ["list" x "list"] --> "list"
   "dc#1" :: ["list"] --> "list"
   "drop#2" :: ["nat" x "list"] --> "list"
   "take#2" :: ["nat" x "list"] --> "list"
   "halve#1" :: ["nat"] --> "nat"
   "const_f#2" :: ["list" x "list"] --> "list"
   "leq#2" :: ["nat" x "nat"] --> "bool"
   "length#1" :: ["list"] --> "nat"
   "map#2" :: ["list"] --> "list"
   "main" :: ["list"] --> "list")
(RULES
 "divide_ys#1"("Cons"("v451","Cons"("v63","v79")),"S"("0"())) -> "Cons"("Cons"("v451","Nil"()),"Cons"("Cons"("v63","v79"),"Nil"()))
 "divide_ys#1"("Cons"("v451","Cons"("v112","v128")),"S"("S"("v44"))) -> "Cons"("Cons"("v451","Cons"("v112","take#2"("v44","v128"))),"Cons"("drop#2"("v44","v128"),"Nil"()))
 "cond_merge_ys_zs_2"("True"(),"Cons"("v7","v8"),"Cons"("v5","v6"),"v4","v3","v2","v1") -> "Cons"("v4","merge#2"("v3","Cons"("v5","v6")))
 "cond_merge_ys_zs_2"("False"(),"Cons"("v7","v8"),"Cons"("v5","v6"),"v4","v3","v2","v1") -> "Cons"("v2","merge#2"("Cons"("v7","v8"),"v1"))
 "merge#2"("Nil"(),"v2") -> "v2"
 "merge#2"("Cons"("v4","v2"),"Nil"()) -> "Cons"("v4","v2")
 "merge#2"("Cons"("v8","v6"),"Cons"("v4","v2")) -> "cond_merge_ys_zs_2"("leq#2"("v8","v4"),"Cons"("v8","v6"),"Cons"("v4","v2"),"v8","v6","v4","v2")
 "dc#1"("Nil"()) -> "Nil"()
 "dc#1"("Cons"("v229","Nil"())) -> "Cons"("v229","Nil"())
 "dc#1"("Cons"("v3","Cons"("v2","v1"))) -> "const_f#2"("Cons"("v3","Cons"("v2","v1")),"map#2"("divide_ys#1"("Cons"("v3","Cons"("v2","v1")),"S"("halve#1"("length#1"("v1"))))))
 "drop#2"("0"(),"v2") -> "v2"
 "drop#2"("S"("0"()),"Nil"()) -> "bot[1]"()
 "drop#2"("S"("v10"),"Cons"("v56","v64")) -> "drop#2"("v10","v64")
 "take#2"("0"(),"v2") -> "Nil"()
 "take#2"("S"("0"()),"Nil"()) -> "Cons"("bot[0]"(),"Nil"())
 "take#2"("S"("v22"),"Cons"("v56","v64")) -> "Cons"("v56","take#2"("v22","v64"))
 "halve#1"("0"()) -> "0"()
 "halve#1"("S"("0"())) -> "S"("0"())
 "halve#1"("S"("S"("v14"))) -> "S"("halve#1"("v14"))
 "const_f#2"("Cons"("v4","Cons"("v5","v6")),"Cons"("v3","Cons"("v2","v1"))) -> "merge#2"("v3","v2")
 "leq#2"("0"(),"v16") -> "True"()
 "leq#2"("S"("v20"),"0"()) -> "False"()
 "leq#2"("S"("v4"),"S"("v2")) -> "leq#2"("v4","v2")
 "length#1"("Nil"()) -> "0"()
 "length#1"("Cons"("v6","v8")) -> "S"("length#1"("v8"))
 "map#2"("Nil"()) -> "Nil"()
 "map#2"("Cons"("v2","v1")) -> "Cons"("dc#1"("v2"),"map#2"("v1"))
 "main"("v113") -> "dc#1"("v113"))


BEST_CASE(Omega(1),?)