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