16.52/16.54	unsat
