MAYBE
UNSAT
"/tmp/SMTS15620-10" (line 1, column 6):
The smt problem could not be solved (was unsat).


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

(STRATEGY
 INNERMOST)
(VAR
 "v2" "v4" "v8" "v6" "v5" "v3" "v1" "v12" "v112" "v144" "v160" "v18"
 "v14" "v10" "v11" "v7" "v9" "v20" "v48" "v56" "v16")
(DATATYPES
   "bool" = < "True", "False" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X), "bot[0]" >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "compare_list#2" :: ["list" x "list"] --> "bool"
   "cond_mergesort_compare_log_l_l_2" :: ["pair" x "nat"] --> "list"
   "mergesort#3" :: ["nat" x "list"] --> "list"
   "merge#3" :: ["list" x "list"] --> "list"
   "cond_split_l_2" :: ["pair" x "list" x "list"] --> "pair"
   "split#1" :: ["list"] --> "pair"
   "ite2#3" :: ["bool" x "bool" x "bool"] --> "bool"
   "ite_b#2" :: ["bool" x "list" x "list"] --> "list"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "compare_list#2"("Nil"(),"v2") -> "True"()
 "compare_list#2"("Cons"("v4","v2"),"Nil"()) -> "False"()
 "compare_list#2"("Cons"("v8","v6"),"Cons"("v4","v2")) -> "ite2#3"("eqNat#2"("v8","v4"),"compare_list#2"("v6","v2"),"leqNat#2"("v8","v4"))
 "cond_mergesort_compare_log_l_l_2"("Pair"("Cons"("v4","v5"),"Cons"("v2","v3")),"v1") -> "merge#3"("mergesort#3"("v1","Cons"("v4","v5")),"mergesort#3"("v1","Cons"("v2","v3")))
 "mergesort#3"("0"(),"Cons"("v1","v2")) -> "Nil"()
 "mergesort#3"("S"("S"("S"("S"("S"("S"("0"())))))),"Nil"()) -> "bot[0]"()
 "mergesort#3"("S"("v4"),"Cons"("v8","Nil"())) -> "Cons"("v8","Nil"())
 "mergesort#3"("S"("v12"),"Cons"("v112","Cons"("v144","v160"))) -> "cond_mergesort_compare_log_l_l_2"("cond_split_l_2"("split#1"("v160"),"v112","v144"),"v12")
 "merge#3"("Nil"(),"v2") -> "v2"
 "merge#3"("Cons"("v4","v2"),"Nil"()) -> "Cons"("v4","v2")
 "merge#3"("Cons"("v18","v14"),"Cons"("v10","v6")) -> "ite_b#2"("compare_list#2"("v18","v10"),"Cons"("v18","merge#3"("v14","Cons"("v10","v6"))),"Cons"("v10","merge#3"("Cons"("v18","v14"),"v6")))
 "cond_split_l_2"("Pair"("v11","v12"),"v7","v9") -> "Pair"("Cons"("v7","v11"),"Cons"("v9","v12"))
 "split#1"("Nil"()) -> "Pair"("Nil"(),"Nil"())
 "split#1"("Cons"("v14","Nil"())) -> "Pair"("Cons"("v14","Nil"()),"Nil"())
 "split#1"("Cons"("v14","Cons"("v18","v20"))) -> "cond_split_l_2"("split#1"("v20"),"v14","v18")
 "ite2#3"("True"(),"v48","v56") -> "v48"
 "ite2#3"("False"(),"v48","v56") -> "v56"
 "ite_b#2"("True"(),"Cons"("v6","v8"),"Cons"("v2","v4")) -> "Cons"("v6","v8")
 "ite_b#2"("False"(),"Cons"("v6","v8"),"Cons"("v2","v4")) -> "Cons"("v2","v4")
 "eqNat#2"("0"(),"0"()) -> "True"()
 "eqNat#2"("S"("v16"),"0"()) -> "False"()
 "eqNat#2"("S"("v4"),"S"("v2")) -> "eqNat#2"("v4","v2")
 "eqNat#2"("0"(),"S"("v16")) -> "False"()
 "leqNat#2"("0"(),"v8") -> "True"()
 "leqNat#2"("S"("v4"),"S"("v2")) -> "leqNat#2"("v2","v4")
 "leqNat#2"("S"("v12"),"0"()) -> "False"()
 "main"("v1") -> "mergesort#3"("S"("S"("S"("S"("S"("S"("0"())))))),"v1"))


MAYBE