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