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


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

(STRATEGY
 INNERMOST)
(VAR
 "v3" "v5" "v7" "v2" "v10" "v4" "v12" "v8" "v14" "v0")
(DATATYPES
   "expr" = µX.< "Add"(X, X), "Nat"("nat"), "Sub"(X, X) >
   "nat" = µX.< "Zero", "Succ"(X) >)
(SIGNATURES
   "cond_eval_expr_1" :: ["nat" x "expr"] --> "nat"
   "cond_eval_expr_3" :: ["nat" x "nat"] --> "nat"
   "cond_eval_expr_2" :: ["nat" x "expr"] --> "nat"
   "eval#1" :: ["expr"] --> "nat"
   "main" :: ["expr"] --> "nat")
(RULES
 "cond_eval_expr_1"("Zero"(),"v3") -> "eval#1"("v3")
 "cond_eval_expr_1"("Succ"("v5"),"v3") -> "Succ"("eval#1"("Add"("Nat"("v5"),"v3")))
 "cond_eval_expr_3"("Zero"(),"v5") -> "Zero"()
 "cond_eval_expr_3"("Succ"("v7"),"v5") -> "eval#1"("Sub"("Nat"("v7"),"Nat"("v5")))
 "cond_eval_expr_2"("Zero"(),"v2") -> "eval#1"("v2")
 "cond_eval_expr_2"("Succ"("v10"),"v5") -> "cond_eval_expr_3"("eval#1"("v5"),"v10")
 "eval#1"("Nat"("v4")) -> "v4"
 "eval#1"("Add"("v10","v12")) -> "cond_eval_expr_1"("eval#1"("v10"),"v12")
 "eval#1"("Sub"("v8","v14")) -> "cond_eval_expr_2"("eval#1"("v14"),"v8")
 "main"("v0") -> "eval#1"("v0"))


MAYBE