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


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

(STRATEGY
 INNERMOST)
(VAR
 "v1" "v2" "v19" "v11" "v4" "v3" "v6" "v8" "v20" "v24" "v10" "v12"
 "v16")
(DATATYPES
   "bool" = < "True", "False", "compare_list_l1"("list") >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "compare_list_l1#1" :: ["list" x "list"] --> "bool"
   "cond_quicksort_gt_xyz_1" :: ["pair" x "list"] --> "list"
   "quicksort#2" :: ["list"] --> "list"
   "cond_partition_f_l_1" :: ["pair" x "bool" x "list"] --> "pair"
   "partition#2" :: ["bool" x "list"] --> "pair"
   "append#2" :: ["list" x "list"] --> "list"
   "ite3_b#2" :: ["bool" x "bool" x "bool"] --> "bool"
   "ite_b#2" :: ["bool" x "pair" x "pair"] --> "pair"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "compare_list_l1#1"("Nil"(),"v1") -> "True"()
 "compare_list_l1#1"("Cons"("v2","v1"),"Nil"()) -> "False"()
 "compare_list_l1#1"("Cons"("v19","v2"),"Cons"("v11","v4")) -> "ite3_b#2"("eqNat#2"("v19","v11"),"compare_list_l1#1"("v2","v4"),"leqNat#2"("v19","v11"))
 "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"("compare_list_l1"("v4"),"v6"),"v4")
 "cond_partition_f_l_1"("Pair"("v4","v3"),"compare_list_l1"("v2"),"v1") -> "ite_b#2"("compare_list_l1#1"("v2","v1"),"Pair"("v4","Cons"("v1","v3")),"Pair"("Cons"("v1","v4"),"v3"))
 "partition#2"("compare_list_l1"("v1"),"Nil"()) -> "Pair"("Nil"(),"Nil"())
 "partition#2"("compare_list_l1"("v3"),"Cons"("v2","v1")) -> "cond_partition_f_l_1"("partition#2"("compare_list_l1"("v3"),"v1"),"compare_list_l1"("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")))
 "ite3_b#2"("True"(),"v20","v24") -> "v20"
 "ite3_b#2"("False"(),"v20","v24") -> "v24"
 "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")
 "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") -> "quicksort#2"("v1"))


MAYBE