#include "stdio.h"

int main(void) {
    printf("hello printf: %d\n", 123);
    return 0;
}