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