mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
438 lines
5.3 KiB
INI
438 lines
5.3 KiB
INI
c This Formular is generated by mcnf
|
|
c
|
|
c horn? no
|
|
c forced? no
|
|
c mixed sat? no
|
|
c clause length = 3
|
|
c
|
|
p cnf 100 430
|
|
78 -94 66 0
|
|
38 24 31 0
|
|
-62 21 -46 0
|
|
66 -32 73 0
|
|
-10 62 -39 0
|
|
73 91 -45 0
|
|
-53 78 -21 0
|
|
92 -79 81 0
|
|
-22 41 36 0
|
|
-28 52 94 0
|
|
-17 -20 99 0
|
|
-60 -10 16 0
|
|
40 84 -11 0
|
|
-23 43 -27 0
|
|
-91 64 -20 0
|
|
-92 46 86 0
|
|
28 67 52 0
|
|
-75 87 28 0
|
|
-71 -29 91 0
|
|
-65 -77 90 0
|
|
51 53 -64 0
|
|
78 71 -38 0
|
|
74 -89 -71 0
|
|
50 44 -5 0
|
|
-66 -5 68 0
|
|
75 -40 82 0
|
|
9 -54 96 0
|
|
30 -57 -98 0
|
|
-77 7 -15 0
|
|
72 -12 60 0
|
|
-69 -42 -89 0
|
|
-75 89 -18 0
|
|
-79 -65 56 0
|
|
-46 41 -20 0
|
|
-15 93 78 0
|
|
23 -1 -88 0
|
|
-74 -25 -56 0
|
|
91 74 54 0
|
|
-60 -95 -59 0
|
|
46 69 72 0
|
|
-69 -65 -3 0
|
|
-23 49 -79 0
|
|
68 -31 -46 0
|
|
-39 37 89 0
|
|
76 -63 -12 0
|
|
-50 55 -18 0
|
|
-6 34 -41 0
|
|
57 -79 -11 0
|
|
-97 37 24 0
|
|
29 -9 -3 0
|
|
94 -4 -43 0
|
|
4 62 -87 0
|
|
24 1 -76 0
|
|
21 -99 11 0
|
|
-85 -13 53 0
|
|
75 -46 -11 0
|
|
-70 60 -28 0
|
|
53 -28 -73 0
|
|
2 82 -75 0
|
|
57 -11 71 0
|
|
16 -71 68 0
|
|
93 57 -84 0
|
|
-92 -65 -14 0
|
|
40 95 -57 0
|
|
72 -64 -93 0
|
|
65 89 60 0
|
|
56 8 4 0
|
|
25 -20 -81 0
|
|
-14 23 -68 0
|
|
51 -9 38 0
|
|
-32 16 100 0
|
|
39 2 23 0
|
|
59 66 -69 0
|
|
-12 -17 75 0
|
|
-53 -37 -20 0
|
|
-1 12 86 0
|
|
15 -41 -34 0
|
|
-86 -42 39 0
|
|
-6 -91 60 0
|
|
91 22 -82 0
|
|
-81 12 -73 0
|
|
97 -26 -16 0
|
|
5 48 40 0
|
|
86 -7 -10 0
|
|
-90 -78 100 0
|
|
33 69 23 0
|
|
-79 -31 60 0
|
|
93 65 -68 0
|
|
-52 94 -76 0
|
|
40 -28 41 0
|
|
-51 31 97 0
|
|
-7 15 61 0
|
|
87 -2 55 0
|
|
85 88 -99 0
|
|
86 -53 2 0
|
|
75 83 -27 0
|
|
55 33 18 0
|
|
-7 -43 25 0
|
|
-85 61 6 0
|
|
45 92 84 0
|
|
77 91 18 0
|
|
-60 93 68 0
|
|
16 -20 51 0
|
|
-59 66 -87 0
|
|
-96 94 -84 0
|
|
14 17 90 0
|
|
68 -80 20 0
|
|
-43 72 53 0
|
|
20 71 98 0
|
|
-99 30 -40 0
|
|
-83 -23 95 0
|
|
100 -21 94 0
|
|
52 -99 22 0
|
|
37 11 4 0
|
|
81 -16 -68 0
|
|
-99 -81 94 0
|
|
-52 73 -2 0
|
|
23 26 73 0
|
|
-64 28 10 0
|
|
-79 -61 -16 0
|
|
-98 -40 89 0
|
|
100 45 14 0
|
|
52 -39 -67 0
|
|
31 29 -12 0
|
|
87 5 -16 0
|
|
-93 -100 15 0
|
|
23 -91 -52 0
|
|
77 -44 -5 0
|
|
28 98 -39 0
|
|
25 28 -11 0
|
|
20 30 100 0
|
|
-24 11 58 0
|
|
-37 46 -29 0
|
|
8 11 96 0
|
|
-40 -72 -47 0
|
|
36 18 6 0
|
|
-42 43 37 0
|
|
-23 39 -84 0
|
|
50 -26 -7 0
|
|
64 -12 27 0
|
|
-86 97 -42 0
|
|
-18 -73 3 0
|
|
-93 94 -43 0
|
|
-73 94 -87 0
|
|
-34 2 70 0
|
|
85 -97 -27 0
|
|
-87 -6 30 0
|
|
93 52 95 0
|
|
-97 -1 -33 0
|
|
42 -15 -73 0
|
|
-42 -59 -81 0
|
|
-27 -71 74 0
|
|
-57 -53 85 0
|
|
91 -85 -14 0
|
|
-94 11 -8 0
|
|
51 63 42 0
|
|
-100 58 -98 0
|
|
-7 71 -9 0
|
|
5 12 81 0
|
|
12 -29 -60 0
|
|
2 -46 -44 0
|
|
-69 77 32 0
|
|
23 57 16 0
|
|
27 -53 -50 0
|
|
57 82 13 0
|
|
97 2 54 0
|
|
15 -14 -6 0
|
|
91 2 -13 0
|
|
-44 -60 -14 0
|
|
-77 25 -65 0
|
|
-98 -37 67 0
|
|
-80 91 25 0
|
|
-41 28 6 0
|
|
14 -78 -98 0
|
|
-11 48 89 0
|
|
40 -34 66 0
|
|
17 64 -34 0
|
|
45 90 98 0
|
|
-88 -57 -10 0
|
|
50 -94 -27 0
|
|
67 8 -97 0
|
|
76 -29 -44 0
|
|
-80 -15 82 0
|
|
10 52 -80 0
|
|
98 85 56 0
|
|
-88 90 31 0
|
|
65 98 73 0
|
|
-100 -87 57 0
|
|
-5 -74 71 0
|
|
47 90 92 0
|
|
-27 -2 4 0
|
|
-1 -51 25 0
|
|
-16 58 -18 0
|
|
-91 43 56 0
|
|
-69 -73 -38 0
|
|
-75 -1 54 0
|
|
5 59 90 0
|
|
-61 47 5 0
|
|
61 -9 85 0
|
|
-63 -40 -84 0
|
|
52 -75 59 0
|
|
44 -59 76 0
|
|
-80 48 -54 0
|
|
27 86 -81 0
|
|
22 -65 -91 0
|
|
63 16 66 0
|
|
39 -64 -78 0
|
|
-22 -76 13 0
|
|
48 -85 24 0
|
|
-80 18 -89 0
|
|
61 85 -69 0
|
|
45 -46 52 0
|
|
-87 -81 -23 0
|
|
-37 4 -67 0
|
|
-85 -11 80 0
|
|
-26 -41 -87 0
|
|
83 12 -38 0
|
|
82 21 78 0
|
|
-86 56 -39 0
|
|
-15 -100 -81 0
|
|
-96 -99 -2 0
|
|
74 75 81 0
|
|
-9 -90 -35 0
|
|
-21 80 11 0
|
|
29 46 -26 0
|
|
-70 35 -98 0
|
|
40 90 -65 0
|
|
-35 -10 -63 0
|
|
24 -17 -35 0
|
|
-60 5 -12 0
|
|
-85 -84 -82 0
|
|
94 -90 35 0
|
|
48 -100 70 0
|
|
-41 -13 60 0
|
|
35 94 -37 0
|
|
-4 90 -71 0
|
|
-56 -38 60 0
|
|
-97 100 50 0
|
|
91 57 58 0
|
|
76 -66 39 0
|
|
-99 -89 -35 0
|
|
-40 29 -16 0
|
|
-49 -15 -67 0
|
|
-42 71 -40 0
|
|
-45 96 37 0
|
|
-29 -6 -10 0
|
|
-42 14 11 0
|
|
-25 -61 44 0
|
|
74 -100 95 0
|
|
85 43 11 0
|
|
-42 54 -24 0
|
|
34 59 12 0
|
|
73 41 85 0
|
|
40 6 41 0
|
|
-50 4 82 0
|
|
79 65 -61 0
|
|
1 -49 -37 0
|
|
37 -66 93 0
|
|
63 -23 31 0
|
|
42 -7 -53 0
|
|
-30 46 -41 0
|
|
69 -49 -5 0
|
|
57 98 63 0
|
|
75 -81 68 0
|
|
55 26 -30 0
|
|
82 -79 -43 0
|
|
-78 38 40 0
|
|
80 99 -43 0
|
|
23 -99 -55 0
|
|
-82 8 -88 0
|
|
35 47 -92 0
|
|
-40 -77 52 0
|
|
80 -77 -73 0
|
|
-51 -93 -14 0
|
|
60 82 100 0
|
|
17 -73 -52 0
|
|
78 -16 66 0
|
|
59 77 20 0
|
|
90 56 -5 0
|
|
-95 93 -62 0
|
|
99 -56 72 0
|
|
38 -42 -62 0
|
|
-46 -28 35 0
|
|
-78 -48 95 0
|
|
62 45 -21 0
|
|
-22 -37 -16 0
|
|
40 24 -21 0
|
|
-59 72 -18 0
|
|
33 -13 -23 0
|
|
-56 -57 -17 0
|
|
-36 -1 -92 0
|
|
-31 33 1 0
|
|
-42 -92 98 0
|
|
-34 18 46 0
|
|
29 -1 -97 0
|
|
-1 -12 -76 0
|
|
-70 94 1 0
|
|
-96 86 26 0
|
|
-26 78 -28 0
|
|
11 63 74 0
|
|
-83 8 62 0
|
|
27 70 -18 0
|
|
-61 35 -48 0
|
|
97 52 71 0
|
|
-98 33 -67 0
|
|
-21 -22 -82 0
|
|
7 6 -52 0
|
|
86 -93 -25 0
|
|
-27 -76 4 0
|
|
-1 -97 -58 0
|
|
41 -88 -19 0
|
|
-4 -75 3 0
|
|
-45 85 28 0
|
|
21 45 -82 0
|
|
49 41 77 0
|
|
4 -48 -31 0
|
|
20 74 -75 0
|
|
-57 73 -58 0
|
|
-91 -63 -21 0
|
|
53 34 2 0
|
|
73 -44 58 0
|
|
-2 84 1 0
|
|
50 62 2 0
|
|
82 36 -6 0
|
|
-63 -60 -25 0
|
|
74 -61 -8 0
|
|
-58 66 -57 0
|
|
-87 -91 -25 0
|
|
32 -79 6 0
|
|
-29 44 -74 0
|
|
18 82 -23 0
|
|
-98 69 -52 0
|
|
17 14 -83 0
|
|
11 -33 59 0
|
|
30 -99 -83 0
|
|
-64 -69 -72 0
|
|
73 92 -52 0
|
|
-17 63 -92 0
|
|
79 14 -26 0
|
|
-77 -59 93 0
|
|
49 25 13 0
|
|
-3 84 99 0
|
|
33 23 8 0
|
|
17 1 -25 0
|
|
37 -15 -13 0
|
|
-74 23 99 0
|
|
-93 -46 91 0
|
|
-33 22 -43 0
|
|
74 -44 78 0
|
|
-52 -96 45 0
|
|
55 92 16 0
|
|
33 -79 17 0
|
|
58 -11 -38 0
|
|
54 -41 25 0
|
|
63 -8 -2 0
|
|
25 -43 -62 0
|
|
-66 15 -74 0
|
|
99 -95 63 0
|
|
16 -48 70 0
|
|
46 42 33 0
|
|
-18 74 64 0
|
|
75 -81 -60 0
|
|
-100 -62 -91 0
|
|
-92 -13 34 0
|
|
87 98 54 0
|
|
40 62 -77 0
|
|
48 -16 72 0
|
|
-4 63 -96 0
|
|
80 -16 -5 0
|
|
-25 -63 -55 0
|
|
-81 21 61 0
|
|
48 -72 -17 0
|
|
54 -83 -43 0
|
|
42 -56 -84 0
|
|
-3 -94 23 0
|
|
56 53 25 0
|
|
18 -57 -20 0
|
|
-15 -29 -81 0
|
|
25 -19 -14 0
|
|
-69 67 76 0
|
|
95 -79 99 0
|
|
-68 13 65 0
|
|
-86 61 69 0
|
|
25 -44 64 0
|
|
20 95 11 0
|
|
-97 40 -24 0
|
|
-4 -12 -79 0
|
|
11 -20 -31 0
|
|
73 -29 93 0
|
|
-44 -51 7 0
|
|
-59 -66 87 0
|
|
-73 61 -47 0
|
|
15 -22 -17 0
|
|
-100 24 -11 0
|
|
4 91 -18 0
|
|
57 -3 52 0
|
|
79 57 -70 0
|
|
22 -23 -2 0
|
|
21 -68 77 0
|
|
98 -63 -15 0
|
|
-1 -30 62 0
|
|
61 -52 4 0
|
|
10 98 34 0
|
|
64 -58 69 0
|
|
-65 86 -91 0
|
|
39 -2 -93 0
|
|
47 14 -18 0
|
|
-61 -53 92 0
|
|
-94 -28 -85 0
|
|
-90 32 -59 0
|
|
44 49 60 0
|
|
2 96 -27 0
|
|
13 -5 -22 0
|
|
33 -92 -13 0
|
|
91 43 12 0
|
|
-8 67 71 0
|
|
81 5 -16 0
|
|
-77 37 -65 0
|
|
-84 -73 54 0
|
|
-77 80 -51 0
|
|
-11 36 40 0
|
|
1 -84 -47 0
|
|
76 -67 7 0
|
|
-3 49 21 0
|
|
64 21 91 0
|
|
88 20 -56 0
|
|
70 1 42 0
|
|
-87 93 -99 0
|
|
-41 -35 -13 0
|
|
-73 -55 -78 0
|