MAYBE UNSAT "/tmp/SMTS23052-9" (line 1, column 6): The smt problem could not be solved (was unsat). Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v2" "v5" "v4" "v1") (DATATYPES "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) > "nat" = µX.< "0", "S"(X) >) (SIGNATURES "map#2" :: ["list"] --> "list" "mult#2" :: ["nat" x "nat"] --> "nat" "plus#2" :: ["nat" x "nat"] --> "nat" "main" :: ["list"] --> "list") (RULES "map#2"("Nil"()) -> "Nil"() "map#2"("Cons"("v2","v5")) -> "Cons"("mult#2"("v2","mult#2"("v2","v2")),"map#2"("v5")) "mult#2"("0"(),"v2") -> "0"() "mult#2"("S"("v4"),"v2") -> "S"("plus#2"("mult#2"("v4","v2"),"v2")) "plus#2"("v4","0"()) -> "v4" "plus#2"("v4","S"("v2")) -> "S"("plus#2"("v4","v2")) "main"("v1") -> "map#2"("v1")) MAYBE