]> matita.cs.unibo.it Git - helm.git/blob - matita/tests/TPTP/log.300.26-5.menvcorti.con_rating
tagged 0.5.0-rc1
[helm.git] / matita / tests / TPTP / log.300.26-5.menvcorti.con_rating
1 Unsatisfiable/COL023-1.ma ... FAIL (* Rating : 0.00 
2 Unsatisfiable/COL027-1.ma ... FAIL (* Rating : 0.00 
3 Unsatisfiable/COL029-1.ma ... FAIL (* Rating : 0.00 
4 Unsatisfiable/COL031-1.ma ... FAIL (* Rating : 0.00 
5 Unsatisfiable/COL039-1.ma ... FAIL (* Rating : 0.00 
6 Unsatisfiable/COL052-1.ma ... FAIL (* Rating : 0.00 
7 Unsatisfiable/COL053-1.ma ... FAIL (* Rating : 0.00 
8 Unsatisfiable/COL059-1.ma ... FAIL (* Rating : 0.00 
9 Unsatisfiable/GRP170-1.ma ... FAIL (* Rating : 0.00 
10 Unsatisfiable/GRP170-2.ma ... FAIL (* Rating : 0.00 
11 Unsatisfiable/GRP170-3.ma ... FAIL (* Rating : 0.00 
12 Unsatisfiable/GRP170-4.ma ... FAIL (* Rating : 0.00 
13 Unsatisfiable/GRP195-1.ma ... FAIL (* Rating : 0.00 
14 Unsatisfiable/GRP415-1.ma ... FAIL (* Rating : 0.00 
15 Unsatisfiable/LAT010-1.ma ... FAIL (* Rating : 0.00 
16 Unsatisfiable/LAT021-1.ma ... FAIL (* Rating : 0.00 
17 Unsatisfiable/LCL162-1.ma ... FAIL (* Rating : 0.00 
18 Unsatisfiable/BOO026-1.ma ... FAIL (* Rating : 0.07 
19 Unsatisfiable/BOO028-1.ma ... FAIL (* Rating : 0.07 
20 Unsatisfiable/BOO072-1.ma ... FAIL (* Rating : 0.07 
21 Unsatisfiable/BOO074-1.ma ... FAIL (* Rating : 0.07 
22 Unsatisfiable/COL002-4.ma ... FAIL (* Rating : 0.07 
23 Unsatisfiable/COL020-1.ma ... FAIL (* Rating : 0.07 
24 Unsatisfiable/COL026-1.ma ... FAIL (* Rating : 0.07 
25 Unsatisfiable/COL033-1.ma ... FAIL (* Rating : 0.07 
26 Unsatisfiable/COL070-1.ma ... FAIL (* Rating : 0.07 
27 Unsatisfiable/GRP122-1.ma ... FAIL (* Rating : 0.07 
28 Unsatisfiable/GRP185-1.ma ... FAIL (* Rating : 0.07 
29 Unsatisfiable/GRP185-2.ma ... FAIL (* Rating : 0.07 
30 Unsatisfiable/GRP413-1.ma ... FAIL (* Rating : 0.07 
31 Unsatisfiable/GRP414-1.ma ... FAIL (* Rating : 0.07 
32 Unsatisfiable/GRP416-1.ma ... FAIL (* Rating : 0.07 
33 Unsatisfiable/GRP418-1.ma ... FAIL (* Rating : 0.07 
34 Unsatisfiable/GRP425-1.ma ... FAIL (* Rating : 0.07 
35 Unsatisfiable/GRP443-1.ma ... FAIL (* Rating : 0.07 
36 Unsatisfiable/LAT011-1.ma ... FAIL (* Rating : 0.07 
37 Unsatisfiable/COL030-1.ma ... FAIL (* Rating : 0.14 
38 Unsatisfiable/COL032-1.ma ... FAIL (* Rating : 0.14 
39 Unsatisfiable/COL035-1.ma ... FAIL (* Rating : 0.14 
40 Unsatisfiable/COL042-6.ma ... FAIL (* Rating : 0.14 
41 Unsatisfiable/COL042-7.ma ... FAIL (* Rating : 0.14 
42 Unsatisfiable/COL042-8.ma ... FAIL (* Rating : 0.14 
43 Unsatisfiable/COL042-9.ma ... FAIL (* Rating : 0.14 
44 Unsatisfiable/GRP014-1.ma ... FAIL (* Rating : 0.14 
45 Unsatisfiable/GRP178-1.ma ... FAIL (* Rating : 0.14 
46 Unsatisfiable/GRP178-2.ma ... FAIL (* Rating : 0.14 
47 Unsatisfiable/GRP184-2.ma ... FAIL (* Rating : 0.14 
48 Unsatisfiable/GRP417-1.ma ... FAIL (* Rating : 0.14 
49 Unsatisfiable/GRP421-1.ma ... FAIL (* Rating : 0.14 
50 Unsatisfiable/GRP426-1.ma ... FAIL (* Rating : 0.14 
51 Unsatisfiable/GRP429-1.ma ... FAIL (* Rating : 0.14 
52 Unsatisfiable/GRP442-1.ma ... FAIL (* Rating : 0.14 
53 Unsatisfiable/GRP502-1.ma ... FAIL (* Rating : 0.14 
54 Unsatisfiable/GRP503-1.ma ... FAIL (* Rating : 0.14 
55 Unsatisfiable/GRP504-1.ma ... FAIL (* Rating : 0.14 
56 Unsatisfiable/LAT044-1.ma ... FAIL (* Rating : 0.14 
57 Unsatisfiable/LAT168-1.ma ... FAIL (* Rating : 0.14 
58 Unsatisfiable/RNG021-6.ma ... FAIL (* Rating : 0.14 
59 Unsatisfiable/BOO031-1.ma ... FAIL (* Rating : 0.21 
60 Unsatisfiable/BOO067-1.ma ... FAIL (* Rating : 0.21 
61 Unsatisfiable/COL044-1.ma ... FAIL (* Rating : 0.21 
62 Unsatisfiable/GRP177-2.ma ... FAIL (* Rating : 0.21 
63 Unsatisfiable/GRP184-3.ma ... FAIL (* Rating : 0.21 
64 Unsatisfiable/GRP185-3.ma ... FAIL (* Rating : 0.21 
65 Unsatisfiable/GRP185-4.ma ... FAIL (* Rating : 0.21 
66 Unsatisfiable/GRP203-1.ma ... FAIL (* Rating : 0.21 
67 Unsatisfiable/GRP444-1.ma ... FAIL (* Rating : 0.21 
68 Unsatisfiable/LAT022-1.ma ... FAIL (* Rating : 0.21 
69 Unsatisfiable/LAT023-1.ma ... FAIL (* Rating : 0.21 
70 Unsatisfiable/LCL138-1.ma ... FAIL (* Rating : 0.21 
71 Unsatisfiable/RNG019-6.ma ... FAIL (* Rating : 0.21 
72 Unsatisfiable/RNG019-7.ma ... FAIL (* Rating : 0.21 
73 Unsatisfiable/RNG020-7.ma ... FAIL (* Rating : 0.21 
74 Unsatisfiable/RNG021-7.ma ... FAIL (* Rating : 0.21 
75 Unsatisfiable/COL037-1.ma ... FAIL (* Rating : 0.29 
76 Unsatisfiable/COL049-1.ma ... FAIL (* Rating : 0.29 
77 Unsatisfiable/GRP184-1.ma ... FAIL (* Rating : 0.29 
78 Unsatisfiable/GRP200-1.ma ... FAIL (* Rating : 0.29 
79 Unsatisfiable/GRP419-1.ma ... FAIL (* Rating : 0.29 
80 Unsatisfiable/GRP422-1.ma ... FAIL (* Rating : 0.29 
81 Unsatisfiable/RNG020-6.ma ... FAIL (* Rating : 0.29 
82 Unsatisfiable/RNG025-4.ma ... FAIL (* Rating : 0.29 
83 Unsatisfiable/RNG025-6.ma ... FAIL (* Rating : 0.29 
84 Unsatisfiable/BOO073-1.ma ... FAIL (* Rating : 0.36 
85 Unsatisfiable/COL011-1.ma ... FAIL (* Rating : 0.36 
86 Unsatisfiable/COL041-1.ma ... FAIL (* Rating : 0.36 
87 Unsatisfiable/COL057-1.ma ... FAIL (* Rating : 0.36 
88 Unsatisfiable/COL060-1.ma ... FAIL (* Rating : 0.36 
89 Unsatisfiable/COL061-1.ma ... FAIL (* Rating : 0.36 
90 Unsatisfiable/GRP179-3.ma ... FAIL (* Rating : 0.36 
91 Unsatisfiable/GRP183-4.ma ... FAIL (* Rating : 0.36 
92 Unsatisfiable/GRP186-2.ma ... FAIL (* Rating : 0.36 
93 Unsatisfiable/GRP201-1.ma ... FAIL (* Rating : 0.36 
94 Unsatisfiable/GRP420-1.ma ... FAIL (* Rating : 0.36 
95 Unsatisfiable/GRP423-1.ma ... FAIL (* Rating : 0.36 
96 Unsatisfiable/LAT080-1.ma ... FAIL (* Rating : 0.36 
97 Unsatisfiable/LAT083-1.ma ... FAIL (* Rating : 0.36 
98 Unsatisfiable/LAT092-1.ma ... FAIL (* Rating : 0.36 
99 Unsatisfiable/LAT094-1.ma ... FAIL (* Rating : 0.36 
100 Unsatisfiable/LAT096-1.ma ... FAIL (* Rating : 0.36 
101 Unsatisfiable/LAT097-1.ma ... FAIL (* Rating : 0.36 
102 Unsatisfiable/RNG025-5.ma ... FAIL (* Rating : 0.36 
103 Unsatisfiable/COL002-5.ma ... FAIL (* Rating : 0.43 
104 Unsatisfiable/COL034-1.ma ... FAIL (* Rating : 0.43 
105 Unsatisfiable/GRP167-4.ma ... FAIL (* Rating : 0.43 
106 Unsatisfiable/GRP180-2.ma ... FAIL (* Rating : 0.43 
107 Unsatisfiable/GRP183-1.ma ... FAIL (* Rating : 0.43 
108 Unsatisfiable/GRP183-2.ma ... FAIL (* Rating : 0.43 
109 Unsatisfiable/GRP183-3.ma ... FAIL (* Rating : 0.43 
110 Unsatisfiable/GRP202-1.ma ... FAIL (* Rating : 0.43 
111 Unsatisfiable/GRP205-1.ma ... FAIL (* Rating : 0.43 
112 Unsatisfiable/LAT038-1.ma ... FAIL (* Rating : 0.43 
113 Unsatisfiable/LAT087-1.ma ... FAIL (* Rating : 0.43 
114 Unsatisfiable/LAT093-1.ma ... FAIL (* Rating : 0.43 
115 Unsatisfiable/LAT095-1.ma ... FAIL (* Rating : 0.43 
116 Unsatisfiable/RNG025-7.ma ... FAIL (* Rating : 0.43 
117 Unsatisfiable/BOO023-1.ma ... FAIL (* Rating : 0.50 
118 Unsatisfiable/COL044-7.ma ... FAIL (* Rating : 0.50 
119 Unsatisfiable/COL062-1.ma ... FAIL (* Rating : 0.50 
120 Unsatisfiable/COL063-1.ma ... FAIL (* Rating : 0.50 
121 Unsatisfiable/GRP024-5.ma ... FAIL (* Rating : 0.50 
122 Unsatisfiable/GRP167-3.ma ... FAIL (* Rating : 0.50 
123 Unsatisfiable/GRP179-1.ma ... FAIL (* Rating : 0.50 
124 Unsatisfiable/GRP179-2.ma ... FAIL (* Rating : 0.50 
125 Unsatisfiable/GRP180-1.ma ... FAIL (* Rating : 0.50 
126 Unsatisfiable/GRP505-1.ma ... FAIL (* Rating : 0.50 
127 Unsatisfiable/LAT020-1.ma ... FAIL (* Rating : 0.50 
128 Unsatisfiable/LAT084-1.ma ... FAIL (* Rating : 0.50 
129 Unsatisfiable/LAT086-1.ma ... FAIL (* Rating : 0.50 
130 Unsatisfiable/LAT171-1.ma ... FAIL (* Rating : 0.50 
131 Unsatisfiable/RNG009-5.ma ... FAIL (* Rating : 0.50 
132 Unsatisfiable/RNG009-7.ma ... FAIL (* Rating : 0.50 
133 Unsatisfiable/RNG026-7.ma ... FAIL (* Rating : 0.50 
134 Unsatisfiable/COL004-1.ma ... FAIL (* Rating : 0.57 
135 Unsatisfiable/COL006-1.ma ... FAIL (* Rating : 0.57 
136 Unsatisfiable/COL036-1.ma ... FAIL (* Rating : 0.57 
137 Unsatisfiable/GRP186-1.ma ... FAIL (* Rating : 0.57 
138 Unsatisfiable/GRP507-1.ma ... FAIL (* Rating : 0.57 
139 Unsatisfiable/GRP508-1.ma ... FAIL (* Rating : 0.57 
140 Unsatisfiable/LAT081-1.ma ... FAIL (* Rating : 0.57 
141 Unsatisfiable/LAT085-1.ma ... FAIL (* Rating : 0.57 
142 Unsatisfiable/RNG026-6.ma ... FAIL (* Rating : 0.57 
143 Unsatisfiable/COL006-5.ma ... FAIL (* Rating : 0.64 
144 Unsatisfiable/COL006-6.ma ... FAIL (* Rating : 0.64 
145 Unsatisfiable/COL006-7.ma ... FAIL (* Rating : 0.64 
146 Unsatisfiable/COL038-1.ma ... FAIL (* Rating : 0.64 
147 Unsatisfiable/COL044-6.ma ... FAIL (* Rating : 0.64 
148 Unsatisfiable/COL044-9.ma ... FAIL (* Rating : 0.64 
149 Unsatisfiable/COL046-1.ma ... FAIL (* Rating : 0.64 
150 Unsatisfiable/COL064-1.ma ... FAIL (* Rating : 0.64 
151 Unsatisfiable/GRP187-1.ma ... FAIL (* Rating : 0.64 
152 Unsatisfiable/GRP506-1.ma ... FAIL (* Rating : 0.64 
153 Unsatisfiable/LAT082-1.ma ... FAIL (* Rating : 0.64 
154 Unsatisfiable/LAT142-1.ma ... FAIL (* Rating : 0.64 
155 Unsatisfiable/LAT160-1.ma ... FAIL (* Rating : 0.64 
156 Unsatisfiable/BOO076-1.ma ... FAIL (* Rating : 0.71 
157 Unsatisfiable/COL043-3.ma ... FAIL (* Rating : 0.71 
158 Unsatisfiable/COL044-8.ma ... FAIL (* Rating : 0.71 
159 Unsatisfiable/COL065-1.ma ... FAIL (* Rating : 0.71 
160 Unsatisfiable/GRP181-1.ma ... FAIL (* Rating : 0.71 
161 Unsatisfiable/GRP181-2.ma ... FAIL (* Rating : 0.71 
162 Unsatisfiable/LAT148-1.ma ... FAIL (* Rating : 0.71 
163 Unsatisfiable/COL003-1.ma ... FAIL (* Rating : 0.79 
164 Unsatisfiable/LAT146-1.ma ... FAIL (* Rating : 0.79 
165 Unsatisfiable/LAT147-1.ma ... FAIL (* Rating : 0.79 
166 Unsatisfiable/LAT152-1.ma ... FAIL (* Rating : 0.79 
167 Unsatisfiable/LAT154-1.ma ... FAIL (* Rating : 0.79 
168 Unsatisfiable/LAT170-1.ma ... FAIL (* Rating : 0.79 
169 Unsatisfiable/LAT174-1.ma ... FAIL (* Rating : 0.79 
170 Unsatisfiable/COL042-1.ma ... FAIL (* Rating : 0.86 
171 Unsatisfiable/COL043-1.ma ... FAIL (* Rating : 0.86 
172 Unsatisfiable/LAT144-1.ma ... FAIL (* Rating : 0.86 
173 Unsatisfiable/LAT150-1.ma ... FAIL (* Rating : 0.86 
174 Unsatisfiable/LAT151-1.ma ... FAIL (* Rating : 0.86 
175 Unsatisfiable/LAT155-1.ma ... FAIL (* Rating : 0.86 
176 Unsatisfiable/LAT157-1.ma ... FAIL (* Rating : 0.86 
177 Unsatisfiable/LAT159-1.ma ... FAIL (* Rating : 0.86 
178 Unsatisfiable/LAT162-1.ma ... FAIL (* Rating : 0.86 
179 Unsatisfiable/LAT169-1.ma ... FAIL (* Rating : 0.86 
180 Unsatisfiable/RNG027-5.ma ... FAIL (* Rating : 0.86 
181 Unsatisfiable/RNG027-7.ma ... FAIL (* Rating : 0.86 
182 Unsatisfiable/RNG027-8.ma ... FAIL (* Rating : 0.86 
183 Unsatisfiable/RNG027-9.ma ... FAIL (* Rating : 0.86 
184 Unsatisfiable/RNG028-5.ma ... FAIL (* Rating : 0.86 
185 Unsatisfiable/RNG028-7.ma ... FAIL (* Rating : 0.86 
186 Unsatisfiable/RNG028-8.ma ... FAIL (* Rating : 0.86 
187 Unsatisfiable/RNG028-9.ma ... FAIL (* Rating : 0.86 
188 Unsatisfiable/RNG029-5.ma ... FAIL (* Rating : 0.86 
189 Unsatisfiable/RNG029-6.ma ... FAIL (* Rating : 0.86 
190 Unsatisfiable/RNG029-7.ma ... FAIL (* Rating : 0.86 
191 Unsatisfiable/RNG035-7.ma ... FAIL (* Rating : 0.86 
192 Unsatisfiable/ROB006-1.ma ... FAIL (* Rating : 0.86 
193 Unsatisfiable/ROB026-1.ma ... FAIL (* Rating : 0.86 
194 Unsatisfiable/COL066-1.ma ... FAIL (* Rating : 0.93 
195 Unsatisfiable/GRP164-1.ma ... FAIL (* Rating : 0.93 
196 Unsatisfiable/GRP164-2.ma ... FAIL (* Rating : 0.93 
197 Unsatisfiable/GRP196-1.ma ... FAIL (* Rating : 0.93 
198 Unsatisfiable/LAT018-1.ma ... FAIL (* Rating : 0.93 
199 Unsatisfiable/LAT070-1.ma ... FAIL (* Rating : 0.93 
200 Unsatisfiable/LAT145-1.ma ... FAIL (* Rating : 0.93 
201 Unsatisfiable/LAT149-1.ma ... FAIL (* Rating : 0.93 
202 Unsatisfiable/LAT153-1.ma ... FAIL (* Rating : 0.93 
203 Unsatisfiable/LAT158-1.ma ... FAIL (* Rating : 0.93 
204 Unsatisfiable/LAT163-1.ma ... FAIL (* Rating : 0.93 
205 Unsatisfiable/LAT164-1.ma ... FAIL (* Rating : 0.93 
206 Unsatisfiable/LAT165-1.ma ... FAIL (* Rating : 0.93 
207 Unsatisfiable/LAT166-1.ma ... FAIL (* Rating : 0.93 
208 Unsatisfiable/LAT167-1.ma ... FAIL (* Rating : 0.93 
209 Unsatisfiable/LAT172-1.ma ... FAIL (* Rating : 0.93 
210 Unsatisfiable/LAT173-1.ma ... FAIL (* Rating : 0.93 
211 Unsatisfiable/LAT175-1.ma ... FAIL (* Rating : 0.93 
212 Unsatisfiable/LAT176-1.ma ... FAIL (* Rating : 0.93 
213 Unsatisfiable/LAT072-1.ma ... FAIL (* Rating : 1.00 
214 Unsatisfiable/LAT074-1.ma ... FAIL (* Rating : 1.00 
215 Unsatisfiable/LAT075-1.ma ... FAIL (* Rating : 1.00 
216 Unsatisfiable/LAT076-1.ma ... FAIL (* Rating : 1.00 
217 Unsatisfiable/LAT077-1.ma ... FAIL (* Rating : 1.00 
218 Unsatisfiable/LAT078-1.ma ... FAIL (* Rating : 1.00 
219 Unsatisfiable/LAT079-1.ma ... FAIL (* Rating : 1.00 
220 Unsatisfiable/LAT138-1.ma ... FAIL (* Rating : 1.00 
221 Unsatisfiable/LAT139-1.ma ... FAIL (* Rating : 1.00 
222 Unsatisfiable/LAT140-1.ma ... FAIL (* Rating : 1.00 
223 Unsatisfiable/LAT141-1.ma ... FAIL (* Rating : 1.00 
224 Unsatisfiable/LAT161-1.ma ... FAIL (* Rating : 1.00 
225 Unsatisfiable/LAT177-1.ma ... FAIL (* Rating : 1.00 
226 Unsatisfiable/ROB001-1.ma ... FAIL (* Rating : 1.00 
227 Unsatisfiable/BOO029-1.ma ... OK (* Rating : 0.00 
228 Unsatisfiable/COL051-1.ma ... OK (* Rating : 0.00 
229 Unsatisfiable/COL058-1.ma ... OK (* Rating : 0.00 
230 Unsatisfiable/COL075-2.ma ... OK (* Rating : 0.00 
231 Unsatisfiable/GRP119-1.ma ... OK (* Rating : 0.00 
232 Unsatisfiable/GRP120-1.ma ... OK (* Rating : 0.00 
233 Unsatisfiable/GRP121-1.ma ... OK (* Rating : 0.00 
234 Unsatisfiable/GRP427-1.ma ... OK (* Rating : 0.00 
235 Unsatisfiable/GRP428-1.ma ... OK (* Rating : 0.00 
236 Unsatisfiable/GRP430-1.ma ... OK (* Rating : 0.00 
237 Unsatisfiable/GRP433-1.ma ... OK (* Rating : 0.00 
238 Unsatisfiable/GRP445-1.ma ... OK (* Rating : 0.00 
239 Unsatisfiable/GRP446-1.ma ... OK (* Rating : 0.00 
240 Unsatisfiable/GRP448-1.ma ... OK (* Rating : 0.00 
241 Unsatisfiable/GRP449-1.ma ... OK (* Rating : 0.00 
242 Unsatisfiable/GRP451-1.ma ... OK (* Rating : 0.00 
243 Unsatisfiable/GRP461-1.ma ... OK (* Rating : 0.00 
244 Unsatisfiable/GRP462-1.ma ... OK (* Rating : 0.00 
245 Unsatisfiable/GRP464-1.ma ... OK (* Rating : 0.00 
246 Unsatisfiable/GRP465-1.ma ... OK (* Rating : 0.00 
247 Unsatisfiable/GRP466-1.ma ... OK (* Rating : 0.00 
248 Unsatisfiable/GRP482-1.ma ... OK (* Rating : 0.00 
249 Unsatisfiable/GRP483-1.ma ... OK (* Rating : 0.00 
250 Unsatisfiable/GRP499-1.ma ... OK (* Rating : 0.00 
251 Unsatisfiable/GRP521-1.ma ... OK (* Rating : 0.00 
252 Unsatisfiable/GRP522-1.ma ... OK (* Rating : 0.00 
253 Unsatisfiable/GRP523-1.ma ... OK (* Rating : 0.00 
254 Unsatisfiable/GRP524-1.ma ... OK (* Rating : 0.00 
255 Unsatisfiable/GRP525-1.ma ... OK (* Rating : 0.00 
256 Unsatisfiable/GRP526-1.ma ... OK (* Rating : 0.00 
257 Unsatisfiable/GRP527-1.ma ... OK (* Rating : 0.00 
258 Unsatisfiable/GRP528-1.ma ... OK (* Rating : 0.00 
259 Unsatisfiable/GRP529-1.ma ... OK (* Rating : 0.00 
260 Unsatisfiable/GRP530-1.ma ... OK (* Rating : 0.00 
261 Unsatisfiable/GRP531-1.ma ... OK (* Rating : 0.00 
262 Unsatisfiable/GRP532-1.ma ... OK (* Rating : 0.00 
263 Unsatisfiable/GRP533-1.ma ... OK (* Rating : 0.00 
264 Unsatisfiable/GRP534-1.ma ... OK (* Rating : 0.00 
265 Unsatisfiable/GRP535-1.ma ... OK (* Rating : 0.00 
266 Unsatisfiable/GRP536-1.ma ... OK (* Rating : 0.00 
267 Unsatisfiable/GRP537-1.ma ... OK (* Rating : 0.00 
268 Unsatisfiable/GRP538-1.ma ... OK (* Rating : 0.00 
269 Unsatisfiable/GRP539-1.ma ... OK (* Rating : 0.00 
270 Unsatisfiable/GRP540-1.ma ... OK (* Rating : 0.00 
271 Unsatisfiable/GRP553-1.ma ... OK (* Rating : 0.00 
272 Unsatisfiable/GRP554-1.ma ... OK (* Rating : 0.00 
273 Unsatisfiable/GRP555-1.ma ... OK (* Rating : 0.00 
274 Unsatisfiable/GRP557-1.ma ... OK (* Rating : 0.00 
275 Unsatisfiable/GRP585-1.ma ... OK (* Rating : 0.00 
276 Unsatisfiable/GRP589-1.ma ... OK (* Rating : 0.00 
277 Unsatisfiable/GRP611-1.ma ... OK (* Rating : 0.00 
278 Unsatisfiable/LAT012-1.ma ... OK (* Rating : 0.00 
279 Unsatisfiable/LAT014-1.ma ... OK (* Rating : 0.00 
280 Unsatisfiable/LAT088-1.ma ... OK (* Rating : 0.00 
281 Unsatisfiable/LAT089-1.ma ... OK (* Rating : 0.00 
282 Unsatisfiable/LAT090-1.ma ... OK (* Rating : 0.00 
283 Unsatisfiable/SYN080-1.ma ... OK (* Rating : 0.00 
284 Unsatisfiable/BOO021-1.ma ... OK (* Rating : 0.07 
285 Unsatisfiable/BOO022-1.ma ... OK (* Rating : 0.07 
286 Unsatisfiable/COL056-1.ma ... OK (* Rating : 0.07 
287 Unsatisfiable/GRP436-1.ma ... OK (* Rating : 0.07 
288 Unsatisfiable/GRP450-1.ma ... OK (* Rating : 0.07 
289 Unsatisfiable/GRP472-1.ma ... OK (* Rating : 0.07 
290 Unsatisfiable/GRP591-1.ma ... OK (* Rating : 0.07 
291 Unsatisfiable/LAT091-1.ma ... OK (* Rating : 0.07 
292 Unsatisfiable/GRP440-1.ma ... OK (* Rating : 0.14 
293 Unsatisfiable/GRP447-1.ma ... OK (* Rating : 0.14 
294 Unsatisfiable/GRP452-1.ma ... OK (* Rating : 0.14 
295 Unsatisfiable/GRP478-1.ma ... OK (* Rating : 0.14 
296 Unsatisfiable/LAT013-1.ma ... OK (* Rating : 0.14 
297 Unsatisfiable/LAT026-1.ma ... OK (* Rating : 0.14 
298 Unsatisfiable/GRP441-1.ma ... OK (* Rating : 0.21 
299 Unsatisfiable/GRP453-1.ma ... OK (* Rating : 0.21 
300 Unsatisfiable/GRP469-1.ma ... OK (* Rating : 0.21 
301 Unsatisfiable/GRP475-1.ma ... OK (* Rating : 0.21 
302 Unsatisfiable/LAT007-1.ma ... OK (* Rating : 0.36 
303 Unsatisfiable/ROB006-2.ma ... OK (* Rating : 0.86 
304 Unsatisfiable/ROB031-1.ma ... OK (* Rating : 1.00 
305 Unsatisfiable/ROB032-1.ma ... OK (* Rating : 1.00 
306 Unsatisfiable/ALG006-1.ma ... OK TIME NEEDED: 1.44 (* Rating : 0.00 
307 Unsatisfiable/ALG007-1.ma ... OK TIME NEEDED: 2.83 (* Rating : 0.00 
308 Unsatisfiable/BOO001-1.ma ... OK TIME NEEDED: 0.69 (* Rating : 0.00 
309 Unsatisfiable/BOO002-2.ma ... OK TIME NEEDED: 19.60 (* Rating : 0.00 
310 Unsatisfiable/BOO003-2.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
311 Unsatisfiable/BOO003-4.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
312 Unsatisfiable/BOO004-2.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
313 Unsatisfiable/BOO004-4.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
314 Unsatisfiable/BOO005-2.ma ... OK TIME NEEDED: 0.13 (* Rating : 0.00 
315 Unsatisfiable/BOO005-4.ma ... OK TIME NEEDED: 0.12 (* Rating : 0.00 
316 Unsatisfiable/BOO006-2.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
317 Unsatisfiable/BOO006-4.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
318 Unsatisfiable/BOO008-4.ma ... OK TIME NEEDED: 52.56 (* Rating : 0.00 
319 Unsatisfiable/BOO009-2.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
320 Unsatisfiable/BOO009-4.ma ... OK TIME NEEDED: 0.29 (* Rating : 0.00 
321 Unsatisfiable/BOO010-2.ma ... OK TIME NEEDED: 0.07 (* Rating : 0.00 
322 Unsatisfiable/BOO010-4.ma ... OK TIME NEEDED: 0.07 (* Rating : 0.00 
323 Unsatisfiable/BOO011-2.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
324 Unsatisfiable/BOO011-4.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
325 Unsatisfiable/BOO012-2.ma ... OK TIME NEEDED: 0.46 (* Rating : 0.00 
326 Unsatisfiable/BOO012-4.ma ... OK TIME NEEDED: 0.51 (* Rating : 0.00 
327 Unsatisfiable/BOO013-2.ma ... OK TIME NEEDED: 0.36 (* Rating : 0.00 
328 Unsatisfiable/BOO013-4.ma ... OK TIME NEEDED: 0.66 (* Rating : 0.00 
329 Unsatisfiable/BOO014-2.ma ... OK TIME NEEDED: 4.44 (* Rating : 0.00 
330 Unsatisfiable/BOO014-4.ma ... OK TIME NEEDED: 13.50 (* Rating : 0.00 
331 Unsatisfiable/BOO015-2.ma ... OK TIME NEEDED: 3.48 (* Rating : 0.00 
332 Unsatisfiable/BOO015-4.ma ... OK TIME NEEDED: 13.30 (* Rating : 0.00 
333 Unsatisfiable/BOO016-2.ma ... OK TIME NEEDED: 0.22 (* Rating : 0.00 
334 Unsatisfiable/BOO017-2.ma ... OK TIME NEEDED: 0.20 (* Rating : 0.00 
335 Unsatisfiable/BOO018-4.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
336 Unsatisfiable/BOO024-1.ma ... OK TIME NEEDED: 2.44 (* Rating : 0.00 
337 Unsatisfiable/BOO068-1.ma ... OK TIME NEEDED: 1.61 (* Rating : 0.00 
338 Unsatisfiable/BOO069-1.ma ... OK TIME NEEDED: 0.80 (* Rating : 0.00 
339 Unsatisfiable/BOO070-1.ma ... OK TIME NEEDED: 1.84 (* Rating : 0.00 
340 Unsatisfiable/BOO071-1.ma ... OK TIME NEEDED: 0.81 (* Rating : 0.00 
341 Unsatisfiable/BOO075-1.ma ... OK TIME NEEDED: 0.54 (* Rating : 0.00 
342 Unsatisfiable/COL002-1.ma ... OK TIME NEEDED: 250.20 (* Rating : 0.00 
343 Unsatisfiable/COL007-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
344 Unsatisfiable/COL008-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
345 Unsatisfiable/COL012-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
346 Unsatisfiable/COL013-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
347 Unsatisfiable/COL014-1.ma ... OK TIME NEEDED: 0.12 (* Rating : 0.00 
348 Unsatisfiable/COL015-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
349 Unsatisfiable/COL016-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
350 Unsatisfiable/COL017-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
351 Unsatisfiable/COL018-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
352 Unsatisfiable/COL019-1.ma ... OK TIME NEEDED: 27.26 (* Rating : 0.00 
353 Unsatisfiable/COL021-1.ma ... OK TIME NEEDED: 0.34 (* Rating : 0.00 
354 Unsatisfiable/COL022-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
355 Unsatisfiable/COL024-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
356 Unsatisfiable/COL025-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
357 Unsatisfiable/COL045-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
358 Unsatisfiable/COL048-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
359 Unsatisfiable/COL050-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
360 Unsatisfiable/COL058-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
361 Unsatisfiable/COL058-3.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
362 Unsatisfiable/COL060-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
363 Unsatisfiable/COL060-3.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
364 Unsatisfiable/COL061-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
365 Unsatisfiable/COL061-3.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
366 Unsatisfiable/COL062-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
367 Unsatisfiable/COL062-3.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
368 Unsatisfiable/COL063-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
369 Unsatisfiable/COL063-3.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
370 Unsatisfiable/COL063-4.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
371 Unsatisfiable/COL063-5.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
372 Unsatisfiable/COL063-6.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
373 Unsatisfiable/COL064-3.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
374 Unsatisfiable/COL064-6.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
375 Unsatisfiable/COL064-8.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
376 Unsatisfiable/COL066-2.ma ... OK TIME NEEDED: 1.21 (* Rating : 0.00 
377 Unsatisfiable/COL066-3.ma ... OK TIME NEEDED: 1.20 (* Rating : 0.00 
378 Unsatisfiable/COL083-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
379 Unsatisfiable/COL084-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
380 Unsatisfiable/COL085-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
381 Unsatisfiable/COL086-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
382 Unsatisfiable/GRP001-2.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
383 Unsatisfiable/GRP001-4.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
384 Unsatisfiable/GRP002-2.ma ... OK TIME NEEDED: 9.84 (* Rating : 0.00 
385 Unsatisfiable/GRP002-3.ma ... OK TIME NEEDED: 8.65 (* Rating : 0.00 
386 Unsatisfiable/GRP002-4.ma ... OK TIME NEEDED: 13.35 (* Rating : 0.00 
387 Unsatisfiable/GRP010-4.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
388 Unsatisfiable/GRP011-4.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
389 Unsatisfiable/GRP012-4.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
390 Unsatisfiable/GRP022-2.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
391 Unsatisfiable/GRP023-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
392 Unsatisfiable/GRP115-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
393 Unsatisfiable/GRP116-1.ma ... OK TIME NEEDED: 0.29 (* Rating : 0.00 
394 Unsatisfiable/GRP117-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
395 Unsatisfiable/GRP118-1.ma ... OK TIME NEEDED: 0.07 (* Rating : 0.00 
396 Unsatisfiable/GRP136-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
397 Unsatisfiable/GRP137-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
398 Unsatisfiable/GRP138-1.ma ... OK TIME NEEDED: 10.54 (* Rating : 0.00 
399 Unsatisfiable/GRP139-1.ma ... OK TIME NEEDED: 0.12 (* Rating : 0.00 
400 Unsatisfiable/GRP140-1.ma ... OK TIME NEEDED: 7.30 (* Rating : 0.00 
401 Unsatisfiable/GRP141-1.ma ... OK TIME NEEDED: 0.12 (* Rating : 0.00 
402 Unsatisfiable/GRP142-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
403 Unsatisfiable/GRP143-1.ma ... OK TIME NEEDED: 0.07 (* Rating : 0.00 
404 Unsatisfiable/GRP144-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
405 Unsatisfiable/GRP145-1.ma ... OK TIME NEEDED: 0.07 (* Rating : 0.00 
406 Unsatisfiable/GRP146-1.ma ... OK TIME NEEDED: 0.16 (* Rating : 0.00 
407 Unsatisfiable/GRP147-1.ma ... OK TIME NEEDED: 57.43 (* Rating : 0.00 
408 Unsatisfiable/GRP148-1.ma ... OK TIME NEEDED: 43.78 (* Rating : 0.00 
409 Unsatisfiable/GRP149-1.ma ... OK TIME NEEDED: 0.16 (* Rating : 0.00 
410 Unsatisfiable/GRP150-1.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
411 Unsatisfiable/GRP151-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
412 Unsatisfiable/GRP152-1.ma ... OK TIME NEEDED: 0.08 (* Rating : 0.00 
413 Unsatisfiable/GRP153-1.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
414 Unsatisfiable/GRP154-1.ma ... OK TIME NEEDED: 0.27 (* Rating : 0.00 
415 Unsatisfiable/GRP155-1.ma ... OK TIME NEEDED: 0.34 (* Rating : 0.00 
416 Unsatisfiable/GRP156-1.ma ... OK TIME NEEDED: 0.36 (* Rating : 0.00 
417 Unsatisfiable/GRP157-1.ma ... OK TIME NEEDED: 0.18 (* Rating : 0.00 
418 Unsatisfiable/GRP158-1.ma ... OK TIME NEEDED: 0.22 (* Rating : 0.00 
419 Unsatisfiable/GRP159-1.ma ... OK TIME NEEDED: 0.20 (* Rating : 0.00 
420 Unsatisfiable/GRP160-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
421 Unsatisfiable/GRP161-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
422 Unsatisfiable/GRP162-1.ma ... OK TIME NEEDED: 0.16 (* Rating : 0.00 
423 Unsatisfiable/GRP163-1.ma ... OK TIME NEEDED: 0.18 (* Rating : 0.00 
424 Unsatisfiable/GRP165-1.ma ... OK TIME NEEDED: 88.00 (* Rating : 0.00 
425 Unsatisfiable/GRP165-2.ma ... OK TIME NEEDED: 83.45 (* Rating : 0.00 
426 Unsatisfiable/GRP166-1.ma ... OK TIME NEEDED: 4.62 (* Rating : 0.00 
427 Unsatisfiable/GRP166-2.ma ... OK TIME NEEDED: 102.88 (* Rating : 0.00 
428 Unsatisfiable/GRP166-3.ma ... OK TIME NEEDED: 144.57 (* Rating : 0.00 
429 Unsatisfiable/GRP166-4.ma ... OK TIME NEEDED: 123.60 (* Rating : 0.00 
430 Unsatisfiable/GRP169-1.ma ... OK TIME NEEDED: 37.22 (* Rating : 0.00 
431 Unsatisfiable/GRP169-2.ma ... OK TIME NEEDED: 36.29 (* Rating : 0.00 
432 Unsatisfiable/GRP171-1.ma ... OK TIME NEEDED: 4.60 (* Rating : 0.00 
433 Unsatisfiable/GRP171-2.ma ... OK TIME NEEDED: 4.62 (* Rating : 0.00 
434 Unsatisfiable/GRP172-1.ma ... OK TIME NEEDED: 3.86 (* Rating : 0.00 
435 Unsatisfiable/GRP172-2.ma ... OK TIME NEEDED: 3.99 (* Rating : 0.00 
436 Unsatisfiable/GRP173-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
437 Unsatisfiable/GRP174-1.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
438 Unsatisfiable/GRP175-1.ma ... OK TIME NEEDED: 89.89 (* Rating : 0.00 
439 Unsatisfiable/GRP175-2.ma ... OK TIME NEEDED: 85.68 (* Rating : 0.00 
440 Unsatisfiable/GRP175-3.ma ... OK TIME NEEDED: 90.00 (* Rating : 0.00 
441 Unsatisfiable/GRP175-4.ma ... OK TIME NEEDED: 88.31 (* Rating : 0.00 
442 Unsatisfiable/GRP176-1.ma ... OK TIME NEEDED: 0.36 (* Rating : 0.00 
443 Unsatisfiable/GRP176-2.ma ... OK TIME NEEDED: 0.34 (* Rating : 0.00 
444 Unsatisfiable/GRP182-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
445 Unsatisfiable/GRP182-2.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
446 Unsatisfiable/GRP182-3.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
447 Unsatisfiable/GRP182-4.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
448 Unsatisfiable/GRP184-4.ma ... OK TIME NEEDED: 293.47 (* Rating : 0.00 
449 Unsatisfiable/GRP186-3.ma ... OK TIME NEEDED: 0.20 (* Rating : 0.00 
450 Unsatisfiable/GRP186-4.ma ... OK TIME NEEDED: 0.22 (* Rating : 0.00 
451 Unsatisfiable/GRP188-1.ma ... OK TIME NEEDED: 0.08 (* Rating : 0.00 
452 Unsatisfiable/GRP188-2.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
453 Unsatisfiable/GRP189-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
454 Unsatisfiable/GRP189-2.ma ... OK TIME NEEDED: 0.06 (* Rating : 0.00 
455 Unsatisfiable/GRP190-1.ma ... OK TIME NEEDED: 42.71 (* Rating : 0.00 
456 Unsatisfiable/GRP190-2.ma ... OK TIME NEEDED: 42.82 (* Rating : 0.00 
457 Unsatisfiable/GRP191-1.ma ... OK TIME NEEDED: 44.97 (* Rating : 0.00 
458 Unsatisfiable/GRP191-2.ma ... OK TIME NEEDED: 44.78 (* Rating : 0.00 
459 Unsatisfiable/GRP193-1.ma ... OK TIME NEEDED: 160.12 (* Rating : 0.00 
460 Unsatisfiable/GRP193-2.ma ... OK TIME NEEDED: 137.38 (* Rating : 0.00 
461 Unsatisfiable/GRP206-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
462 Unsatisfiable/GRP406-1.ma ... OK TIME NEEDED: 258.25 (* Rating : 0.00 
463 Unsatisfiable/GRP407-1.ma ... OK TIME NEEDED: 267.52 (* Rating : 0.00 
464 Unsatisfiable/GRP408-1.ma ... OK TIME NEEDED: 271.12 (* Rating : 0.00 
465 Unsatisfiable/GRP409-1.ma ... OK TIME NEEDED: 7.14 (* Rating : 0.00 
466 Unsatisfiable/GRP412-1.ma ... OK TIME NEEDED: 38.24 (* Rating : 0.00 
467 Unsatisfiable/GRP424-1.ma ... OK TIME NEEDED: 21.08 (* Rating : 0.00 
468 Unsatisfiable/GRP431-1.ma ... OK TIME NEEDED: 30.97 (* Rating : 0.00 
469 Unsatisfiable/GRP432-1.ma ... OK TIME NEEDED: 35.68 (* Rating : 0.00 
470 Unsatisfiable/GRP434-1.ma ... OK TIME NEEDED: 75.44 (* Rating : 0.00 
471 Unsatisfiable/GRP435-1.ma ... OK TIME NEEDED: 99.68 (* Rating : 0.00 
472 Unsatisfiable/GRP454-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
473 Unsatisfiable/GRP455-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
474 Unsatisfiable/GRP457-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
475 Unsatisfiable/GRP458-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
476 Unsatisfiable/GRP459-1.ma ... OK TIME NEEDED: 0.19 (* Rating : 0.00 
477 Unsatisfiable/GRP460-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
478 Unsatisfiable/GRP463-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
479 Unsatisfiable/GRP467-1.ma ... OK TIME NEEDED: 0.48 (* Rating : 0.00 
480 Unsatisfiable/GRP468-1.ma ... OK TIME NEEDED: 1.85 (* Rating : 0.00 
481 Unsatisfiable/GRP481-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
482 Unsatisfiable/GRP484-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
483 Unsatisfiable/GRP485-1.ma ... OK TIME NEEDED: 0.08 (* Rating : 0.00 
484 Unsatisfiable/GRP486-1.ma ... OK TIME NEEDED: 0.35 (* Rating : 0.00 
485 Unsatisfiable/GRP487-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
486 Unsatisfiable/GRP488-1.ma ... OK TIME NEEDED: 0.70 (* Rating : 0.00 
487 Unsatisfiable/GRP489-1.ma ... OK TIME NEEDED: 1.10 (* Rating : 0.00 
488 Unsatisfiable/GRP490-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
489 Unsatisfiable/GRP491-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
490 Unsatisfiable/GRP492-1.ma ... OK TIME NEEDED: 0.47 (* Rating : 0.00 
491 Unsatisfiable/GRP493-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
492 Unsatisfiable/GRP494-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
493 Unsatisfiable/GRP495-1.ma ... OK TIME NEEDED: 0.25 (* Rating : 0.00 
494 Unsatisfiable/GRP496-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
495 Unsatisfiable/GRP497-1.ma ... OK TIME NEEDED: 0.13 (* Rating : 0.00 
496 Unsatisfiable/GRP498-1.ma ... OK TIME NEEDED: 0.32 (* Rating : 0.00 
497 Unsatisfiable/GRP509-1.ma ... OK TIME NEEDED: 0.60 (* Rating : 0.00 
498 Unsatisfiable/GRP510-1.ma ... OK TIME NEEDED: 0.08 (* Rating : 0.00 
499 Unsatisfiable/GRP511-1.ma ... OK TIME NEEDED: 0.77 (* Rating : 0.00 
500 Unsatisfiable/GRP512-1.ma ... OK TIME NEEDED: 0.13 (* Rating : 0.00 
501 Unsatisfiable/GRP513-1.ma ... OK TIME NEEDED: 0.64 (* Rating : 0.00 
502 Unsatisfiable/GRP514-1.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
503 Unsatisfiable/GRP515-1.ma ... OK TIME NEEDED: 0.57 (* Rating : 0.00 
504 Unsatisfiable/GRP516-1.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
505 Unsatisfiable/GRP517-1.ma ... OK TIME NEEDED: 0.53 (* Rating : 0.00 
506 Unsatisfiable/GRP518-1.ma ... OK TIME NEEDED: 0.10 (* Rating : 0.00 
507 Unsatisfiable/GRP519-1.ma ... OK TIME NEEDED: 1.23 (* Rating : 0.00 
508 Unsatisfiable/GRP520-1.ma ... OK TIME NEEDED: 0.10 (* Rating : 0.00 
509 Unsatisfiable/GRP541-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
510 Unsatisfiable/GRP542-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
511 Unsatisfiable/GRP543-1.ma ... OK TIME NEEDED: 0.21 (* Rating : 0.00 
512 Unsatisfiable/GRP544-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
513 Unsatisfiable/GRP545-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
514 Unsatisfiable/GRP546-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
515 Unsatisfiable/GRP547-1.ma ... OK TIME NEEDED: 0.50 (* Rating : 0.00 
516 Unsatisfiable/GRP548-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
517 Unsatisfiable/GRP549-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
518 Unsatisfiable/GRP551-1.ma ... OK TIME NEEDED: 0.41 (* Rating : 0.00 
519 Unsatisfiable/GRP552-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.00 
520 Unsatisfiable/GRP556-1.ma ... OK TIME NEEDED: 0.65 (* Rating : 0.00 
521 Unsatisfiable/GRP558-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
522 Unsatisfiable/GRP559-1.ma ... OK TIME NEEDED: 1.24 (* Rating : 0.00 
523 Unsatisfiable/GRP560-1.ma ... OK TIME NEEDED: 0.20 (* Rating : 0.00 
524 Unsatisfiable/GRP561-1.ma ... OK TIME NEEDED: 0.13 (* Rating : 0.00 
525 Unsatisfiable/GRP562-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
526 Unsatisfiable/GRP563-1.ma ... OK TIME NEEDED: 3.89 (* Rating : 0.00 
527 Unsatisfiable/GRP564-1.ma ... OK TIME NEEDED: 0.13 (* Rating : 0.00 
528 Unsatisfiable/GRP565-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
529 Unsatisfiable/GRP566-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
530 Unsatisfiable/GRP569-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
531 Unsatisfiable/GRP570-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
532 Unsatisfiable/GRP573-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
533 Unsatisfiable/GRP574-1.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
534 Unsatisfiable/GRP576-1.ma ... OK TIME NEEDED: 0.16 (* Rating : 0.00 
535 Unsatisfiable/GRP577-1.ma ... OK TIME NEEDED: 0.08 (* Rating : 0.00 
536 Unsatisfiable/GRP578-1.ma ... OK TIME NEEDED: 0.19 (* Rating : 0.00 
537 Unsatisfiable/GRP580-1.ma ... OK TIME NEEDED: 0.52 (* Rating : 0.00 
538 Unsatisfiable/GRP581-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
539 Unsatisfiable/GRP582-1.ma ... OK TIME NEEDED: 0.14 (* Rating : 0.00 
540 Unsatisfiable/GRP584-1.ma ... OK TIME NEEDED: 0.42 (* Rating : 0.00 
541 Unsatisfiable/GRP586-1.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
542 Unsatisfiable/GRP587-1.ma ... OK TIME NEEDED: 7.98 (* Rating : 0.00 
543 Unsatisfiable/GRP588-1.ma ... OK TIME NEEDED: 0.41 (* Rating : 0.00 
544 Unsatisfiable/GRP590-1.ma ... OK TIME NEEDED: 0.15 (* Rating : 0.00 
545 Unsatisfiable/GRP593-1.ma ... OK TIME NEEDED: 1.24 (* Rating : 0.00 
546 Unsatisfiable/GRP594-1.ma ... OK TIME NEEDED: 1.02 (* Rating : 0.00 
547 Unsatisfiable/GRP597-1.ma ... OK TIME NEEDED: 0.52 (* Rating : 0.00 
548 Unsatisfiable/GRP605-1.ma ... OK TIME NEEDED: 0.56 (* Rating : 0.00 
549 Unsatisfiable/GRP606-1.ma ... OK TIME NEEDED: 0.35 (* Rating : 0.00 
550 Unsatisfiable/GRP607-1.ma ... OK TIME NEEDED: 1.27 (* Rating : 0.00 
551 Unsatisfiable/GRP608-1.ma ... OK TIME NEEDED: 0.40 (* Rating : 0.00 
552 Unsatisfiable/GRP613-1.ma ... OK TIME NEEDED: 0.48 (* Rating : 0.00 
553 Unsatisfiable/GRP614-1.ma ... OK TIME NEEDED: 0.25 (* Rating : 0.00 
554 Unsatisfiable/GRP616-1.ma ... OK TIME NEEDED: 0.27 (* Rating : 0.00 
555 Unsatisfiable/LAT009-1.ma ... OK TIME NEEDED: 271.20 (* Rating : 0.00 
556 Unsatisfiable/LAT019-1.ma ... OK TIME NEEDED: 165.91 (* Rating : 0.00 
557 Unsatisfiable/LAT028-1.ma ... OK TIME NEEDED: 45.13 (* Rating : 0.00 
558 Unsatisfiable/LAT031-1.ma ... OK TIME NEEDED: 60.22 (* Rating : 0.00 
559 Unsatisfiable/LAT032-1.ma ... OK TIME NEEDED: 1.63 (* Rating : 0.00 
560 Unsatisfiable/LAT033-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
561 Unsatisfiable/LAT034-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
562 Unsatisfiable/LAT039-1.ma ... OK TIME NEEDED: 0.41 (* Rating : 0.00 
563 Unsatisfiable/LAT039-2.ma ... OK TIME NEEDED: 0.41 (* Rating : 0.00 
564 Unsatisfiable/LAT040-1.ma ... OK TIME NEEDED: 0.94 (* Rating : 0.00 
565 Unsatisfiable/LAT042-1.ma ... OK TIME NEEDED: 22.84 (* Rating : 0.00 
566 Unsatisfiable/LAT043-1.ma ... OK TIME NEEDED: 23.72 (* Rating : 0.00 
567 Unsatisfiable/LCL110-2.ma ... OK TIME NEEDED: 0.26 (* Rating : 0.00 
568 Unsatisfiable/LCL112-2.ma ... OK TIME NEEDED: 0.27 (* Rating : 0.00 
569 Unsatisfiable/LCL113-2.ma ... OK TIME NEEDED: 0.28 (* Rating : 0.00 
570 Unsatisfiable/LCL114-2.ma ... OK TIME NEEDED: 0.35 (* Rating : 0.00 
571 Unsatisfiable/LCL115-2.ma ... OK TIME NEEDED: 0.55 (* Rating : 0.00 
572 Unsatisfiable/LCL116-2.ma ... OK TIME NEEDED: 4.89 (* Rating : 0.00 
573 Unsatisfiable/LCL132-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
574 Unsatisfiable/LCL133-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
575 Unsatisfiable/LCL134-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
576 Unsatisfiable/LCL135-1.ma ... OK TIME NEEDED: 0.05 (* Rating : 0.00 
577 Unsatisfiable/LCL139-1.ma ... OK TIME NEEDED: 0.34 (* Rating : 0.00 
578 Unsatisfiable/LCL140-1.ma ... OK TIME NEEDED: 0.27 (* Rating : 0.00 
579 Unsatisfiable/LCL141-1.ma ... OK TIME NEEDED: 0.55 (* Rating : 0.00 
580 Unsatisfiable/LCL153-1.ma ... OK TIME NEEDED: 0.30 (* Rating : 0.00 
581 Unsatisfiable/LCL154-1.ma ... OK TIME NEEDED: 0.26 (* Rating : 0.00 
582 Unsatisfiable/LCL155-1.ma ... OK TIME NEEDED: 0.29 (* Rating : 0.00 
583 Unsatisfiable/LCL156-1.ma ... OK TIME NEEDED: 0.25 (* Rating : 0.00 
584 Unsatisfiable/LCL157-1.ma ... OK TIME NEEDED: 0.26 (* Rating : 0.00 
585 Unsatisfiable/LCL158-1.ma ... OK TIME NEEDED: 0.30 (* Rating : 0.00 
586 Unsatisfiable/LCL159-1.ma ... OK TIME NEEDED: 1.40 (* Rating : 0.00 
587 Unsatisfiable/LCL161-1.ma ... OK TIME NEEDED: 0.09 (* Rating : 0.00 
588 Unsatisfiable/LCL164-1.ma ... OK TIME NEEDED: 0.14 (* Rating : 0.00 
589 Unsatisfiable/LDA001-1.ma ... OK TIME NEEDED: 0.04 (* Rating : 0.00 
590 Unsatisfiable/LDA002-1.ma ... OK TIME NEEDED: 10.74 (* Rating : 0.00 
591 Unsatisfiable/LDA007-3.ma ... OK TIME NEEDED: 0.11 (* Rating : 0.00 
592 Unsatisfiable/RNG007-4.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
593 Unsatisfiable/RNG011-5.ma ... OK TIME NEEDED: 0.24 (* Rating : 0.00 
594 Unsatisfiable/RNG012-6.ma ... OK TIME NEEDED: 51.47 (* Rating : 0.00 
595 Unsatisfiable/RNG013-6.ma ... OK TIME NEEDED: 50.47 (* Rating : 0.00 
596 Unsatisfiable/RNG014-6.ma ... OK TIME NEEDED: 48.93 (* Rating : 0.00 
597 Unsatisfiable/RNG015-6.ma ... OK TIME NEEDED: 48.44 (* Rating : 0.00 
598 Unsatisfiable/RNG016-6.ma ... OK TIME NEEDED: 50.42 (* Rating : 0.00 
599 Unsatisfiable/RNG017-6.ma ... OK TIME NEEDED: 50.79 (* Rating : 0.00 
600 Unsatisfiable/RNG018-6.ma ... OK TIME NEEDED: 48.34 (* Rating : 0.00 
601 Unsatisfiable/RNG023-6.ma ... OK TIME NEEDED: 0.18 (* Rating : 0.00 
602 Unsatisfiable/RNG023-7.ma ... OK TIME NEEDED: 0.29 (* Rating : 0.00 
603 Unsatisfiable/RNG024-6.ma ... OK TIME NEEDED: 0.17 (* Rating : 0.00 
604 Unsatisfiable/RNG024-7.ma ... OK TIME NEEDED: 0.29 (* Rating : 0.00 
605 Unsatisfiable/ROB002-1.ma ... OK TIME NEEDED: 0.03 (* Rating : 0.00 
606 Unsatisfiable/ROB003-1.ma ... OK TIME NEEDED: 47.87 (* Rating : 0.00 
607 Unsatisfiable/ROB004-1.ma ... OK TIME NEEDED: 24.39 (* Rating : 0.00 
608 Unsatisfiable/ROB008-1.ma ... OK TIME NEEDED: 122.13 (* Rating : 0.00 
609 Unsatisfiable/ROB009-1.ma ... OK TIME NEEDED: 0.80 (* Rating : 0.00 
610 Unsatisfiable/ROB010-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
611 Unsatisfiable/ROB013-1.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.00 
612 Unsatisfiable/ROB022-1.ma ... OK TIME NEEDED: 173.21 (* Rating : 0.00 
613 Unsatisfiable/ROB023-1.ma ... OK TIME NEEDED: 191.39 (* Rating : 0.00 
614 Unsatisfiable/ROB030-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
615 Unsatisfiable/SYN083-1.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.00 
616 Unsatisfiable/ALG005-1.ma ... OK TIME NEEDED: 27.54 (* Rating : 0.07 
617 Unsatisfiable/BOO002-1.ma ... OK TIME NEEDED: 14.36 (* Rating : 0.07 
618 Unsatisfiable/BOO007-4.ma ... OK TIME NEEDED: 60.41 (* Rating : 0.07 
619 Unsatisfiable/BOO008-2.ma ... OK TIME NEEDED: 98.05 (* Rating : 0.07 
620 Unsatisfiable/BOO025-1.ma ... OK TIME NEEDED: 40.06 (* Rating : 0.07 
621 Unsatisfiable/COL001-1.ma ... OK TIME NEEDED: 105.21 (* Rating : 0.07 
622 Unsatisfiable/COL001-2.ma ... OK TIME NEEDED: 27.06 (* Rating : 0.07 
623 Unsatisfiable/COL009-1.ma ... OK TIME NEEDED: 121.79 (* Rating : 0.07 
624 Unsatisfiable/COL010-1.ma ... OK TIME NEEDED: 0.97 (* Rating : 0.07 
625 Unsatisfiable/COL064-2.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.07 
626 Unsatisfiable/COL064-4.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.07 
627 Unsatisfiable/COL064-5.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.07 
628 Unsatisfiable/COL064-7.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.07 
629 Unsatisfiable/COL064-9.ma ... OK TIME NEEDED: 0.00 (* Rating : 0.07 
630 Unsatisfiable/GRP168-1.ma ... OK TIME NEEDED: 0.28 (* Rating : 0.07 
631 Unsatisfiable/GRP168-2.ma ... OK TIME NEEDED: 0.38 (* Rating : 0.07 
632 Unsatisfiable/GRP192-1.ma ... OK TIME NEEDED: 0.20 (* Rating : 0.07 
633 Unsatisfiable/GRP403-1.ma ... OK TIME NEEDED: 28.55 (* Rating : 0.07 
634 Unsatisfiable/GRP437-1.ma ... OK TIME NEEDED: 81.72 (* Rating : 0.07 
635 Unsatisfiable/GRP438-1.ma ... OK TIME NEEDED: 122.27 (* Rating : 0.07 
636 Unsatisfiable/GRP439-1.ma ... OK TIME NEEDED: 31.35 (* Rating : 0.07 
637 Unsatisfiable/GRP456-1.ma ... OK TIME NEEDED: 0.18 (* Rating : 0.07 
638 Unsatisfiable/GRP473-1.ma ... OK TIME NEEDED: 66.00 (* Rating : 0.07 
639 Unsatisfiable/GRP474-1.ma ... OK TIME NEEDED: 85.37 (* Rating : 0.07 
640 Unsatisfiable/GRP500-1.ma ... OK TIME NEEDED: 24.13 (* Rating : 0.07 
641 Unsatisfiable/GRP550-1.ma ... OK TIME NEEDED: 0.02 (* Rating : 0.07 
642 Unsatisfiable/GRP572-1.ma ... OK TIME NEEDED: 0.22 (* Rating : 0.07 
643 Unsatisfiable/GRP579-1.ma ... OK TIME NEEDED: 3.97 (* Rating : 0.07 
644 Unsatisfiable/GRP583-1.ma ... OK TIME NEEDED: 0.76 (* Rating : 0.07 
645 Unsatisfiable/GRP592-1.ma ... OK TIME NEEDED: 0.22 (* Rating : 0.07 
646 Unsatisfiable/GRP595-1.ma ... OK TIME NEEDED: 0.15 (* Rating : 0.07 
647 Unsatisfiable/GRP596-1.ma ... OK TIME NEEDED: 0.25 (* Rating : 0.07 
648 Unsatisfiable/GRP598-1.ma ... OK TIME NEEDED: 0.20 (* Rating : 0.07 
649 Unsatisfiable/GRP599-1.ma ... OK TIME NEEDED: 0.96 (* Rating : 0.07 
650 Unsatisfiable/GRP600-1.ma ... OK TIME NEEDED: 0.30 (* Rating : 0.07 
651 Unsatisfiable/GRP601-1.ma ... OK TIME NEEDED: 1.06 (* Rating : 0.07 
652 Unsatisfiable/GRP602-1.ma ... OK TIME NEEDED: 0.47 (* Rating : 0.07 
653 Unsatisfiable/GRP603-1.ma ... OK TIME NEEDED: 0.47 (* Rating : 0.07 
654 Unsatisfiable/GRP604-1.ma ... OK TIME NEEDED: 0.61 (* Rating : 0.07 
655 Unsatisfiable/GRP609-1.ma ... OK TIME NEEDED: 1.06 (* Rating : 0.07 
656 Unsatisfiable/GRP610-1.ma ... OK TIME NEEDED: 0.27 (* Rating : 0.07 
657 Unsatisfiable/GRP612-1.ma ... OK TIME NEEDED: 0.28 (* Rating : 0.07 
658 Unsatisfiable/GRP615-1.ma ... OK TIME NEEDED: 0.68 (* Rating : 0.07 
659 Unsatisfiable/LAT008-1.ma ... OK TIME NEEDED: 0.78 (* Rating : 0.07 
660 Unsatisfiable/LAT027-1.ma ... OK TIME NEEDED: 49.64 (* Rating : 0.07 
661 Unsatisfiable/LAT045-1.ma ... OK TIME NEEDED: 0.37 (* Rating : 0.07 
662 Unsatisfiable/LCL111-2.ma ... OK TIME NEEDED: 5.72 (* Rating : 0.07 
663 Unsatisfiable/RNG008-3.ma ... OK TIME NEEDED: 3.54 (* Rating : 0.07 
664 Unsatisfiable/RNG008-4.ma ... OK TIME NEEDED: 0.18 (* Rating : 0.07 
665 Unsatisfiable/RNG008-7.ma ... OK TIME NEEDED: 17.42 (* Rating : 0.07 
666 Unsatisfiable/ROB005-1.ma ... OK TIME NEEDED: 221.06 (* Rating : 0.07 
667 Unsatisfiable/BOO007-2.ma ... OK TIME NEEDED: 72.77 (* Rating : 0.14 
668 Unsatisfiable/GRP167-5.ma ... OK TIME NEEDED: 1.12 (* Rating : 0.14 
669 Unsatisfiable/GRP479-1.ma ... OK TIME NEEDED: 23.91 (* Rating : 0.14 
670 Unsatisfiable/GRP501-1.ma ... OK TIME NEEDED: 56.48 (* Rating : 0.14 
671 Unsatisfiable/GRP567-1.ma ... OK TIME NEEDED: 0.89 (* Rating : 0.14 
672 Unsatisfiable/GRP568-1.ma ... OK TIME NEEDED: 0.46 (* Rating : 0.14 
673 Unsatisfiable/GRP571-1.ma ... OK TIME NEEDED: 1.14 (* Rating : 0.14 
674 Unsatisfiable/GRP575-1.ma ... OK TIME NEEDED: 2.19 (* Rating : 0.14 
675 Unsatisfiable/LAT006-1.ma ... OK TIME NEEDED: 9.83 (* Rating : 0.14 
676 Unsatisfiable/LAT143-1.ma ... OK TIME NEEDED: 149.59 (* Rating : 0.14 
677 Unsatisfiable/LCL109-6.ma ... OK TIME NEEDED: 49.25 (* Rating : 0.14 
678 Unsatisfiable/LCL160-1.ma ... OK TIME NEEDED: 255.01 (* Rating : 0.14 
679 Unsatisfiable/LCL163-1.ma ... OK TIME NEEDED: 6.24 (* Rating : 0.14 
680 Unsatisfiable/BOO034-1.ma ... OK TIME NEEDED: 0.94 (* Rating : 0.21 
681 Unsatisfiable/COL004-3.ma ... OK TIME NEEDED: 0.01 (* Rating : 0.21 
682 Unsatisfiable/GRP167-1.ma ... OK TIME NEEDED: 3.28 (* Rating : 0.21 
683 Unsatisfiable/GRP167-2.ma ... OK TIME NEEDED: 2.83 (* Rating : 0.21 
684 Unsatisfiable/GRP404-1.ma ... OK TIME NEEDED: 69.93 (* Rating : 0.21 
685 Unsatisfiable/GRP405-1.ma ... OK TIME NEEDED: 70.94 (* Rating : 0.21 
686 Unsatisfiable/GRP410-1.ma ... OK TIME NEEDED: 10.96 (* Rating : 0.21 
687 Unsatisfiable/GRP411-1.ma ... OK TIME NEEDED: 12.26 (* Rating : 0.21 
688 Unsatisfiable/GRP470-1.ma ... OK TIME NEEDED: 115.05 (* Rating : 0.21 
689 Unsatisfiable/GRP471-1.ma ... OK TIME NEEDED: 140.02 (* Rating : 0.21 
690 Unsatisfiable/GRP476-1.ma ... OK TIME NEEDED: 86.40 (* Rating : 0.21 
691 Unsatisfiable/GRP477-1.ma ... OK TIME NEEDED: 88.63 (* Rating : 0.21 
692 Unsatisfiable/GRP480-1.ma ... OK TIME NEEDED: 28.09 (* Rating : 0.21 
693 Unsatisfiable/GRP114-1.ma ... OK TIME NEEDED: 8.54 (* Rating : 0.29 
694 Unsatisfiable/LCL109-2.ma ... OK TIME NEEDED: 71.47 (* Rating : 0.29 
695 Unsatisfiable/GRP181-3.ma ... OK TIME NEEDED: 16.87 (* Rating : 0.43 
696 Unsatisfiable/GRP181-4.ma ... OK TIME NEEDED: 27.77 (* Rating : 0.43 
697 Unsatisfiable/LAT156-1.ma ... OK TIME NEEDED: 218.93 (* Rating : 0.64 
698 Unsatisfiable/LAT017-1.ma ... OK TIME NEEDED: 148.94 (* Rating : 0.71