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


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

(STRATEGY
 INNERMOST)
(VAR
 "v9" "v10" "v11" "v2" "v1" "v4" "v3" "v8" "v16" "v20")
(DATATYPES
   "exp" = µX.< "Eadd"(X, X), "Emult"(X, X), "Ediv"(X, X), "Econst"("nat") >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >
   "triple" = < "Triple"("__ANY_TYPE__", "__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "cond_eval_e_1" :: ["triple"] --> "nat"
   "eval#1" :: ["exp"] --> "nat"
   "mult#2" :: ["nat" x "nat"] --> "nat"
   "cond_div_mod_n_m_2" :: ["triple" x "nat"] --> "triple"
   "cond_div_mod_n_m" :: ["pair" x "nat"] --> "triple"
   "div_mod#2" :: ["nat" x "nat"] --> "triple"
   "plus#2" :: ["nat" x "nat"] --> "nat"
   "minus'#2" :: ["nat" x "nat"] --> "nat"
   "main" :: ["exp"] --> "nat")
(RULES
 "cond_eval_e_1"("Triple"("v9","v10","v11")) -> "v9"
 "eval#1"("Eadd"("v2","v1")) -> "plus#2"("eval#1"("v2"),"eval#1"("v1"))
 "eval#1"("Emult"("v2","v1")) -> "mult#2"("eval#1"("v2"),"eval#1"("v1"))
 "eval#1"("Ediv"("v2","v1")) -> "cond_eval_e_1"("div_mod#2"("eval#1"("v2"),"eval#1"("v1")))
 "eval#1"("Econst"("v1")) -> "v1"
 "mult#2"("0"(),"v2") -> "0"()
 "mult#2"("S"("v4"),"v2") -> "S"("plus#2"("mult#2"("v4","v2"),"v2"))
 "cond_div_mod_n_m_2"("Triple"("v4","v3","v2"),"v1") -> "Triple"("plus#2"("S"("0"()),"v4"),"v3","v1")
 "cond_div_mod_n_m"("Pair"("0"(),"v2"),"v1") -> "Triple"("0"(),"v1","v2")
 "cond_div_mod_n_m"("Pair"("S"("v3"),"v2"),"v1") -> "cond_div_mod_n_m_2"("div_mod#2"("S"("v3"),"v2"),"v2")
 "div_mod#2"("v8","v4") -> "cond_div_mod_n_m"("Pair"("minus'#2"("v8","v4"),"v4"),"v8")
 "plus#2"("v8","0"()) -> "v8"
 "plus#2"("v4","S"("v2")) -> "S"("plus#2"("v4","v2"))
 "minus'#2"("0"(),"v16") -> "0"()
 "minus'#2"("S"("v20"),"0"()) -> "S"("v20")
 "minus'#2"("S"("v4"),"S"("v2")) -> "minus'#2"("v4","v2")
 "main"("v20") -> "eval#1"("v20"))


MAYBE