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


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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v2" "v14" "v10" "v6" "v8" "v40" "v48" "v16" "v12" "v1")
(DATATYPES
   "bool" = < "True", "False" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >)
(SIGNATURES
   "isort#2" :: ["list"] --> "list"
   "insert#3" :: ["list" x "list"] --> "list"
   "compare_list#2" :: ["list" x "list"] --> "bool"
   "ite2#3" :: ["bool" x "bool" x "bool"] --> "bool"
   "ite_cond#2" :: ["bool" x "list" x "list"] --> "list"
   "ltNat#2" :: ["nat" x "nat"] --> "bool"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "isort#2"("Nil"()) -> "Nil"()
 "isort#2"("Cons"("v4","v2")) -> "insert#3"("v4","isort#2"("v2"))
 "insert#3"("v2","Nil"()) -> "Cons"("v2","Nil"())
 "insert#3"("v14","Cons"("v10","v6")) -> "ite_cond#2"("compare_list#2"("v10","v14"),"Cons"("v10","insert#3"("v14","v6")),"Cons"("v14","Cons"("v10","v6")))
 "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"),"ltNat#2"("v8","v4"))
 "ite2#3"("True"(),"v40","v48") -> "v40"
 "ite2#3"("False"(),"v40","v48") -> "v48"
 "ite_cond#2"("True"(),"Cons"("v8","v10"),"Cons"("v2","Cons"("v4","v6"))) -> "Cons"("v8","v10")
 "ite_cond#2"("False"(),"Cons"("v8","v10"),"Cons"("v2","Cons"("v4","v6"))) -> "Cons"("v2","Cons"("v4","v6"))
 "ltNat#2"("v8","0"()) -> "False"()
 "ltNat#2"("0"(),"S"("v16")) -> "True"()
 "ltNat#2"("S"("v4"),"S"("v2")) -> "ltNat#2"("v4","v2")
 "eqNat#2"("0"(),"0"()) -> "True"()
 "eqNat#2"("S"("v12"),"0"()) -> "False"()
 "eqNat#2"("S"("v4"),"S"("v2")) -> "eqNat#2"("v4","v2")
 "eqNat#2"("0"(),"S"("v12")) -> "False"()
 "main"("v1") -> "isort#2"("v1"))


MAYBE