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