392.02/392.89	unsat
