603.14/607.82	unsat
