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