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