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