module pigeons sig Pigeon { where: Hole } sig Hole {} pred principle[] { all disj p1, p2: Pigeon | p1.where != p2.where } run principle for exactly 20 Pigeon, exactly 19 Hole