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