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


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

(STRATEGY
 INNERMOST)
(VAR
 "v18" "v32" "v56" "v16" "v11" "v224" "v3" "v2" "v1" "v4" "v47"
 "v39" "v8" "v6" "v10" "v12" "v0")
(DATATYPES
   "bool" = < "quicksort_gt_xxs_2"("nat"), "True", "False" >
   "either" = < "Left"("__ANY_TYPE__"), "Right"("__ANY_TYPE__") >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "walk_f#2" :: ["list" x "list"] --> "list"
   "cond_quicksort_gt_xxs_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"
   "leq#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "walk_f#2"("Nil"(),"v18") -> "v18"
 "walk_f#2"("Cons"("Left"("v32"),"v56"),"v16") -> "walk_f#2"("v56","Cons"("Left"("v32"),"v16"))
 "walk_f#2"("Cons"("Right"("v11"),"v56"),"v224") -> "walk_f#2"("v56","Cons"("Right"("quicksort#2"("v11")),"v224"))
 "cond_quicksort_gt_xxs_1"("Pair"("v3","v2"),"v1") -> "append#2"("quicksort#2"("v3"),"Cons"("v1","quicksort#2"("v2")))
 "quicksort#2"("Nil"()) -> "Nil"()
 "quicksort#2"("Cons"("v4","v2")) -> "cond_quicksort_gt_xxs_1"("partition#2"("quicksort_gt_xxs_2"("v4"),"v2"),"v4")
 "cond_partition_f_l_1"("Pair"("v47","v39"),"quicksort_gt_xxs_2"("v4"),"v2") -> "ite_b#2"("leq#2"("v4","v2"),"Pair"("v47","Cons"("v2","v39")),"Pair"("Cons"("v2","v47"),"v39"))
 "partition#2"("quicksort_gt_xxs_2"("v1"),"Nil"()) -> "Pair"("Nil"(),"Nil"())
 "partition#2"("quicksort_gt_xxs_2"("v3"),"Cons"("v2","v1")) -> "cond_partition_f_l_1"("partition#2"("quicksort_gt_xxs_2"("v3"),"v1"),"quicksort_gt_xxs_2"("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")
 "leq#2"("v4","0"()) -> "True"()
 "leq#2"("S"("v4"),"S"("v2")) -> "leq#2"("v4","v2")
 "leq#2"("0"(),"S"("v12")) -> "False"()
 "main"("v0") -> "walk_f#2"("v0","Nil"()))


MAYBE