```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
// Suppose there are h holes and p pigeons to put in the holes. Every
// pigeon should be in a hole and no more than one pigeon is in one
// hole. Consider the case h=N and p=N+1. In [GrZa03], it is proved
// that BDDs have lower bound 1.63^n for pigeonhole n, while there
// are polynomial resolution proofs.
//
// **************************************************************************

macro N=5;

module PigeonHole( [N+1][N]bool p_in_h) {
nothing;
} satisfies {
s: assert
not(
// -- all pigeons are in a hole -------------
( forall(i=0..N) exists(j=0..N-1) p_in_h[i][j] ) &
// -- in every hole, there is a pigeon -------------
( forall(j=0..N-1) exists(i=0..N) p_in_h[i][j] ) &
// -- if pigeon i is in hole j, then no other pigeon
// -- is in hole j
( forall(i=0..N) forall(j=0..N-1)
(p_in_h[i][j] -> forall(k=0..N-1) ((k!=i) -> !p_in_h[k][j])) )
);
}
```