#include <stdio.h>
void main() {
   printf("(\"%c\", \"%c\", \"%c\", \"%c\")\n", '\001', '\177', '\200', '\367');
}
