812.52/814.58	unsat
