/*
 * 
 * author: nutz
 * date: 2015-04-29
 */

#include<stddef.h>
#include<stdio.h>

/*@ requires \false;
  @ ensures \true;
  @*/
int main() {
  return 0;
}