7.20/7.26	unsat
