0.20/0.54	unsat
