1001.99/1007.31	unsat
