787.23/790.92	unsat
