15.57/18.45	unsat
