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