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


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

(STRATEGY
 INNERMOST)
(VAR
 "v2" "v5" "v3" "v4" "v1" "v7" "v9")
(DATATYPES
   "list" = µX.< "cons_x"("__ANY_TYPE__"), "comp_f_g"(X, X), "Cons"("__ANY_TYPE__", X), "Nil" >
   "tree" = µX.< "Leaf"("__ANY_TYPE__"), "Node"(X, X) >)
(SIGNATURES
   "walk#1" :: ["tree"] --> "list"
   "comp_f_g#1" :: ["list" x "list" x "list"] --> "list"
   "main" :: ["tree"] --> "list")
(RULES
 "walk#1"("Leaf"("v2")) -> "cons_x"("v2")
 "walk#1"("Node"("v5","v3")) -> "comp_f_g"("walk#1"("v5"),"walk#1"("v3"))
 "comp_f_g#1"("comp_f_g"("v4","v5"),"comp_f_g"("v2","v3"),"v1") -> "comp_f_g#1"("v4","v5","comp_f_g#1"("v2","v3","v1"))
 "comp_f_g#1"("comp_f_g"("v7","v9"),"cons_x"("v2"),"v4") -> "comp_f_g#1"("v7","v9","Cons"("v2","v4"))
 "comp_f_g#1"("cons_x"("v2"),"comp_f_g"("v5","v7"),"v3") -> "Cons"("v2","comp_f_g#1"("v5","v7","v3"))
 "comp_f_g#1"("cons_x"("v5"),"cons_x"("v2"),"v4") -> "Cons"("v5","Cons"("v2","v4"))
 "main"("Leaf"("v4")) -> "Cons"("v4","Nil"())
 "main"("Node"("v9","v5")) -> "comp_f_g#1"("walk#1"("v9"),"walk#1"("v5"),"Nil"()))


BEST_CASE(Omega(1),?)