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