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