21.55/25.57	unsat
