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