MAYBE
UNSAT
"/tmp/SMTS32139-3" (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" "v39" "v35" "v18" "v14" "v10" "v8" "v24"
 "v28" "v7" "v5" "v12" "v20" "v16")
(DATATYPES
   "bool" = < "True", "False", "compare_a"("pair") >
   "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil" >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "not#1" :: ["bool"] --> "bool"
   "cond_quicksort_gt_xyz_1" :: ["pair" x "pair"] --> "list"
   "quicksort#2" :: ["list"] --> "list"
   "cond_partition_f_l_1" :: ["pair" x "bool" x "pair"] --> "pair"
   "partition#2" :: ["bool" x "list"] --> "pair"
   "append#2" :: ["list" x "list"] --> "list"
   "ite2_b#2" :: ["bool" x "bool" x "bool"] --> "bool"
   "ite_b#2" :: ["bool" x "pair" x "pair"] --> "pair"
   "ltNat#2" :: ["nat" x "nat"] --> "bool"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "not#1"("True"()) -> "False"()
 "not#1"("False"()) -> "True"()
 "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_a"("v4"),"v6"),"v4")
 "cond_partition_f_l_1"("Pair"("v39","v35"),"compare_a"("Pair"("v18","v14")),"Pair"("v10","v6")) -> "ite_b#2"("ite2_b#2"("not#1"("eqNat#2"("v18","v10")),"ltNat#2"("v18","v10"),"leqNat#2"("v14","v6")),"Pair"("v39","Cons"("Pair"("v10","v6"),"v35")),"Pair"("Cons"("Pair"("v10","v6"),"v39"),"v35"))
 "partition#2"("compare_a"("v1"),"Nil"()) -> "Pair"("Nil"(),"Nil"())
 "partition#2"("compare_a"("v3"),"Cons"("v2","v1")) -> "cond_partition_f_l_1"("partition#2"("compare_a"("v3"),"v1"),"compare_a"("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")))
 "ite2_b#2"("True"(),"v24","v28") -> "v24"
 "ite2_b#2"("False"(),"v24","v28") -> "v28"
 "ite_b#2"("True"(),"Pair"("v8","Cons"("Pair"("v6","v7"),"v5")),"Pair"("Cons"("Pair"("v3","v4"),"v2"),"v1")) -> "Pair"("v8","Cons"("Pair"("v6","v7"),"v5"))
 "ite_b#2"("False"(),"Pair"("v8","Cons"("Pair"("v6","v7"),"v5")),"Pair"("Cons"("Pair"("v3","v4"),"v2"),"v1")) -> "Pair"("Cons"("Pair"("v3","v4"),"v2"),"v1")
 "ltNat#2"("v12","0"()) -> "False"()
 "ltNat#2"("0"(),"S"("v20")) -> "True"()
 "ltNat#2"("S"("v4"),"S"("v2")) -> "ltNat#2"("v4","v2")
 "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