-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathclauses.tmp
435 lines (435 loc) · 5.8 KB
/
clauses.tmp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
p cnf 616 434
3289 0
-3289 691 1894 923 0
2309 0
-2309 272 592 1208 552 1533 149 1386 290 0
2506 0
-2506 734 761 1231 841 307 210 789 1243 0
2299 0
-2299 619 141 895 0
3060 0
-3060 122 731 1152 1077 1657 0
3335 0
-3335 1516 0
2294 0
-2294 1914 1891 643 1429 613 1281 867 137 1253 0
2223 0
-2223 1845 1959 745 936 83 0
2224 0
-2224 1957 83 2052 458 1133 372 1444 0
3076 0
-3076 1184 0
2545 0
-2545 1756 324 913 343 1878 86 803 1583 1084 0
3353 0
-3353 180 0
2652 0
-2652 1922 1100 2030 1764 1343 463 350 0
2435 0
-2435 245 404 1037 1847 0
3228 0
-3228 566 1592 1914 1896 2008 0
3007 0
-3007 1771 1557 458 1121 1819 2011 130 0
2349 0
-2349 903 1310 1731 179 332 0
3321 0
-3321 1389 0
3261 0
-3261 678 0
2746 0
-2746 1411 745 581 931 1551 1619 0
3167 0
-3167 664 350 0
2748 0
-2748 62 855 548 1387 1529 1152 0
2511 0
-2511 311 378 319 762 190 659 1326 633 2074 1440 1761 0
3093 0
-3093 1159 1600 1230 1220 0
2603 0
-2603 1869 978 409 0
2925 0
-2925 1442 1360 2024 1721 1605 846 0
2883 0
-2883 1188 1831 1800 1244 739 763 1349 486 1462 1949 0
2340 0
-2340 1269 1339 1778 1373 171 386 0
2230 0
-2230 87 2091 444 1878 0
3159 0
-3159 1087 1764 1402 0
2525 0
-2525 619 323 1233 1397 0
3305 0
-3305 1941 0
2387 0
-2387 1033 789 209 1115 0
2953 0
-2953 918 0
3334 0
-3334 2041 0
3277 0
-3277 1801 2055 0
2855 0
-2855 728 770 881 2087 0
3361 0
-3361 1463 0
2734 0
-2734 2047 1653 232 2083 1631 1056 569 0
2943 0
-2943 896 901 1730 0
2955 0
-2955 924 1305 2071 148 1528 927 0
3058 0
-3058 943 1150 198 0
3098 0
-3098 132 713 640 1922 0
2938 0
-2938 520 886 1151 1646 0
2518 0
-2518 2 793 1978 477 317 0
2151 0
-2151 1012 31 74 1258 0
3171 0
-3171 1456 0
3197 0
-3197 1883 1121 0
3339 0
-3339 1331 0
3201 0
-3201 1565 0
2697 0
-2697 116 606 511 0
2989 0
-2989 1715 602 0
2821 0
-2821 1748 1026 859 1669 644 398 1735 777 976 0
3130 0
-3130 817 1947 1363 985 1649 0
2849 0
-2849 716 1738 1929 1504 1998 634 0
2971 0
-2971 966 0
2985 0
-2985 1412 1579 1856 1000 1186 1409 1941 0
2402 0
-2402 852 721 800 1636 217 1862 922 0
3279 0
-3279 1409 0
2967 0
-2967 1498 950 0
3139 0
-3139 1348 0
2198 0
-2198 65 1332 561 1661 102 476 815 430 322 887 0
2548 0
-2548 347 0
3324 0
-3324 1397 0
3181 0
-3181 1486 0
2325 0
-2325 499 456 94 783 161 0
2399 0
-2399 376 1887 108 825 1789 0
3211 0
-3211 1597 1762 152 1954 1657 172 322 0
2154 0
-2154 1717 244 958 1924 112 33 0
3319 0
-3319 837 0
2970 0
-2970 1170 1888 964 632 388 1649 1293 2086 1439 1038 741 996 1092 0
2485 0
-2485 1326 289 1319 1737 170 0
-691 690 0
-1894 1895 0
-923 922 0
-272 271 0
-592 591 0
-1208 1209 0
-552 551 0
-1533 1534 0
-149 150 0
-1386 1387 0
-290 289 0
-734 735 0
-761 760 0
-1231 1230 0
-841 840 0
-307 308 0
-210 209 0
-789 788 0
-1243 1242 0
-619 620 0
-141 142 0
-895 894 0
-122 121 0
-731 730 0
-1152 1153 0
-1077 1076 0
-1657 1658 0
-1516 1515 0
-1914 1913 0
-1891 1890 0
-643 644 0
-1429 1428 0
-613 614 0
-1281 1280 0
-867 866 0
-137 138 0
-1253 1252 0
-1845 1063 0
-1959 1960 0
-745 744 0
-936 937 0
-83 84 0
-1957 1958 0
-2052 2053 0
-458 457 0
-1133 1132 0
-372 371 0
-1444 1445 0
-1184 1185 0
-1756 1755 0
-324 323 0
-913 912 0
-343 344 0
-1878 1879 0
-86 85 0
-803 802 0
-1583 1584 0
-1084 1085 0
-180 179 0
-1922 1921 0
-1100 1101 0
-2030 2031 0
-1764 1763 0
-1343 1342 0
-463 464 0
-350 349 0
-245 246 0
-404 403 0
-1037 1036 0
-1847 1846 0
-566 565 0
-1592 1591 0
-1896 1897 0
-2008 2009 0
-1771 1772 0
-1557 1558 0
-1121 1120 0
-1819 1820 0
-2011 2010 0
-130 129 0
-903 902 0
-1310 1311 0
-1731 1732 0
-179 180 0
-332 331 0
-1389 1388 0
-678 677 0
-1411 1410 0
-581 582 0
-931 930 0
-1551 1552 0
-1619 1620 0
-664 663 0
-62 61 0
-855 854 0
-548 679 0
-1387 1386 0
-1529 1530 0
-311 312 0
-378 377 0
-319 320 0
-762 763 0
-190 189 0
-659 660 0
-1326 1327 0
-633 634 0
-2074 2073 0
-1440 1441 0
-1761 1762 0
-1159 1158 0
-1600 1599 0
-1230 1231 0
-1220 1221 0
-1869 1868 0
-978 979 0
-409 410 0
-1442 1443 0
-1360 1361 0
-2024 2025 0
-1721 1722 0
-1605 1606 0
-846 847 0
-1188 1189 0
-1831 1832 0
-1800 1801 0
-1244 1245 0
-739 738 0
-763 762 0
-1349 1348 0
-486 485 0
-1462 1463 0
-1949 1950 0
-1269 1268 0
-1339 1338 0
-1778 1779 0
-1373 1372 0
-171 172 0
-386 385 0
-87 88 0
-2091 2092 0
-444 443 0
-1087 1086 0
-1402 1403 0
-323 324 0
-1233 1232 0
-1397 1396 0
-1941 1942 0
-1033 1032 0
-209 210 0
-1115 1114 0
-918 919 0
-2041 2040 0
-1801 1800 0
-2055 2054 0
-728 729 0
-770 771 0
-881 880 0
-2087 2088 0
-1463 1462 0
-2047 2046 0
-1653 1654 0
-232 231 0
-2083 2084 0
-1631 1632 0
-1056 1057 0
-569 570 0
-896 897 0
-901 900 0
-1730 1729 0
-924 925 0
-1305 1304 0
-2071 2072 0
-148 147 0
-1528 1527 0
-927 926 0
-943 942 0
-1150 1151 0
-198 197 0
-132 131 0
-713 712 0
-640 639 0
-520 519 0
-886 887 0
-1151 1150 0
-1646 1645 0
-2 1 0
-793 792 0
-1978 1977 0
-477 478 0
-317 318 0
-1012 1013 0
-31 32 0
-74 73 0
-1258 1259 0
-1456 1457 0
-1883 1882 0
-1331 1330 0
-1565 1566 0
-116 115 0
-606 605 0
-511 512 0
-1715 1716 0
-602 601 0
-1748 1747 0
-1026 1027 0
-859 858 0
-1669 1670 0
-644 643 0
-398 397 0
-1735 1736 0
-777 776 0
-976 977 0
-817 816 0
-1947 1948 0
-1363 1362 0
-985 984 0
-1649 1650 0
-716 717 0
-1738 1737 0
-1929 1930 0
-1504 1503 0
-1998 1999 0
-634 633 0
-966 967 0
-1412 1413 0
-1579 1580 0
-1856 1857 0
-1000 1001 0
-1186 1187 0
-1409 1408 0
-852 853 0
-721 720 0
-800 801 0
-1636 1635 0
-217 218 0
-1862 1863 0
-922 923 0
-1498 1499 0
-950 951 0
-1348 1349 0
-65 66 0
-1332 1333 0
-561 562 0
-1661 1662 0
-102 101 0
-476 475 0
-815 814 0
-430 429 0
-322 321 0
-887 886 0
-347 348 0
-1486 1487 0
-499 500 0
-456 455 0
-94 93 0
-783 782 0
-161 162 0
-376 375 0
-1887 1886 0
-108 107 0
-825 824 0
-1789 1788 0
-1597 1598 0
-1762 1761 0
-152 151 0
-1954 1953 0
-172 171 0
-1717 1718 0
-244 243 0
-958 959 0
-1924 1923 0
-112 111 0
-33 34 0
-837 836 0
-1170 1171 0
-1888 1889 0
-964 965 0
-632 631 0
-388 387 0
-1293 1292 0
-2086 2085 0
-1439 1438 0
-1038 1039 0
-741 740 0
-996 997 0
-1092 1093 0
-289 290 0
-1319 1318 0
-1737 1738 0
-170 169 0