BEST_CASE(Omega(1),?) UNSAT "/tmp/SMTS21071-4" (line 1, column 6): The smt problem could not be solved (was unsat). Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v1" "v2" "v6" "v4" "v8" "v16") (DATATYPES "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) > "tree" = µX.< "Leaf"("__ANY_TYPE__"), "Node"(X, X) >) (SIGNATURES "revApp#2" :: ["list" x "list"] --> "list" "dfsAcc#3" :: ["tree" x "list"] --> "list" "main" :: ["tree"] --> "list") (RULES "revApp#2"("Nil"(),"Cons"("v1","v2")) -> "Cons"("v1","v2") "revApp#2"("Cons"("v6","v4"),"v2") -> "revApp#2"("v4","Cons"("v6","v2")) "dfsAcc#3"("Leaf"("v8"),"v16") -> "Cons"("v8","v16") "dfsAcc#3"("Node"("v6","v4"),"v2") -> "dfsAcc#3"("v4","dfsAcc#3"("v6","v2")) "main"("v1") -> "revApp#2"("dfsAcc#3"("v1","Nil"()),"Nil"())) BEST_CASE(Omega(1),?)