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


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

(STRATEGY
 INNERMOST)
(VAR
 "v1" "v2" "v8" "v16" "v4" "v12")
(DATATYPES
   "expr" = µX.< "Nat"("nat"), "Add"(X, X), "Sub"(X, X) >
   "nat" = µX.< "Zero", "Succ"(X) >)
(SIGNATURES
   "eval#1" :: ["expr"] --> "nat"
   "sub#2" :: ["nat" x "nat"] --> "nat"
   "add#2" :: ["nat" x "nat"] --> "nat"
   "main" :: ["expr"] --> "nat")
(RULES
 "eval#1"("Nat"("v1")) -> "v1"
 "eval#1"("Add"("v2","v1")) -> "add#2"("eval#1"("v2"),"eval#1"("v1"))
 "eval#1"("Sub"("v2","v1")) -> "sub#2"("eval#1"("v2"),"eval#1"("v1"))
 "sub#2"("v8","Zero"()) -> "v8"
 "sub#2"("Zero"(),"Succ"("v16")) -> "Zero"()
 "sub#2"("Succ"("v4"),"Succ"("v2")) -> "sub#2"("v4","v2")
 "add#2"("Zero"(),"v8") -> "v8"
 "add#2"("Succ"("v4"),"v2") -> "Succ"("add#2"("v4","v2"))
 "main"("v12") -> "eval#1"("v12"))


MAYBE