-------------------------------------------------------------------------------- Execute format string : ./dctp-10.21p Problems list file : nne0-problems Output file : nne0-output Summary file : nne0-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.1 0 ANA001-1 timeout 301.3 45 ANA002-1 timeout 301.3 45 ANA002-2 theorem 12.2 21 ANA002-3 timeout 301.2 36 ANA002-4 theorem 12.4 21 ANA003-4 timeout 302.3 52 ANA004-4 timeout 302.4 234 ANA004-5 timeout 301.3 45 ANA005-4 timeout 301.2 61 ANA005-5 timeout 301.3 36 CAT007-3 theorem 0.1 0 COM002-2 theorem 0.1 0 COM003-1 theorem 15.8 8 COM003-2 theorem 0.1 0 COM005-1 timeout 300.2 10 COM006-1 timeout 301.2 13 FLD001-3 theorem 0.1 0 FLD002-3 theorem 0.4 0 FLD003-1 theorem 16.4 10 FLD004-1 theorem 1.6 0 FLD005-1 timeout 301.3 38 FLD005-3 theorem 4.5 28 FLD006-1 theorem 0.5 0 FLD006-3 theorem 0.1 0 FLD007-1 timeout 301.3 45 FLD007-3 theorem 11.4 55 FLD008-1 timeout 301.2 38 FLD008-2 timeout 301.2 55 FLD008-3 timeout 301.2 46 FLD008-4 theorem 14.4 22 FLD009-1 timeout 301.2 13 FLD009-3 theorem 11.7 22 FLD010-1 theorem 11.2 37 FLD010-3 theorem 0.1 0 FLD010-5 theorem 3.2 22 FLD011-1 timeout 301.3 28 FLD011-3 timeout 301.3 55 FLD012-1 timeout 301.3 45 FLD012-2 timeout 301.3 54 FLD012-3 timeout 301.3 55 FLD012-4 timeout 301.3 55 FLD013-1 theorem 0.1 0 FLD013-2 theorem 0.1 0 FLD013-3 theorem 0.2 0 FLD013-4 theorem 0.1 0 FLD013-5 theorem 0.1 0 FLD014-1 timeout 301.2 45 FLD014-3 theorem 0.3 0 FLD015-1 timeout 301.3 37 FLD015-3 theorem 0.7 0 FLD016-1 timeout 301.2 21 FLD016-3 theorem 1.2 0 FLD016-5 theorem 15.5 37 FLD017-1 theorem 0.1 0 FLD017-3 theorem 0.1 0 FLD018-1 theorem 16.3 10 FLD018-3 theorem 0.1 0 FLD019-1 theorem 11.3 22 FLD019-3 theorem 0.1 0 FLD020-1 timeout 301.3 54 FLD020-3 theorem 0.1 0 FLD021-1 theorem 0.1 0 FLD021-3 theorem 0.1 0 FLD022-1 timeout 301.3 45 FLD022-3 theorem 12.3 22 FLD023-1 theorem 0.2 0 FLD023-3 theorem 0.1 0 FLD024-1 timeout 301.2 36 FLD024-3 theorem 0.1 0 FLD025-1 theorem 0.1 0 FLD025-2 theorem 0.1 0 FLD025-3 theorem 0.1 0 FLD025-4 theorem 0.1 0 FLD025-5 theorem 0.1 0 FLD026-1 timeout 301.2 46 FLD026-3 theorem 88.0 37 FLD027-1 timeout 301.3 21 FLD027-3 theorem 1.0 0 FLD028-1 timeout 301.3 46 FLD028-3 theorem 2.4 10 FLD029-1 timeout 301.3 28 FLD029-3 theorem 145.4 47 FLD030-1 theorem 0.1 0 FLD030-2 theorem 0.1 0 FLD030-3 theorem 0.1 0 FLD030-4 theorem 0.1 0 FLD031-1 theorem 142.3 22 FLD031-3 theorem 0.1 0 FLD031-5 theorem 0.2 0 FLD032-1 theorem 0.3 0 FLD032-3 theorem 0.1 0 FLD033-1 timeout 301.3 62 FLD033-3 theorem 0.1 0 FLD034-1 theorem 0.1 0 FLD034-3 theorem 0.1 0 FLD035-1 timeout 301.4 70 FLD035-3 theorem 1.9 6 FLD036-1 timeout 301.3 53 FLD036-3 theorem 3.8 10 FLD037-1 theorem 0.3 0 FLD037-3 theorem 0.1 0 FLD038-1 timeout 301.3 53 FLD038-3 theorem 0.1 0 FLD039-1 theorem 0.1 0 FLD039-3 theorem 0.1 0 FLD040-1 timeout 300.3 45 FLD040-3 theorem 0.7 0 FLD040-5 theorem 1.2 0 FLD041-1 timeout 301.3 28 FLD041-2 timeout 301.3 39 FLD041-3 theorem 20.2 47 FLD041-4 theorem 221.1 18 FLD043-1 timeout 301.2 28 FLD043-3 theorem 0.1 0 FLD043-5 theorem 9.5 37 FLD044-1 timeout 301.2 38 FLD044-2 timeout 301.2 45 FLD044-3 timeout 301.2 38 FLD044-4 timeout 301.2 16 FLD045-1 timeout 301.1 22 FLD045-2 timeout 301.2 17 FLD045-3 timeout 301.1 0 FLD045-4 timeout 301.1 0 FLD046-1 timeout 301.4 28 FLD046-3 timeout 301.4 55 FLD047-1 timeout 301.4 38 FLD047-2 timeout 301.4 53 FLD047-3 timeout 301.4 114 FLD047-4 timeout 301.4 48 FLD048-1 timeout 301.4 38 FLD048-2 timeout 301.4 81 FLD048-3 timeout 301.4 133 FLD048-4 timeout 301.3 88 FLD049-1 timeout 301.3 29 FLD049-2 timeout 301.3 46 FLD049-3 timeout 301.3 97 FLD049-4 theorem 15.8 13 FLD050-1 timeout 301.2 21 FLD050-2 timeout 301.3 47 FLD050-3 theorem 63.5 16 FLD050-4 theorem 17.3 28 FLD051-1 timeout 301.4 36 FLD051-2 timeout 301.4 81 FLD051-3 timeout 301.4 141 FLD051-4 timeout 308.4 74 FLD052-1 timeout 301.2 36 FLD052-2 timeout 301.2 44 FLD052-3 timeout 301.2 37 FLD052-4 timeout 301.2 29 FLD053-1 timeout 301.2 16 FLD053-2 timeout 301.2 63 FLD053-3 timeout 301.2 17 FLD053-4 timeout 301.2 29 FLD054-1 timeout 301.2 22 FLD054-2 timeout 301.2 22 FLD054-3 timeout 301.2 22 FLD054-4 timeout 301.2 17 FLD055-1 theorem 0.1 0 FLD055-3 theorem 0.1 0 FLD056-1 theorem 0.1 0 FLD056-3 theorem 0.1 0 FLD057-1 timeout 301.1 13 FLD057-3 timeout 301.2 16 FLD058-1 theorem 0.1 0 FLD058-3 theorem 0.1 0 FLD059-1 theorem 0.1 0 FLD059-2 theorem 0.1 0 FLD059-3 theorem 0.1 0 FLD059-4 theorem 0.1 0 FLD060-1 theorem 0.1 0 FLD060-2 theorem 0.3 0 FLD060-3 theorem 45.6 36 FLD060-4 theorem 5.1 16 FLD061-1 theorem 0.1 0 FLD061-2 theorem 0.3 0 FLD061-3 theorem 15.9 10 FLD061-4 theorem 10.3 22 FLD062-1 timeout 301.3 27 FLD062-3 theorem 51.0 22 FLD063-1 timeout 301.3 22 FLD063-3 timeout 301.3 28 FLD064-1 theorem 76.3 98 FLD064-3 theorem 11.2 36 FLD065-1 theorem 70.8 17 FLD065-3 theorem 0.5 0 FLD066-1 timeout 301.2 8 FLD066-3 theorem 1.2 0 FLD067-1 theorem 0.2 0 FLD067-2 theorem 74.7 0 FLD067-3 theorem 11.1 29 FLD067-4 theorem 0.1 0 FLD068-1 timeout 301.3 21 FLD068-2 timeout 301.3 29 FLD068-3 timeout 301.3 45 FLD068-4 theorem 0.1 0 FLD069-1 theorem 0.1 0 FLD069-3 theorem 0.1 0 FLD070-1 theorem 0.1 0 FLD070-2 theorem 0.6 0 FLD070-3 theorem 0.1 0 FLD070-4 theorem 0.1 0 FLD071-1 theorem 0.1 0 FLD071-2 theorem 0.1 0 FLD071-3 theorem 0.1 0 FLD071-4 theorem 0.1 0 FLD072-1 timeout 301.3 36 FLD072-2 timeout 301.3 28 FLD072-3 timeout 301.2 21 FLD072-4 timeout 301.2 22 FLD073-1 timeout 301.2 22 FLD073-2 timeout 301.2 22 FLD073-3 timeout 301.2 16 FLD073-4 timeout 301.2 37 FLD074-1 timeout 301.2 28 FLD074-2 timeout 301.2 37 FLD074-3 timeout 301.2 16 FLD074-4 timeout 301.2 16 FLD075-1 timeout 301.2 8 FLD075-2 timeout 301.1 17 FLD075-3 timeout 301.2 12 FLD075-4 timeout 301.2 8 FLD076-1 timeout 301.1 0 FLD076-2 timeout 301.4 36 FLD076-3 timeout 301.4 38 FLD076-4 timeout 301.4 46 FLD077-1 timeout 301.4 54 FLD077-2 timeout 301.4 53 FLD077-3 timeout 301.4 38 FLD077-4 timeout 301.3 55 FLD078-1 timeout 301.4 46 FLD078-2 timeout 301.3 45 FLD078-3 timeout 301.3 63 FLD078-4 timeout 301.3 57 FLD079-1 timeout 301.3 28 FLD079-2 timeout 301.3 21 FLD079-3 timeout 301.3 45 FLD079-4 timeout 301.3 28 FLD080-1 timeout 301.2 17 FLD080-2 timeout 301.2 17 FLD080-3 timeout 301.2 21 FLD080-4 timeout 301.2 46 FLD081-1 timeout 301.2 21 FLD081-2 timeout 301.2 16 FLD081-3 timeout 301.2 16 FLD081-4 timeout 301.2 10 FLD082-1 timeout 301.2 0 FLD082-3 timeout 301.1 0 FLD083-1 timeout 301.4 45 FLD083-3 timeout 301.4 45 FLD084-1 timeout 301.4 22 FLD084-3 timeout 301.4 46 FLD085-1 timeout 301.4 21 FLD085-3 timeout 304.4 55 FLD086-1 timeout 305.4 13 FLD086-3 timeout 301.2 38 FLD087-1 timeout 301.2 28 FLD087-3 timeout 301.2 37 FLD088-1 timeout 301.2 28 FLD088-3 timeout 301.2 36 FLD089-1 timeout 301.2 22 FLD089-3 timeout 301.2 23 FLD090-1 timeout 301.2 8 FLD090-3 timeout 301.2 13 FLD091-1 timeout 301.1 8 FLD091-3 timeout 301.2 0 FLD092-1 timeout 301.4 37 FLD092-3 timeout 301.8 46 FLD093-1 timeout 301.4 28 FLD093-3 timeout 301.3 88 FLD094-1 timeout 301.4 37 FLD094-3 timeout 301.3 57 FLD095-1 timeout 301.4 45 FLD095-2 timeout 301.4 56 FLD095-3 timeout 301.3 28 FLD095-4 timeout 301.3 63 FLD096-1 timeout 301.3 38 FLD096-2 timeout 301.3 48 FLD096-3 timeout 301.3 22 FLD096-4 timeout 301.3 37 FLD097-1 timeout 301.3 48 FLD097-2 timeout 301.3 28 FLD097-3 timeout 301.3 28 FLD097-4 timeout 301.3 17 FLD098-1 timeout 301.3 44 FLD098-2 timeout 301.3 54 FLD098-3 timeout 301.3 22 FLD098-4 timeout 301.3 13 FLD099-1 timeout 301.2 36 FLD099-2 timeout 301.2 17 FLD099-3 timeout 301.3 46 FLD099-4 timeout 301.2 10 FLD100-1 timeout 301.2 16 FLD100-2 timeout 301.2 28 FLD100-3 timeout 301.2 13 FLD100-4 timeout 301.2 13 GRA001-1 theorem 0.1 0 GRP025-3 timeout 301.2 16 GRP026-3 timeout 301.2 13 GRP027-2 timeout 301.2 13 GRP039-6 theorem 3.9 8 GRP123-1.003 theorem 0.1 0 GRP123-1.005 non_thm 0.3 0 GRP123-2.003 theorem 0.1 0 GRP123-2.005 non_thm 0.3 0 GRP123-3.003 theorem 0.1 0 GRP123-3.004 non_thm 0.2 0 GRP123-4.003 theorem 0.1 0 GRP123-4.004 non_thm 0.1 0 GRP123-6.003 theorem 0.1 0 GRP123-6.005 non_thm 0.1 0 GRP123-7.003 theorem 0.1 0 GRP123-7.005 non_thm 0.1 0 GRP123-8.003 theorem 0.1 0 GRP123-8.004 non_thm 0.2 0 GRP123-9.003 theorem 0.1 0 GRP123-9.004 non_thm 0.1 0 GRP124-1.004 theorem 0.1 0 GRP124-1.005 non_thm 0.2 0 GRP124-2.004 theorem 0.1 0 GRP124-2.005 non_thm 0.1 0 GRP124-3.004 theorem 0.1 0 GRP124-3.005 non_thm 2.3 6 GRP124-4.004 theorem 0.1 0 GRP124-4.005 non_thm 0.2 0 GRP124-6.004 theorem 0.1 0 GRP124-6.005 non_thm 0.1 0 GRP124-7.004 theorem 0.1 0 GRP124-7.005 non_thm 0.2 0 GRP124-8.004 theorem 0.1 0 GRP124-8.005 non_thm 1.6 0 GRP124-9.004 theorem 0.1 0 GRP124-9.005 non_thm 0.2 0 GRP125-1.003 theorem 0.1 0 GRP125-1.004 non_thm 0.1 0 GRP125-2.004 non_thm 0.1 0 GRP125-2.005 theorem 0.1 0 GRP125-3.004 non_thm 0.1 0 GRP125-3.005 theorem 0.2 0 GRP125-4.003 theorem 0.1 0 GRP125-4.004 non_thm 0.1 0 GRP126-1.004 theorem 0.1 0 GRP126-1.005 non_thm 0.1 0 GRP126-2.004 theorem 0.1 0 GRP126-2.005 non_thm 0.1 0 GRP126-3.004 theorem 0.1 0 GRP126-3.005 non_thm 0.4 0 GRP126-4.004 theorem 0.1 0 GRP126-4.005 non_thm 0.1 0 GRP127-1.004 theorem 0.1 0 GRP127-1.005 non_thm 0.1 0 GRP127-2.005 non_thm 0.1 0 GRP127-2.006 theorem 0.1 0 GRP127-3.004 theorem 0.1 0 GRP127-3.005 non_thm 0.4 0 GRP127-4.004 theorem 0.1 0 GRP127-4.005 non_thm 0.1 0 GRP128-1.003 theorem 0.1 0 GRP128-1.004 non_thm 0.5 0 GRP128-2.004 non_thm 0.1 0 GRP128-2.006 theorem 0.3 0 GRP128-3.004 non_thm 0.5 0 GRP128-3.005 theorem 1.0 0 GRP128-4.003 theorem 0.1 0 GRP128-4.004 non_thm 0.1 0 GRP129-1.003 theorem 0.1 0 GRP129-1.005 non_thm 5.8 6 GRP129-2.004 theorem 0.1 0 GRP129-2.005 non_thm 0.1 0 GRP129-3.004 theorem 0.2 0 GRP129-3.005 non_thm 11.3 6 GRP129-4.004 theorem 0.3 0 GRP129-4.005 non_thm 0.8 0 GRP130-1.003 theorem 0.1 0 GRP130-1.005 non_thm 2.2 6 GRP130-2.003 theorem 0.1 0 GRP130-2.005 non_thm 0.2 0 GRP130-3.003 theorem 0.1 0 GRP130-3.004 non_thm 0.4 0 GRP130-4.003 theorem 0.1 0 GRP130-4.004 non_thm 0.2 0 GRP131-1.002 theorem 0.1 0 GRP131-1.005 non_thm 0.2 0 GRP131-2.002 theorem 0.1 0 GRP131-2.005 non_thm 0.3 0 GRP132-1.002 theorem 0.1 0 GRP132-1.005 non_thm 2.2 6 GRP132-2.002 theorem 0.1 0 GRP132-2.005 non_thm 0.3 0 GRP133-1.003 theorem 0.1 0 GRP133-1.004 non_thm 0.1 0 GRP133-2.003 theorem 0.1 0 GRP133-2.004 non_thm 0.1 0 GRP134-1.003 theorem 0.1 0 GRP134-1.005 non_thm 0.1 0 GRP134-2.003 theorem 0.1 0 GRP134-2.005 non_thm 0.1 0 GRP135-1.002 theorem 0.1 0 GRP135-1.005 non_thm 6.9 6 GRP135-2.002 theorem 0.1 0 GRP135-2.005 non_thm 0.2 0 HWV003-3 theorem 0.1 0 HWV005-1 theorem 0.1 0 HWV005-2 theorem 0.1 0 HWV006-1 theorem 0.3 0 HWV006-2 theorem 0.3 0 HWV007-1 theorem 0.3 0 HWV007-2 theorem 0.2 0 HWV008-1.001 theorem 0.3 0 HWV008-1.002 theorem 0.3 0 HWV008-2.001 theorem 0.2 0 HWV008-2.002 theorem 0.2 0 HWV034-1 non_thm 0.1 0 HWV034-2 non_thm 0.1 0 HWV035-1 non_thm 0.1 0 HWV035-2 non_thm 0.1 0 HWV036-1 non_thm 0.1 0 HWV036-2 non_thm 0.1 0 KRS001-1 theorem 0.1 0 KRS002-1 theorem 0.1 0 KRS003-1 theorem 0.1 0 KRS005-1 non_thm 0.1 0 KRS006-1 non_thm 0.1 0 KRS007-1 non_thm 0.1 0 KRS008-1 non_thm 0.1 0 KRS009-1 non_thm 0.1 0 KRS010-1 theorem 0.1 0 KRS011-1 non_thm 0.1 0 KRS012-1 theorem 0.1 0 KRS013-1 theorem 0.1 0 KRS014-1 non_thm 0.1 0 KRS015-1 theorem 0.1 0 KRS016-1 non_thm 0.1 0 KRS017-1 theorem 0.1 0 LCL181-2 theorem 0.1 0 LCL230-2 theorem 0.1 0 MGT004-1 theorem 0.2 0 MGT007-1 theorem 0.3 0 MGT016-1 theorem 0.1 0 MGT018-1 theorem 0.1 0 MGT022-1 theorem 0.1 0 MGT022-2 theorem 0.1 0 MGT028-1 theorem 0.1 0 MGT030-1 theorem 0.1 0 MGT036-1 theorem 0.1 0 MGT036-2 theorem 0.1 0 MGT041-2 theorem 0.1 0 MSC001-1 theorem 0.3 0 MSC002-1 theorem 0.1 0 MSC002-2 theorem 0.1 0 MSC003-1 theorem 0.1 0 MSC004-1 theorem 0.1 0 MSC006-1 theorem 0.1 0 MSC007-1.008 theorem 1.9 0 MSC008-1.002 theorem 0.1 0 MSC008-1.010 timeout 300.3 13 MSC008-2.002 theorem 0.1 0 MSC009-1 non_thm 0.1 0 NLP026-1 non_thm 0.1 0 NLP027-1 non_thm 0.1 0 NLP028-1 non_thm 0.1 0 NLP029-1 non_thm 0.1 0 NLP030-1 non_thm 0.1 0 NLP031-1 non_thm 0.1 0 NLP032-1 non_thm 84.0 45 NLP033-1 non_thm 0.4 0 NLP034-1 timeout 301.2 10 NLP035-1 timeout 301.2 12 NLP043-1 non_thm 0.1 0 NLP044-1 non_thm 0.1 0 NLP045-1 non_thm 0.1 0 NLP046-1 non_thm 0.1 0 NLP047-1 non_thm 0.1 0 NLP048-1 non_thm 0.1 0 NLP059-1 non_thm 0.1 0 NLP060-1 non_thm 4.3 6 NLP061-1 non_thm 0.1 0 NLP062-1 non_thm 0.1 0 NLP063-1 non_thm 9.5 0 NLP064-1 non_thm 0.1 0 NLP065-1 non_thm 0.1 0 NLP066-1 non_thm 0.1 0 NLP067-1 non_thm 0.1 0 NLP068-1 non_thm 0.1 0 NLP079-1 theorem 0.1 0 NLP080-1 theorem 0.1 0 NLP081-1 theorem 0.1 0 NLP094-1 theorem 0.1 0 NLP095-1 non_thm 0.1 0 NLP096-1 non_thm 0.1 0 NLP097-1 non_thm 0.1 0 NLP098-1 non_thm 0.1 0 NLP099-1 non_thm 0.1 0 NLP100-1 non_thm 0.1 0 NLP101-1 non_thm 0.1 0 NLP102-1 non_thm 0.1 0 NLP103-1 non_thm 0.1 0 NLP114-1 non_thm 0.1 0 NLP115-1 non_thm 0.1 0 NLP116-1 non_thm 0.1 0 NLP117-1 theorem 0.1 0 NLP118-1 non_thm 0.1 0 NLP119-1 non_thm 0.1 0 NLP120-1 non_thm 0.1 0 NLP121-1 non_thm 0.1 0 NLP122-1 theorem 0.1 0 NLP123-1 non_thm 0.1 0 NLP130-1 non_thm 0.1 0 NLP131-1 non_thm 0.1 0 NLP132-1 non_thm 0.1 0 NLP133-1 non_thm 0.1 0 NLP134-1 non_thm 0.1 0 NLP135-1 non_thm 0.1 0 NLP136-1 non_thm 0.1 0 NLP137-1 non_thm 0.1 0 NLP138-1 non_thm 0.1 0 NLP139-1 non_thm 0.1 0 NLP160-1 non_thm 0.1 0 NLP161-1 non_thm 0.1 0 NLP162-1 non_thm 0.1 0 NLP163-1 non_thm 0.1 0 NLP164-1 non_thm 0.2 0 NLP165-1 non_thm 0.2 0 NLP166-1 non_thm 0.2 0 NLP167-1 non_thm 0.1 0 NLP168-1 non_thm 0.1 0 NLP169-1 non_thm 0.1 0 NLP190-1 non_thm 0.1 0 NLP191-1 non_thm 0.1 0 NLP192-1 non_thm 0.1 0 NLP193-1 non_thm 0.1 0 NLP194-1 non_thm 0.1 0 NLP195-1 non_thm 0.1 0 NLP196-1 non_thm 0.1 0 NLP197-1 non_thm 0.1 0 NLP198-1 non_thm 0.1 0 NLP199-1 non_thm 0.1 0 NLP221-1 non_thm 0.1 0 NLP222-1 non_thm 0.1 0 NLP223-1 non_thm 0.1 0 NLP230-1 non_thm 0.2 0 NLP231-1 non_thm 0.1 0 NLP232-1 non_thm 0.1 0 NLP233-1 non_thm 0.2 0 NLP234-1 non_thm 0.1 0 NLP235-1 non_thm 0.1 0 NLP236-1 non_thm 0.1 0 NLP237-1 non_thm 0.1 0 NLP238-1 non_thm 0.1 0 NLP239-1 non_thm 0.1 0 NUM014-1 theorem 0.1 0 NUM015-1 theorem 0.1 0 NUM016-1 theorem 0.1 0 NUM016-2 theorem 0.1 0 NUM021-1 theorem 0.2 0 NUM022-1 theorem 0.1 0 NUM025-2 theorem 0.1 0 NUM027-1 theorem 0.7 0 NUM285-1 non_thm 0.1 0 NUM288-1 non_thm 0.1 0 PLA002-1 theorem 0.1 0 PLA002-2 theorem 0.1 0 PUZ001-1 theorem 0.1 0 PUZ001-3 non_thm 0.1 0 PUZ002-1 theorem 0.1 0 PUZ004-1 theorem 0.1 0 PUZ005-1 theorem 0.1 0 PUZ009-1 theorem 0.1 0 PUZ010-1 theorem 0.9 0 PUZ012-1 theorem 0.1 0 PUZ013-1 theorem 0.1 0 PUZ014-1 theorem 0.1 0 PUZ015-2.006 theorem 0.4 0 PUZ016-2.004 non_thm 0.1 0 PUZ016-2.005 theorem 0.1 0 PUZ017-1 theorem 30.6 6 PUZ018-1 theorem 0.1 0 PUZ018-2 non_thm 0.1 0 PUZ019-1 theorem 0.1 0 PUZ021-1 theorem 0.7 0 PUZ023-1 theorem 0.1 0 PUZ024-1 theorem 0.1 0 PUZ025-1 theorem 0.1 0 PUZ026-1 theorem 0.1 0 PUZ027-1 theorem 0.1 0 PUZ028-1 non_thm 0.1 0 PUZ028-2 non_thm 0.1 0 PUZ028-3 non_thm 0.4 0 PUZ028-4 non_thm 0.3 0 PUZ028-5 theorem 0.1 0 PUZ028-6 theorem 0.4 0 PUZ029-1 theorem 0.1 0 PUZ030-1 theorem 0.1 0 PUZ030-2 theorem 0.1 0 PUZ031-1 theorem 0.1 0 PUZ032-1 theorem 0.1 0 PUZ033-1 theorem 0.1 0 PUZ034-1.003 timeout 301.4 45 PUZ034-1.004 theorem 117.2 37 PUZ035-1 theorem 0.1 0 PUZ035-2 theorem 0.1 0 PUZ035-3 theorem 0.1 0 PUZ035-4 theorem 0.1 0 PUZ035-5 theorem 0.1 0 PUZ035-6 theorem 0.1 0 PUZ035-7 theorem 0.1 0 PUZ044-1 non_thm 0.1 0 PUZ045-1 non_thm 0.1 0 SET001-1 theorem 0.1 0 SET002-1 theorem 0.1 0 SET003-1 theorem 0.1 0 SET004-1 theorem 0.1 0 SET005-1 theorem 0.1 0 SET006-1 theorem 0.1 0 SET007-1 theorem 0.1 0 SET008-1 theorem 0.1 0 SET009-1 theorem 0.1 0 SET010-1 theorem 0.1 0 SET011-1 theorem 0.1 0 SET012-1 theorem 137.5 61 SET012-2 theorem 15.6 21 SET013-1 timeout 301.2 16 SET013-2 theorem 21.6 13 SET014-2 theorem 14.3 36 SET015-1 timeout 301.3 28 SET015-2 theorem 36.5 45 SET043-5 theorem 0.1 0 SET044-5 theorem 0.1 0 SET045-5 theorem 0.1 0 SET046-5 theorem 0.1 0 SET047-5 theorem 0.1 0 SET055-6 theorem 0.1 0 SET055-7 theorem 0.1 0 SET777-1 non_thm 0.1 0 SET778-1 non_thm 0.1 0 SET779-1 non_thm 0.1 0 SET780-1 non_thm 0.1 0 SET781-1 timeout 301.3 60 SET786-1 theorem 0.1 0 SWV001-1 theorem 0.1 0 SWV009-1 theorem 0.1 0 SYN001-1.005 theorem 0.1 0 SYN002-1.007.008 theorem 0.1 0 SYN006-1 theorem 0.1 0 SYN008-1 theorem 0.1 0 SYN009-1 theorem 0.1 0 SYN009-2 theorem 0.1 0 SYN009-3 theorem 0.1 0 SYN009-4 theorem 0.1 0 SYN011-1 theorem 0.1 0 SYN012-1 theorem 0.1 0 SYN014-2 theorem 0.1 0 SYN015-2 theorem 0.1 0 SYN028-1 theorem 0.1 0 SYN029-1 theorem 0.1 0 SYN030-1 theorem 0.1 0 SYN031-1 theorem 0.1 0 SYN032-1 theorem 0.1 0 SYN034-1 theorem 0.1 0 SYN036-1 theorem 1.3 0 SYN036-2 non_thm 85.1 15 SYN036-3 theorem 0.1 0 SYN036-4 theorem 0.1 0 SYN037-1 theorem 0.1 0 SYN037-2 theorem 0.1 0 SYN038-1 theorem 0.1 0 SYN039-1 theorem 0.1 0 SYN044-1 theorem 0.1 0 SYN045-1 theorem 0.1 0 SYN047-1 theorem 0.1 0 SYN051-1 theorem 0.1 0 SYN052-1 theorem 0.1 0 SYN053-1 theorem 0.1 0 SYN054-1 theorem 0.1 0 SYN055-1 theorem 0.1 0 SYN056-1 non_thm 0.1 0 SYN059-1 non_thm 0.1 0 SYN060-1 theorem 0.1 0 SYN061-1 theorem 0.1 0 SYN063-1 theorem 0.1 0 SYN066-1 theorem 0.1 0 SYN067-1 theorem 3.6 6 SYN067-2 theorem 13.2 6 SYN067-3 theorem 2.4 6 SYN069-1 theorem 0.1 0 SYN070-1 theorem 0.1 0 SYN081-1 theorem 0.1 0 SYN082-1 theorem 0.1 0 SYN084-1 non_thm 0.1 0 SYN084-2 theorem 0.1 0 SYN091-1.003 non_thm 0.1 0 SYN092-1.003 non_thm 0.1 0 SYN093-1.002 theorem 0.1 0 SYN094-1.005 theorem 0.1 0 SYN097-1.002 theorem 0.1 0 SYN098-1.002 theorem 0.1 0 SYN099-1.003 theorem 0.1 0 SYN100-1.005 theorem 0.1 0 SYN304-1 non_thm 0.1 0 SYN306-1 non_thm 0.1 0 SYN307-1 non_thm 0.1 0 SYN308-1 non_thm 0.1 0 SYN309-1 non_thm 0.1 0 SYN313-1.001.002 theorem 0.1 0 SYN314-1.002.001 timeout 301.3 20 SYN315-1 theorem 0.1 0 SYN316-1 timeout 300.3 26 SYN317-1 non_thm 0.1 0 SYN319-1 theorem 0.1 0 SYN320-1 non_thm 0.1 0 SYN321-1 theorem 0.1 0 SYN323-1 theorem 0.1 0 SYN324-1 timeout 300.3 26 SYN325-1 theorem 0.1 0 SYN326-1 theorem 0.1 0 SYN327-1 theorem 0.1 0 SYN328-1 theorem 0.1 0 SYN330-1 timeout 301.3 28 SYN331-1 theorem 0.1 0 SYN332-1 theorem 0.1 0 SYN334-1 theorem 0.1 0 SYN335-1 timeout 301.3 27 SYN343-1 theorem 0.1 0 SYN344-1 non_thm 0.1 0 SYN345-1 theorem 0.1 0 SYN347-1 theorem 0.1 0 SYN348-1 non_thm 0.1 0 SYN349-1 theorem 0.1 0 SYN350-1 theorem 0.1 0 SYN351-1 timeout 301.3 72 SYN352-1 theorem 0.1 0 SYN353-1 timeout 300.2 15 SYN354-1 theorem 0.1 0 SYN418-1 non_thm 1.5 0 SYN419-1 non_thm 0.7 0 SYN420-1 non_thm 0.6 0 SYN421-1 non_thm 1.2 6 SYN422-1 non_thm 1.2 0 SYN423-1 non_thm 1.3 0 SYN424-1 non_thm 3.0 6 SYN425-1 non_thm 1.2 0 SYN426-1 non_thm 1.8 0 SYN427-1 non_thm 5.9 16 SYN428-1 non_thm 1.8 0 SYN429-1 non_thm 1.5 0 SYN430-1 non_thm 0.1 0 SYN431-1 non_thm 0.1 0 SYN432-1 non_thm 0.1 0 SYN433-1 non_thm 0.3 0 SYN434-1 non_thm 5.6 6 SYN435-1 non_thm 0.3 0 SYN436-1 theorem 20.1 7 SYN437-1 non_thm 30.4 7 SYN438-1 non_thm 3.5 6 SYN439-1 theorem 170.7 6 SYN440-1 theorem 95.6 6 SYN441-1 non_thm 31.6 8 SYN442-1 theorem 42.4 6 SYN443-1 theorem 46.6 6 SYN444-1 theorem 21.1 6 SYN445-1 theorem 2.6 6 SYN446-1 non_thm 1.4 0 SYN447-1 theorem 129.9 7 SYN448-1 theorem 8.1 6 SYN449-1 non_thm 36.9 6 SYN450-1 theorem 3.9 6 SYN451-1 theorem 7.0 7 SYN452-1 theorem 9.3 6 SYN453-1 non_thm 35.5 6 SYN454-1 theorem 8.0 6 SYN455-1 theorem 11.5 6 SYN456-1 non_thm 41.3 6 SYN457-1 theorem 46.9 6 SYN458-1 theorem 16.8 0 SYN459-1 theorem 3.7 6 SYN460-1 theorem 70.6 6 SYN461-1 theorem 37.6 7 SYN462-1 theorem 39.5 6 SYN463-1 non_thm 2.0 0 SYN464-1 non_thm 0.5 0 SYN465-1 theorem 23.7 7 SYN466-1 theorem 14.6 6 SYN467-1 theorem 58.6 6 SYN468-1 theorem 13.4 6 SYN469-1 theorem 15.9 6 SYN470-1 theorem 22.0 6 SYN471-1 theorem 9.1 6 SYN472-1 theorem 41.1 6 SYN473-1 theorem 26.1 6 SYN474-1 theorem 11.5 6 SYN475-1 theorem 6.1 6 SYN476-1 theorem 73.3 6 SYN477-1 theorem 43.6 6 SYN478-1 theorem 36.8 6 SYN479-1 theorem 20.4 6 SYN480-1 theorem 106.8 6 SYN481-1 theorem 42.3 6 SYN482-1 theorem 118.8 6 SYN483-1 theorem 7.0 6 SYN484-1 theorem 2.4 6 SYN485-1 theorem 28.6 6 SYN486-1 theorem 7.2 6 SYN487-1 theorem 7.7 6 SYN488-1 theorem 15.1 6 SYN489-1 theorem 70.2 6 SYN490-1 non_thm 0.1 0 SYN491-1 non_thm 0.1 0 SYN492-1 non_thm 0.1 0 SYN493-1 non_thm 0.1 0 SYN494-1 non_thm 0.1 0 SYN495-1 non_thm 0.1 0 SYN496-1 non_thm 0.1 0 SYN497-1 non_thm 0.1 0 SYN498-1 theorem 8.6 6 SYN499-1 theorem 17.1 7 SYN500-1 theorem 26.1 6 SYN501-1 theorem 14.2 6 SYN502-1 theorem 9.0 6 SYN503-1 theorem 14.4 6 SYN504-1 theorem 8.5 6 SYN505-1 theorem 17.4 6 SYN506-1 theorem 2.3 6 SYN507-1 theorem 22.3 10 SYN508-1 theorem 10.7 6 SYN509-1 theorem 4.0 6 SYN510-1 theorem 12.3 6 SYN511-1 theorem 44.0 6 SYN512-1 theorem 4.9 6 SYN513-1 non_thm 0.5 0 SYN514-1 non_thm 4.7 12 SYN515-1 non_thm 0.1 0 SYN516-1 non_thm 0.1 0 SYN517-1 non_thm 0.1 0 SYN518-1 non_thm 1.4 0 SYN519-1 non_thm 141.9 12 SYN520-1 non_thm 1.2 0 SYN521-1 non_thm 0.1 0 SYN522-1 non_thm 0.1 0 SYN523-1 non_thm 0.1 0 SYN524-1 non_thm 0.1 0 SYN525-1 non_thm 0.1 0 SYN526-1 non_thm 0.1 0 SYN527-1 non_thm 0.1 0 SYN528-1 non_thm 0.1 0 SYN529-1 non_thm 0.2 0 SYN530-1 non_thm 0.1 0 SYN531-1 non_thm 0.1 0 SYN532-1 non_thm 0.1 0 SYN533-1 non_thm 0.1 0 SYN534-1 non_thm 0.1 0 SYN535-1 non_thm 0.1 0 SYN536-1 non_thm 0.1 0 SYN537-1 non_thm 0.1 0 SYN538-1 non_thm 0.1 0 SYN539-1 non_thm 0.2 0 SYN540-1 non_thm 0.1 0 SYN541-1 non_thm 0.1 0 SYN542-1 non_thm 1.2 0 SYN543-1 non_thm 30.5 6 SYN544-1 non_thm 0.5 0 SYN545-1 non_thm 0.5 0 SYN546-1 non_thm 4.1 21 SYN547-1 non_thm 0.9 0 SYN554-1 theorem 0.1 0 SYN560-1 theorem 115.4 53 SYN567-1 theorem 0.1 0 SYN568-1 theorem 0.1 0 SYN571-1 theorem 0.1 0 SYN573-1 theorem 0.1 0 SYN574-1 theorem 0.1 0 SYN575-1 theorem 0.1 0 SYN576-1 theorem 0.4 0 SYN578-1 theorem 0.1 0 SYN579-1 theorem 0.1 0 SYN580-1 theorem 0.1 0 SYN581-1 theorem 0.1 0 SYN582-1 theorem 0.1 0 SYN583-1 theorem 0.3 0 SYN585-1 theorem 8.9 45 SYN586-1 theorem 0.1 0 SYN587-1 theorem 0.1 0 SYN591-1 theorem 0.1 0 SYN592-1 theorem 0.1 0 SYN593-1 theorem 0.1 0 SYN594-1 theorem 0.1 0 SYN595-1 theorem 0.1 0 SYN604-1 theorem 4.2 20 SYN605-1 theorem 11.1 27 SYN606-1 theorem 11.1 0 SYN607-1 theorem 11.1 27 SYN608-1 theorem 11.1 21 SYN609-1 theorem 11.2 27 SYN610-1 theorem 11.2 21 SYN611-1 theorem 11.1 12 SYN612-1 theorem 11.2 21 SYN613-1 theorem 0.1 0 SYN619-1 theorem 0.1 0 SYN620-1 theorem 0.1 0 SYN621-1 theorem 0.1 0 SYN622-1 theorem 0.1 0 SYN623-1 theorem 0.1 0 SYN624-1 theorem 0.1 0 SYN625-1 theorem 14.2 21 SYN626-1 theorem 0.1 0 SYN627-1 theorem 0.1 0 SYN630-1 theorem 0.1 0 SYN633-1 theorem 0.1 0 SYN634-1 theorem 0.1 0 SYN635-1 theorem 0.1 0 SYN636-1 theorem 0.1 0 SYN641-1 theorem 0.2 0 SYN642-1 theorem 0.2 0 SYN643-1 theorem 0.2 0 SYN644-1 theorem 14.9 21 SYN645-1 theorem 0.2 0 SYN648-1 theorem 16.3 9 SYN650-1 theorem 8.1 16 SYN656-1 theorem 0.2 0 SYN657-1 theorem 0.1 0 SYN658-1 theorem 0.1 0 SYN659-1 theorem 0.1 0 SYN660-1 theorem 0.1 0 SYN661-1 theorem 0.1 0 SYN662-1 theorem 0.1 0 SYN663-1 theorem 0.1 0 SYN664-1 theorem 0.1 0 SYN665-1 theorem 0.1 0 SYN666-1 theorem 0.1 0 SYN667-1 theorem 0.1 0 SYN668-1 theorem 0.1 0 SYN669-1 theorem 0.1 0 SYN670-1 theorem 0.1 0 SYN671-1 theorem 0.1 0 SYN672-1 theorem 0.1 0 SYN673-1 theorem 3.1 12 SYN674-1 theorem 0.1 0 SYN675-1 theorem 0.1 0 SYN676-1 theorem 0.1 0 SYN677-1 theorem 0.1 0 SYN678-1 theorem 0.1 0 SYN679-1 theorem 0.1 0 SYN680-1 theorem 0.1 0 SYN681-1 theorem 0.1 0 SYN682-1 theorem 0.1 0 SYN683-1 theorem 0.2 0 SYN684-1 theorem 0.1 0 SYN685-1 theorem 0.1 0 SYN686-1 theorem 0.1 0 SYN687-1 theorem 15.6 16 SYN690-1 theorem 0.5 0 SYN692-1 theorem 0.3 0 SYN693-1 theorem 0.3 0 SYN694-1 theorem 0.2 0 SYN695-1 theorem 0.2 0 SYN696-1 theorem 0.2 0 SYN697-1 theorem 2.1 0 SYN698-1 theorem 0.2 0 SYN699-1 theorem 3.7 12 SYN700-1 theorem 0.2 0 SYN701-1 theorem 2.1 9 SYN710-1 theorem 0.1 0 SYN713-1 theorem 0.1 0 SYN714-1 theorem 0.1 0 SYN717-1 theorem 0.1 0 SYN718-1 theorem 4.7 0 SYN724-1 theorem 0.1 0 SYN726-1 theorem 0.1 0 SYN728-1 theorem 0.1 0 SYN734-1 non_thm 115.4 101 SYN735-1 non_thm 0.1 0 SYN736-1 non_thm 82.4 42 SYN737-1 non_thm 11.1 16 SYN738-1 non_thm 0.1 0 SYN739-1 non_thm 11.1 6 SYN740-1 non_thm 14.2 15 SYN741-1 timeout 301.4 26 SYN742-1 non_thm 14.2 15 SYN743-1 non_thm 0.1 0 SYN744-1 non_thm 0.1 0 SYN745-1 non_thm 83.3 93 SYN746-1 non_thm 255.3 10 SYN747-1 timeout 300.1 7 SYN748-1 non_thm 0.1 0 SYN749-1 non_thm 14.1 9 SYN750-1 timeout 301.4 94 SYN751-1 timeout 301.4 101 SYN752-1 non_thm 0.1 0 SYN753-1 timeout 301.3 26 SYN754-1 non_thm 83.4 76 SYN755-1 theorem 0.2 0 SYN756-1 non_thm 0.1 0 SYN757-1 non_thm 0.1 0 SYN758-1 theorem 0.7 0 SYN759-1 theorem 0.3 0 SYN760-1 non_thm 0.5 0 SYN761-1 timeout 300.2 12 SYN762-1 theorem 1.0 0 SYN763-1 timeout 301.2 68 SYN764-1 timeout 300.2 15 SYN765-1 timeout 300.2 15 SYN766-1 timeout 301.2 16 SYN767-1 timeout 301.2 15 SYN768-1 non_thm 115.2 12 SYN769-1 non_thm 11.1 6 SYN770-1 non_thm 115.1 6 SYN771-1 non_thm 115.1 6 SYN772-1 non_thm 0.1 0 SYN773-1 non_thm 115.2 27 SYN774-1 non_thm 0.1 0 SYN775-1 timeout 300.2 16 SYN776-1 non_thm 255.2 12 SYN777-1 non_thm 0.1 0 SYN778-1 non_thm 0.1 0 SYN779-1 timeout 301.4 21 SYN780-1 non_thm 0.1 0 SYN781-1 non_thm 0.1 0 SYN782-1 timeout 301.4 28 SYN783-1 non_thm 0.1 0 SYN784-1 theorem 2.5 6 SYN785-1 non_thm 14.2 16 SYN786-1 non_thm 0.1 0 SYN787-1 non_thm 0.1 0 SYN788-1 timeout 301.3 21 SYN789-1 timeout 300.3 16 SYN790-1 timeout 301.3 27 SYN791-1 non_thm 0.1 0 SYN792-1 timeout 300.3 16 SYN793-1 non_thm 0.1 0 SYN794-1 non_thm 14.2 17 SYN795-1 timeout 300.2 16 SYN796-1 theorem 1.9 0 SYN797-1 non_thm 0.1 0 SYN798-1 non_thm 14.2 10 SYN799-1 timeout 300.1 0 SYN800-1 timeout 300.1 0 SYN801-1 timeout 300.4 13 SYN802-1 timeout 300.4 13 SYN803-1 timeout 301.4 27 SYN804-1 non_thm 0.1 0 SYN805-1 timeout 301.4 21 SYN806-1 timeout 301.4 21 SYN807-1 non_thm 0.1 0 SYN808-1 non_thm 0.1 0 SYN809-1 timeout 301.4 21 SYN810-1 non_thm 0.1 0 SYN811-1 non_thm 23.9 12 SYN812-1 non_thm 75.3 45 SYN813-1 theorem 12.0 8 SYN814-1 timeout 300.6 10 SYN815-1 non_thm 23.1 27 SYN816-1 non_thm 20.6 28 SYN817-1 non_thm 25.5 16 SYN818-1 non_thm 150.3 53 SYN819-1 theorem 9.6 8 SYN820-1 theorem 9.5 0 SYN821-1 non_thm 29.7 28 SYN822-1 non_thm 34.2 28 SYN823-1 non_thm 1.3 0 SYN824-1 non_thm 16.0 16 SYN825-1 non_thm 24.2 44 SYN826-1 non_thm 27.3 10 SYN827-1 non_thm 2.2 7 SYN828-1 non_thm 9.7 21 SYN829-1 non_thm 42.4 53 SYN830-1 non_thm 47.3 53 SYN831-1 non_thm 43.6 53 SYN832-1 non_thm 36.2 10 SYN833-1 theorem 3.3 7 SYN834-1 theorem 3.2 7 SYN835-1 non_thm 2.6 7 SYN836-1 theorem 2.3 7 SYN837-1 theorem 12.0 10 SYN838-1 non_thm 12.5 0 SYN839-1 non_thm 55.2 62 SYN840-1 non_thm 54.2 62 SYN841-1 non_thm 55.2 62 SYN842-1 non_thm 65.3 62 SYN843-1 theorem 5.1 6 SYN844-1 theorem 4.1 8 SYN845-1 theorem 5.0 6 SYN846-1 theorem 16.4 12 SYN847-1 theorem 14.7 10 SYN848-1 theorem 16.1 10 SYN849-1 theorem 13.9 10 SYN850-1 theorem 14.8 28 SYN851-1 non_thm 13.5 28 SYN852-1 non_thm 72.6 16 SYN853-1 non_thm 68.9 62 SYN854-1 non_thm 70.8 62 SYN855-1 non_thm 64.0 61 SYN856-1 theorem 5.8 8 SYN857-1 theorem 7.3 8 SYN858-1 theorem 4.0 10 SYN859-1 theorem 4.2 0 SYN860-1 theorem 4.5 12 SYN861-1 theorem 15.4 27 SYN862-1 theorem 16.1 28 SYN863-1 non_thm 16.3 28 SYN864-1 non_thm 14.9 10 SYN865-1 theorem 16.7 28 SYN866-1 theorem 16.6 28 SYN867-1 non_thm 0.1 0 SYN868-1 non_thm 0.1 0 SYN869-1 theorem 0.2 0 SYN870-1 non_thm 0.2 0 SYN871-1 theorem 0.3 0 SYN872-1 non_thm 0.6 0 SYN873-1 theorem 0.3 0 SYN874-1 theorem 0.3 0 SYN875-1 theorem 0.3 0 SYN876-1 theorem 0.4 0 SYN877-1 theorem 0.4 0 SYN878-1 theorem 0.5 0 SYN879-1 theorem 0.5 0 SYN880-1 theorem 1.0 0 SYN881-1 theorem 0.7 0 SYN882-1 theorem 1.1 0 SYN883-1 theorem 1.2 6 SYN884-1 theorem 1.3 0 SYN885-1 theorem 32.8 0 SYN886-1 theorem 1.3 7 SYN887-1 theorem 1.4 0 SYN888-1 non_thm 1.4 0 SYN889-1 theorem 0.6 0 SYN890-1 theorem 0.6 0 SYN891-1 theorem 0.6 0 SYN892-1 theorem 0.6 0 SYN893-1 theorem 0.8 0 SYN894-1 theorem 0.9 0 SYN895-1 theorem 1.3 6 SYN896-1 theorem 1.2 0 SYN897-1 theorem 3.4 12 SYN898-1 theorem 3.2 9 SYN899-1 theorem 3.5 7 SYN900-1 theorem 2.7 7 SYN901-1 theorem 5.5 0 SYN902-1 non_thm 1.6 7 SYN903-1 non_thm 0.8 0 SYN904-1 non_thm 2.7 9 SYN905-1 non_thm 5.7 20 SYN906-1 timeout 301.4 21 SYN907-1 non_thm 3.5 8 SYN908-1 non_thm 28.4 35 SYN909-1 non_thm 2.6 10 SYN910-1 non_thm 10.9 13 SYN911-1 timeout 301.6 43 SYN912-1 non_thm 33.1 44 SYN913-1 timeout 301.4 20 TOP001-1 non_thm 14.2 21 TOP001-2 theorem 11.8 16 TOP002-1 timeout 301.4 63 TOP002-2 theorem 0.1 0 TOP003-1 timeout 301.4 45 TOP003-2 non_thm 0.1 0 TOP004-1 theorem 0.1 0 TOP004-2 theorem 0.1 0 TOP005-1 timeout 301.4 55 TOP005-2 theorem 0.2 0 TOP006-1 non_thm 14.2 37 TOP007-1 timeout 301.3 45 TOP008-1 timeout 301.3 28 TOP009-1 timeout 301.3 36 TOP010-1 timeout 301.3 28 TOP011-1 non_thm 14.2 28 TOP012-1 timeout 301.2 28 TOP013-1 timeout 301.2 21 TOP014-1 timeout 301.2 21 TOP015-1 timeout 301.2 13 TOP016-1 timeout 301.2 13 TOP017-1 timeout 301.2 0 TOP018-1 timeout 301.5 36 TOP019-1 timeout 301.4 27