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