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