printf"%d000",<>/<>/1e3