282.12/282.90	unsat
