1027.98/1032.67	unsat
