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