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


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

(STRATEGY
 INNERMOST)
(VAR
 "v3" "v12" "v14" "v1" "v4" "v2" "v5" "v8")
(DATATYPES
   "Unit" = < "bot[0]", "bot[3]", "bot[4]" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "llist" = µX.< "ConsL"("__ANY_TYPE__", X), "fibs", "fibs_2", "zipwith_l_f_xs_ys"(X, X) >
   "nat" = µX.< "S"(X), "0" >)
(SIGNATURES
   "fibs_2#1" :: ["Unit"] --> "llist"
   "cond_take_l_n_xs" :: ["llist" x "nat"] --> "list"
   "plus#2" :: ["nat" x "nat"] --> "nat"
   "cond_zipwith_l_f_xs_ys_1" :: ["llist" x "nat" x "llist"] --> "llist"
   "cond_zipwith_l_f_xs_ys" :: ["llist" x "llist"] --> "llist"
   "zipwith_l_f_xs_ys#1" :: ["llist" x "llist" x "Unit"] --> "llist"
   "zipwith_l#3" :: ["llist" x "llist"] --> "llist"
   "main" :: ["nat"] --> "list")
(RULES
 "fibs_2#1"("v3") -> "ConsL"("S"("0"()),"zipwith_l#3"("fibs"(),"fibs_2"()))
 "cond_take_l_n_xs"("ConsL"("v12","v14"),"0"()) -> "Nil"()
 "cond_take_l_n_xs"("ConsL"("0"(),"fibs_2"()),"S"("v1")) -> "Cons"("0"(),"cond_take_l_n_xs"("fibs_2#1"("bot[0]"()),"v1"))
 "cond_take_l_n_xs"("ConsL"("v4","zipwith_l_f_xs_ys"("v3","v2")),"S"("v1")) -> "Cons"("v4","cond_take_l_n_xs"("zipwith_l_f_xs_ys#1"("v3","v2","bot[0]"()),"v1"))
 "plus#2"("0"(),"v12") -> "v12"
 "plus#2"("S"("v4"),"v2") -> "S"("plus#2"("v4","v2"))
 "cond_zipwith_l_f_xs_ys_1"("ConsL"("v4","v3"),"v2","v1") -> "ConsL"("plus#2"("v2","v4"),"zipwith_l#3"("v1","v3"))
 "cond_zipwith_l_f_xs_ys"("ConsL"("v4","v3"),"zipwith_l_f_xs_ys"("v2","v1")) -> "cond_zipwith_l_f_xs_ys_1"("zipwith_l_f_xs_ys#1"("v2","v1","bot[3]"()),"v4","v3")
 "cond_zipwith_l_f_xs_ys"("ConsL"("v2","v1"),"fibs_2"()) -> "cond_zipwith_l_f_xs_ys_1"("fibs_2#1"("bot[3]"()),"v2","v1")
 "zipwith_l_f_xs_ys#1"("fibs"(),"v5","v3") -> "cond_zipwith_l_f_xs_ys"("ConsL"("0"(),"fibs_2"()),"v5")
 "zipwith_l_f_xs_ys#1"("fibs_2"(),"v2","v1") -> "cond_zipwith_l_f_xs_ys"("fibs_2#1"("bot[4]"()),"v2")
 "zipwith_l_f_xs_ys#1"("zipwith_l_f_xs_ys"("v4","v3"),"v2","v1") -> "cond_zipwith_l_f_xs_ys"("zipwith_l_f_xs_ys#1"("v4","v3","bot[4]"()),"v2")
 "zipwith_l#3"("v8","v4") -> "zipwith_l_f_xs_ys"("v8","v4")
 "main"("v12") -> "cond_take_l_n_xs"("ConsL"("0"(),"fibs_2"()),"v12"))


MAYBE