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


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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v6" "v3" "v2" "v1" "v44" "v40" "v8" "v32" "v28" "v48" "v20")
(DATATYPES
   "bool" = < "True", "False", "bot[0]#1" >
   "bool_expr" = µX.< "Var"("nat"), "Not"(X), "And"(X, X), "Or"(X, X) >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "table_make#3" :: ["list" x "list" x "bool_expr"] --> "list"
   "eval#2" :: ["list" x "bool_expr"] --> "bool"
   "concat#2" :: ["list" x "list"] --> "list"
   "aux#2" :: ["list" x "list"] --> "list"
   "assoc#2" :: ["nat" x "list"] --> "bool"
   "lor#2" :: ["bool" x "bool"] --> "bool"
   "land#2" :: ["bool" x "bool"] --> "bool"
   "lnot#1" :: ["bool"] --> "bool"
   "ite#3" :: ["bool" x "bool" x "bool"] --> "bool"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["bool_expr" x "list" x "list"] --> "list")
(RULES
 "table_make#3"("v4","Nil"(),"v6") -> "Cons"("Pair"("aux#2"("Nil"(),"v4"),"eval#2"("v4","v6")),"Nil"())
 "table_make#3"("v4","Cons"("v3","v2"),"v1") -> "concat#2"("table_make#3"("Cons"("Pair"("v3","True"()),"v4"),"v2","v1"),"table_make#3"("Cons"("Pair"("v3","False"()),"v4"),"v2","v1"))
 "eval#2"("v4","Var"("v2")) -> "assoc#2"("v2","v4")
 "eval#2"("v4","Not"("v2")) -> "lnot#1"("eval#2"("v4","v2"))
 "eval#2"("v6","And"("v4","v2")) -> "land#2"("eval#2"("v6","v4"),"eval#2"("v6","v2"))
 "eval#2"("v6","Or"("v4","v2")) -> "lor#2"("eval#2"("v6","v4"),"eval#2"("v6","v2"))
 "concat#2"("Nil"(),"v44") -> "v44"
 "concat#2"("Cons"("v6","v4"),"v2") -> "Cons"("v6","concat#2"("v4","v2"))
 "aux#2"("v40","Nil"()) -> "v40"
 "aux#2"("v6","Cons"("v4","v2")) -> "aux#2"("Cons"("v4","v6"),"v2")
 "assoc#2"("v2","Nil"()) -> "bot[0]#1"()
 "assoc#2"("v8","Cons"("Pair"("v6","v4"),"v2")) -> "ite#3"("eqNat#2"("v6","v8"),"v4","assoc#2"("v8","v2"))
 "lor#2"("True"(),"v32") -> "True"()
 "lor#2"("False"(),"v32") -> "v32"
 "land#2"("False"(),"v28") -> "False"()
 "land#2"("True"(),"v28") -> "v28"
 "lnot#1"("True"()) -> "False"()
 "lnot#1"("False"()) -> "True"()
 "ite#3"("True"(),"v40","v48") -> "v40"
 "ite#3"("False"(),"v40","v48") -> "v48"
 "eqNat#2"("0"(),"0"()) -> "True"()
 "eqNat#2"("S"("v20"),"0"()) -> "False"()
 "eqNat#2"("S"("v4"),"S"("v2")) -> "eqNat#2"("v4","v2")
 "eqNat#2"("0"(),"S"("v20")) -> "False"()
 "main"("v3","v2","v1") -> "table_make#3"("v2","v1","v3"))


MAYBE