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