BEST_CASE(Omega(1),?)
UNSAT
"/tmp/SMTS9113-3" (line 1, column 8):
The smt solver ran in a timeout.