Initially, i thought
to be the shortest AWK code but then found that it stops "after" printing 42.
I wonder what the 9-byte accepted code looks like...
EDIT: Turns out the input file is already known and the number preceding 42 is 19. So, here goes...
or even better with 5-byte code..