872.43/878.10	unsat
