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