c at-most-one of 12 pidgeon in 11 holes c p1@1 1 c p2@1 2 c p3@1 3 c p4@1 4 c p5@1 5 c p6@1 6 c p7@1 7 c p8@1 8 c p9@1 9 c p10@1 10 c p11@1 11 c p12@1 12 c p1@2 13 c p2@2 14 c p3@2 15 c p4@2 16 c p5@2 17 c p6@2 18 c p7@2 19 c p8@2 20 c p9@2 21 c p10@2 22 c p11@2 23 c p12@2 24 c p1@3 25 c p2@3 26 c p3@3 27 c p4@3 28 c p5@3 29 c p6@3 30 c p7@3 31 c p8@3 32 c p9@3 33 c p10@3 34 c p11@3 35 c p12@3 36 c p1@4 37 c p2@4 38 c p3@4 39 c p4@4 40 c p5@4 41 c p6@4 42 c p7@4 43 c p8@4 44 c p9@4 45 c p10@4 46 c p11@4 47 c p12@4 48 c p1@5 49 c p2@5 50 c p3@5 51 c p4@5 52 c p5@5 53 c p6@5 54 c p7@5 55 c p8@5 56 c p9@5 57 c p10@5 58 c p11@5 59 c p12@5 60 c p1@6 61 c p2@6 62 c p3@6 63 c p4@6 64 c p5@6 65 c p6@6 66 c p7@6 67 c p8@6 68 c p9@6 69 c p10@6 70 c p11@6 71 c p12@6 72 c p1@7 73 c p2@7 74 c p3@7 75 c p4@7 76 c p5@7 77 c p6@7 78 c p7@7 79 c p8@7 80 c p9@7 81 c p10@7 82 c p11@7 83 c p12@7 84 c p1@8 85 c p2@8 86 c p3@8 87 c p4@8 88 c p5@8 89 c p6@8 90 c p7@8 91 c p8@8 92 c p9@8 93 c p10@8 94 c p11@8 95 c p12@8 96 c p1@9 97 c p2@9 98 c p3@9 99 c p4@9 100 c p5@9 101 c p6@9 102 c p7@9 103 c p8@9 104 c p9@9 105 c p10@9 106 c p11@9 107 c p12@9 108 c p1@10 109 c p2@10 110 c p3@10 111 c p4@10 112 c p5@10 113 c p6@10 114 c p7@10 115 c p8@10 116 c p9@10 117 c p10@10 118 c p11@10 119 c p12@10 120 c p1@11 121 c p2@11 122 c p3@11 123 c p4@11 124 c p5@11 125 c p6@11 126 c p7@11 127 c p8@11 128 c p9@11 129 c p10@11 130 c p11@11 131 c p12@11 132 p cnf 132 738 -1 -2 0 -1 -3 0 -1 -4 0 -1 -5 0 -1 -6 0 -1 -7 0 -1 -8 0 -1 -9 0 -1 -10 0 -1 -11 0 -1 -12 0 -2 -3 0 -2 -4 0 -2 -5 0 -2 -6 0 -2 -7 0 -2 -8 0 -2 -9 0 -2 -10 0 -2 -11 0 -2 -12 0 -3 -4 0 -3 -5 0 -3 -6 0 -3 -7 0 -3 -8 0 -3 -9 0 -3 -10 0 -3 -11 0 -3 -12 0 -4 -5 0 -4 -6 0 -4 -7 0 -4 -8 0 -4 -9 0 -4 -10 0 -4 -11 0 -4 -12 0 -5 -6 0 -5 -7 0 -5 -8 0 -5 -9 0 -5 -10 0 -5 -11 0 -5 -12 0 -6 -7 0 -6 -8 0 -6 -9 0 -6 -10 0 -6 -11 0 -6 -12 0 -7 -8 0 -7 -9 0 -7 -10 0 -7 -11 0 -7 -12 0 -8 -9 0 -8 -10 0 -8 -11 0 -8 -12 0 -9 -10 0 -9 -11 0 -9 -12 0 -10 -11 0 -10 -12 0 -11 -12 0 -13 -14 0 -13 -15 0 -13 -16 0 -13 -17 0 -13 -18 0 -13 -19 0 -13 -20 0 -13 -21 0 -13 -22 0 -13 -23 0 -13 -24 0 -14 -15 0 -14 -16 0 -14 -17 0 -14 -18 0 -14 -19 0 -14 -20 0 -14 -21 0 -14 -22 0 -14 -23 0 -14 -24 0 -15 -16 0 -15 -17 0 -15 -18 0 -15 -19 0 -15 -20 0 -15 -21 0 -15 -22 0 -15 -23 0 -15 -24 0 -16 -17 0 -16 -18 0 -16 -19 0 -16 -20 0 -16 -21 0 -16 -22 0 -16 -23 0 -16 -24 0 -17 -18 0 -17 -19 0 -17 -20 0 -17 -21 0 -17 -22 0 -17 -23 0 -17 -24 0 -18 -19 0 -18 -20 0 -18 -21 0 -18 -22 0 -18 -23 0 -18 -24 0 -19 -20 0 -19 -21 0 -19 -22 0 -19 -23 0 -19 -24 0 -20 -21 0 -20 -22 0 -20 -23 0 -20 -24 0 -21 -22 0 -21 -23 0 -21 -24 0 -22 -23 0 -22 -24 0 -23 -24 0 -25 -26 0 -25 -27 0 -25 -28 0 -25 -29 0 -25 -30 0 -25 -31 0 -25 -32 0 -25 -33 0 -25 -34 0 -25 -35 0 -25 -36 0 -26 -27 0 -26 -28 0 -26 -29 0 -26 -30 0 -26 -31 0 -26 -32 0 -26 -33 0 -26 -34 0 -26 -35 0 -26 -36 0 -27 -28 0 -27 -29 0 -27 -30 0 -27 -31 0 -27 -32 0 -27 -33 0 -27 -34 0 -27 -35 0 -27 -36 0 -28 -29 0 -28 -30 0 -28 -31 0 -28 -32 0 -28 -33 0 -28 -34 0 -28 -35 0 -28 -36 0 -29 -30 0 -29 -31 0 -29 -32 0 -29 -33 0 -29 -34 0 -29 -35 0 -29 -36 0 -30 -31 0 -30 -32 0 -30 -33 0 -30 -34 0 -30 -35 0 -30 -36 0 -31 -32 0 -31 -33 0 -31 -34 0 -31 -35 0 -31 -36 0 -32 -33 0 -32 -34 0 -32 -35 0 -32 -36 0 -33 -34 0 -33 -35 0 -33 -36 0 -34 -35 0 -34 -36 0 -35 -36 0 -37 -38 0 -37 -39 0 -37 -40 0 -37 -41 0 -37 -42 0 -37 -43 0 -37 -44 0 -37 -45 0 -37 -46 0 -37 -47 0 -37 -48 0 -38 -39 0 -38 -40 0 -38 -41 0 -38 -42 0 -38 -43 0 -38 -44 0 -38 -45 0 -38 -46 0 -38 -47 0 -38 -48 0 -39 -40 0 -39 -41 0 -39 -42 0 -39 -43 0 -39 -44 0 -39 -45 0 -39 -46 0 -39 -47 0 -39 -48 0 -40 -41 0 -40 -42 0 -40 -43 0 -40 -44 0 -40 -45 0 -40 -46 0 -40 -47 0 -40 -48 0 -41 -42 0 -41 -43 0 -41 -44 0 -41 -45 0 -41 -46 0 -41 -47 0 -41 -48 0 -42 -43 0 -42 -44 0 -42 -45 0 -42 -46 0 -42 -47 0 -42 -48 0 -43 -44 0 -43 -45 0 -43 -46 0 -43 -47 0 -43 -48 0 -44 -45 0 -44 -46 0 -44 -47 0 -44 -48 0 -45 -46 0 -45 -47 0 -45 -48 0 -46 -47 0 -46 -48 0 -47 -48 0 -49 -50 0 -49 -51 0 -49 -52 0 -49 -53 0 -49 -54 0 -49 -55 0 -49 -56 0 -49 -57 0 -49 -58 0 -49 -59 0 -49 -60 0 -50 -51 0 -50 -52 0 -50 -53 0 -50 -54 0 -50 -55 0 -50 -56 0 -50 -57 0 -50 -58 0 -50 -59 0 -50 -60 0 -51 -52 0 -51 -53 0 -51 -54 0 -51 -55 0 -51 -56 0 -51 -57 0 -51 -58 0 -51 -59 0 -51 -60 0 -52 -53 0 -52 -54 0 -52 -55 0 -52 -56 0 -52 -57 0 -52 -58 0 -52 -59 0 -52 -60 0 -53 -54 0 -53 -55 0 -53 -56 0 -53 -57 0 -53 -58 0 -53 -59 0 -53 -60 0 -54 -55 0 -54 -56 0 -54 -57 0 -54 -58 0 -54 -59 0 -54 -60 0 -55 -56 0 -55 -57 0 -55 -58 0 -55 -59 0 -55 -60 0 -56 -57 0 -56 -58 0 -56 -59 0 -56 -60 0 -57 -58 0 -57 -59 0 -57 -60 0 -58 -59 0 -58 -60 0 -59 -60 0 -61 -62 0 -61 -63 0 -61 -64 0 -61 -65 0 -61 -66 0 -61 -67 0 -61 -68 0 -61 -69 0 -61 -70 0 -61 -71 0 -61 -72 0 -62 -63 0 -62 -64 0 -62 -65 0 -62 -66 0 -62 -67 0 -62 -68 0 -62 -69 0 -62 -70 0 -62 -71 0 -62 -72 0 -63 -64 0 -63 -65 0 -63 -66 0 -63 -67 0 -63 -68 0 -63 -69 0 -63 -70 0 -63 -71 0 -63 -72 0 -64 -65 0 -64 -66 0 -64 -67 0 -64 -68 0 -64 -69 0 -64 -70 0 -64 -71 0 -64 -72 0 -65 -66 0 -65 -67 0 -65 -68 0 -65 -69 0 -65 -70 0 -65 -71 0 -65 -72 0 -66 -67 0 -66 -68 0 -66 -69 0 -66 -70 0 -66 -71 0 -66 -72 0 -67 -68 0 -67 -69 0 -67 -70 0 -67 -71 0 -67 -72 0 -68 -69 0 -68 -70 0 -68 -71 0 -68 -72 0 -69 -70 0 -69 -71 0 -69 -72 0 -70 -71 0 -70 -72 0 -71 -72 0 -73 -74 0 -73 -75 0 -73 -76 0 -73 -77 0 -73 -78 0 -73 -79 0 -73 -80 0 -73 -81 0 -73 -82 0 -73 -83 0 -73 -84 0 -74 -75 0 -74 -76 0 -74 -77 0 -74 -78 0 -74 -79 0 -74 -80 0 -74 -81 0 -74 -82 0 -74 -83 0 -74 -84 0 -75 -76 0 -75 -77 0 -75 -78 0 -75 -79 0 -75 -80 0 -75 -81 0 -75 -82 0 -75 -83 0 -75 -84 0 -76 -77 0 -76 -78 0 -76 -79 0 -76 -80 0 -76 -81 0 -76 -82 0 -76 -83 0 -76 -84 0 -77 -78 0 -77 -79 0 -77 -80 0 -77 -81 0 -77 -82 0 -77 -83 0 -77 -84 0 -78 -79 0 -78 -80 0 -78 -81 0 -78 -82 0 -78 -83 0 -78 -84 0 -79 -80 0 -79 -81 0 -79 -82 0 -79 -83 0 -79 -84 0 -80 -81 0 -80 -82 0 -80 -83 0 -80 -84 0 -81 -82 0 -81 -83 0 -81 -84 0 -82 -83 0 -82 -84 0 -83 -84 0 -85 -86 0 -85 -87 0 -85 -88 0 -85 -89 0 -85 -90 0 -85 -91 0 -85 -92 0 -85 -93 0 -85 -94 0 -85 -95 0 -85 -96 0 -86 -87 0 -86 -88 0 -86 -89 0 -86 -90 0 -86 -91 0 -86 -92 0 -86 -93 0 -86 -94 0 -86 -95 0 -86 -96 0 -87 -88 0 -87 -89 0 -87 -90 0 -87 -91 0 -87 -92 0 -87 -93 0 -87 -94 0 -87 -95 0 -87 -96 0 -88 -89 0 -88 -90 0 -88 -91 0 -88 -92 0 -88 -93 0 -88 -94 0 -88 -95 0 -88 -96 0 -89 -90 0 -89 -91 0 -89 -92 0 -89 -93 0 -89 -94 0 -89 -95 0 -89 -96 0 -90 -91 0 -90 -92 0 -90 -93 0 -90 -94 0 -90 -95 0 -90 -96 0 -91 -92 0 -91 -93 0 -91 -94 0 -91 -95 0 -91 -96 0 -92 -93 0 -92 -94 0 -92 -95 0 -92 -96 0 -93 -94 0 -93 -95 0 -93 -96 0 -94 -95 0 -94 -96 0 -95 -96 0 -97 -98 0 -97 -99 0 -97 -100 0 -97 -101 0 -97 -102 0 -97 -103 0 -97 -104 0 -97 -105 0 -97 -106 0 -97 -107 0 -97 -108 0 -98 -99 0 -98 -100 0 -98 -101 0 -98 -102 0 -98 -103 0 -98 -104 0 -98 -105 0 -98 -106 0 -98 -107 0 -98 -108 0 -99 -100 0 -99 -101 0 -99 -102 0 -99 -103 0 -99 -104 0 -99 -105 0 -99 -106 0 -99 -107 0 -99 -108 0 -100 -101 0 -100 -102 0 -100 -103 0 -100 -104 0 -100 -105 0 -100 -106 0 -100 -107 0 -100 -108 0 -101 -102 0 -101 -103 0 -101 -104 0 -101 -105 0 -101 -106 0 -101 -107 0 -101 -108 0 -102 -103 0 -102 -104 0 -102 -105 0 -102 -106 0 -102 -107 0 -102 -108 0 -103 -104 0 -103 -105 0 -103 -106 0 -103 -107 0 -103 -108 0 -104 -105 0 -104 -106 0 -104 -107 0 -104 -108 0 -105 -106 0 -105 -107 0 -105 -108 0 -106 -107 0 -106 -108 0 -107 -108 0 -109 -110 0 -109 -111 0 -109 -112 0 -109 -113 0 -109 -114 0 -109 -115 0 -109 -116 0 -109 -117 0 -109 -118 0 -109 -119 0 -109 -120 0 -110 -111 0 -110 -112 0 -110 -113 0 -110 -114 0 -110 -115 0 -110 -116 0 -110 -117 0 -110 -118 0 -110 -119 0 -110 -120 0 -111 -112 0 -111 -113 0 -111 -114 0 -111 -115 0 -111 -116 0 -111 -117 0 -111 -118 0 -111 -119 0 -111 -120 0 -112 -113 0 -112 -114 0 -112 -115 0 -112 -116 0 -112 -117 0 -112 -118 0 -112 -119 0 -112 -120 0 -113 -114 0 -113 -115 0 -113 -116 0 -113 -117 0 -113 -118 0 -113 -119 0 -113 -120 0 -114 -115 0 -114 -116 0 -114 -117 0 -114 -118 0 -114 -119 0 -114 -120 0 -115 -116 0 -115 -117 0 -115 -118 0 -115 -119 0 -115 -120 0 -116 -117 0 -116 -118 0 -116 -119 0 -116 -120 0 -117 -118 0 -117 -119 0 -117 -120 0 -118 -119 0 -118 -120 0 -119 -120 0 -121 -122 0 -121 -123 0 -121 -124 0 -121 -125 0 -121 -126 0 -121 -127 0 -121 -128 0 -121 -129 0 -121 -130 0 -121 -131 0 -121 -132 0 -122 -123 0 -122 -124 0 -122 -125 0 -122 -126 0 -122 -127 0 -122 -128 0 -122 -129 0 -122 -130 0 -122 -131 0 -122 -132 0 -123 -124 0 -123 -125 0 -123 -126 0 -123 -127 0 -123 -128 0 -123 -129 0 -123 -130 0 -123 -131 0 -123 -132 0 -124 -125 0 -124 -126 0 -124 -127 0 -124 -128 0 -124 -129 0 -124 -130 0 -124 -131 0 -124 -132 0 -125 -126 0 -125 -127 0 -125 -128 0 -125 -129 0 -125 -130 0 -125 -131 0 -125 -132 0 -126 -127 0 -126 -128 0 -126 -129 0 -126 -130 0 -126 -131 0 -126 -132 0 -127 -128 0 -127 -129 0 -127 -130 0 -127 -131 0 -127 -132 0 -128 -129 0 -128 -130 0 -128 -131 0 -128 -132 0 -129 -130 0 -129 -131 0 -129 -132 0 -130 -131 0 -130 -132 0 -131 -132 0 1 13 25 37 49 61 73 85 97 109 121 0 2 14 26 38 50 62 74 86 98 110 122 0 3 15 27 39 51 63 75 87 99 111 123 0 4 16 28 40 52 64 76 88 100 112 124 0 5 17 29 41 53 65 77 89 101 113 125 0 6 18 30 42 54 66 78 90 102 114 126 0 7 19 31 43 55 67 79 91 103 115 127 0 8 20 32 44 56 68 80 92 104 116 128 0 9 21 33 45 57 69 81 93 105 117 129 0 10 22 34 46 58 70 82 94 106 118 130 0 11 23 35 47 59 71 83 95 107 119 131 0 12 24 36 48 60 72 84 96 108 120 132 0