Padding does not change the answers: 32 texts one by one versus one batch of 32.
  same labels: true, largest score difference 0.00e+00

Time to classify 32 texts, median of 5 runs after a warm-up, by batch size:
  batch size  1:   230 ms in total,   7.2 ms per text
  batch size  4:   204 ms in total,   6.4 ms per text
  batch size  8:   166 ms in total,   5.2 ms per text
  batch size 16:   142 ms in total,   4.4 ms per text
  batch size 32:   134 ms in total,   4.2 ms per text
