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