BEST_CASE(Omega(1),?)
UNSAT
"/tmp/SMTS3621-1" (line 1, column 6):
The smt problem could not be solved (was unsat).


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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v2" "v8" "v6" "v10" "v48" "v56" "v20" "v12" "v16" "v1")
(DATATYPES
   "bool" = < "bot[0]", "bot[1]", "bot[2]", "False", "True" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >
   "tree" = < "Leaf"("list"), "Node"("list", "treelist") >
   "treelist" = µX.< "ConsTree"("__ANY_TYPE__", X), "NilTree" >)
(SIGNATURES
   "lookup#2" :: ["nat" x "tree"] --> "bool"
   "anyEq#2" :: ["nat" x "list"] --> "bool"
   "ite2#3" :: ["bool" x "bool" x "bool"] --> "bool"
   "ite#3" :: ["bool" x "bool"] --> "bool"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["nat" x "tree"] --> "bool")
(RULES
 "lookup#2"("v4","Leaf"("v2")) -> "anyEq#2"("v4","v2")
 "lookup#2"("v4","Node"("Nil"(),"ConsTree"("v2","NilTree"()))) -> "lookup#2"("v4","v2")
 "lookup#2"("v8","Node"("Nil"(),"ConsTree"("v6","ConsTree"("v4","v2")))) -> "bot[0]"()
 "lookup#2"("v2","Node"("Nil"(),"NilTree"())) -> "bot[1]"()
 "lookup#2"("v10","Node"("Cons"("v8","v6"),"ConsTree"("v4","v2"))) -> "ite2#3"("leqNat#2"("v10","v8"),"lookup#2"("v10","v4"),"lookup#2"("v10","Node"("v6","v2")))
 "lookup#2"("v6","Node"("Cons"("v4","v2"),"NilTree"())) -> "bot[2]"()
 "anyEq#2"("v2","Nil"()) -> "False"()
 "anyEq#2"("v6","Cons"("v4","v2")) -> "ite#3"("eqNat#2"("v6","v4"),"anyEq#2"("v6","v2"))
 "ite2#3"("True"(),"v48","v56") -> "v48"
 "ite2#3"("False"(),"v48","v56") -> "v56"
 "ite#3"("True"(),"v4") -> "True"()
 "ite#3"("False"(),"v4") -> "v4"
 "eqNat#2"("0"(),"0"()) -> "True"()
 "eqNat#2"("S"("v20"),"0"()) -> "False"()
 "eqNat#2"("S"("v4"),"S"("v2")) -> "eqNat#2"("v4","v2")
 "eqNat#2"("0"(),"S"("v20")) -> "False"()
 "leqNat#2"("0"(),"v12") -> "True"()
 "leqNat#2"("S"("v4"),"S"("v2")) -> "leqNat#2"("v2","v4")
 "leqNat#2"("S"("v16"),"0"()) -> "False"()
 "main"("v2","v1") -> "lookup#2"("v2","v1"))


BEST_CASE(Omega(1),?)