c pigeon-10: placing 11 pigeons into 10 holes
c 
c File generated by 'pigeonhole', (c) Tjark Weber
c 
c The SAT encoding of this problem is very straightforward.  For each pigeon i
c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
c is placed in hole j.  Then we have n+1 clauses which say that a pigeon has
c to be placed in some hole.  Then for each hole we have a set of clauses
c ensuring that only one single pigeon is placed into that hole.
c 
c This encoding leads to a total of (n+1) * n propositional variables and
c (n+1) + n * (n * (n+1) / 2) clauses.
c 
c The resulting SAT problem is unsatisfiable.
c 
p cnf 110 561
1 2 3 4 5 6 7 8 9 10 0
11 12 13 14 15 16 17 18 19 20 0
21 22 23 24 25 26 27 28 29 30 0
31 32 33 34 35 36 37 38 39 40 0
41 42 43 44 45 46 47 48 49 50 0
51 52 53 54 55 56 57 58 59 60 0
61 62 63 64 65 66 67 68 69 70 0
71 72 73 74 75 76 77 78 79 80 0
81 82 83 84 85 86 87 88 89 90 0
91 92 93 94 95 96 97 98 99 100 0
101 102 103 104 105 106 107 108 109 110 0
-1 -11 0
-1 -21 0
-1 -31 0
-1 -41 0
-1 -51 0
-1 -61 0
-1 -71 0
-1 -81 0
-1 -91 0
-1 -101 0
-11 -21 0
-11 -31 0
-11 -41 0
-11 -51 0
-11 -61 0
-11 -71 0
-11 -81 0
-11 -91 0
-11 -101 0
-21 -31 0
-21 -41 0
-21 -51 0
-21 -61 0
-21 -71 0
-21 -81 0
-21 -91 0
-21 -101 0
-31 -41 0
-31 -51 0
-31 -61 0
-31 -71 0
-31 -81 0
-31 -91 0
-31 -101 0
-41 -51 0
-41 -61 0
-41 -71 0
-41 -81 0
-41 -91 0
-41 -101 0
-51 -61 0
-51 -71 0
-51 -81 0
-51 -91 0
-51 -101 0
-61 -71 0
-61 -81 0
-61 -91 0
-61 -101 0
-71 -81 0
-71 -91 0
-71 -101 0
-81 -91 0
-81 -101 0
-91 -101 0
-2 -12 0
-2 -22 0
-2 -32 0
-2 -42 0
-2 -52 0
-2 -62 0
-2 -72 0
-2 -82 0
-2 -92 0
-2 -102 0
-12 -22 0
-12 -32 0
-12 -42 0
-12 -52 0
-12 -62 0
-12 -72 0
-12 -82 0
-12 -92 0
-12 -102 0
-22 -32 0
-22 -42 0
-22 -52 0
-22 -62 0
-22 -72 0
-22 -82 0
-22 -92 0
-22 -102 0
-32 -42 0
-32 -52 0
-32 -62 0
-32 -72 0
-32 -82 0
-32 -92 0
-32 -102 0
-42 -52 0
-42 -62 0
-42 -72 0
-42 -82 0
-42 -92 0
-42 -102 0
-52 -62 0
-52 -72 0
-52 -82 0
-52 -92 0
-52 -102 0
-62 -72 0
-62 -82 0
-62 -92 0
-62 -102 0
-72 -82 0
-72 -92 0
-72 -102 0
-82 -92 0
-82 -102 0
-92 -102 0
-3 -13 0
-3 -23 0
-3 -33 0
-3 -43 0
-3 -53 0
-3 -63 0
-3 -73 0
-3 -83 0
-3 -93 0
-3 -103 0
-13 -23 0
-13 -33 0
-13 -43 0
-13 -53 0
-13 -63 0
-13 -73 0
-13 -83 0
-13 -93 0
-13 -103 0
-23 -33 0
-23 -43 0
-23 -53 0
-23 -63 0
-23 -73 0
-23 -83 0
-23 -93 0
-23 -103 0
-33 -43 0
-33 -53 0
-33 -63 0
-33 -73 0
-33 -83 0
-33 -93 0
-33 -103 0
-43 -53 0
-43 -63 0
-43 -73 0
-43 -83 0
-43 -93 0
-43 -103 0
-53 -63 0
-53 -73 0
-53 -83 0
-53 -93 0
-53 -103 0
-63 -73 0
-63 -83 0
-63 -93 0
-63 -103 0
-73 -83 0
-73 -93 0
-73 -103 0
-83 -93 0
-83 -103 0
-93 -103 0
-4 -14 0
-4 -24 0
-4 -34 0
-4 -44 0
-4 -54 0
-4 -64 0
-4 -74 0
-4 -84 0
-4 -94 0
-4 -104 0
-14 -24 0
-14 -34 0
-14 -44 0
-14 -54 0
-14 -64 0
-14 -74 0
-14 -84 0
-14 -94 0
-14 -104 0
-24 -34 0
-24 -44 0
-24 -54 0
-24 -64 0
-24 -74 0
-24 -84 0
-24 -94 0
-24 -104 0
-34 -44 0
-34 -54 0
-34 -64 0
-34 -74 0
-34 -84 0
-34 -94 0
-34 -104 0
-44 -54 0
-44 -64 0
-44 -74 0
-44 -84 0
-44 -94 0
-44 -104 0
-54 -64 0
-54 -74 0
-54 -84 0
-54 -94 0
-54 -104 0
-64 -74 0
-64 -84 0
-64 -94 0
-64 -104 0
-74 -84 0
-74 -94 0
-74 -104 0
-84 -94 0
-84 -104 0
-94 -104 0
-5 -15 0
-5 -25 0
-5 -35 0
-5 -45 0
-5 -55 0
-5 -65 0
-5 -75 0
-5 -85 0
-5 -95 0
-5 -105 0
-15 -25 0
-15 -35 0
-15 -45 0
-15 -55 0
-15 -65 0
-15 -75 0
-15 -85 0
-15 -95 0
-15 -105 0
-25 -35 0
-25 -45 0
-25 -55 0
-25 -65 0
-25 -75 0
-25 -85 0
-25 -95 0
-25 -105 0
-35 -45 0
-35 -55 0
-35 -65 0
-35 -75 0
-35 -85 0
-35 -95 0
-35 -105 0
-45 -55 0
-45 -65 0
-45 -75 0
-45 -85 0
-45 -95 0
-45 -105 0
-55 -65 0
-55 -75 0
-55 -85 0
-55 -95 0
-55 -105 0
-65 -75 0
-65 -85 0
-65 -95 0
-65 -105 0
-75 -85 0
-75 -95 0
-75 -105 0
-85 -95 0
-85 -105 0
-95 -105 0
-6 -16 0
-6 -26 0
-6 -36 0
-6 -46 0
-6 -56 0
-6 -66 0
-6 -76 0
-6 -86 0
-6 -96 0
-6 -106 0
-16 -26 0
-16 -36 0
-16 -46 0
-16 -56 0
-16 -66 0
-16 -76 0
-16 -86 0
-16 -96 0
-16 -106 0
-26 -36 0
-26 -46 0
-26 -56 0
-26 -66 0
-26 -76 0
-26 -86 0
-26 -96 0
-26 -106 0
-36 -46 0
-36 -56 0
-36 -66 0
-36 -76 0
-36 -86 0
-36 -96 0
-36 -106 0
-46 -56 0
-46 -66 0
-46 -76 0
-46 -86 0
-46 -96 0
-46 -106 0
-56 -66 0
-56 -76 0
-56 -86 0
-56 -96 0
-56 -106 0
-66 -76 0
-66 -86 0
-66 -96 0
-66 -106 0
-76 -86 0
-76 -96 0
-76 -106 0
-86 -96 0
-86 -106 0
-96 -106 0
-7 -17 0
-7 -27 0
-7 -37 0
-7 -47 0
-7 -57 0
-7 -67 0
-7 -77 0
-7 -87 0
-7 -97 0
-7 -107 0
-17 -27 0
-17 -37 0
-17 -47 0
-17 -57 0
-17 -67 0
-17 -77 0
-17 -87 0
-17 -97 0
-17 -107 0
-27 -37 0
-27 -47 0
-27 -57 0
-27 -67 0
-27 -77 0
-27 -87 0
-27 -97 0
-27 -107 0
-37 -47 0
-37 -57 0
-37 -67 0
-37 -77 0
-37 -87 0
-37 -97 0
-37 -107 0
-47 -57 0
-47 -67 0
-47 -77 0
-47 -87 0
-47 -97 0
-47 -107 0
-57 -67 0
-57 -77 0
-57 -87 0
-57 -97 0
-57 -107 0
-67 -77 0
-67 -87 0
-67 -97 0
-67 -107 0
-77 -87 0
-77 -97 0
-77 -107 0
-87 -97 0
-87 -107 0
-97 -107 0
-8 -18 0
-8 -28 0
-8 -38 0
-8 -48 0
-8 -58 0
-8 -68 0
-8 -78 0
-8 -88 0
-8 -98 0
-8 -108 0
-18 -28 0
-18 -38 0
-18 -48 0
-18 -58 0
-18 -68 0
-18 -78 0
-18 -88 0
-18 -98 0
-18 -108 0
-28 -38 0
-28 -48 0
-28 -58 0
-28 -68 0
-28 -78 0
-28 -88 0
-28 -98 0
-28 -108 0
-38 -48 0
-38 -58 0
-38 -68 0
-38 -78 0
-38 -88 0
-38 -98 0
-38 -108 0
-48 -58 0
-48 -68 0
-48 -78 0
-48 -88 0
-48 -98 0
-48 -108 0
-58 -68 0
-58 -78 0
-58 -88 0
-58 -98 0
-58 -108 0
-68 -78 0
-68 -88 0
-68 -98 0
-68 -108 0
-78 -88 0
-78 -98 0
-78 -108 0
-88 -98 0
-88 -108 0
-98 -108 0
-9 -19 0
-9 -29 0
-9 -39 0
-9 -49 0
-9 -59 0
-9 -69 0
-9 -79 0
-9 -89 0
-9 -99 0
-9 -109 0
-19 -29 0
-19 -39 0
-19 -49 0
-19 -59 0
-19 -69 0
-19 -79 0
-19 -89 0
-19 -99 0
-19 -109 0
-29 -39 0
-29 -49 0
-29 -59 0
-29 -69 0
-29 -79 0
-29 -89 0
-29 -99 0
-29 -109 0
-39 -49 0
-39 -59 0
-39 -69 0
-39 -79 0
-39 -89 0
-39 -99 0
-39 -109 0
-49 -59 0
-49 -69 0
-49 -79 0
-49 -89 0
-49 -99 0
-49 -109 0
-59 -69 0
-59 -79 0
-59 -89 0
-59 -99 0
-59 -109 0
-69 -79 0
-69 -89 0
-69 -99 0
-69 -109 0
-79 -89 0
-79 -99 0
-79 -109 0
-89 -99 0
-89 -109 0
-99 -109 0
-10 -20 0
-10 -30 0
-10 -40 0
-10 -50 0
-10 -60 0
-10 -70 0
-10 -80 0
-10 -90 0
-10 -100 0
-10 -110 0
-20 -30 0
-20 -40 0
-20 -50 0
-20 -60 0
-20 -70 0
-20 -80 0
-20 -90 0
-20 -100 0
-20 -110 0
-30 -40 0
-30 -50 0
-30 -60 0
-30 -70 0
-30 -80 0
-30 -90 0
-30 -100 0
-30 -110 0
-40 -50 0
-40 -60 0
-40 -70 0
-40 -80 0
-40 -90 0
-40 -100 0
-40 -110 0
-50 -60 0
-50 -70 0
-50 -80 0
-50 -90 0
-50 -100 0
-50 -110 0
-60 -70 0
-60 -80 0
-60 -90 0
-60 -100 0
-60 -110 0
-70 -80 0
-70 -90 0
-70 -100 0
-70 -110 0
-80 -90 0
-80 -100 0
-80 -110 0
-90 -100 0
-90 -110 0
-100 -110 0