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


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

(STRATEGY
 INNERMOST)
(VAR
 "v12" "v13" "v14" "v11" "v24" "v2" "v1" "v4" "v3" "v8" "v16" "v28")
(DATATYPES
   "bool" = < "True", "False" >
   "exp" = µX.< "Eadd"(X, X), "Emult"(X, X), "Ediv"(X, X), "Econst"("nat") >
   "nat" = µX.< "0", "ite_b#2"("bool", X), "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >
   "triple" = < "Triple"("__ANY_TYPE__", "__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "cond_eval_e_1" :: ["triple"] --> "nat"
   "eval_e_6#1" :: ["exp" x "nat"] --> "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"("v12","v13","v14")) -> "v12"
 "eval_e_6#1"("v11","0"()) -> "ite_b#2"("True"(),"cond_eval_e_1"("div_mod#2"("eval#1"("v11"),"0"())))
 "eval_e_6#1"("v11","S"("v24")) -> "ite_b#2"("False"(),"cond_eval_e_1"("div_mod#2"("eval#1"("v11"),"S"("v24"))))
 "eval_e_6#1"("v11","S"("0"())) -> "ite_b#2"("True"(),"cond_eval_e_1"("div_mod#2"("eval#1"("v11"),"S"("0"()))))
 "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")) -> "eval_e_6#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"("v16","0"()) -> "v16"
 "plus#2"("v4","S"("v2")) -> "S"("plus#2"("v4","v2"))
 "minus'#2"("0"(),"v24") -> "0"()
 "minus'#2"("S"("v28"),"0"()) -> "S"("v28")
 "minus'#2"("S"("v4"),"S"("v2")) -> "minus'#2"("v4","v2")
 "main"("v28") -> "eval#1"("v28"))


MAYBE