563.12/563.42	unsat
