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