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