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