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