342.02/342.76	unsat
