5.34/5.57	unsat
