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