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