Comment by schoen

I didn't think we were allowed to even potentially change the order, so I used

  awk '{if (!c[$0]) { print }; c[$0] = 1 }'