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