5.30/7.54	unsat
