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


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


MAYBE