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


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

(STRATEGY
 INNERMOST)
(VAR
 "v11" "v2" "v40" "v23" "v8" "v4" "v6" "v16" "v20" "v12" "v1")
(DATATYPES
   "int" = µX.< "0", "S"(X), "M"(X) >
   "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil" >)
(SIGNATURES
   "cond_scanr_f_z_xs_1" :: ["list" x "int"] --> "list"
   "scanr#3" :: ["list"] --> "list"
   "foldl#3" :: ["int" x "list"] --> "int"
   "minus#2" :: ["int" x "int"] --> "int"
   "plus#2" :: ["int" x "int"] --> "int"
   "max#2" :: ["int" x "int"] --> "int"
   "main" :: ["list"] --> "int")
(RULES
 "cond_scanr_f_z_xs_1"("Cons"("0"(),"v11"),"0"()) -> "Cons"("0"(),"Cons"("0"(),"v11"))
 "cond_scanr_f_z_xs_1"("Cons"("S"("v2"),"v11"),"0"()) -> "Cons"("S"("v2"),"Cons"("S"("v2"),"v11"))
 "cond_scanr_f_z_xs_1"("Cons"("0"(),"v11"),"M"("v2")) -> "Cons"("0"(),"Cons"("0"(),"v11"))
 "cond_scanr_f_z_xs_1"("Cons"("S"("v40"),"v23"),"M"("0"())) -> "Cons"("S"("v40"),"Cons"("S"("v40"),"v23"))
 "cond_scanr_f_z_xs_1"("Cons"("S"("v8"),"v23"),"M"("S"("v4"))) -> "Cons"("minus#2"("v8","v4"),"Cons"("S"("v8"),"v23"))
 "cond_scanr_f_z_xs_1"("Cons"("0"(),"v11"),"S"("v2")) -> "Cons"("S"("v2"),"Cons"("0"(),"v11"))
 "cond_scanr_f_z_xs_1"("Cons"("S"("v2"),"v11"),"S"("v4")) -> "Cons"("plus#2"("S"("v4"),"S"("v2")),"Cons"("S"("v2"),"v11"))
 "scanr#3"("Nil"()) -> "Cons"("0"(),"Nil"())
 "scanr#3"("Cons"("v4","v2")) -> "cond_scanr_f_z_xs_1"("scanr#3"("v2"),"v4")
 "foldl#3"("v2","Nil"()) -> "v2"
 "foldl#3"("v6","Cons"("v4","v2")) -> "foldl#3"("max#2"("v6","v4"),"v2")
 "minus#2"("0"(),"v16") -> "0"()
 "minus#2"("S"("v20"),"0"()) -> "S"("v20")
 "minus#2"("S"("v4"),"S"("v2")) -> "minus#2"("v4","v2")
 "plus#2"("0"(),"S"("v2")) -> "S"("v2")
 "plus#2"("S"("v4"),"S"("v2")) -> "S"("plus#2"("v4","S"("v2")))
 "max#2"("0"(),"v8") -> "v8"
 "max#2"("S"("v12"),"0"()) -> "S"("v12")
 "max#2"("S"("v4"),"S"("v2")) -> "S"("max#2"("v4","v2"))
 "main"("v1") -> "foldl#3"("0"(),"scanr#3"("v1")))


MAYBE