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