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