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


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"))


MAYBE