5.30/5.42	unsat
