872.86/872.90	unsat
