1022.21/1023.84	unsat
