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