c File: pret150_75.cnf c c SOURCE: Daniel Pretolani (daniele@crt.umontreal.ca) c c DESCRIPTION: Unsatisfiable instances of a graph 2-coloring with c parity constraints. c c ----------- DIMACS Challenge - CNF format ----------- c c TRISAT Generator (Pretolani 1990) c c (Even) number of nodes ==> 100 c Charge ( 0 = sat. / 1 = unsat. ) ==> 1 c Horn Percentage (min -> 25; max -> 75) ==> 75 c Number of Propositional variables ==> 150 c Number of Clauses ==> 400 c Nodes with Charge = 1 ==> 99 c Horn Percentage (exact) ==> 74.000 c c ----------------------------------------------------- p cnf 150 400 -3 -2 -1 0 3 2 -1 0 2 1 -3 0 3 1 -2 0 6 5 4 0 6 -5 -4 0 5 -6 -4 0 4 -6 -5 0 9 8 7 0 9 -8 -7 0 8 -9 -7 0 7 -9 -8 0 12 11 10 0 12 -11 -10 0 11 -12 -10 0 10 -12 -11 0 15 14 13 0 15 -14 -13 0 14 -15 -13 0 13 -15 -14 0 18 17 16 0 18 -17 -16 0 17 -18 -16 0 16 -18 -17 0 21 20 19 0 21 -20 -19 0 20 -21 -19 0 19 -21 -20 0 24 23 22 0 24 -23 -22 0 23 -24 -22 0 22 -24 -23 0 27 26 25 0 27 -26 -25 0 26 -27 -25 0 25 -27 -26 0 30 29 28 0 30 -29 -28 0 29 -30 -28 0 28 -30 -29 0 33 32 31 0 33 -32 -31 0 32 -33 -31 0 31 -33 -32 0 36 35 34 0 36 -35 -34 0 35 -36 -34 0 34 -36 -35 0 39 38 37 0 39 -38 -37 0 38 -39 -37 0 37 -39 -38 0 42 41 40 0 42 -41 -40 0 41 -42 -40 0 40 -42 -41 0 45 44 43 0 45 -44 -43 0 44 -45 -43 0 43 -45 -44 0 48 47 46 0 48 -47 -46 0 47 -48 -46 0 46 -48 -47 0 51 50 49 0 51 -50 -49 0 50 -51 -49 0 49 -51 -50 0 54 53 52 0 54 -53 -52 0 53 -54 -52 0 52 -54 -53 0 57 56 55 0 57 -56 -55 0 56 -57 -55 0 55 -57 -56 0 60 59 58 0 60 -59 -58 0 59 -60 -58 0 58 -60 -59 0 63 62 61 0 63 -62 -61 0 62 -63 -61 0 61 -63 -62 0 66 65 64 0 66 -65 -64 0 65 -66 -64 0 64 -66 -65 0 69 68 67 0 69 -68 -67 0 68 -69 -67 0 67 -69 -68 0 72 71 70 0 72 -71 -70 0 71 -72 -70 0 70 -72 -71 0 75 74 73 0 75 -74 -73 0 74 -75 -73 0 73 -75 -74 0 78 77 76 0 78 -77 -76 0 77 -78 -76 0 76 -78 -77 0 81 80 79 0 81 -80 -79 0 80 -81 -79 0 79 -81 -80 0 84 83 82 0 84 -83 -82 0 83 -84 -82 0 82 -84 -83 0 87 86 85 0 87 -86 -85 0 86 -87 -85 0 85 -87 -86 0 90 89 88 0 90 -89 -88 0 89 -90 -88 0 88 -90 -89 0 93 92 91 0 93 -92 -91 0 92 -93 -91 0 91 -93 -92 0 96 95 94 0 96 -95 -94 0 95 -96 -94 0 94 -96 -95 0 99 98 97 0 99 -98 -97 0 98 -99 -97 0 97 -99 -98 0 101 100 97 0 101 -100 -97 0 100 -101 -97 0 97 -101 -100 0 102 36 7 0 102 -36 -7 0 36 -102 -7 0 7 -102 -36 0 102 35 31 0 102 -35 -31 0 35 -102 -31 0 31 -102 -35 0 104 103 3 0 104 -103 -3 0 103 -104 -3 0 3 -104 -103 0 103 40 2 0 103 -40 -2 0 40 -103 -2 0 2 -103 -40 0 106 105 39 0 106 -105 -39 0 105 -106 -39 0 39 -106 -105 0 105 104 38 0 105 -104 -38 0 104 -105 -38 0 38 -105 -104 0 107 42 16 0 107 -42 -16 0 42 -107 -16 0 16 -107 -42 0 107 41 37 0 107 -41 -37 0 41 -107 -37 0 37 -107 -41 0 109 108 15 0 109 -108 -15 0 108 -109 -15 0 15 -109 -108 0 108 46 14 0 108 -46 -14 0 46 -108 -14 0 14 -108 -46 0 111 110 45 0 111 -110 -45 0 110 -111 -45 0 45 -111 -110 0 110 109 44 0 110 -109 -44 0 109 -110 -44 0 44 -110 -109 0 112 106 48 0 112 -106 -48 0 106 -112 -48 0 48 -112 -106 0 112 47 43 0 112 -47 -43 0 47 -112 -43 0 43 -112 -47 0 114 113 18 0 114 -113 -18 0 113 -114 -18 0 18 -114 -113 0 113 52 17 0 113 -52 -17 0 52 -113 -17 0 17 -113 -52 0 115 51 10 0 115 -51 -10 0 51 -115 -10 0 10 -115 -51 0 115 114 50 0 115 -114 -50 0 114 -115 -50 0 50 -115 -114 0 116 54 13 0 116 -54 -13 0 54 -116 -13 0 13 -116 -54 0 116 53 49 0 116 -53 -49 0 53 -116 -49 0 49 -116 -53 0 118 117 6 0 118 -117 -6 0 117 -118 -6 0 6 -118 -117 0 117 58 5 0 117 -58 -5 0 58 -117 -5 0 5 -117 -58 0 120 119 57 0 120 -119 -57 0 119 -120 -57 0 57 -120 -119 0 119 118 56 0 119 -118 -56 0 118 -119 -56 0 56 -119 -118 0 121 60 22 0 121 -60 -22 0 60 -121 -22 0 22 -121 -60 0 121 59 55 0 121 -59 -55 0 59 -121 -55 0 55 -121 -59 0 123 122 21 0 123 -122 -21 0 122 -123 -21 0 21 -123 -122 0 122 64 20 0 122 -64 -20 0 64 -122 -20 0 20 -122 -64 0 125 124 63 0 125 -124 -63 0 124 -125 -63 0 63 -125 -124 0 124 123 62 0 124 -123 -62 0 123 -124 -62 0 62 -124 -123 0 126 120 66 0 126 -120 -66 0 120 -126 -66 0 66 -126 -120 0 126 65 61 0 126 -65 -61 0 65 -126 -61 0 61 -126 -65 0 128 127 24 0 128 -127 -24 0 127 -128 -24 0 24 -128 -127 0 127 70 23 0 127 -70 -23 0 70 -127 -23 0 23 -127 -70 0 129 69 1 0 129 -69 -1 0 69 -129 -1 0 1 -129 -69 0 129 128 68 0 129 -128 -68 0 128 -129 -68 0 68 -129 -128 0 130 72 19 0 130 -72 -19 0 72 -130 -19 0 19 -130 -72 0 130 71 67 0 130 -71 -67 0 71 -130 -67 0 67 -130 -71 0 132 131 9 0 132 -131 -9 0 131 -132 -9 0 9 -132 -131 0 131 76 8 0 131 -76 -8 0 76 -131 -8 0 8 -131 -76 0 134 133 75 0 134 -133 -75 0 133 -134 -75 0 75 -134 -133 0 133 132 74 0 133 -132 -74 0 132 -133 -74 0 74 -133 -132 0 135 78 28 0 135 -78 -28 0 78 -135 -28 0 28 -135 -78 0 135 77 73 0 135 -77 -73 0 77 -135 -73 0 73 -135 -77 0 137 136 27 0 137 -136 -27 0 136 -137 -27 0 27 -137 -136 0 136 82 26 0 136 -82 -26 0 82 -136 -26 0 26 -136 -82 0 138 111 81 0 138 -111 -81 0 111 -138 -81 0 81 -138 -111 0 138 137 80 0 138 -137 -80 0 137 -138 -80 0 80 -138 -137 0 139 134 84 0 139 -134 -84 0 134 -139 -84 0 84 -139 -134 0 139 83 79 0 139 -83 -79 0 83 -139 -79 0 79 -139 -83 0 141 140 30 0 141 -140 -30 0 140 -141 -30 0 30 -141 -140 0 140 88 29 0 140 -88 -29 0 88 -140 -29 0 29 -140 -88 0 142 87 4 0 142 -87 -4 0 87 -142 -4 0 4 -142 -87 0 142 141 86 0 142 -141 -86 0 141 -142 -86 0 86 -142 -141 0 143 90 25 0 143 -90 -25 0 90 -143 -25 0 25 -143 -90 0 143 89 85 0 143 -89 -85 0 89 -143 -85 0 85 -143 -89 0 145 144 12 0 145 -144 -12 0 144 -145 -12 0 12 -145 -144 0 144 94 11 0 144 -94 -11 0 94 -144 -11 0 11 -144 -94 0 146 101 93 0 146 -101 -93 0 101 -146 -93 0 93 -146 -101 0 146 145 92 0 146 -145 -92 0 145 -146 -92 0 92 -146 -145 0 147 96 34 0 147 -96 -34 0 96 -147 -34 0 34 -147 -96 0 147 95 91 0 147 -95 -91 0 95 -147 -91 0 91 -147 -95 0 149 148 33 0 149 -148 -33 0 148 -149 -33 0 33 -149 -148 0 148 100 32 0 148 -100 -32 0 100 -148 -32 0 32 -148 -100 0 150 125 99 0 150 -125 -99 0 125 -150 -99 0 99 -150 -125 0 150 149 98 0 150 -149 -98 0 149 -150 -98 0 98 -150 -149 0 0