924.51/927.34	unsat
