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