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


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

(STRATEGY
 INNERMOST)
(VAR
 "v3" "v2" "v1" "v4" "v6" "v23" "v19" "v8" "v10" "v12")
(DATATYPES
   "bool" = < "main_xs_1"("nat"), "True", "False" >
   "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil" >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "cond_quicksort_gt_xyz_1" :: ["pair" x "nat"] --> "list"
   "quicksort#2" :: ["list"] --> "list"
   "cond_partition_f_l_1" :: ["pair" x "bool" x "nat"] --> "pair"
   "partition#2" :: ["bool" x "list"] --> "pair"
   "append#2" :: ["list" x "list"] --> "list"
   "ite_b#2" :: ["bool" x "pair" x "pair"] --> "pair"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "cond_quicksort_gt_xyz_1"("Pair"("v3","v2"),"v1") -> "append#2"("quicksort#2"("v3"),"Cons"("v1","quicksort#2"("v2")))
 "quicksort#2"("Nil"()) -> "Nil"()
 "quicksort#2"("Cons"("v4","v6")) -> "cond_quicksort_gt_xyz_1"("partition#2"("main_xs_1"("v4"),"v6"),"v4")
 "cond_partition_f_l_1"("Pair"("v23","v19"),"main_xs_1"("v4"),"v2") -> "ite_b#2"("leqNat#2"("v4","v2"),"Pair"("v23","Cons"("v2","v19")),"Pair"("Cons"("v2","v23"),"v19"))
 "partition#2"("main_xs_1"("v1"),"Nil"()) -> "Pair"("Nil"(),"Nil"())
 "partition#2"("main_xs_1"("v3"),"Cons"("v2","v1")) -> "cond_partition_f_l_1"("partition#2"("main_xs_1"("v3"),"v1"),"main_xs_1"("v3"),"v2")
 "append#2"("Nil"(),"Cons"("v2","v4")) -> "Cons"("v2","v4")
 "append#2"("Cons"("v8","v6"),"Cons"("v2","v4")) -> "Cons"("v8","append#2"("v6","Cons"("v2","v4")))
 "ite_b#2"("True"(),"Pair"("v8","Cons"("v10","v12")),"Pair"("Cons"("v2","v4"),"v6")) -> "Pair"("v8","Cons"("v10","v12"))
 "ite_b#2"("False"(),"Pair"("v8","Cons"("v10","v12")),"Pair"("Cons"("v2","v4"),"v6")) -> "Pair"("Cons"("v2","v4"),"v6")
 "leqNat#2"("0"(),"v8") -> "True"()
 "leqNat#2"("S"("v4"),"S"("v2")) -> "leqNat#2"("v2","v4")
 "leqNat#2"("S"("v12"),"0"()) -> "False"()
 "main"("v1") -> "quicksort#2"("v1"))


MAYBE