<filename>tests/sat/Models/c715.180.SAT.dimacs.test.py
input = """
c num blocks = 1
c num vars = 180
c minblockids[0] = 1
c maxblockids[0] = 180
p cnf 180 715
-122 80 -60 0
-96 -119 153 0
-22 -126 1 0
180 -123 -48 0
82 -38 -51 0
-116 -16 -174 0
108 103 -92 0
-77 63 -117 0
-118 -131 -52 0
139 38 57 0
107 99 -156 0
9 -45 -131 0
18 179 -15 0
-98 -106 44 0
-49 -140 -6 0
-122 -67 -26 0
164 -107 -152 0
157 55 -24 0
6 150 -142 0
106 52 161 0
-90 99 117 0
-121 29 134 0
102 134 -85 0
5 102 -149 0
76 48 55 0
59 111 -56 0
110 -163 -126 0
46 -20 89 0
15 141 -48 0
-2 63 65 0
71 82 78 0
19 -79 -7 0
111 178 -140 0
13 -86 30 0
114 41 -108 0
53 82 -14 0
159 -75 25 0
-64 177 109 0
123 7 121 0
69 149 90 0
-53 -178 -159 0
10 -158 144 0
-23 35 25 0
177 74 -46 0
-159 -26 55 0
69 49 -16 0
17 69 92 0
142 25 -169 0
88 -100 5 0
-40 -55 179 0
118 -76 136 0
112 -25 91 0
158 127 112 0
88 169 -1 0
129 -131 90 0
-27 144 -38 0
82 -174 -135 0
-54 1 -138 0
-152 -6 -80 0
166 38 78 0
141 -8 -40 0
-129 79 95 0
-17 129 110 0
-159 -62 129 0
155 -71 -118 0
41 37 -101 0
-50 -85 14 0
-8 136 133 0
-146 -119 175 0
-96 20 152 0
144 -168 19 0
-14 84 -38 0
175 -136 11 0
-129 19 -48 0
-73 -20 178 0
-170 -107 -104 0
8 -71 -170 0
-100 -101 15 0
-83 120 -128 0
-21 -152 75 0
-81 -65 75 0
71 108 -87 0
-148 163 60 0
179 36 143 0
95 -4 -141 0
-177 2 -129 0
164 105 113 0
2 -8 43 0
-104 106 114 0
12 61 48 0
-58 -128 84 0
-58 -12 -80 0
-137 -65 179 0
-21 -71 -16 0
79 -59 -41 0
-93 -89 -60 0
123 -81 141 0
173 100 -45 0
2 139 -92 0
-137 -19 -84 0
-76 -160 111 0
174 78 80 0
-10 -2 -41 0
-34 -115 -69 0
9 -150 82 0
1 122 59 0
168 136 -99 0
175 17 -61 0
-21 -103 -96 0
160 8 -55 0
75 20 90 0
41 -91 80 0
-67 175 19 0
-16 -10 -78 0
-122 14 -77 0
-1 141 114 0
-39 105 -137 0
39 73 -173 0
-123 150 -142 0
-14 -162 -70 0
137 61 -175 0
-59 -53 -95 0
-93 -113 94 0
152 99 147 0
152 -47 82 0
-92 26 144 0
57 -21 129 0
24 6 18 0
-64 -109 80 0
106 -177 128 0
-113 -103 46 0
-173 -46 39 0
-106 -65 -15 0
101 169 -19 0
65 90 -16 0
-69 85 29 0
111 -45 164 0
161 21 17 0
156 95 -139 0
14 -40 -76 0
-122 -77 -149 0
-85 -113 -68 0
142 -77 118 0
-161 -104 -132 0
-104 26 43 0
129 -59 126 0
-25 43 -13 0
-26 -69 71 0
-133 178 62 0
-27 -8 -85 0
21 -27 75 0
103 -122 110 0
179 164 -71 0
72 -43 -10 0
-56 -136 29 0
17 97 -9 0
32 114 -101 0
123 24 -15 0
172 145 -87 0
-171 150 50 0
80 23 -66 0
158 -88 59 0
32 9 -155 0
173 -32 -167 0
179 75 54 0
-81 123 125 0
-51 141 87 0
-31 -63 -65 0
-155 -105 12 0
-104 -55 -166 0
-31 -91 127 0
39 44 -35 0
179 100 -81 0
-147 108 -104 0
4 -117 25 0
153 7 69 0
54 27 118 0
24 -163 98 0
140 -2 -57 0
-47 137 -75 0
110 31 56 0
111 -21 -102 0
54 -129 -37 0
-74 132 -99 0
160 -112 32 0
-8 155 -129 0
100 43 -143 0
-141 114 61 0
104 -90 7 0
-166 -80 172 0
-79 80 100 0
-76 86 4 0
-23 -91 138 0
176 105 96 0
-135 114 -144 0
18 161 40 0
-156 95 155 0
38 -147 109 0
-106 94 177 0
9 172 65 0
46 174 -31 0
133 -166 106 0
-15 27 107 0
-141 -61 -92 0
98 -102 124 0
-14 91 61 0
99 168 -16 0
-24 -128 -33 0
-126 -6 -90 0
143 -41 31 0
172 173 -156 0
-144 -2 59 0
-157 125 -136 0
108 144 1 0
123 -90 -37 0
-168 -7 100 0
68 101 -103 0
-165 117 -15 0
-93 57 -157 0
63 -53 137 0
-19 -73 87 0
164 -84 45 0
-105 153 -140 0
-110 -115 138 0
-65 141 120 0
31 163 173 0
105 -76 127 0
21 -145 106 0
24 -17 15 0
25 -43 121 0
-137 33 50 0
111 -45 31 0
143 -147 6 0
58 -2 111 0
100 132 -145 0
-12 -137 46 0
-36 -18 139 0
109 -72 78 0
114 39 -3 0
-84 51 -92 0
-28 45 -164 0
-179 -109 -78 0
79 -18 112 0
-99 -149 36 0
-101 23 -1 0
127 -163 21 0
167 -102 178 0
-172 161 129 0
29 86 -32 0
-100 174 -121 0
9 -81 -179 0
61 76 -64 0
114 -80 -9 0
-6 -133 -112 0
22 -21 -27 0
179 -84 48 0
-137 -9 107 0
129 32 85 0
-62 45 -111 0
-29 -117 -105 0
-138 -70 173 0
60 -73 175 0
6 66 173 0
79 -99 -27 0
23 -103 -89 0
174 98 -163 0
13 48 -159 0
-48 -152 -94 0
15 10 -11 0
142 114 -140 0
-23 86 53 0
146 61 -108 0
66 70 -6 0
161 -54 110 0
-103 51 -59 0
-43 -127 -177 0
25 58 -154 0
-11 -92 48 0
4 -96 35 0
102 172 -116 0
32 117 -18 0
89 57 -171 0
107 99 -85 0
75 125 -150 0
-146 51 139 0
-154 -40 -145 0
-138 20 -31 0
-64 -1 -114 0
-60 53 117 0
-153 79 27 0
-68 -78 -135 0
-47 -101 49 0
-49 147 -120 0
91 123 -48 0
-76 87 -86 0
21 -81 9 0
-169 97 78 0
-25 105 -145 0
160 -118 153 0
-163 -55 88 0
17 -74 -8 0
-6 20 -37 0
-151 67 83 0
115 65 -100 0
55 135 -2 0
30 -146 10 0
5 -28 -44 0
127 110 -21 0
-46 -40 6 0
85 174 152 0
60 -63 156 0
-2 -132 -63 0
144 75 -123 0
133 85 159 0
75 -12 139 0
-56 172 -126 0
138 -179 -13 0
58 91 -4 0
124 -65 91 0
-94 4 -13 0
-59 10 -7 0
-39 21 -64 0
60 46 -24 0
-144 136 -73 0
175 -11 30 0
-71 -28 105 0
130 153 -48 0
-53 10 -109 0
175 98 -75 0
-23 79 8 0
179 83 51 0
-93 -95 121 0
92 14 73 0
155 68 -140 0
-135 59 -129 0
-34 -106 -7 0
72 75 126 0
115 137 66 0
-51 -2 174 0
-167 81 -164 0
42 6 63 0
164 -38 67 0
-74 149 64 0
-154 144 -41 0
50 125 80 0
-172 -69 144 0
74 -129 158 0
116 26 45 0
-113 4 -78 0
-13 12 -122 0
78 -9 -109 0
-22 -82 76 0
-161 86 -150 0
-175 37 160 0
26 122 44 0
-163 -119 124 0
179 -166 105 0
165 34 -16 0
43 -178 -33 0
-69 108 172 0
9 -174 65 0
-63 -154 66 0
32 -95 76 0
-92 -34 -170 0
-114 -85 100 0
109 34 -134 0
-151 -163 155 0
25 76 -115 0
-147 13 164 0
71 35 -63 0
-128 -19 69 0
119 98 124 0
92 167 99 0
100 -62 -161 0
174 101 -80 0
-106 104 71 0
-43 82 -10 0
149 92 -152 0
-74 66 -99 0
64 177 161 0
-121 -30 101 0
88 160 27 0
128 -27 160 0
74 -141 67 0
55 54 -44 0
62 -115 114 0
-88 -148 143 0
43 157 -37 0
65 -41 -108 0
89 101 -18 0
-60 124 154 0
-76 32 159 0
-135 -132 36 0
141 121 -109 0
-101 -161 145 0
39 -113 61 0
42 -49 -117 0
60 151 -131 0
37 -43 173 0
-8 -40 -52 0
-6 32 39 0
140 165 153 0
-5 153 36 0
147 156 134 0
91 -75 -31 0
124 -135 -120 0
-69 -173 115 0
28 -42 -114 0
-34 -39 63 0
113 -10 53 0
-50 -70 -43 0
80 20 -87 0
-52 -173 -135 0
4 -129 171 0
129 -141 -160 0
-96 -147 -146 0
118 -108 -83 0
-130 166 38 0
-167 47 -26 0
-164 151 40 0
131 -15 -126 0
4 -28 -101 0
-108 137 -21 0
106 -163 -100 0
115 -144 -69 0
116 -83 141 0
22 160 -25 0
-116 67 -64 0
-61 126 -46 0
133 65 150 0
-130 -59 103 0
-94 -85 -171 0
-6 135 -140 0
156 84 142 0
-105 177 154 0
112 28 99 0
-104 2 -3 0
-30 55 -141 0
40 -26 -121 0
-139 -155 130 0
88 75 165 0
-117 -116 74 0
-73 142 -169 0
122 -19 -78 0
161 -59 -99 0
-92 159 -4 0
-137 -171 -153 0
-111 91 -74 0
-70 48 -100 0
148 -18 -25 0
72 97 -165 0
-55 119 -17 0
-120 81 -143 0
70 -88 -23 0
65 112 116 0
-66 -97 86 0
137 -146 106 0
-83 34 81 0
114 -159 105 0
-148 -6 81 0
6 -165 -94 0
-136 -45 -17 0
-94 -30 -80 0
-134 -73 38 0
-7 10 -12 0
175 36 -151 0
-55 -12 -134 0
108 -8 -33 0
13 -180 -130 0
-53 -12 -168 0
-20 -107 -109 0
6 122 -3 0
-138 -65 118 0
21 -101 -81 0
17 141 -55 0
81 -88 53 0
63 72 -92 0
98 39 43 0
-123 -140 180 0
-29 79 -86 0
164 -119 42 0
49 -76 -170 0
-74 32 -137 0
-31 -123 164 0
-173 -30 -120 0
143 177 -134 0
15 89 26 0
45 -61 127 0
25 130 -102 0
66 42 59 0
-166 21 -27 0
-112 -13 -149 0
58 46 -34 0
-3 -65 -1 0
41 -101 -75 0
173 -125 -169 0
-71 21 -161 0
162 -119 148 0
-95 -174 1 0
-72 152 -120 0
-14 101 -34 0
-34 175 -152 0
-111 155 7 0
-49 -30 87 0
-64 85 -136 0
-172 -23 85 0
-55 148 -64 0
129 115 -35 0
61 25 -148 0
90 -72 -68 0
-151 176 -144 0
-111 100 -20 0
15 122 1 0
46 124 154 0
-132 87 172 0
-38 146 83 0
-137 -101 -161 0
-76 -18 166 0
139 -51 -19 0
76 -93 29 0
-114 125 12 0
79 -32 151 0
-87 -15 9 0
-141 127 -22 0
36 -94 33 0
148 28 173 0
-103 -21 168 0
81 -127 78 0
164 12 -25 0
-71 123 66 0
74 140 28 0
-128 -7 162 0
42 101 55 0
-180 114 -149 0
-43 42 177 0
20 66 -43 0
-92 129 78 0
-7 35 -104 0
-158 -38 -83 0
-79 135 60 0
-50 -102 -86 0
108 88 -102 0
-124 7 20 0
89 17 84 0
165 7 100 0
-158 -159 63 0
73 -158 -45 0
49 90 38 0
59 166 -16 0
-124 -138 52 0
-63 130 142 0
180 110 108 0
36 154 -142 0
109 108 -37 0
-118 -30 143 0
-111 26 86 0
-73 -22 -72 0
-117 156 -125 0
8 -107 52 0
-125 -99 25 0
2 158 5 0
138 -90 111 0
24 -50 27 0
-3 130 -7 0
132 -77 21 0
-51 -136 -134 0
148 112 125 0
-118 -6 58 0
53 106 -153 0
30 -40 108 0
-91 44 166 0
-29 -76 154 0
84 162 -52 0
130 68 95 0
57 -15 49 0
-152 -139 128 0
-69 158 -21 0
-20 -69 -99 0
-128 57 117 0
33 71 -63 0
125 -89 -134 0
-130 141 155 0
51 63 138 0
89 62 -57 0
170 164 -74 0
-34 -45 -21 0
103 161 60 0
71 126 106 0
-179 6 -104 0
77 -28 -24 0
-71 96 50 0
-144 6 9 0
-158 70 -43 0
15 -68 -13 0
-73 -70 -32 0
112 -174 19 0
-146 176 -124 0
-130 4 96 0
-173 71 -125 0
155 148 138 0
-140 -144 128 0
-118 -80 12 0
11 -76 40 0
60 -113 73 0
109 24 -150 0
-17 166 1 0
-106 -165 151 0
-36 -110 -120 0
166 150 158 0
-99 -71 134 0
-54 11 -136 0
32 -31 82 0
67 -29 69 0
-94 -8 -126 0
-13 28 -99 0
163 122 112 0
-27 -115 -105 0
-49 43 47 0
102 -139 -161 0
-35 127 136 0
-121 108 132 0
60 160 153 0
-126 163 -22 0
81 -85 -143 0
134 178 -59 0
-29 -10 -48 0
-37 -46 167 0
33 -124 109 0
-20 -45 -138 0
-157 105 101 0
2 144 -56 0
-101 -178 46 0
-123 -41 1 0
-155 -37 -82 0
170 39 73 0
175 -89 -168 0
92 -118 -122 0
154 161 22 0
30 -54 -56 0
-178 -72 46 0
5 174 -162 0
46 -56 -101 0
-63 -32 -62 0
20 -40 -56 0
10 111 101 0
20 -97 -99 0
8 -60 179 0
-16 37 27 0
-37 81 35 0
-27 -11 -107 0
-15 -18 -102 0
-56 -108 13 0
-68 3 58 0
100 -143 -51 0
13 166 -16 0
-136 -163 131 0
125 147 -150 0
-155 180 57 0
-172 -128 145 0
53 44 123 0
-117 -177 89 0
20 108 58 0
-94 -131 -105 0
46 -33 -87 0
-74 82 174 0
79 -163 125 0
-20 109 163 0
40 90 42 0
159 110 -154 0
-139 -73 40 0
-35 -15 -68 0
163 140 56 0
-115 84 158 0
175 3 -150 0
172 -70 164 0
-19 55 61 0
135 -82 126 0
-95 -150 48 0
109 -107 106 0
170 -111 -169 0
-2 -19 39 0
36 143 82 0
-65 -85 -32 0
89 171 74 0
-110 104 106 0
164 -97 -113 0
172 -168 30 0
28 -37 -126 0
-63 36 162 0
112 -162 41 0
-8 -180 -156 0
84 109 -137 0
93 -173 -154 0
53 -49 -50 0
-122 39 -99 0
-72 -60 37 0
154 49 75 0
145 152 -129 0
-143 -60 86 0
-176 94 -180 0
144 -151 131 0
-75 21 -114 0
-64 177 89 0
-83 82 -115 0
46 -91 -34 0
105 117 -146 0
139 -45 176 0
-154 -41 -163 0
-110 20 45 0
-121 136 -20 0
-126 -10 -13 0
139 39 -91 0
104 39 67 0
153 177 -103 0
-79 32 -63 0
"""

output = "SAT"
