-------------------------------------------------------------------------------- Execute format string : ./dctp.1.31 -negpref -complexity -fullrewrite -alternate -resisol Problems list file : nne-problems Output file : nne-output Summary file : nne-summary Time limit : 300 s Memory limit : 500 MB -------------------------------------------------------------------------------- Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug ALG002-1 theorem 0.0 6 ANA001-1 timeout 300.0 45 ANA002-1 timeout 300.0 89 ANA002-2 timeout 300.0 144 ANA002-3 timeout 300.0 101 ANA002-4 timeout 300.0 131 ANA003-4 timeout 300.0 125 ANA004-4 timeout 300.0 133 ANA004-5 timeout 300.0 79 ANA005-4 timeout 300.0 87 ANA005-5 timeout 300.0 147 CAT007-3 theorem 0.0 6 COM002-2 theorem 0.0 6 COM003-1 theorem 2.3 6 COM003-2 theorem 0.0 6 COM005-1 timeout 300.0 10 COM006-1 timeout 300.0 10 FLD001-3 theorem 0.0 6 FLD002-3 theorem 0.4 8 FLD003-1 timeout 300.0 81 FLD004-1 timeout 300.0 106 FLD005-1 timeout 300.0 110 FLD005-3 theorem 0.4 8 FLD006-1 theorem 1.0 8 FLD006-3 theorem 0.0 6 FLD007-1 timeout 300.0 128 FLD007-3 memory 125.9 499 FLD008-1 timeout 300.0 81 FLD008-2 timeout 300.0 299 FLD008-3 timeout 300.0 434 FLD008-4 theorem 1.2 8 FLD009-1 timeout 300.0 114 FLD009-3 theorem 0.5 10 FLD010-1 timeout 300.0 165 FLD010-3 theorem 0.0 6 FLD010-5 theorem 2.0 16 FLD011-1 timeout 300.0 282 FLD011-3 memory 130.6 499 FLD012-1 timeout 300.0 131 FLD012-2 timeout 300.1 361 FLD012-3 timeout 300.0 429 FLD012-4 theorem 190.7 234 FLD013-1 theorem 0.1 6 FLD013-2 theorem 0.1 6 FLD013-3 theorem 1.7 13 FLD013-4 theorem 0.0 6 FLD013-5 theorem 0.0 6 FLD014-1 timeout 300.0 127 FLD014-3 theorem 0.1 6 FLD015-1 timeout 300.0 62 FLD015-3 theorem 0.1 6 FLD016-1 timeout 300.0 315 FLD016-3 theorem 0.1 4 FLD016-5 theorem 0.3 6 FLD017-1 theorem 0.1 6 FLD017-3 theorem 0.0 6 FLD018-1 theorem 77.7 73 FLD018-3 theorem 0.0 6 FLD019-1 theorem 44.7 46 FLD019-3 theorem 0.0 6 FLD020-1 timeout 300.0 152 FLD020-3 theorem 0.0 6 FLD021-1 theorem 0.1 6 FLD021-3 theorem 0.0 6 FLD022-1 timeout 300.0 198 FLD022-3 theorem 0.2 4 FLD023-1 timeout 300.0 104 FLD023-3 theorem 0.0 6 FLD024-1 timeout 300.0 148 FLD024-3 theorem 0.0 6 FLD025-1 theorem 0.1 6 FLD025-2 theorem 0.2 6 FLD025-3 theorem 0.6 8 FLD025-4 theorem 0.0 6 FLD025-5 theorem 0.0 6 FLD026-1 timeout 300.0 104 FLD026-3 timeout 300.0 453 FLD027-1 timeout 300.0 123 FLD027-3 theorem 0.1 6 FLD028-1 timeout 300.0 349 FLD028-3 theorem 0.1 6 FLD029-1 timeout 300.0 349 FLD029-3 theorem 3.1 22 FLD030-1 theorem 0.0 6 FLD030-2 theorem 0.1 6 FLD030-3 theorem 0.2 6 FLD030-4 theorem 0.0 6 FLD031-1 theorem 89.1 73 FLD031-3 theorem 0.0 6 FLD031-5 theorem 0.3 8 FLD032-1 theorem 41.7 46 FLD032-3 theorem 0.0 6 FLD033-1 timeout 300.0 143 FLD033-3 theorem 0.0 6 FLD034-1 theorem 0.1 6 FLD034-3 theorem 0.0 6 FLD035-1 timeout 300.0 198 FLD035-3 theorem 0.1 4 FLD036-1 timeout 300.0 194 FLD036-3 theorem 0.1 6 FLD037-1 theorem 195.0 123 FLD037-3 theorem 0.0 6 FLD038-1 timeout 300.0 148 FLD038-3 theorem 0.0 6 FLD039-1 theorem 0.0 6 FLD039-3 theorem 0.0 6 FLD040-1 timeout 300.0 191 FLD040-3 theorem 3.1 17 FLD040-5 theorem 3.3 16 FLD041-1 timeout 300.0 107 FLD041-2 timeout 300.0 344 FLD041-3 theorem 0.3 4 FLD041-4 theorem 14.4 53 FLD043-1 timeout 300.0 311 FLD043-3 theorem 0.1 6 FLD043-5 theorem 5.7 28 FLD044-1 timeout 300.0 81 FLD044-2 timeout 300.0 377 FLD044-3 memory 216.5 499 FLD044-4 timeout 300.0 204 FLD045-1 timeout 300.0 81 FLD045-2 timeout 300.0 361 FLD045-3 memory 217.0 499 FLD045-4 memory 146.8 499 FLD046-1 timeout 300.0 282 FLD046-3 memory 122.6 499 FLD047-1 timeout 300.0 189 FLD047-2 memory 257.3 499 FLD047-3 memory 256.5 500 FLD047-4 timeout 300.0 361 FLD048-1 timeout 300.0 369 FLD048-2 timeout 300.0 107 FLD048-3 timeout 300.0 445 FLD048-4 timeout 300.0 404 FLD049-1 timeout 300.0 377 FLD049-2 memory 260.6 499 FLD049-3 timeout 300.0 413 FLD049-4 theorem 10.6 55 FLD050-1 timeout 300.0 361 FLD050-2 memory 293.6 500 FLD050-3 timeout 300.0 463 FLD050-4 theorem 15.2 80 FLD051-1 timeout 300.0 385 FLD051-2 timeout 300.0 107 FLD051-3 timeout 300.0 437 FLD051-4 timeout 300.0 412 FLD052-1 timeout 300.0 361 FLD052-2 timeout 300.0 107 FLD052-3 memory 243.5 499 FLD052-4 memory 157.9 499 FLD053-1 timeout 300.0 377 FLD053-2 timeout 300.0 166 FLD053-3 memory 242.4 499 FLD053-4 timeout 300.0 461 FLD054-1 timeout 300.0 131 FLD054-2 memory 199.8 499 FLD054-3 timeout 300.1 487 FLD054-4 timeout 300.0 220 FLD055-1 theorem 0.0 6 FLD055-3 theorem 0.1 6 FLD056-1 theorem 0.0 4 FLD056-3 theorem 0.0 6 FLD057-1 timeout 300.0 53 FLD057-3 timeout 300.0 266 FLD058-1 theorem 0.0 6 FLD058-3 theorem 0.0 6 FLD059-1 theorem 0.0 6 FLD059-2 theorem 0.1 6 FLD059-3 theorem 0.0 4 FLD059-4 theorem 0.0 6 FLD060-1 theorem 0.1 6 FLD060-2 theorem 1.8 6 FLD060-3 theorem 93.8 28 FLD060-4 theorem 2.0 8 FLD061-1 theorem 0.2 6 FLD061-2 theorem 14.0 21 FLD061-3 timeout 300.0 57 FLD061-4 theorem 0.9 8 FLD062-1 timeout 300.0 16 FLD062-3 timeout 300.0 37 FLD063-1 timeout 300.0 13 FLD063-3 timeout 300.0 29 FLD064-1 timeout 300.0 80 FLD064-3 theorem 27.5 29 FLD065-1 timeout 300.0 81 FLD065-3 theorem 0.1 6 FLD066-1 timeout 300.0 29 FLD066-3 theorem 0.5 4 FLD067-1 timeout 300.0 17 FLD067-2 theorem 3.7 8 FLD067-3 timeout 300.0 37 FLD067-4 theorem 0.3 6 FLD068-1 timeout 300.0 22 FLD068-2 timeout 300.0 81 FLD068-3 timeout 300.0 38 FLD068-4 theorem 0.0 6 FLD069-1 theorem 0.3 6 FLD069-3 theorem 0.0 6 FLD070-1 theorem 0.0 6 FLD070-2 theorem 0.1 6 FLD070-3 theorem 0.0 6 FLD070-4 theorem 0.0 6 FLD071-1 theorem 0.0 6 FLD071-2 theorem 0.1 6 FLD071-3 theorem 0.0 6 FLD071-4 theorem 0.0 6 FLD072-1 timeout 300.0 21 FLD072-2 timeout 300.0 148 FLD072-3 timeout 300.0 38 FLD072-4 timeout 300.0 380 FLD073-1 timeout 300.0 21 FLD073-2 timeout 300.0 64 FLD073-3 timeout 300.0 29 FLD073-4 timeout 300.0 347 FLD074-1 timeout 300.0 37 FLD074-2 timeout 300.0 369 FLD074-3 timeout 300.0 99 FLD074-4 timeout 300.0 355 FLD075-1 timeout 300.0 37 FLD075-2 timeout 300.0 194 FLD075-3 timeout 300.0 38 FLD075-4 timeout 300.0 338 FLD076-1 timeout 300.0 63 FLD076-2 timeout 300.0 369 FLD076-3 timeout 300.0 446 FLD076-4 timeout 300.0 234 FLD077-1 timeout 300.0 88 FLD077-2 timeout 300.0 198 FLD077-3 timeout 300.0 380 FLD077-4 timeout 300.0 292 FLD078-1 timeout 300.0 37 FLD078-2 timeout 300.0 65 FLD078-3 memory 248.3 499 FLD078-4 memory 209.4 499 FLD079-1 timeout 300.0 40 FLD079-2 timeout 300.0 94 FLD079-3 memory 259.0 500 FLD079-4 memory 243.0 499 FLD080-1 timeout 300.0 79 FLD080-2 timeout 300.0 28 FLD080-3 timeout 300.0 396 FLD080-4 memory 195.7 499 FLD081-1 timeout 300.0 82 FLD081-2 memory 225.7 500 FLD081-3 timeout 300.0 55 FLD081-4 memory 174.5 498 FLD082-1 timeout 300.0 46 FLD082-3 memory 162.3 499 FLD083-1 timeout 300.0 46 FLD083-3 memory 163.4 499 FLD084-1 timeout 300.0 38 FLD084-3 memory 165.5 499 FLD085-1 timeout 300.0 38 FLD085-3 memory 160.2 499 FLD086-1 timeout 300.0 245 FLD086-3 memory 112.1 500 FLD087-1 timeout 300.0 261 FLD087-3 memory 210.7 499 FLD088-1 timeout 300.0 187 FLD088-3 memory 137.2 500 FLD089-1 timeout 300.0 241 FLD089-3 memory 133.4 499 FLD090-1 timeout 300.0 283 FLD090-3 timeout 300.0 479 FLD091-1 timeout 300.0 303 FLD091-3 timeout 300.0 429 FLD092-1 timeout 300.0 98 FLD092-3 timeout 300.0 470 FLD093-1 timeout 300.0 362 FLD093-3 timeout 300.0 437 FLD094-1 timeout 300.0 127 FLD094-3 timeout 300.0 437 FLD095-1 timeout 300.0 65 FLD095-2 timeout 300.0 200 FLD095-3 timeout 300.0 404 FLD095-4 timeout 300.0 102 FLD096-1 timeout 300.0 149 FLD096-2 timeout 300.0 338 FLD096-3 timeout 300.1 404 FLD096-4 timeout 300.0 111 FLD097-1 timeout 300.0 105 FLD097-2 timeout 300.0 111 FLD097-3 timeout 300.0 300 FLD097-4 timeout 300.0 48 FLD098-1 timeout 300.0 96 FLD098-2 timeout 300.0 404 FLD098-3 timeout 300.0 313 FLD098-4 timeout 300.0 103 FLD099-1 timeout 300.0 178 FLD099-2 timeout 300.0 114 FLD099-3 memory 145.5 499 FLD099-4 timeout 300.0 351 FLD100-1 timeout 300.0 21 FLD100-2 timeout 300.0 203 FLD100-3 timeout 300.0 82 FLD100-4 timeout 300.0 127 GRA001-1 theorem 0.0 6 GRP025-3 timeout 300.0 375 GRP026-3 timeout 300.0 438 GRP027-2 timeout 300.0 429 GRP039-6 theorem 1.6 8 GRP123-1.003 theorem 0.0 6 GRP123-1.005 non_thm 1.2 6 GRP123-2.003 theorem 0.0 6 GRP123-2.005 non_thm 0.4 6 GRP123-3.003 theorem 0.0 6 GRP123-3.004 non_thm 0.1 6 GRP123-4.003 theorem 0.0 6 GRP123-4.004 non_thm 0.0 6 GRP123-6.003 theorem 0.0 6 GRP123-6.005 non_thm 1.1 6 GRP123-7.003 theorem 0.0 6 GRP123-7.005 non_thm 1.1 6 GRP123-8.003 theorem 0.0 6 GRP123-8.004 non_thm 0.1 6 GRP123-9.003 theorem 0.0 6 GRP123-9.004 non_thm 0.0 6 GRP124-1.004 theorem 0.0 6 GRP124-1.005 non_thm 0.8 6 GRP124-2.004 theorem 0.0 6 GRP124-2.005 non_thm 0.3 6 GRP124-3.004 theorem 0.1 6 GRP124-3.005 non_thm 0.9 6 GRP124-4.004 theorem 0.0 6 GRP124-4.005 non_thm 0.5 6 GRP124-6.004 theorem 0.0 6 GRP124-6.005 non_thm 1.8 6 GRP124-7.004 theorem 0.0 4 GRP124-7.005 non_thm 1.8 6 GRP124-8.004 theorem 0.1 6 GRP124-8.005 non_thm 0.4 6 GRP124-9.004 theorem 0.0 6 GRP124-9.005 non_thm 1.8 6 GRP125-1.003 theorem 0.0 6 GRP125-1.004 non_thm 0.0 6 GRP125-2.004 non_thm 0.0 6 GRP125-2.005 theorem 0.1 4 GRP125-3.004 non_thm 0.1 6 GRP125-3.005 theorem 4.3 6 GRP125-4.003 theorem 0.0 6 GRP125-4.004 non_thm 0.0 6 GRP126-1.004 theorem 0.0 6 GRP126-1.005 non_thm 0.2 6 GRP126-2.004 theorem 0.0 6 GRP126-2.005 non_thm 0.1 6 GRP126-3.004 theorem 0.1 4 GRP126-3.005 non_thm 0.6 6 GRP126-4.004 theorem 0.0 6 GRP126-4.005 non_thm 0.7 6 GRP127-1.004 theorem 0.0 6 GRP127-1.005 non_thm 0.3 6 GRP127-2.005 non_thm 0.1 4 GRP127-2.006 theorem 0.2 6 GRP127-3.004 theorem 0.1 4 GRP127-3.005 non_thm 3.4 6 GRP127-4.004 theorem 0.0 6 GRP127-4.005 non_thm 0.4 6 GRP128-1.003 theorem 0.0 6 GRP128-1.004 non_thm 0.5 6 GRP128-2.004 non_thm 0.2 6 GRP128-2.006 timeout 300.0 6 GRP128-3.004 non_thm 3.4 6 GRP128-3.005 timeout 300.0 6 GRP128-4.003 theorem 0.0 6 GRP128-4.004 non_thm 0.9 6 GRP129-1.003 theorem 0.0 6 GRP129-1.005 timeout 300.0 6 GRP129-2.004 theorem 3.7 6 GRP129-2.005 timeout 300.0 6 GRP129-3.004 theorem 45.8 6 GRP129-3.005 timeout 300.0 6 GRP129-4.004 theorem 1.6 6 GRP129-4.005 non_thm 187.7 6 GRP130-1.003 theorem 0.0 6 GRP130-1.005 non_thm 103.0 6 GRP130-2.003 theorem 0.0 4 GRP130-2.005 non_thm 108.0 6 GRP130-3.003 theorem 0.1 6 GRP130-3.004 non_thm 9.3 6 GRP130-4.003 theorem 0.0 6 GRP130-4.004 non_thm 0.2 6 GRP131-1.002 theorem 0.0 6 GRP131-1.005 non_thm 3.5 6 GRP131-2.002 theorem 0.0 4 GRP131-2.005 timeout 300.0 6 GRP132-1.002 theorem 0.0 6 GRP132-1.005 non_thm 8.1 6 GRP132-2.002 theorem 0.0 6 GRP132-2.005 non_thm 64.3 6 GRP133-1.003 theorem 0.0 6 GRP133-1.004 non_thm 0.2 6 GRP133-2.003 theorem 0.0 6 GRP133-2.004 non_thm 0.3 6 GRP134-1.003 theorem 0.0 6 GRP134-1.005 non_thm 11.0 6 GRP134-2.003 theorem 0.0 6 GRP134-2.005 non_thm 20.7 6 GRP135-1.002 theorem 0.0 6 GRP135-1.005 timeout 300.0 6 GRP135-2.002 theorem 0.0 4 GRP135-2.005 timeout 300.0 6 HWV003-3 theorem 0.0 6 HWV005-1 theorem 0.0 6 HWV005-2 theorem 0.0 6 HWV006-1 theorem 0.0 4 HWV006-2 theorem 0.0 4 HWV007-1 theorem 0.0 6 HWV007-2 theorem 0.0 4 HWV008-1.001 theorem 0.0 6 HWV008-1.002 theorem 0.0 6 HWV008-2.001 theorem 0.0 6 HWV008-2.002 theorem 0.0 6 HWV034-1 non_thm 0.0 4 HWV034-2 non_thm 0.0 6 HWV035-1 non_thm 0.0 6 HWV035-2 non_thm 0.0 6 HWV036-1 non_thm 0.0 6 HWV036-2 non_thm 0.0 6 KRS001-1 theorem 0.0 6 KRS002-1 theorem 0.0 4 KRS003-1 theorem 0.0 6 KRS005-1 non_thm 0.0 4 KRS006-1 non_thm 0.0 6 KRS007-1 non_thm 0.0 6 KRS008-1 non_thm 4.7 6 KRS009-1 non_thm 0.1 6 KRS010-1 theorem 0.0 6 KRS011-1 non_thm 0.0 6 KRS012-1 theorem 0.0 6 KRS013-1 theorem 0.0 6 KRS014-1 non_thm 0.0 4 KRS015-1 theorem 0.0 6 KRS016-1 non_thm 0.0 6 KRS017-1 theorem 0.0 4 LCL181-2 theorem 0.0 6 LCL230-2 theorem 0.0 4 MGT004-1 theorem 0.0 4 MGT007-1 theorem 0.0 4 MGT016-1 theorem 0.0 6 MGT018-1 theorem 0.0 4 MGT022-1 theorem 0.0 6 MGT022-2 theorem 0.0 6 MGT028-1 theorem 0.0 4 MGT030-1 theorem 0.0 4 MGT036-1 theorem 0.0 6 MGT036-2 theorem 0.0 4 MGT041-2 theorem 0.0 6 MSC001-1 theorem 0.3 8 MSC002-1 theorem 0.0 4 MSC002-2 theorem 0.0 6 MSC003-1 theorem 0.0 6 MSC004-1 theorem 0.0 6 MSC006-1 theorem 0.0 6 MSC007-1.008 theorem 2.5 6 MSC008-1.002 theorem 0.1 6 MSC008-1.010 timeout 300.0 8 MSC008-2.002 theorem 0.0 6 MSC009-1 non_thm 0.0 6 NLP026-1 non_thm 9.7 21 NLP027-1 timeout 300.0 80 NLP028-1 timeout 300.0 79 NLP029-1 timeout 300.0 70 NLP030-1 timeout 300.0 122 NLP031-1 non_thm 2.9 6 NLP032-1 timeout 300.0 16 NLP033-1 timeout 300.0 8 NLP034-1 timeout 300.0 70 NLP035-1 timeout 300.0 27 NLP043-1 non_thm 0.0 6 NLP044-1 non_thm 0.0 6 NLP045-1 non_thm 0.0 6 NLP046-1 non_thm 0.0 6 NLP047-1 non_thm 0.0 6 NLP048-1 non_thm 0.0 4 NLP059-1 non_thm 0.0 6 NLP060-1 timeout 300.0 6 NLP061-1 non_thm 0.3 6 NLP062-1 non_thm 0.0 4 NLP063-1 timeout 300.0 6 NLP064-1 non_thm 9.1 9 NLP065-1 non_thm 114.4 6 NLP066-1 non_thm 0.0 6 NLP067-1 non_thm 0.1 6 NLP068-1 non_thm 0.0 4 NLP079-1 theorem 0.0 6 NLP080-1 theorem 0.0 6 NLP081-1 theorem 0.0 6 NLP094-1 theorem 0.0 6 NLP095-1 non_thm 0.0 6 NLP096-1 non_thm 0.0 6 NLP097-1 non_thm 0.0 6 NLP098-1 non_thm 0.0 6 NLP099-1 non_thm 0.0 6 NLP100-1 non_thm 0.0 6 NLP101-1 non_thm 0.0 6 NLP102-1 non_thm 0.0 6 NLP103-1 non_thm 0.0 4 NLP114-1 non_thm 0.0 6 NLP115-1 non_thm 0.0 6 NLP116-1 non_thm 0.0 6 NLP117-1 theorem 0.0 6 NLP118-1 non_thm 0.0 6 NLP119-1 non_thm 0.0 6 NLP120-1 non_thm 0.0 6 NLP121-1 non_thm 0.0 6 NLP122-1 theorem 0.0 6 NLP123-1 non_thm 0.0 6 NLP130-1 non_thm 0.0 6 NLP131-1 non_thm 0.0 6 NLP132-1 non_thm 0.0 6 NLP133-1 non_thm 0.0 4 NLP134-1 non_thm 0.0 6 NLP135-1 non_thm 0.0 6 NLP136-1 non_thm 0.0 6 NLP137-1 non_thm 0.0 6 NLP138-1 non_thm 0.0 4 NLP139-1 non_thm 0.0 6 NLP160-1 non_thm 0.1 4 NLP161-1 non_thm 0.1 6 NLP162-1 non_thm 0.1 6 NLP163-1 non_thm 0.2 6 NLP164-1 non_thm 0.2 6 NLP165-1 non_thm 0.2 6 NLP166-1 non_thm 0.1 6 NLP167-1 non_thm 0.1 6 NLP168-1 non_thm 0.1 6 NLP169-1 non_thm 0.1 6 NLP190-1 non_thm 0.1 6 NLP191-1 non_thm 0.1 6 NLP192-1 non_thm 0.1 6 NLP193-1 non_thm 0.1 6 NLP194-1 non_thm 0.1 6 NLP195-1 non_thm 0.1 6 NLP196-1 non_thm 0.1 6 NLP197-1 non_thm 0.0 6 NLP198-1 non_thm 0.1 6 NLP199-1 non_thm 0.1 6 NLP221-1 non_thm 0.0 6 NLP222-1 non_thm 0.0 6 NLP223-1 non_thm 0.0 6 NLP230-1 non_thm 0.1 6 NLP231-1 non_thm 0.0 6 NLP232-1 non_thm 0.0 6 NLP233-1 non_thm 0.0 6 NLP234-1 non_thm 0.0 6 NLP235-1 non_thm 0.0 6 NLP236-1 non_thm 0.2 6 NLP237-1 non_thm 0.2 6 NLP238-1 non_thm 0.2 6 NLP239-1 non_thm 0.2 6 NUM014-1 theorem 0.0 6 NUM015-1 theorem 0.0 6 NUM016-1 theorem 0.0 6 NUM016-2 theorem 0.0 6 NUM021-1 theorem 0.1 6 NUM022-1 theorem 0.0 6 NUM025-2 theorem 0.0 6 NUM027-1 theorem 0.4 6 NUM285-1 non_thm 0.0 6 NUM288-1 non_thm 0.0 0 PLA002-1 theorem 0.0 4 PLA002-2 theorem 0.0 6 PUZ001-1 theorem 0.0 4 PUZ001-3 non_thm 0.0 6 PUZ002-1 theorem 0.0 6 PUZ004-1 theorem 0.0 6 PUZ005-1 theorem 0.0 6 PUZ009-1 theorem 0.0 6 PUZ010-1 theorem 39.5 6 PUZ012-1 theorem 0.0 6 PUZ013-1 theorem 0.0 6 PUZ014-1 theorem 0.0 6 PUZ015-2.006 theorem 0.6 6 PUZ016-2.004 non_thm 0.0 6 PUZ016-2.005 theorem 0.1 6 PUZ017-1 theorem 40.4 6 PUZ018-1 theorem 0.0 6 PUZ018-2 non_thm 0.0 6 PUZ019-1 theorem 0.0 4 PUZ021-1 theorem 0.5 7 PUZ023-1 theorem 0.0 4 PUZ024-1 theorem 0.0 4 PUZ025-1 theorem 0.0 6 PUZ026-1 theorem 0.0 6 PUZ027-1 theorem 0.0 6 PUZ028-1 non_thm 0.0 6 PUZ028-2 non_thm 0.0 6 PUZ028-3 non_thm 0.3 6 PUZ028-4 non_thm 0.2 6 PUZ028-5 theorem 0.1 6 PUZ028-6 theorem 0.2 6 PUZ029-1 theorem 0.0 6 PUZ030-1 theorem 0.0 6 PUZ030-2 theorem 0.0 6 PUZ031-1 theorem 0.0 6 PUZ032-1 theorem 0.0 6 PUZ033-1 theorem 0.0 0 PUZ034-1.003 timeout 300.0 317 PUZ034-1.004 memory 183.6 499 PUZ035-1 theorem 0.0 4 PUZ035-2 theorem 0.0 6 PUZ035-3 theorem 0.0 4 PUZ035-4 theorem 0.0 6 PUZ035-5 theorem 0.0 6 PUZ035-6 theorem 0.0 6 PUZ035-7 theorem 0.0 6 PUZ044-1 non_thm 0.0 6 PUZ045-1 non_thm 0.0 6 SET001-1 theorem 0.0 4 SET002-1 theorem 0.0 6 SET003-1 theorem 0.0 6 SET004-1 theorem 0.0 6 SET005-1 theorem 0.0 6 SET006-1 theorem 0.0 6 SET007-1 theorem 0.0 6 SET008-1 theorem 0.0 0 SET009-1 theorem 0.0 6 SET010-1 theorem 0.0 6 SET011-1 theorem 0.0 6 SET012-1 timeout 300.0 357 SET012-2 theorem 1.3 8 SET013-1 timeout 300.0 252 SET013-2 theorem 0.7 6 SET014-2 timeout 300.0 96 SET015-1 timeout 300.0 273 SET015-2 theorem 0.8 6 SET043-5 theorem 0.0 6 SET044-5 theorem 0.0 6 SET045-5 theorem 0.0 4 SET046-5 theorem 0.0 6 SET047-5 theorem 0.0 0 SET055-6 theorem 1.4 11 SET055-7 theorem 0.1 6 SET777-1 non_thm 0.0 6 SET778-1 non_thm 0.0 6 SET779-1 non_thm 0.0 6 SET780-1 non_thm 0.0 6 SET781-1 timeout 300.0 111 SET786-1 theorem 0.0 6 SWV001-1 theorem 0.0 6 SWV009-1 theorem 0.0 4 SYN001-1.005 theorem 0.0 4 SYN002-1.007.008 theorem 0.0 6 SYN006-1 theorem 0.0 0 SYN008-1 theorem 0.0 6 SYN009-1 theorem 0.0 6 SYN009-2 theorem 0.0 6 SYN009-3 theorem 0.0 6 SYN009-4 theorem 0.0 6 SYN011-1 theorem 0.0 6 SYN012-1 theorem 0.0 6 SYN014-2 theorem 0.0 6 SYN015-2 theorem 0.0 6 SYN028-1 theorem 0.0 4 SYN029-1 theorem 0.0 6 SYN030-1 theorem 0.0 6 SYN031-1 theorem 0.0 6 SYN032-1 theorem 0.0 6 SYN034-1 theorem 0.0 6 SYN036-1 timeout 300.0 10 SYN036-2 non_thm 1.5 6 SYN036-3 theorem 0.0 4 SYN036-4 theorem 0.1 6 SYN037-1 theorem 0.0 6 SYN037-2 theorem 0.0 6 SYN038-1 theorem 0.0 6 SYN039-1 theorem 0.1 6 SYN044-1 theorem 0.0 6 SYN045-1 theorem 0.0 6 SYN047-1 theorem 0.0 6 SYN051-1 theorem 0.0 6 SYN052-1 theorem 0.0 6 SYN053-1 theorem 0.0 6 SYN054-1 theorem 0.0 6 SYN055-1 theorem 0.0 6 SYN056-1 non_thm 0.0 4 SYN059-1 non_thm 0.0 6 SYN060-1 theorem 0.0 6 SYN061-1 theorem 0.0 0 SYN063-1 theorem 0.0 6 SYN066-1 theorem 0.0 0 SYN067-1 theorem 3.1 6 SYN067-2 theorem 32.2 6 SYN067-3 theorem 20.7 6 SYN069-1 theorem 0.0 6 SYN070-1 theorem 0.0 4 SYN081-1 theorem 0.0 4 SYN082-1 theorem 0.0 4 SYN084-1 non_thm 0.0 4 SYN084-2 theorem 0.0 6 SYN091-1.003 non_thm 0.0 4 SYN092-1.003 non_thm 0.0 6 SYN093-1.002 theorem 0.0 6 SYN094-1.005 theorem 0.0 6 SYN097-1.002 theorem 0.0 4 SYN098-1.002 theorem 0.0 6 SYN099-1.003 theorem 0.0 6 SYN100-1.005 theorem 0.0 6 SYN304-1 non_thm 0.0 6 SYN306-1 non_thm 0.0 4 SYN307-1 non_thm 0.0 6 SYN308-1 non_thm 0.0 4 SYN309-1 non_thm 0.0 0 SYN313-1.001.002 theorem 0.0 6 SYN314-1.002.001 timeout 300.0 93 SYN315-1 theorem 0.0 6 SYN316-1 timeout 300.0 67 SYN317-1 non_thm 0.0 4 SYN319-1 theorem 0.0 6 SYN320-1 non_thm 0.0 6 SYN321-1 theorem 0.0 6 SYN323-1 theorem 0.0 6 SYN324-1 timeout 300.0 75 SYN325-1 theorem 0.0 6 SYN326-1 theorem 0.0 6 SYN327-1 theorem 0.0 6 SYN328-1 theorem 0.0 6 SYN330-1 timeout 300.0 105 SYN331-1 theorem 0.0 6 SYN332-1 theorem 0.0 6 SYN334-1 theorem 0.0 6 SYN335-1 timeout 300.0 69 SYN343-1 theorem 0.0 6 SYN344-1 non_thm 0.0 4 SYN345-1 theorem 0.0 6 SYN347-1 theorem 0.0 6 SYN348-1 non_thm 0.0 6 SYN349-1 theorem 0.0 4 SYN350-1 theorem 0.0 6 SYN351-1 timeout 300.0 411 SYN352-1 theorem 0.0 6 SYN353-1 timeout 300.0 53 SYN354-1 theorem 0.0 6 SYN418-1 non_thm 1.0 6 SYN419-1 non_thm 0.7 6 SYN420-1 non_thm 0.5 6 SYN421-1 non_thm 1.2 6 SYN422-1 non_thm 1.1 6 SYN423-1 non_thm 1.2 8 SYN424-1 non_thm 2.8 8 SYN425-1 non_thm 1.1 6 SYN426-1 non_thm 1.9 8 SYN427-1 non_thm 5.3 27 SYN428-1 non_thm 1.0 10 SYN429-1 non_thm 1.2 10 SYN430-1 non_thm 0.0 6 SYN431-1 non_thm 0.0 6 SYN432-1 non_thm 0.1 6 SYN433-1 non_thm 10.9 6 SYN434-1 timeout 300.0 8 SYN435-1 non_thm 0.6 6 SYN436-1 timeout 300.0 8 SYN437-1 timeout 300.0 8 SYN438-1 timeout 300.0 8 SYN439-1 timeout 300.0 8 SYN440-1 timeout 300.0 6 SYN441-1 timeout 300.0 7 SYN442-1 timeout 300.0 8 SYN443-1 timeout 300.0 8 SYN444-1 theorem 265.4 10 SYN445-1 theorem 10.2 6 SYN446-1 non_thm 79.5 8 SYN447-1 timeout 300.0 6 SYN448-1 timeout 300.0 8 SYN449-1 timeout 300.0 8 SYN450-1 theorem 51.0 8 SYN451-1 timeout 300.0 8 SYN452-1 theorem 11.3 6 SYN453-1 timeout 300.0 10 SYN454-1 timeout 300.0 8 SYN455-1 timeout 300.0 8 SYN456-1 timeout 300.0 8 SYN457-1 timeout 300.0 8 SYN458-1 timeout 300.0 10 SYN459-1 theorem 166.5 8 SYN460-1 timeout 300.0 8 SYN461-1 timeout 300.0 8 SYN462-1 timeout 300.0 8 SYN463-1 timeout 300.0 8 SYN464-1 non_thm 0.3 6 SYN465-1 timeout 300.0 8 SYN466-1 timeout 300.0 8 SYN467-1 theorem 75.2 6 SYN468-1 theorem 219.8 8 SYN469-1 timeout 300.0 8 SYN470-1 timeout 300.0 12 SYN471-1 theorem 36.4 6 SYN472-1 timeout 300.0 8 SYN473-1 timeout 300.0 8 SYN474-1 theorem 162.9 8 SYN475-1 theorem 43.7 6 SYN476-1 timeout 300.0 8 SYN477-1 timeout 300.0 8 SYN478-1 theorem 63.5 8 SYN479-1 timeout 300.0 10 SYN480-1 timeout 300.0 8 SYN481-1 timeout 300.0 8 SYN482-1 timeout 300.0 8 SYN483-1 theorem 79.0 8 SYN484-1 theorem 6.2 6 SYN485-1 timeout 300.0 8 SYN486-1 theorem 299.7 8 SYN487-1 timeout 300.0 8 SYN488-1 timeout 300.0 8 SYN489-1 timeout 300.0 8 SYN490-1 non_thm 0.0 6 SYN491-1 non_thm 0.0 6 SYN492-1 non_thm 0.0 6 SYN493-1 non_thm 0.0 6 SYN494-1 non_thm 0.0 6 SYN495-1 non_thm 0.0 6 SYN496-1 non_thm 0.0 6 SYN497-1 non_thm 0.0 6 SYN498-1 timeout 300.0 8 SYN499-1 timeout 300.0 8 SYN500-1 timeout 300.0 8 SYN501-1 theorem 154.6 6 SYN502-1 timeout 300.0 8 SYN503-1 theorem 256.3 8 SYN504-1 theorem 41.6 6 SYN505-1 theorem 31.7 6 SYN506-1 theorem 47.6 6 SYN507-1 timeout 300.0 8 SYN508-1 theorem 18.1 6 SYN509-1 theorem 45.1 6 SYN510-1 theorem 72.2 8 SYN511-1 theorem 14.3 6 SYN512-1 theorem 33.4 6 SYN513-1 non_thm 0.3 6 SYN514-1 non_thm 89.8 12 SYN515-1 non_thm 0.0 6 SYN516-1 non_thm 0.0 6 SYN517-1 non_thm 0.0 6 SYN518-1 non_thm 1.3 10 SYN519-1 timeout 300.0 16 SYN520-1 non_thm 1.0 6 SYN521-1 non_thm 0.0 6 SYN522-1 non_thm 0.0 6 SYN523-1 non_thm 0.0 6 SYN524-1 non_thm 0.0 6 SYN525-1 non_thm 0.0 6 SYN526-1 non_thm 0.1 6 SYN527-1 non_thm 0.0 6 SYN528-1 non_thm 0.0 6 SYN529-1 non_thm 0.0 6 SYN530-1 non_thm 0.0 6 SYN531-1 non_thm 0.0 4 SYN532-1 non_thm 0.0 6 SYN533-1 non_thm 0.0 6 SYN534-1 non_thm 0.0 6 SYN535-1 non_thm 0.0 6 SYN536-1 non_thm 0.0 6 SYN537-1 non_thm 0.1 6 SYN538-1 non_thm 0.0 6 SYN539-1 non_thm 0.1 6 SYN540-1 non_thm 0.1 6 SYN541-1 non_thm 0.0 6 SYN542-1 timeout 300.0 12 SYN543-1 timeout 300.0 8 SYN544-1 non_thm 0.4 6 SYN545-1 non_thm 0.4 6 SYN546-1 non_thm 11.2 44 SYN547-1 non_thm 0.8 6 SYN554-1 theorem 0.0 6 SYN560-1 timeout 300.0 170 SYN567-1 theorem 0.0 6 SYN568-1 theorem 0.0 0 SYN571-1 theorem 0.0 6 SYN573-1 theorem 0.5 6 SYN574-1 theorem 0.0 6 SYN575-1 theorem 0.0 4 SYN576-1 theorem 0.5 6 SYN578-1 theorem 0.0 6 SYN579-1 theorem 0.0 4 SYN580-1 theorem 0.0 6 SYN581-1 theorem 0.0 6 SYN582-1 theorem 0.0 6 SYN583-1 theorem 0.0 6 SYN585-1 theorem 8.7 45 SYN586-1 theorem 0.2 6 SYN587-1 theorem 0.0 6 SYN591-1 theorem 0.0 6 SYN592-1 theorem 0.0 6 SYN593-1 theorem 0.0 4 SYN594-1 theorem 0.0 6 SYN595-1 theorem 0.0 6 SYN604-1 theorem 1.5 12 SYN605-1 timeout 300.0 77 SYN606-1 timeout 300.0 60 SYN607-1 timeout 300.0 77 SYN608-1 timeout 300.0 60 SYN609-1 timeout 300.0 77 SYN610-1 timeout 300.0 60 SYN611-1 timeout 300.0 77 SYN612-1 timeout 300.0 60 SYN613-1 theorem 0.0 6 SYN619-1 theorem 0.0 6 SYN620-1 theorem 0.0 6 SYN621-1 theorem 0.0 6 SYN622-1 theorem 0.0 6 SYN623-1 theorem 0.1 6 SYN624-1 theorem 0.1 6 SYN625-1 theorem 0.0 6 SYN626-1 theorem 0.0 6 SYN627-1 theorem 0.0 6 SYN630-1 theorem 0.0 6 SYN633-1 timeout 300.0 27 SYN634-1 theorem 139.6 26 SYN635-1 timeout 300.0 43 SYN636-1 timeout 300.0 34 SYN641-1 theorem 0.1 6 SYN642-1 theorem 0.0 6 SYN643-1 theorem 0.0 6 SYN644-1 timeout 300.0 16 SYN645-1 theorem 0.1 4 SYN648-1 theorem 0.3 8 SYN650-1 timeout 300.0 27 SYN656-1 theorem 0.0 4 SYN657-1 timeout 300.0 36 SYN658-1 timeout 300.0 36 SYN659-1 theorem 0.1 6 SYN660-1 theorem 0.0 6 SYN661-1 theorem 0.0 6 SYN662-1 theorem 0.0 6 SYN663-1 theorem 0.0 6 SYN664-1 theorem 0.0 6 SYN665-1 theorem 0.0 6 SYN666-1 theorem 0.0 6 SYN667-1 theorem 0.0 6 SYN668-1 theorem 0.0 6 SYN669-1 theorem 0.0 6 SYN670-1 theorem 0.0 6 SYN671-1 theorem 0.0 6 SYN672-1 theorem 0.0 6 SYN673-1 timeout 300.0 27 SYN674-1 theorem 0.0 6 SYN675-1 theorem 0.0 6 SYN676-1 theorem 0.0 6 SYN677-1 theorem 0.0 6 SYN678-1 theorem 0.0 6 SYN679-1 theorem 0.0 6 SYN680-1 theorem 0.0 6 SYN681-1 theorem 0.0 6 SYN682-1 theorem 0.0 6 SYN683-1 theorem 0.0 6 SYN684-1 theorem 0.0 6 SYN685-1 theorem 0.0 6 SYN686-1 theorem 0.1 4 SYN687-1 theorem 0.0 6 SYN690-1 theorem 0.1 6 SYN692-1 theorem 5.5 16 SYN693-1 theorem 5.6 16 SYN694-1 theorem 3.5 21 SYN695-1 theorem 5.1 16 SYN696-1 theorem 3.1 16 SYN697-1 theorem 4.3 16 SYN698-1 theorem 3.4 21 SYN699-1 theorem 5.4 16 SYN700-1 theorem 3.1 16 SYN701-1 theorem 4.3 16 SYN710-1 theorem 0.1 6 SYN713-1 theorem 0.0 6 SYN714-1 theorem 0.0 6 SYN717-1 theorem 0.0 6 SYN718-1 theorem 0.1 6 SYN724-1 theorem 0.0 4 SYN726-1 theorem 0.0 6 SYN728-1 theorem 0.0 4 SYN734-1 timeout 300.0 84 SYN735-1 non_thm 0.0 6 SYN736-1 timeout 300.0 159 SYN737-1 timeout 300.0 42 SYN738-1 non_thm 0.0 6 SYN739-1 timeout 300.0 109 SYN740-1 non_thm 0.0 6 SYN741-1 timeout 300.0 34 SYN742-1 non_thm 0.0 4 SYN743-1 non_thm 0.0 6 SYN744-1 non_thm 0.0 6 SYN745-1 timeout 300.0 20 SYN746-1 timeout 300.0 8 SYN747-1 timeout 300.0 20 SYN748-1 non_thm 0.0 6 SYN749-1 non_thm 0.0 6 SYN750-1 timeout 300.0 68 SYN751-1 timeout 300.0 193 SYN752-1 timeout 300.0 85 SYN753-1 timeout 300.0 12 SYN754-1 non_thm 0.0 4 SYN755-1 theorem 4.9 6 SYN756-1 non_thm 0.0 6 SYN757-1 timeout 300.0 59 SYN758-1 timeout 300.0 9 SYN759-1 timeout 300.0 10 SYN760-1 non_thm 0.0 6 SYN761-1 timeout 300.0 12 SYN762-1 timeout 300.0 10 SYN763-1 timeout 300.0 51 SYN764-1 timeout 300.0 52 SYN765-1 timeout 300.0 10 SYN766-1 timeout 300.0 186 SYN767-1 timeout 300.0 10 SYN768-1 timeout 300.0 21 SYN769-1 non_thm 0.0 6 SYN770-1 timeout 300.0 8 SYN771-1 timeout 300.0 10 SYN772-1 non_thm 0.0 6 SYN773-1 timeout 300.0 88 SYN774-1 non_thm 0.0 6 SYN775-1 timeout 300.0 6 SYN776-1 timeout 300.0 6 SYN777-1 timeout 300.0 8 SYN778-1 timeout 300.0 6 SYN779-1 timeout 300.0 8 SYN780-1 non_thm 0.0 6 SYN781-1 timeout 300.0 36 SYN782-1 timeout 300.0 13 SYN783-1 timeout 300.0 16 SYN784-1 timeout 300.0 6 SYN785-1 non_thm 0.0 6 SYN786-1 non_thm 0.0 6 SYN787-1 timeout 300.0 8 SYN788-1 timeout 300.0 10 SYN789-1 timeout 300.0 6 SYN790-1 memory 36.5 499 SYN791-1 timeout 300.0 8 SYN792-1 timeout 300.0 10 SYN793-1 timeout 300.0 12 SYN794-1 non_thm 0.0 6 SYN795-1 timeout 300.0 8 SYN796-1 timeout 300.0 6 SYN797-1 non_thm 0.8 6 SYN798-1 non_thm 0.0 6 SYN799-1 timeout 300.0 6 SYN800-1 timeout 300.0 6 SYN801-1 timeout 300.0 8 SYN802-1 timeout 300.0 6 SYN803-1 timeout 300.0 8 SYN804-1 timeout 300.0 6 SYN805-1 timeout 300.0 10 SYN806-1 timeout 300.0 8 SYN807-1 timeout 300.0 8 SYN808-1 timeout 300.0 8 SYN809-1 timeout 300.0 8 SYN810-1 timeout 300.0 8 SYN811-1 non_thm 22.7 12 SYN812-1 non_thm 62.9 61 SYN813-1 theorem 11.7 15 SYN814-1 non_thm 63.3 27 SYN815-1 non_thm 17.1 28 SYN816-1 non_thm 17.0 27 SYN817-1 non_thm 20.5 28 SYN818-1 non_thm 128.0 78 SYN819-1 theorem 8.9 18 SYN820-1 theorem 10.0 18 SYN821-1 non_thm 23.9 36 SYN822-1 non_thm 28.1 36 SYN823-1 non_thm 1.0 18 SYN824-1 non_thm 13.2 18 SYN825-1 non_thm 12.8 44 SYN826-1 non_thm 15.2 45 SYN827-1 non_thm 1.8 18 SYN828-1 non_thm 5.2 21 SYN829-1 non_thm 23.9 53 SYN830-1 non_thm 26.4 62 SYN831-1 non_thm 24.3 53 SYN832-1 non_thm 20.6 45 SYN833-1 theorem 2.9 18 SYN834-1 theorem 2.8 18 SYN835-1 non_thm 2.2 18 SYN836-1 theorem 1.8 7 SYN837-1 theorem 10.7 12 SYN838-1 non_thm 6.8 27 SYN839-1 non_thm 31.0 70 SYN840-1 non_thm 30.5 62 SYN841-1 non_thm 32.1 70 SYN842-1 non_thm 37.5 62 SYN843-1 theorem 4.6 21 SYN844-1 theorem 4.1 21 SYN845-1 theorem 5.5 8 SYN846-1 theorem 15.3 21 SYN847-1 theorem 13.3 21 SYN848-1 theorem 14.8 12 SYN849-1 theorem 12.5 21 SYN850-1 theorem 8.7 28 SYN851-1 non_thm 7.7 28 SYN852-1 non_thm 43.9 62 SYN853-1 non_thm 39.9 62 SYN854-1 non_thm 41.0 62 SYN855-1 non_thm 38.5 62 SYN856-1 theorem 5.7 21 SYN857-1 theorem 7.1 21 SYN858-1 theorem 2.6 12 SYN859-1 theorem 2.7 21 SYN860-1 theorem 3.0 21 SYN861-1 theorem 9.3 28 SYN862-1 theorem 9.8 28 SYN863-1 timeout 300.0 112 SYN864-1 non_thm 8.8 28 SYN865-1 theorem 10.5 27 SYN866-1 theorem 10.6 28 SYN867-1 non_thm 0.0 21 SYN868-1 non_thm 0.0 6 SYN869-1 theorem 0.1 21 SYN870-1 non_thm 0.1 21 SYN871-1 theorem 0.1 21 SYN872-1 non_thm 0.2 21 SYN873-1 theorem 0.3 21 SYN874-1 theorem 0.3 21 SYN875-1 theorem 0.4 6 SYN876-1 theorem 0.3 21 SYN877-1 theorem 0.3 21 SYN878-1 theorem 0.5 6 SYN879-1 theorem 1.7 21 SYN880-1 theorem 0.8 21 SYN881-1 theorem 0.5 6 SYN882-1 theorem 1.0 21 SYN883-1 theorem 1.0 21 SYN884-1 theorem 1.1 21 SYN885-1 theorem 1.8 21 SYN886-1 theorem 1.1 21 SYN887-1 theorem 1.2 21 SYN888-1 non_thm 0.9 21 SYN889-1 theorem 0.5 21 SYN890-1 theorem 0.5 21 SYN891-1 theorem 0.5 21 SYN892-1 theorem 0.5 21 SYN893-1 theorem 0.7 6 SYN894-1 theorem 0.7 21 SYN895-1 theorem 1.3 21 SYN896-1 theorem 1.1 21 SYN897-1 timeout 300.0 162 SYN898-1 theorem 3.0 21 SYN899-1 theorem 3.3 21 SYN900-1 theorem 2.4 21 SYN901-1 theorem 5.0 21 SYN902-1 non_thm 1.0 21 SYN903-1 non_thm 0.7 21 SYN904-1 non_thm 2.6 21 SYN905-1 non_thm 5.4 21 SYN906-1 timeout 300.0 149 SYN907-1 non_thm 3.3 21 SYN908-1 non_thm 14.1 44 SYN909-1 non_thm 2.4 20 SYN910-1 non_thm 10.2 43 SYN911-1 timeout 300.0 34 SYN912-1 non_thm 17.5 52 SYN913-1 timeout 300.0 21 TOP001-1 timeout 300.0 36 TOP001-2 theorem 36.7 52 TOP002-1 timeout 300.0 21 TOP002-2 theorem 0.0 21 TOP003-1 timeout 300.0 21 TOP003-2 non_thm 0.0 21 TOP004-1 theorem 0.0 6 TOP004-2 theorem 0.0 6 TOP005-1 timeout 300.0 35 TOP005-2 theorem 26.6 21 TOP006-1 timeout 300.0 53 TOP007-1 timeout 300.0 100 TOP008-1 timeout 300.0 45 TOP009-1 timeout 300.0 158 TOP010-1 timeout 300.0 81 TOP011-1 timeout 300.0 36 TOP012-1 timeout 300.0 180 TOP013-1 timeout 300.0 45 TOP014-1 timeout 300.0 64 TOP015-1 timeout 300.0 45 TOP016-1 timeout 300.0 224 TOP017-1 timeout 300.0 64 TOP018-1 timeout 300.0 184 TOP019-1 timeout 300.0 98