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