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