5.30/5.56	unsat
