char scratchbuffer[1000];

#include <String.h>
#include <stdio.h>

void debug(char* msg)
// {fprintf(stderr,msg); fprintf(stderr,"\n"); fflush(stderr);}
{}