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