607.51/609.66	unsat
