232.12/232.52	unsat
