c Weighted CNF
c from Selman's wff generator
p wcnf 150 1000 5278
5278 123 -121 0
5278 66 -130 0
5278 94 88 0
5278 -150 94 0
5278 77 138 0
5278 -32 -77 0
5278 29 -135 0
5278 -149 -3 0
5278 31 51 0
5278 -81 8 0
5278 78 115 0
5278 -61 -57 0
5278 44 113 0
5278 39 103 0
5278 88 -71 0
5278 74 -126 0
5278 -27 -91 0
5278 -99 68 0
5278 33 -142 0
5278 -48 -145 0
5278 107 -83 0
5278 35 -56 0
5278 126 98 0
5278 74 -114 0
5278 55 118 0
5278 35 31 0
5278 23 75 0
5278 69 89 0
5278 21 27 0
5278 83 84 0
5278 -31 -85 0
5278 48 -111 0
5278 -78 -110 0
5278 140 132 0
5278 -56 -39 0
5278 -128 -93 0
5278 120 20 0
5278 -103 -80 0
5278 -15 68 0
5278 28 -141 0
5278 101 -117 0
5278 -98 96 0
5278 -134 -35 0
5278 -128 -126 0
5278 -146 -13 0
5278 -93 -110 0
5278 27 19 0
5278 10 -31 0
5278 148 -76 0
5278 -21 3 0
5278 -37 75 0
5278 -50 75 0
5278 -88 110 0
5278 -70 -74 0
5278 -92 -4 0
5278 34 8 0
5278 -83 -110 0
5278 -113 -74 0
5278 148 75 0
5278 -150 -124 0
5278 -84 85 0
5278 -9 -102 0
5278 105 -97 0
5278 105 110 0
5278 -70 145 0
5278 69 100 0
5278 -24 43 0
5278 -16 -57 0
5278 -141 -75 0
5278 -26 -49 0
5278 -146 -149 0
5278 -109 138 0
5278 133 129 0
5278 -78 -90 0
5278 -133 -81 0
5278 -137 -82 0
5278 -7 48 0
5278 97 -76 0
5278 74 131 0
5278 118 -29 0
5278 7 -119 0
5278 59 119 0
5278 50 9 0
5278 91 -136 0
5278 -33 -141 0
5278 66 -141 0
5278 121 -112 0
5278 141 -81 0
5278 -49 -41 0
5278 -9 117 0
5278 -125 37 0
5278 22 109 0
5278 100 139 0
5278 129 -104 0
5278 66 26 0
5278 106 77 0
5278 -117 -134 0
5278 100 110 0
5278 -147 129 0
5278 87 149 0
5278 138 -106 0
5278 60 -55 0
5278 81 104 0
5278 31 -83 0
5278 -67 3 0
5278 -113 -7 0
5278 -135 79 0
5278 -77 49 0
5278 5 8 0
5278 63 -97 0
5278 50 -69 0
5278 -2 69 0
5278 -71 51 0
5278 -58 25 0
5278 -103 119 0
5278 -18 70 0
5278 -77 -125 0
5278 -71 -124 0
5278 43 9 0
5278 -78 -129 0
5278 29 -46 0
5278 -70 24 0
5278 143 91 0
5278 10 -146 0
5278 120 118 0
5278 92 -56 0
5278 65 -62 0
5278 -41 139 0
5278 34 -22 0
5278 -46 133 0
5278 74 -27 0
5278 22 -81 0
5278 48 -95 0
5278 -150 43 0
5278 105 -150 0
5278 138 46 0
5278 -68 -69 0
5278 51 -99 0
5278 125 -51 0
5278 -131 77 0
5278 21 19 0
5278 -62 140 0
5278 -140 10 0
5278 -73 -149 0
5278 123 68 0
5278 69 -17 0
5278 -74 -43 0
5278 30 128 0
5278 -145 -41 0
5278 -125 -126 0
6 136 102 0
8 100 105 0
2 -22 -91 0
3 107 39 0
8 82 -9 0
1 136 -51 0
2 -92 120 0
8 96 -90 0
10 -41 -32 0
4 136 37 0
4 -128 -56 0
10 -95 7 0
4 -15 -145 0
7 -46 -147 0
2 117 96 0
2 -35 -85 0
5 116 -130 0
4 -17 -129 0
4 -35 -56 0
10 62 -44 0
10 -39 -142 0
5 139 -56 0
8 1 125 0
10 -59 8 0
4 -138 27 0
8 -5 84 0
1 139 78 0
8 -121 23 0
10 -14 52 0
4 -107 -15 0
5 -140 123 0
6 130 -104 0
1 -130 -48 0
6 131 -119 0
9 46 41 0
8 63 -146 0
7 -47 121 0
10 -135 -35 0
6 7 -105 0
7 -58 94 0
3 141 -74 0
9 -42 -45 0
6 -85 -111 0
6 107 131 0
6 101 -2 0
7 37 118 0
8 72 -81 0
1 24 132 0
1 -55 -39 0
1 83 77 0
10 38 -138 0
1 -118 89 0
5 91 -3 0
7 120 62 0
10 143 48 0
9 30 -37 0
4 75 17 0
1 94 -64 0
7 -52 40 0
3 -129 122 0
4 125 -91 0
2 -3 -65 0
9 113 -6 0
4 -42 -43 0
7 -59 106 0
7 -20 149 0
2 -38 108 0
4 -79 29 0
6 -119 -130 0
7 -45 132 0
10 -138 127 0
8 -19 -75 0
6 -31 119 0
5 -118 62 0
4 20 -63 0
1 91 105 0
2 85 -148 0
2 -130 -145 0
1 -121 -135 0
2 59 -142 0
2 -111 -146 0
1 -58 -112 0
3 25 -103 0
7 58 -26 0
7 -24 54 0
2 -48 106 0
6 91 -117 0
1 -108 74 0
2 -70 -79 0
3 41 78 0
4 31 -79 0
6 -104 -54 0
4 -108 50 0
2 6 -101 0
9 -67 30 0
1 -104 34 0
8 -112 88 0
1 15 53 0
4 -131 -97 0
3 150 -62 0
7 -112 -43 0
4 144 135 0
1 -15 -8 0
3 -41 27 0
9 114 -139 0
4 41 71 0
4 -17 5 0
10 -67 17 0
5 -59 86 0
4 -70 -58 0
2 65 -46 0
7 -73 41 0
4 30 112 0
4 -33 38 0
4 42 -45 0
1 -61 -39 0
6 125 131 0
10 -38 -133 0
1 29 -30 0
7 -70 -16 0
2 127 2 0
4 39 -109 0
3 3 124 0
5 12 -25 0
5 5 54 0
1 -37 8 0
5 37 -52 0
3 67 2 0
1 3 74 0
9 -32 111 0
5 -84 -10 0
8 -34 131 0
2 -34 111 0
5 -119 74 0
10 -125 150 0
1 -2 17 0
9 90 -136 0
3 96 17 0
10 -26 103 0
4 -83 -56 0
7 16 -26 0
2 -99 20 0
10 -20 101 0
1 117 47 0
6 33 -70 0
4 86 -32 0
2 134 132 0
1 37 115 0
4 141 -69 0
2 88 -26 0
8 -126 -124 0
5 -20 2 0
6 72 25 0
10 -57 38 0
10 -20 138 0
1 -103 -139 0
1 57 -145 0
5 -20 -41 0
3 -15 80 0
1 -82 85 0
3 110 117 0
8 4 129 0
9 -116 13 0
5 1 37 0
2 32 41 0
9 81 -5 0
5 -84 133 0
1 67 66 0
2 33 28 0
5 6 -98 0
4 110 -138 0
8 25 48 0
6 -88 70 0
4 -74 3 0
9 136 94 0
2 -10 40 0
8 -67 120 0
1 67 137 0
2 -125 -81 0
1 129 5 0
3 -75 -13 0
9 16 49 0
6 142 28 0
8 67 -132 0
9 101 120 0
5 106 -98 0
9 -29 31 0
9 35 -135 0
9 -147 7 0
2 56 112 0
10 140 65 0
2 46 -91 0
9 60 94 0
8 -42 59 0
7 -90 -24 0
1 -8 149 0
6 6 40 0
1 -2 -28 0
2 93 -6 0
7 -96 85 0
6 29 150 0
5 -59 -115 0
5 -139 -66 0
2 65 55 0
8 -95 -17 0
4 -44 -87 0
3 -92 132 0
6 67 -110 0
4 110 62 0
5 26 5 0
6 70 -139 0
6 44 -12 0
3 -28 33 0
1 120 20 0
4 -2 32 0
2 142 -140 0
6 -52 -28 0
3 -32 -137 0
10 -126 103 0
5 114 -139 0
4 22 -92 0
9 112 -121 0
6 3 -150 0
3 -140 45 0
7 -73 -66 0
2 52 60 0
3 12 -142 0
3 -131 55 0
3 -146 -30 0
4 1 44 0
10 -43 102 0
9 147 92 0
9 7 41 0
5 -100 -80 0
10 -72 133 0
7 38 54 0
8 -84 -44 0
3 -87 -61 0
2 12 83 0
2 -25 85 0
7 -126 -101 0
8 30 -27 0
8 10 125 0
10 -29 -54 0
9 98 70 0
1 131 -133 0
1 66 -26 0
4 -111 -77 0
3 28 62 0
10 88 -50 0
8 -24 10 0
7 64 73 0
9 143 -61 0
4 -43 -60 0
9 86 115 0
5 -42 19 0
5 -81 146 0
1 -46 134 0
7 -144 109 0
8 32 136 0
5 -46 -114 0
7 24 -112 0
6 76 -94 0
3 113 139 0
1 134 13 0
5 -146 -26 0
10 134 70 0
8 55 -114 0
7 77 -36 0
1 148 86 0
10 29 -64 0
4 53 78 0
8 90 -94 0
7 120 -14 0
3 -83 -119 0
7 -83 8 0
8 -43 128 0
3 -64 -17 0
10 -81 -4 0
10 82 117 0
3 -61 85 0
8 -99 29 0
7 148 -100 0
1 108 -89 0
1 -47 41 0
5 -4 91 0
6 -24 -128 0
5 148 -109 0
6 64 -79 0
3 -61 62 0
3 -81 20 0
10 -109 118 0
9 9 121 0
8 62 -64 0
3 41 107 0
9 -66 -124 0
3 53 -1 0
3 -62 -12 0
7 32 -92 0
10 -60 3 0
3 -123 63 0
6 -127 98 0
3 55 -43 0
1 -16 26 0
3 27 -20 0
5 -32 6 0
7 98 110 0
10 112 -46 0
7 -109 -4 0
7 -102 87 0
10 -129 -8 0
9 33 74 0
4 -94 -95 0
6 101 77 0
10 37 -89 0
4 -135 -129 0
10 132 -52 0
5 -138 -130 0
9 -137 64 0
5 -138 -26 0
7 120 75 0
1 -1 93 0
5 31 22 0
5 -150 -118 0
8 19 137 0
8 -117 -3 0
4 -67 86 0
1 -111 -51 0
10 126 -39 0
10 132 118 0
10 139 -49 0
3 -17 137 0
6 124 -34 0
2 37 -16 0
4 101 17 0
8 -68 141 0
6 30 142 0
1 110 -32 0
7 -81 -51 0
2 -37 55 0
7 -89 -24 0
7 -39 -143 0
1 10 -86 0
1 -77 -43 0
2 -35 -137 0
10 -19 -140 0
4 41 -27 0
2 -82 27 0
5 -50 -37 0
3 -30 75 0
7 -11 -129 0
2 21 83 0
4 70 -10 0
1 150 139 0
6 -15 -83 0
2 -109 53 0
9 -90 -112 0
10 37 24 0
2 -2 122 0
9 -55 -27 0
9 36 124 0
1 113 -99 0
2 32 -42 0
5 -94 39 0
2 1 95 0
5 -119 -9 0
2 -130 68 0
7 94 -69 0
5 43 70 0
9 -19 90 0
9 131 55 0
2 -94 -39 0
5 -134 -110 0
10 118 -64 0
2 -131 65 0
7 134 140 0
10 60 -68 0
6 -8 -14 0
8 69 18 0
5 -56 20 0
8 -130 -85 0
5 148 -62 0
6 127 -28 0
1 -17 -106 0
5 24 18 0
2 32 -131 0
2 -148 81 0
4 -101 -65 0
1 149 -82 0
4 -144 -73 0
3 -100 -28 0
9 133 66 0
4 84 -46 0
4 26 56 0
4 -137 -25 0
5 90 -19 0
8 -100 -45 0
5 117 60 0
2 87 143 0
3 59 -75 0
4 -120 -112 0
1 17 21 0
4 -46 -96 0
8 115 107 0
1 1 -8 0
5 68 70 0
5 62 -67 0
1 -142 -149 0
1 -110 -68 0
3 -89 -126 0
5 -72 69 0
8 -25 42 0
7 -50 -107 0
10 -26 -28 0
9 95 -44 0
2 43 18 0
1 -86 4 0
1 130 108 0
5 -26 128 0
1 -19 38 0
4 144 70 0
7 -97 6 0
10 -50 -11 0
8 -29 -24 0
10 -28 72 0
3 29 147 0
3 -124 -146 0
8 33 31 0
8 100 95 0
5 -100 -149 0
10 -10 64 0
1 88 -34 0
5 -105 -140 0
3 136 -30 0
8 -25 143 0
6 -23 -11 0
8 105 127 0
3 126 -106 0
6 20 -143 0
8 26 -24 0
5 -14 -42 0
10 -72 -2 0
6 145 58 0
1 -68 87 0
10 -63 8 0
4 114 -129 0
2 -122 -46 0
10 -70 -12 0
5 -54 -92 0
7 94 -39 0
10 -96 74 0
9 10 94 0
4 -102 112 0
10 90 134 0
6 30 -139 0
4 150 37 0
2 129 115 0
8 3 -98 0
1 -21 115 0
9 -58 146 0
2 107 63 0
1 -47 -124 0
9 112 -17 0
7 53 59 0
3 -24 42 0
7 -139 113 0
3 77 -84 0
1 -80 141 0
10 -53 -69 0
8 42 41 0
8 -57 -52 0
4 -110 -130 0
8 22 94 0
4 56 -132 0
5 -66 -58 0
7 49 -111 0
8 29 114 0
7 5 75 0
6 127 -39 0
2 19 11 0
3 104 78 0
6 -59 -69 0
1 -127 109 0
7 -69 -1 0
5 115 -26 0
6 101 -92 0
10 131 -51 0
7 62 81 0
4 9 87 0
1 5 -16 0
6 124 12 0
6 -12 -131 0
1 -6 -8 0
5 99 -126 0
2 -26 -44 0
4 -125 -115 0
1 52 126 0
5 142 -92 0
5 104 -43 0
1 -24 147 0
2 -4 -36 0
2 11 17 0
4 -61 109 0
10 74 -75 0
5 51 69 0
9 11 -70 0
7 -113 -14 0
3 10 20 0
5 -56 150 0
3 -16 -146 0
4 -104 76 0
8 1 129 0
8 -48 34 0
4 103 100 0
4 113 -99 0
3 -119 66 0
10 -66 -99 0
4 95 43 0
9 -118 -75 0
3 -77 -20 0
4 113 52 0
5 72 128 0
8 -28 -148 0
5 133 -13 0
9 102 -90 0
10 -97 73 0
9 147 81 0
9 100 4 0
4 -55 -95 0
3 -72 -2 0
9 149 -137 0
6 149 -52 0
4 -141 -87 0
3 10 56 0
6 -136 -11 0
9 -15 112 0
1 57 -124 0
2 -126 -44 0
1 -31 121 0
6 -22 17 0
4 -103 -74 0
5 -130 -100 0
3 110 -48 0
2 10 50 0
9 24 -91 0
6 -135 121 0
4 92 -77 0
8 -93 24 0
9 98 -74 0
3 24 -127 0
1 -24 94 0
3 -143 2 0
7 92 -142 0
9 -112 136 0
7 63 135 0
5 9 -141 0
9 65 -60 0
5 36 77 0
4 -20 29 0
3 30 -40 0
8 31 -42 0
3 28 -138 0
9 -122 -62 0
2 -53 -147 0
6 56 -120 0
4 47 128 0
10 -6 92 0
7 132 105 0
6 147 54 0
1 -42 51 0
2 -113 60 0
10 -56 -81 0
6 50 -39 0
4 16 53 0
1 145 -89 0
5 -44 64 0
10 118 144 0
5 45 29 0
3 88 -16 0
9 -96 -5 0
7 -44 9 0
3 -61 104 0
1 42 -137 0
4 -51 21 0
2 14 41 0
8 69 49 0
9 -65 87 0
1 92 -106 0
3 114 98 0
3 -51 -123 0
3 110 112 0
10 132 -4 0
6 44 -54 0
2 -103 118 0
1 54 -118 0
1 -73 33 0
5 130 23 0
1 -145 -140 0
8 -101 -150 0
1 -3 141 0
2 45 -129 0
9 97 126 0
10 -94 41 0
8 73 125 0
3 -147 -112 0
1 -101 54 0
2 -54 60 0
2 -51 -59 0
5 -38 -110 0
4 -86 106 0
10 146 130 0
2 -105 -97 0
7 -58 52 0
1 105 40 0
5 100 -43 0
8 -102 -16 0
9 -126 37 0
4 -143 -109 0
8 89 135 0
2 -81 -25 0
6 -76 88 0
1 128 -57 0
2 -100 103 0
1 119 -21 0
2 58 15 0
2 124 95 0
2 -79 93 0
7 -118 100 0
3 37 145 0
9 -52 113 0
7 65 17 0
5 -38 -94 0
7 -109 -133 0
7 -77 32 0
3 125 -98 0
9 -48 -13 0
7 -7 58 0
4 20 -39 0
1 -55 -112 0
2 55 95 0
8 -77 31 0
1 63 88 0
3 -36 -24 0
4 36 112 0
1 -20 116 0
7 -4 10 0
2 122 91 0
10 35 -37 0
10 -68 -135 0
10 73 -122 0
1 146 145 0
6 107 -59 0
10 24 25 0
2 -35 139 0
6 79 -87 0
1 124 72 0
4 56 -37 0
7 -9 38 0
8 32 -128 0
7 -36 108 0
5 -132 129 0
5 117 24 0
1 110 -54 0
2 -126 81 0
2 117 -144 0
3 -31 96 0
1 73 -12 0
8 120 -14 0
7 -143 -104 0
1 127 -138 0
9 41 11 0
4 92 143 0
1 137 56 0
2 -2 11 0
7 23 -130 0
2 -144 -49 0
8 -2 -59 0
8 47 -98 0
1 -109 85 0
8 -77 150 0
7 -56 140 0
2 -1 10 0
3 140 -12 0
7 -60 107 0
3 16 64 0
9 -12 -105 0
8 39 -102 0
7 101 127 0
6 117 -108 0
5 -118 -43 0
3 -54 -4 0
1 111 -58 0
10 122 -64 0
4 -19 36 0
2 138 -122 0
1 -99 51 0
6 9 -8 0
2 -50 -22 0
9 26 -21 0
3 -79 91 0
3 5 149 0
8 -35 135 0
6 -107 103 0
4 -4 55 0
9 -62 -2 0
3 23 69 0
5 90 132 0
7 73 -145 0
1 -143 101 0
6 85 30 0
4 -133 -9 0
8 -63 -65 0
7 -66 -135 0
7 -53 -1 0
4 133 19 0
9 -13 78 0
6 29 -82 0
2 111 -82 0
5 -91 100 0
1 -14 -75 0
6 59 -64 0
7 -64 3 0
1 -22 114 0
6 42 82 0
10 13 -72 0
3 4 -37 0
6 -136 -144 0
6 -69 -76 0
5 -139 97 0
4 -100 -44 0
8 7 49 0
7 -131 -44 0
1 -115 -2 0
4 38 33 0
10 27 -10 0
10 85 102 0
6 -49 -12 0
5 -55 73 0
6 -121 -124 0
6 -17 -79 0
10 -81 -61 0
10 -93 -11 0
4 20 -14 0
6 116 137 0
6 149 3 0
7 -76 133 0
5 -106 -76 0
1 -5 -91 0
8 1 -54 0
9 65 -44 0
2 57 128 0
4 114 -67 0
6 69 -50 0
2 33 -130 0
9 -55 36 0
6 -127 -66 0
4 120 46 0
5 -89 -135 0
2 112 -7 0
8 73 -55 0
8 -105 -53 0
10 -32 -24 0
5 -60 86 0
9 2 -138 0
3 34 -86 0
4 -70 122 0
8 -129 135 0
9 39 -144 0
8 -46 -27 0
3 51 -106 0
5 -42 9 0
8 147 10 0
2 96 18 0
8 140 -117 0
3 101 -2 0
8 -145 62 0
5 -88 -114 0
7 -70 -131 0
9 139 -94 0
3 104 17 0
6 34 14 0
10 -131 -109 0
6 111 -11 0
1 -72 55 0
1 -19 -113 0
5 93 -95 0
7 39 -52 0
5 68 -79 0
9 -93 105 0
8 63 117 0
3 -127 75 0
7 129 -124 0
8 -87 55 0
7 -150 133 0
5 34 -25 0
1 104 72 0
1 -26 -30 0
3 -146 -123 0
9 48 90 0
9 64 -79 0
5 133 -108 0
4 91 -139 0
6 -14 -51 0
7 123 -130 0
1 -9 132 0
8 -104 47 0
4 137 148 0
6 76 51 0
5 9 -79 0
2 68 -62 0
8 113 -148 0
10 -127 -61 0
2 -42 -18 0
4 -65 116 0
1 -113 24 0
3 -75 -2 0
8 81 -138 0
7 -50 104 0
7 -101 -127 0
7 38 -29 0
5 -47 -53 0
9 18 -72 0
3 96 113 0
2 -115 116 0
5 104 135 0
8 88 121 0
2 -98 -112 0
6 140 30 0
10 -83 -141 0
1 -62 9 0
4 122 -100 0
5 -65 132 0
4 116 22 0
9 -143 -36 0
1 -147 -59 0
5 89 142 0
7 -132 19 0
4 27 -51 0
10 -150 80 0
1 -61 64 0
6 -86 -105 0
7 141 -22 0
10 -81 96 0
8 87 146 0
10 -15 10 0
10 61 13 0
10 -92 124 0
8 37 -59 0
7 14 108 0
6 -130 70 0