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