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