5.17/5.26	unsat
