817.16/822.65	unsat
