-------------------------------------------------------------------------------- Execute format string : ./SPASS -PProblem=0 -PGiven=0 -PStatistic=0 -Auto 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 126.0 8 ANA001-1 timeout 300.0 24 ANA002-1 timeout 300.0 31 ANA002-2 timeout 300.0 51 ANA002-3 timeout 300.0 8 ANA002-4 timeout 300.0 10 ANA003-4 theorem 0.0 2 ANA004-4 theorem 0.1 3 ANA004-5 timeout 300.0 8 ANA005-4 timeout 300.0 8 ANA005-5 timeout 300.0 12 CAT007-3 theorem 0.0 2 COM002-2 theorem 0.0 2 COM003-1 theorem 1.0 2 COM003-2 theorem 0.0 2 COM005-1 timeout 235.0 490 COM006-1 timeout 265.7 499 FLD001-3 theorem 115.2 11 FLD002-3 timeout 300.0 11 FLD003-1 timeout 300.0 9 FLD004-1 timeout 300.0 11 FLD005-1 timeout 300.0 10 FLD005-3 theorem 14.1 4 FLD006-1 theorem 0.0 2 FLD006-3 theorem 0.0 2 FLD007-1 timeout 300.0 9 FLD007-3 theorem 0.2 3 FLD008-1 timeout 300.0 10 FLD008-2 timeout 300.0 10 FLD008-3 timeout 300.0 11 FLD008-4 timeout 300.0 10 FLD009-1 timeout 300.0 10 FLD009-3 theorem 19.9 5 FLD010-1 theorem 0.0 2 FLD010-3 theorem 0.0 2 FLD010-5 theorem 1.0 3 FLD011-1 timeout 300.0 10 FLD011-3 theorem 7.6 4 FLD012-1 timeout 300.0 12 FLD012-2 timeout 300.0 9 FLD012-3 timeout 300.0 10 FLD012-4 timeout 300.0 14 FLD013-1 timeout 300.0 12 FLD013-2 timeout 300.0 14 FLD013-3 timeout 300.0 17 FLD013-4 theorem 4.5 4 FLD013-5 theorem 3.2 3 FLD014-1 timeout 300.0 11 FLD014-3 timeout 300.0 10 FLD015-1 timeout 300.0 10 FLD015-3 theorem 2.2 3 FLD016-1 timeout 300.0 9 FLD016-3 timeout 300.0 11 FLD016-5 timeout 300.0 10 FLD017-1 theorem 1.2 3 FLD017-3 theorem 0.1 3 FLD018-1 theorem 0.8 3 FLD018-3 theorem 0.1 3 FLD019-1 theorem 0.7 3 FLD019-3 theorem 0.1 2 FLD020-1 timeout 300.0 11 FLD020-3 theorem 2.9 3 FLD021-1 theorem 1.3 3 FLD021-3 theorem 1.0 3 FLD022-1 timeout 300.0 12 FLD022-3 timeout 300.0 11 FLD023-1 theorem 4.5 4 FLD023-3 theorem 1.9 3 FLD024-1 timeout 300.0 11 FLD024-3 theorem 2.4 3 FLD025-1 timeout 300.0 12 FLD025-2 timeout 300.0 10 FLD025-3 timeout 300.0 16 FLD025-4 theorem 1.7 3 FLD025-5 theorem 0.5 3 FLD026-1 timeout 300.0 11 FLD026-3 timeout 300.0 11 FLD027-1 timeout 300.0 11 FLD027-3 theorem 2.1 3 FLD028-1 timeout 300.0 10 FLD028-3 theorem 257.6 9 FLD029-1 timeout 300.0 11 FLD029-3 timeout 300.0 9 FLD030-1 theorem 0.0 2 FLD030-2 theorem 1.2 3 FLD030-3 theorem 9.7 5 FLD030-4 theorem 0.2 3 FLD031-1 theorem 1.0 3 FLD031-3 theorem 0.1 3 FLD031-5 theorem 4.3 4 FLD032-1 theorem 0.9 3 FLD032-3 theorem 0.1 2 FLD033-1 timeout 300.0 11 FLD033-3 theorem 2.3 3 FLD034-1 theorem 1.3 3 FLD034-3 theorem 0.3 3 FLD035-1 timeout 300.0 11 FLD035-3 timeout 300.0 10 FLD036-1 timeout 300.0 11 FLD036-3 timeout 300.0 10 FLD037-1 theorem 7.7 4 FLD037-3 theorem 0.4 3 FLD038-1 timeout 300.0 10 FLD038-3 theorem 2.6 3 FLD039-1 theorem 0.0 2 FLD039-3 theorem 0.0 2 FLD040-1 timeout 300.0 10 FLD040-3 theorem 28.8 5 FLD040-5 theorem 9.2 4 FLD041-1 timeout 300.0 12 FLD041-2 timeout 300.0 10 FLD041-3 timeout 300.0 9 FLD041-4 timeout 300.0 10 FLD043-1 timeout 300.0 9 FLD043-3 theorem 6.4 4 FLD043-5 timeout 300.0 12 FLD044-1 timeout 300.0 10 FLD044-2 timeout 300.0 10 FLD044-3 timeout 300.0 11 FLD044-4 timeout 300.0 13 FLD045-1 timeout 300.0 10 FLD045-2 timeout 300.0 11 FLD045-3 timeout 300.0 11 FLD045-4 timeout 300.0 13 FLD046-1 timeout 300.0 10 FLD046-3 timeout 300.0 11 FLD047-1 timeout 300.0 12 FLD047-2 timeout 300.0 12 FLD047-3 timeout 300.0 11 FLD047-4 timeout 300.0 10 FLD048-1 timeout 300.0 11 FLD048-2 timeout 300.0 12 FLD048-3 timeout 300.0 12 FLD048-4 timeout 300.0 11 FLD049-1 timeout 300.0 11 FLD049-2 timeout 300.0 12 FLD049-3 timeout 300.0 11 FLD049-4 timeout 300.0 10 FLD050-1 timeout 300.0 11 FLD050-2 timeout 300.0 12 FLD050-3 timeout 300.0 12 FLD050-4 timeout 300.0 13 FLD051-1 timeout 300.0 12 FLD051-2 timeout 300.0 11 FLD051-3 timeout 300.0 12 FLD051-4 timeout 300.0 11 FLD052-1 timeout 300.0 11 FLD052-2 timeout 300.0 14 FLD052-3 timeout 300.0 12 FLD052-4 timeout 300.0 13 FLD053-1 timeout 300.0 11 FLD053-2 timeout 300.0 14 FLD053-3 timeout 300.0 13 FLD053-4 timeout 300.0 13 FLD054-1 timeout 300.0 12 FLD054-2 timeout 300.0 13 FLD054-3 timeout 300.0 11 FLD054-4 timeout 300.0 12 FLD055-1 theorem 0.0 2 FLD055-3 theorem 0.1 2 FLD056-1 theorem 0.0 2 FLD056-3 theorem 0.0 2 FLD057-1 timeout 300.0 9 FLD057-3 timeout 300.0 8 FLD058-1 theorem 0.0 2 FLD058-3 theorem 0.0 2 FLD059-1 theorem 0.0 2 FLD059-2 timeout 300.0 11 FLD059-3 theorem 0.2 3 FLD059-4 theorem 0.0 2 FLD060-1 timeout 300.0 10 FLD060-2 timeout 300.0 10 FLD060-3 timeout 300.0 10 FLD060-4 timeout 300.0 12 FLD061-1 timeout 300.0 13 FLD061-2 timeout 300.0 10 FLD061-3 timeout 300.0 15 FLD061-4 timeout 300.0 11 FLD062-1 timeout 300.0 10 FLD062-3 timeout 300.0 9 FLD063-1 timeout 300.0 11 FLD063-3 timeout 300.0 11 FLD064-1 timeout 300.0 9 FLD064-3 theorem 0.1 2 FLD065-1 timeout 300.0 11 FLD065-3 theorem 0.0 2 FLD066-1 timeout 300.0 12 FLD066-3 timeout 300.0 10 FLD067-1 theorem 4.4 4 FLD067-2 timeout 300.0 11 FLD067-3 theorem 40.7 6 FLD067-4 theorem 0.1 3 FLD068-1 timeout 300.0 10 FLD068-2 timeout 300.0 13 FLD068-3 timeout 300.0 11 FLD068-4 timeout 300.0 11 FLD069-1 timeout 300.0 12 FLD069-3 theorem 0.1 2 FLD070-1 timeout 300.0 10 FLD070-2 timeout 300.0 9 FLD070-3 theorem 7.4 4 FLD070-4 theorem 0.2 3 FLD071-1 theorem 0.1 2 FLD071-2 theorem 0.7 2 FLD071-3 theorem 0.0 2 FLD071-4 theorem 0.0 2 FLD072-1 timeout 300.0 12 FLD072-2 timeout 300.0 11 FLD072-3 timeout 300.0 11 FLD072-4 timeout 300.0 10 FLD073-1 timeout 300.0 10 FLD073-2 timeout 300.0 11 FLD073-3 timeout 300.0 11 FLD073-4 timeout 300.0 11 FLD074-1 timeout 300.0 12 FLD074-2 timeout 300.0 10 FLD074-3 timeout 300.0 11 FLD074-4 timeout 300.0 11 FLD075-1 timeout 300.0 12 FLD075-2 timeout 300.0 9 FLD075-3 timeout 300.0 11 FLD075-4 timeout 300.0 12 FLD076-1 timeout 300.0 10 FLD076-2 timeout 300.0 13 FLD076-3 timeout 300.0 11 FLD076-4 timeout 300.0 11 FLD077-1 timeout 300.0 10 FLD077-2 timeout 300.0 9 FLD077-3 timeout 300.0 11 FLD077-4 timeout 300.0 11 FLD078-1 timeout 300.0 10 FLD078-2 timeout 300.0 11 FLD078-3 timeout 300.0 11 FLD078-4 timeout 300.0 11 FLD079-1 timeout 300.0 10 FLD079-2 timeout 300.0 11 FLD079-3 timeout 300.0 10 FLD079-4 timeout 300.0 11 FLD080-1 timeout 300.0 10 FLD080-2 timeout 300.0 12 FLD080-3 timeout 300.0 9 FLD080-4 timeout 300.0 10 FLD081-1 timeout 300.0 9 FLD081-2 timeout 300.0 10 FLD081-3 timeout 300.0 14 FLD081-4 timeout 300.0 11 FLD082-1 timeout 300.0 11 FLD082-3 timeout 300.0 11 FLD083-1 timeout 300.0 11 FLD083-3 timeout 300.0 10 FLD084-1 timeout 300.0 9 FLD084-3 timeout 300.0 11 FLD085-1 timeout 300.0 10 FLD085-3 timeout 300.0 11 FLD086-1 timeout 300.0 9 FLD086-3 timeout 300.0 9 FLD087-1 timeout 300.0 9 FLD087-3 timeout 300.0 9 FLD088-1 timeout 300.0 10 FLD088-3 timeout 300.0 9 FLD089-1 timeout 300.0 10 FLD089-3 timeout 300.0 9 FLD090-1 timeout 300.0 9 FLD090-3 timeout 300.0 11 FLD091-1 timeout 300.0 9 FLD091-3 timeout 300.0 10 FLD092-1 timeout 300.0 11 FLD092-3 timeout 300.0 9 FLD093-1 timeout 300.0 10 FLD093-3 timeout 300.0 10 FLD094-1 timeout 300.0 10 FLD094-3 timeout 300.0 10 FLD095-1 timeout 300.0 10 FLD095-2 timeout 300.0 10 FLD095-3 timeout 300.0 12 FLD095-4 timeout 300.0 11 FLD096-1 timeout 300.0 12 FLD096-2 timeout 300.0 13 FLD096-3 timeout 300.0 12 FLD096-4 timeout 300.0 13 FLD097-1 timeout 300.0 11 FLD097-2 timeout 300.0 10 FLD097-3 timeout 300.0 11 FLD097-4 timeout 300.0 13 FLD098-1 timeout 300.0 12 FLD098-2 timeout 300.0 10 FLD098-3 timeout 300.0 11 FLD098-4 timeout 300.0 10 FLD099-1 timeout 300.0 10 FLD099-2 timeout 300.0 13 FLD099-3 timeout 300.0 10 FLD099-4 timeout 300.0 12 FLD100-1 timeout 300.0 12 FLD100-2 timeout 300.0 11 FLD100-3 timeout 300.0 11 FLD100-4 timeout 300.0 13 GRA001-1 theorem 0.0 2 GRP025-3 timeout 300.0 27 GRP026-3 timeout 300.0 35 GRP027-2 timeout 300.0 13 GRP039-6 theorem 0.4 3 GRP123-1.003 theorem 0.0 2 GRP123-1.005 timeout 300.0 19 GRP123-2.003 theorem 0.0 2 GRP123-2.005 timeout 300.0 14 GRP123-3.003 theorem 0.0 2 GRP123-3.004 timeout 300.0 14 GRP123-4.003 theorem 0.0 2 GRP123-4.004 timeout 300.0 20 GRP123-6.003 theorem 0.0 2 GRP123-6.005 timeout 300.0 18 GRP123-7.003 theorem 0.0 2 GRP123-7.005 timeout 300.0 18 GRP123-8.003 theorem 0.0 2 GRP123-8.004 timeout 300.0 18 GRP123-9.003 theorem 0.0 2 GRP123-9.004 timeout 300.0 17 GRP124-1.004 theorem 0.1 2 GRP124-1.005 timeout 300.0 27 GRP124-2.004 theorem 0.1 2 GRP124-2.005 timeout 300.0 18 GRP124-3.004 theorem 0.1 2 GRP124-3.005 timeout 300.0 20 GRP124-4.004 theorem 0.1 2 GRP124-4.005 timeout 300.0 14 GRP124-6.004 theorem 0.4 2 GRP124-6.005 timeout 300.0 21 GRP124-7.004 theorem 0.4 2 GRP124-7.005 timeout 300.0 22 GRP124-8.004 theorem 0.6 3 GRP124-8.005 timeout 300.0 18 GRP124-9.004 theorem 0.5 2 GRP124-9.005 timeout 300.0 19 GRP125-1.003 theorem 0.0 2 GRP125-1.004 timeout 300.0 16 GRP125-2.004 timeout 300.0 16 GRP125-2.005 theorem 7.8 3 GRP125-3.004 timeout 300.0 16 GRP125-3.005 theorem 46.1 4 GRP125-4.003 theorem 0.0 2 GRP125-4.004 timeout 300.0 9 GRP126-1.004 theorem 0.0 2 GRP126-1.005 timeout 300.0 19 GRP126-2.004 theorem 0.0 2 GRP126-2.005 timeout 300.0 19 GRP126-3.004 theorem 0.1 2 GRP126-3.005 timeout 300.0 17 GRP126-4.004 theorem 0.1 2 GRP126-4.005 timeout 300.0 12 GRP127-1.004 theorem 0.2 2 GRP127-1.005 timeout 300.0 25 GRP127-2.005 timeout 300.0 13 GRP127-2.006 timeout 300.0 6 GRP127-3.004 theorem 0.1 2 GRP127-3.005 timeout 300.0 12 GRP127-4.004 theorem 0.1 2 GRP127-4.005 timeout 300.0 14 GRP128-1.003 theorem 0.6 3 GRP128-1.004 timeout 300.0 11 GRP128-2.004 timeout 300.0 10 GRP128-2.006 timeout 300.0 9 GRP128-3.004 timeout 300.0 11 GRP128-3.005 theorem 4.8 3 GRP128-4.003 theorem 8.5 3 GRP128-4.004 timeout 300.0 13 GRP129-1.003 theorem 1.6 3 GRP129-1.005 timeout 300.0 7 GRP129-2.004 theorem 38.5 4 GRP129-2.005 timeout 300.0 10 GRP129-3.004 theorem 2.8 3 GRP129-3.005 timeout 300.0 10 GRP129-4.004 theorem 103.2 4 GRP129-4.005 timeout 300.0 8 GRP130-1.003 theorem 0.5 3 GRP130-1.005 timeout 300.0 6 GRP130-2.003 theorem 0.1 2 GRP130-2.005 timeout 300.0 8 GRP130-3.003 theorem 0.1 2 GRP130-3.004 timeout 300.0 12 GRP130-4.003 theorem 9.4 3 GRP130-4.004 timeout 300.0 9 GRP131-1.002 theorem 0.1 2 GRP131-1.005 timeout 300.0 21 GRP131-2.002 theorem 0.1 2 GRP131-2.005 timeout 300.0 11 GRP132-1.002 theorem 0.1 2 GRP132-1.005 timeout 300.0 9 GRP132-2.002 theorem 0.1 2 GRP132-2.005 timeout 300.0 6 GRP133-1.003 theorem 1.7 3 GRP133-1.004 timeout 300.0 12 GRP133-2.003 theorem 0.9 3 GRP133-2.004 timeout 300.0 15 GRP134-1.003 theorem 2.3 3 GRP134-1.005 timeout 300.0 16 GRP134-2.003 theorem 1.0 3 GRP134-2.005 timeout 300.0 15 GRP135-1.002 theorem 0.0 2 GRP135-1.005 timeout 300.0 7 GRP135-2.002 theorem 0.1 2 GRP135-2.005 timeout 300.0 9 HWV003-3 theorem 0.0 2 HWV005-1 theorem 0.0 2 HWV005-2 theorem 0.0 2 HWV006-1 theorem 1.2 3 HWV006-2 theorem 0.1 2 HWV007-1 theorem 2.2 4 HWV007-2 theorem 0.0 2 HWV008-1.001 theorem 1.1 4 HWV008-1.002 theorem 1.4 4 HWV008-2.001 theorem 0.1 2 HWV008-2.002 theorem 0.1 2 HWV034-1 non_thm 0.0 2 HWV034-2 non_thm 0.0 2 HWV035-1 non_thm 0.0 2 HWV035-2 non_thm 0.0 2 HWV036-1 non_thm 0.0 2 HWV036-2 non_thm 0.0 2 KRS001-1 theorem 0.0 2 KRS002-1 theorem 0.0 2 KRS003-1 theorem 0.0 2 KRS005-1 non_thm 0.0 2 KRS006-1 non_thm 0.0 2 KRS007-1 non_thm 0.0 2 KRS008-1 non_thm 0.3 3 KRS009-1 non_thm 0.0 2 KRS010-1 theorem 0.0 2 KRS011-1 non_thm 0.0 2 KRS012-1 theorem 0.0 2 KRS013-1 theorem 0.0 2 KRS014-1 non_thm 0.0 2 KRS015-1 theorem 0.0 2 KRS016-1 non_thm 0.0 2 KRS017-1 theorem 0.0 2 LCL181-2 theorem 0.0 2 LCL230-2 theorem 0.0 2 MGT004-1 theorem 0.0 2 MGT007-1 theorem 0.1 2 MGT016-1 theorem 0.0 2 MGT018-1 theorem 0.0 2 MGT022-1 theorem 0.0 2 MGT022-2 theorem 0.0 2 MGT028-1 theorem 0.0 2 MGT030-1 theorem 0.1 2 MGT036-1 theorem 0.0 2 MGT036-2 theorem 0.0 2 MGT041-2 theorem 0.0 2 MSC001-1 theorem 0.1 3 MSC002-1 theorem 0.0 2 MSC002-2 theorem 0.0 2 MSC003-1 theorem 0.0 2 MSC004-1 theorem 0.0 2 MSC006-1 theorem 0.0 2 MSC007-1.008 theorem 4.8 2 MSC008-1.002 theorem 8.4 4 MSC008-1.010 timeout 300.0 10 MSC008-2.002 theorem 0.5 2 MSC009-1 non_thm 0.0 2 NLP026-1 non_thm 0.4 3 NLP027-1 timeout 300.0 27 NLP028-1 timeout 300.0 66 NLP029-1 timeout 300.0 30 NLP030-1 timeout 300.0 51 NLP031-1 non_thm 3.8 5 NLP032-1 non_thm 16.0 8 NLP033-1 non_thm 1.1 3 NLP034-1 timeout 300.0 26 NLP035-1 timeout 300.0 29 NLP043-1 non_thm 0.0 2 NLP044-1 non_thm 0.0 2 NLP045-1 non_thm 0.0 2 NLP046-1 non_thm 0.0 2 NLP047-1 non_thm 0.0 2 NLP048-1 non_thm 0.0 2 NLP059-1 non_thm 0.2 3 NLP060-1 timeout 300.0 8 NLP061-1 timeout 300.0 8 NLP062-1 timeout 300.0 19 NLP063-1 non_thm 0.3 3 NLP064-1 non_thm 0.3 2 NLP065-1 non_thm 0.1 2 NLP066-1 non_thm 0.0 2 NLP067-1 non_thm 0.0 2 NLP068-1 non_thm 0.0 2 NLP079-1 theorem 0.1 2 NLP080-1 theorem 0.1 2 NLP081-1 theorem 0.1 2 NLP094-1 theorem 0.0 2 NLP095-1 non_thm 0.0 2 NLP096-1 non_thm 0.0 2 NLP097-1 non_thm 0.0 2 NLP098-1 non_thm 0.0 2 NLP099-1 non_thm 0.0 2 NLP100-1 non_thm 0.0 2 NLP101-1 non_thm 0.0 2 NLP102-1 non_thm 0.0 2 NLP103-1 non_thm 0.0 2 NLP114-1 non_thm 0.0 2 NLP115-1 non_thm 0.0 2 NLP116-1 non_thm 0.0 2 NLP117-1 theorem 0.0 2 NLP118-1 non_thm 0.0 2 NLP119-1 non_thm 0.0 2 NLP120-1 non_thm 0.0 2 NLP121-1 non_thm 0.0 2 NLP122-1 theorem 0.0 2 NLP123-1 non_thm 0.0 2 NLP130-1 non_thm 0.0 2 NLP131-1 non_thm 0.0 2 NLP132-1 non_thm 0.0 2 NLP133-1 non_thm 0.0 2 NLP134-1 non_thm 0.0 2 NLP135-1 non_thm 0.0 2 NLP136-1 non_thm 0.0 2 NLP137-1 non_thm 0.0 2 NLP138-1 non_thm 0.0 2 NLP139-1 non_thm 0.0 2 NLP160-1 timeout 300.0 33 NLP161-1 timeout 300.0 33 NLP162-1 timeout 300.0 33 NLP163-1 timeout 300.0 33 NLP164-1 timeout 300.0 33 NLP165-1 timeout 300.0 31 NLP166-1 timeout 300.0 30 NLP167-1 timeout 300.0 32 NLP168-1 timeout 300.0 32 NLP169-1 timeout 300.0 31 NLP190-1 timeout 300.0 30 NLP191-1 timeout 300.0 30 NLP192-1 timeout 300.0 30 NLP193-1 timeout 300.0 31 NLP194-1 timeout 300.0 31 NLP195-1 timeout 300.0 31 NLP196-1 timeout 300.0 31 NLP197-1 timeout 300.0 31 NLP198-1 timeout 300.0 31 NLP199-1 timeout 300.0 30 NLP221-1 non_thm 0.0 2 NLP222-1 non_thm 0.0 2 NLP223-1 non_thm 0.0 2 NLP230-1 non_thm 0.3 3 NLP231-1 non_thm 0.1 3 NLP232-1 non_thm 0.1 3 NLP233-1 non_thm 0.2 3 NLP234-1 non_thm 0.1 3 NLP235-1 non_thm 0.1 3 NLP236-1 non_thm 0.1 3 NLP237-1 non_thm 0.1 3 NLP238-1 non_thm 0.1 3 NLP239-1 non_thm 0.1 3 NUM014-1 theorem 0.0 2 NUM015-1 theorem 0.0 2 NUM016-1 theorem 0.0 2 NUM016-2 theorem 0.0 2 NUM021-1 theorem 0.0 2 NUM022-1 theorem 0.0 2 NUM025-2 theorem 0.0 2 NUM027-1 theorem 0.0 2 NUM285-1 non_thm 0.0 2 NUM288-1 timeout 300.0 111 PLA002-1 theorem 0.0 2 PLA002-2 theorem 0.0 2 PUZ001-1 theorem 0.0 2 PUZ001-3 non_thm 0.0 2 PUZ002-1 theorem 0.0 2 PUZ004-1 theorem 0.0 2 PUZ005-1 theorem 0.0 2 PUZ009-1 theorem 0.0 2 PUZ010-1 theorem 82.3 3 PUZ012-1 theorem 0.0 2 PUZ013-1 theorem 0.0 2 PUZ014-1 theorem 0.0 2 PUZ015-2.006 theorem 0.2 2 PUZ016-2.004 non_thm 0.0 2 PUZ016-2.005 theorem 0.0 2 PUZ017-1 theorem 3.5 4 PUZ018-1 theorem 246.5 6 PUZ018-2 timeout 300.0 13 PUZ019-1 theorem 0.2 3 PUZ021-1 theorem 0.2 2 PUZ023-1 theorem 0.0 2 PUZ024-1 theorem 0.0 2 PUZ025-1 theorem 0.0 2 PUZ026-1 theorem 0.0 2 PUZ027-1 theorem 0.0 2 PUZ028-1 non_thm 0.0 2 PUZ028-2 non_thm 0.0 2 PUZ028-3 non_thm 0.0 2 PUZ028-4 non_thm 0.0 3 PUZ028-5 theorem 0.3 2 PUZ028-6 theorem 0.2 3 PUZ029-1 theorem 0.0 2 PUZ030-1 theorem 0.0 2 PUZ030-2 theorem 0.0 2 PUZ031-1 theorem 0.0 2 PUZ032-1 theorem 0.0 2 PUZ033-1 theorem 0.0 2 PUZ034-1.003 timeout 300.0 9 PUZ034-1.004 timeout 300.0 10 PUZ035-1 theorem 0.0 3 PUZ035-2 theorem 0.0 2 PUZ035-3 theorem 0.0 2 PUZ035-4 theorem 0.0 2 PUZ035-5 theorem 0.0 2 PUZ035-6 theorem 0.0 2 PUZ035-7 theorem 0.0 2 PUZ044-1 non_thm 0.0 2 PUZ045-1 non_thm 0.0 2 SET001-1 theorem 0.0 2 SET002-1 theorem 0.0 2 SET003-1 theorem 0.0 2 SET004-1 theorem 0.0 2 SET005-1 theorem 0.0 3 SET006-1 theorem 0.0 2 SET007-1 theorem 0.0 2 SET008-1 theorem 0.0 2 SET009-1 theorem 0.0 2 SET010-1 theorem 0.7 3 SET011-1 theorem 0.0 3 SET012-1 theorem 0.4 3 SET012-2 theorem 0.6 3 SET013-1 theorem 44.5 7 SET013-2 theorem 16.6 5 SET014-2 timeout 300.0 15 SET015-1 theorem 34.9 6 SET015-2 theorem 47.3 7 SET043-5 theorem 0.0 3 SET044-5 theorem 0.0 2 SET045-5 theorem 0.0 2 SET046-5 theorem 0.0 2 SET047-5 theorem 0.0 2 SET055-6 theorem 0.1 2 SET055-7 theorem 0.0 2 SET777-1 non_thm 0.0 2 SET778-1 non_thm 0.0 2 SET779-1 non_thm 0.0 2 SET780-1 non_thm 0.0 2 SET781-1 timeout 300.0 14 SET786-1 theorem 0.0 3 SWV001-1 theorem 0.0 2 SWV009-1 theorem 0.0 2 SYN001-1.005 theorem 0.0 2 SYN002-1.007.008 theorem 0.0 2 SYN006-1 theorem 0.0 3 SYN008-1 theorem 0.0 3 SYN009-1 theorem 0.0 3 SYN009-2 theorem 0.0 3 SYN009-3 theorem 0.0 3 SYN009-4 theorem 0.0 2 SYN011-1 theorem 0.0 2 SYN012-1 theorem 0.0 2 SYN014-2 theorem 0.0 2 SYN015-2 theorem 1.0 3 SYN028-1 theorem 0.0 3 SYN029-1 theorem 0.0 2 SYN030-1 theorem 0.0 2 SYN031-1 theorem 0.0 2 SYN032-1 theorem 0.0 2 SYN034-1 theorem 0.0 2 SYN036-1 theorem 0.2 2 SYN036-2 non_thm 0.0 2 SYN036-3 theorem 0.0 2 SYN036-4 theorem 0.0 2 SYN037-1 theorem 0.0 2 SYN037-2 theorem 0.0 2 SYN038-1 theorem 0.0 2 SYN039-1 theorem 0.0 2 SYN044-1 theorem 0.0 2 SYN045-1 theorem 0.0 2 SYN047-1 theorem 0.0 2 SYN051-1 theorem 0.0 2 SYN052-1 theorem 0.0 2 SYN053-1 theorem 0.0 2 SYN054-1 theorem 0.0 2 SYN055-1 theorem 0.0 2 SYN056-1 non_thm 0.0 2 SYN059-1 non_thm 0.0 2 SYN060-1 theorem 0.0 2 SYN061-1 theorem 0.0 2 SYN063-1 theorem 0.0 2 SYN066-1 theorem 0.0 2 SYN067-1 theorem 23.5 2 SYN067-2 theorem 81.4 3 SYN067-3 theorem 21.7 3 SYN069-1 theorem 0.0 2 SYN070-1 theorem 0.0 2 SYN081-1 theorem 0.0 2 SYN082-1 theorem 0.0 2 SYN084-1 non_thm 0.0 2 SYN084-2 theorem 0.0 2 SYN091-1.003 non_thm 0.0 2 SYN092-1.003 non_thm 0.0 2 SYN093-1.002 theorem 0.0 2 SYN094-1.005 theorem 0.0 2 SYN097-1.002 theorem 0.0 2 SYN098-1.002 theorem 0.0 2 SYN099-1.003 theorem 0.0 2 SYN100-1.005 theorem 0.0 2 SYN304-1 non_thm 0.0 2 SYN306-1 non_thm 0.0 2 SYN307-1 timeout 300.0 4 SYN308-1 non_thm 0.0 3 SYN309-1 non_thm 0.0 2 SYN313-1.001.002 theorem 0.0 2 SYN314-1.002.001 timeout 300.0 9 SYN315-1 theorem 0.0 3 SYN316-1 non_thm 0.0 3 SYN317-1 non_thm 0.0 2 SYN319-1 theorem 0.0 2 SYN320-1 non_thm 0.0 2 SYN321-1 theorem 0.0 3 SYN323-1 theorem 0.0 2 SYN324-1 non_thm 0.0 2 SYN325-1 theorem 0.0 2 SYN326-1 theorem 0.0 2 SYN327-1 theorem 0.0 2 SYN328-1 theorem 0.0 3 SYN330-1 non_thm 0.0 2 SYN331-1 theorem 0.0 2 SYN332-1 theorem 0.0 2 SYN334-1 theorem 0.0 2 SYN335-1 non_thm 0.0 0 SYN343-1 theorem 0.0 2 SYN344-1 non_thm 0.0 2 SYN345-1 theorem 0.0 2 SYN347-1 theorem 0.0 2 SYN348-1 non_thm 0.0 2 SYN349-1 theorem 0.0 2 SYN350-1 theorem 0.0 2 SYN351-1 non_thm 0.0 2 SYN352-1 theorem 0.0 2 SYN353-1 theorem 0.0 2 SYN354-1 theorem 0.0 2 SYN418-1 non_thm 2.5 6 SYN419-1 non_thm 0.8 4 SYN420-1 non_thm 3.1 5 SYN421-1 non_thm 0.6 3 SYN422-1 non_thm 3.4 5 SYN423-1 non_thm 0.8 3 SYN424-1 non_thm 2.5 5 SYN425-1 non_thm 0.8 3 SYN426-1 non_thm 231.9 28 SYN427-1 non_thm 1.6 4 SYN428-1 non_thm 1.2 4 SYN429-1 non_thm 5.5 6 SYN430-1 non_thm 0.0 2 SYN431-1 non_thm 0.1 2 SYN432-1 non_thm 0.0 2 SYN433-1 non_thm 0.2 2 SYN434-1 non_thm 12.8 3 SYN435-1 non_thm 0.2 2 SYN436-1 theorem 18.3 2 SYN437-1 non_thm 64.5 3 SYN438-1 non_thm 6.1 2 SYN439-1 theorem 80.2 3 SYN440-1 theorem 18.4 3 SYN441-1 non_thm 2.1 3 SYN442-1 theorem 12.7 3 SYN443-1 theorem 6.2 2 SYN444-1 theorem 7.6 2 SYN445-1 theorem 2.9 2 SYN446-1 non_thm 4.4 2 SYN447-1 theorem 51.0 3 SYN448-1 theorem 8.9 3 SYN449-1 non_thm 11.1 2 SYN450-1 theorem 5.1 2 SYN451-1 theorem 7.1 2 SYN452-1 theorem 6.0 2 SYN453-1 non_thm 15.3 3 SYN454-1 theorem 4.5 2 SYN455-1 theorem 6.6 2 SYN456-1 non_thm 20.6 3 SYN457-1 theorem 86.7 3 SYN458-1 theorem 2.6 2 SYN459-1 theorem 6.8 3 SYN460-1 theorem 34.0 3 SYN461-1 theorem 7.9 3 SYN462-1 theorem 11.4 2 SYN463-1 non_thm 1.7 2 SYN464-1 non_thm 14.1 3 SYN465-1 theorem 5.0 2 SYN466-1 theorem 16.2 2 SYN467-1 theorem 24.4 3 SYN468-1 theorem 11.6 2 SYN469-1 theorem 9.9 2 SYN470-1 theorem 13.2 2 SYN471-1 theorem 17.5 3 SYN472-1 theorem 13.0 3 SYN473-1 theorem 15.8 3 SYN474-1 theorem 13.5 2 SYN475-1 theorem 14.2 2 SYN476-1 theorem 10.8 2 SYN477-1 theorem 8.5 2 SYN478-1 theorem 7.0 2 SYN479-1 theorem 11.7 2 SYN480-1 theorem 10.7 2 SYN481-1 theorem 9.9 2 SYN482-1 theorem 12.4 2 SYN483-1 theorem 11.2 2 SYN484-1 theorem 9.8 2 SYN485-1 theorem 11.0 2 SYN486-1 theorem 13.2 2 SYN487-1 theorem 11.6 2 SYN488-1 theorem 12.1 2 SYN489-1 theorem 9.8 2 SYN490-1 non_thm 0.0 2 SYN491-1 non_thm 0.0 2 SYN492-1 non_thm 0.0 2 SYN493-1 non_thm 0.0 2 SYN494-1 non_thm 0.0 2 SYN495-1 non_thm 0.0 2 SYN496-1 non_thm 0.0 2 SYN497-1 non_thm 0.0 2 SYN498-1 theorem 19.5 2 SYN499-1 theorem 8.1 2 SYN500-1 theorem 13.7 2 SYN501-1 theorem 13.7 2 SYN502-1 theorem 4.6 2 SYN503-1 theorem 11.5 3 SYN504-1 theorem 7.5 2 SYN505-1 theorem 7.3 2 SYN506-1 theorem 8.2 2 SYN507-1 theorem 13.8 2 SYN508-1 theorem 12.9 2 SYN509-1 theorem 7.2 2 SYN510-1 theorem 7.7 2 SYN511-1 theorem 5.2 2 SYN512-1 theorem 5.9 2 SYN513-1 non_thm 5.7 5 SYN514-1 timeout 300.0 164 SYN515-1 non_thm 0.0 2 SYN516-1 non_thm 0.0 2 SYN517-1 non_thm 0.0 2 SYN518-1 non_thm 2.3 5 SYN519-1 timeout 300.0 55 SYN520-1 non_thm 2.6 7 SYN521-1 non_thm 0.0 2 SYN522-1 non_thm 0.0 2 SYN523-1 non_thm 0.0 2 SYN524-1 non_thm 0.0 2 SYN525-1 non_thm 0.0 2 SYN526-1 non_thm 0.0 2 SYN527-1 non_thm 0.0 2 SYN528-1 non_thm 0.0 2 SYN529-1 non_thm 0.0 2 SYN530-1 non_thm 0.0 2 SYN531-1 non_thm 0.0 2 SYN532-1 non_thm 0.0 2 SYN533-1 non_thm 0.0 2 SYN534-1 non_thm 0.0 2 SYN535-1 non_thm 0.0 2 SYN536-1 non_thm 0.0 2 SYN537-1 non_thm 0.0 2 SYN538-1 non_thm 0.1 2 SYN539-1 non_thm 0.1 2 SYN540-1 non_thm 0.0 2 SYN541-1 non_thm 0.0 2 SYN542-1 non_thm 0.3 3 SYN543-1 non_thm 0.7 3 SYN544-1 non_thm 0.9 4 SYN545-1 timeout 300.0 67 SYN546-1 non_thm 268.2 142 SYN547-1 non_thm 5.9 9 SYN554-1 theorem 0.0 2 SYN560-1 timeout 300.0 8 SYN567-1 theorem 86.8 6 SYN568-1 theorem 0.0 2 SYN571-1 theorem 0.0 2 SYN573-1 theorem 0.2 2 SYN574-1 theorem 0.2 3 SYN575-1 theorem 0.2 3 SYN576-1 timeout 300.0 8 SYN578-1 theorem 179.1 7 SYN579-1 theorem 189.4 7 SYN580-1 theorem 3.4 3 SYN581-1 theorem 18.2 8 SYN582-1 theorem 17.4 8 SYN583-1 theorem 22.9 9 SYN585-1 theorem 0.0 2 SYN586-1 theorem 7.2 3 SYN587-1 theorem 4.6 3 SYN591-1 timeout 300.0 7 SYN592-1 timeout 300.0 7 SYN593-1 theorem 0.0 2 SYN594-1 theorem 0.1 2 SYN595-1 theorem 0.6 3 SYN604-1 theorem 0.2 3 SYN605-1 timeout 300.0 7 SYN606-1 timeout 300.0 7 SYN607-1 timeout 300.0 7 SYN608-1 timeout 300.0 7 SYN609-1 timeout 300.0 7 SYN610-1 timeout 300.0 7 SYN611-1 timeout 300.0 7 SYN612-1 timeout 300.0 7 SYN613-1 theorem 0.3 2 SYN619-1 theorem 0.0 2 SYN620-1 theorem 9.3 4 SYN621-1 theorem 1.7 3 SYN622-1 theorem 14.5 4 SYN623-1 timeout 300.0 7 SYN624-1 timeout 300.0 10 SYN625-1 timeout 300.0 10 SYN626-1 theorem 3.8 3 SYN627-1 theorem 8.5 4 SYN630-1 theorem 0.4 3 SYN633-1 theorem 0.7 3 SYN634-1 theorem 0.7 3 SYN635-1 theorem 0.9 3 SYN636-1 theorem 0.6 3 SYN641-1 theorem 23.9 4 SYN642-1 theorem 24.6 4 SYN643-1 theorem 23.5 4 SYN644-1 timeout 300.0 8 SYN645-1 timeout 300.0 8 SYN648-1 theorem 0.0 2 SYN650-1 timeout 300.0 9 SYN656-1 theorem 0.2 3 SYN657-1 theorem 0.5 3 SYN658-1 timeout 300.0 10 SYN659-1 theorem 8.3 4 SYN660-1 theorem 3.4 3 SYN661-1 theorem 3.4 3 SYN662-1 theorem 3.9 3 SYN663-1 theorem 3.9 3 SYN664-1 theorem 3.4 3 SYN665-1 theorem 3.3 3 SYN666-1 theorem 3.4 3 SYN667-1 theorem 3.5 3 SYN668-1 theorem 3.5 3 SYN669-1 theorem 3.4 3 SYN670-1 theorem 3.5 3 SYN671-1 theorem 3.6 3 SYN672-1 timeout 300.0 10 SYN673-1 timeout 300.0 9 SYN674-1 theorem 3.3 3 SYN675-1 theorem 3.3 3 SYN676-1 theorem 3.4 3 SYN677-1 theorem 3.5 3 SYN678-1 theorem 3.3 3 SYN679-1 theorem 3.3 3 SYN680-1 theorem 3.3 3 SYN681-1 theorem 3.3 3 SYN682-1 theorem 3.4 3 SYN683-1 theorem 3.3 3 SYN684-1 theorem 3.5 3 SYN685-1 theorem 3.5 3 SYN686-1 theorem 3.5 4 SYN687-1 timeout 300.0 11 SYN690-1 timeout 300.0 8 SYN692-1 theorem 104.6 6 SYN693-1 theorem 102.7 6 SYN694-1 theorem 283.8 8 SYN695-1 theorem 131.1 6 SYN696-1 theorem 299.1 8 SYN697-1 theorem 128.1 6 SYN698-1 theorem 282.3 8 SYN699-1 theorem 125.2 6 SYN700-1 theorem 288.9 8 SYN701-1 theorem 125.2 6 SYN710-1 theorem 0.1 2 SYN713-1 theorem 101.3 7 SYN714-1 theorem 1.1 3 SYN717-1 theorem 0.1 2 SYN718-1 theorem 9.3 6 SYN724-1 theorem 0.0 2 SYN726-1 theorem 0.0 2 SYN728-1 theorem 0.0 2 SYN734-1 non_thm 0.1 2 SYN735-1 non_thm 0.1 2 SYN736-1 timeout 300.0 10 SYN737-1 timeout 300.0 6 SYN738-1 non_thm 0.1 2 SYN739-1 timeout 273.3 497 SYN740-1 non_thm 0.2 3 SYN741-1 timeout 300.0 44 SYN742-1 timeout 300.0 7 SYN743-1 non_thm 2.3 5 SYN744-1 non_thm 3.1 3 SYN745-1 timeout 300.0 46 SYN746-1 timeout 300.0 5 SYN747-1 timeout 300.0 13 SYN748-1 timeout 300.0 11 SYN749-1 timeout 300.0 164 SYN750-1 timeout 300.0 13 SYN751-1 timeout 300.0 15 SYN752-1 timeout 300.0 107 SYN753-1 timeout 300.0 15 SYN754-1 timeout 300.0 17 SYN755-1 theorem 0.1 2 SYN756-1 non_thm 0.2 2 SYN757-1 non_thm 0.3 3 SYN758-1 timeout 300.0 13 SYN759-1 timeout 300.0 12 SYN760-1 timeout 300.0 9 SYN761-1 timeout 300.0 23 SYN762-1 timeout 300.0 9 SYN763-1 timeout 72.3 499 SYN764-1 timeout 300.0 242 SYN765-1 timeout 300.0 25 SYN766-1 timeout 300.0 8 SYN767-1 timeout 300.0 8 SYN768-1 timeout 300.0 11 SYN769-1 timeout 300.0 7 SYN770-1 timeout 300.0 7 SYN771-1 timeout 300.0 9 SYN772-1 non_thm 0.2 4 SYN773-1 timeout 300.0 20 SYN774-1 timeout 300.0 44 SYN775-1 timeout 300.0 23 SYN776-1 timeout 300.0 7 SYN777-1 timeout 300.0 7 SYN778-1 timeout 300.0 9 SYN779-1 timeout 300.0 8 SYN780-1 timeout 300.0 12 SYN781-1 timeout 300.0 9 SYN782-1 timeout 300.0 34 SYN783-1 timeout 300.0 8 SYN784-1 theorem 25.2 4 SYN785-1 timeout 300.0 45 SYN786-1 timeout 300.0 6 SYN787-1 timeout 300.0 6 SYN788-1 timeout 300.0 6 SYN789-1 timeout 300.0 8 SYN790-1 timeout 300.0 376 SYN791-1 timeout 300.0 47 SYN792-1 timeout 300.0 12 SYN793-1 timeout 300.0 12 SYN794-1 timeout 300.0 7 SYN795-1 timeout 300.0 7 SYN796-1 theorem 2.5 4 SYN797-1 timeout 300.0 19 SYN798-1 timeout 300.0 9 SYN799-1 timeout 300.0 6 SYN800-1 timeout 300.0 6 SYN801-1 timeout 300.0 8 SYN802-1 timeout 300.0 9 SYN803-1 timeout 28.5 499 SYN804-1 timeout 300.0 21 SYN805-1 timeout 300.0 143 SYN806-1 timeout 300.0 8 SYN807-1 timeout 300.0 8 SYN808-1 timeout 300.0 21 SYN809-1 timeout 300.0 7 SYN810-1 timeout 300.0 11 SYN811-1 non_thm 7.0 9 SYN812-1 non_thm 54.8 53 SYN813-1 theorem 2.4 17 SYN814-1 timeout 300.0 17 SYN815-1 non_thm 51.9 24 SYN816-1 timeout 300.0 25 SYN817-1 non_thm 127.8 27 SYN818-1 timeout 300.0 72 SYN819-1 theorem 4.9 20 SYN820-1 theorem 11.2 20 SYN821-1 timeout 300.0 29 SYN822-1 timeout 300.0 29 SYN823-1 non_thm 0.7 20 SYN824-1 non_thm 10.0 20 SYN825-1 non_thm 46.8 47 SYN826-1 non_thm 55.4 51 SYN827-1 non_thm 1.3 20 SYN828-1 non_thm 20.0 23 SYN829-1 non_thm 102.6 66 SYN830-1 non_thm 116.5 72 SYN831-1 non_thm 109.1 68 SYN832-1 non_thm 81.9 60 SYN833-1 theorem 1.3 20 SYN834-1 theorem 1.4 20 SYN835-1 non_thm 2.1 20 SYN836-1 theorem 1.7 20 SYN837-1 theorem 7.2 20 SYN838-1 non_thm 33.2 27 SYN839-1 non_thm 147.6 77 SYN840-1 non_thm 144.9 77 SYN841-1 non_thm 148.1 77 SYN842-1 non_thm 191.9 85 SYN843-1 theorem 2.1 23 SYN844-1 theorem 1.8 23 SYN845-1 theorem 1.9 23 SYN846-1 theorem 9.8 10 SYN847-1 theorem 8.9 23 SYN848-1 theorem 8.8 23 SYN849-1 theorem 7.3 23 SYN850-1 theorem 35.2 28 SYN851-1 non_thm 37.6 27 SYN852-1 non_thm 265.4 86 SYN853-1 non_thm 204.8 85 SYN854-1 non_thm 199.5 85 SYN855-1 non_thm 192.7 82 SYN856-1 theorem 2.5 23 SYN857-1 theorem 2.2 23 SYN858-1 theorem 11.9 10 SYN859-1 theorem 8.1 23 SYN860-1 theorem 10.1 10 SYN861-1 theorem 41.7 28 SYN862-1 theorem 40.9 29 SYN863-1 non_thm 37.9 27 SYN864-1 non_thm 56.6 29 SYN865-1 theorem 44.4 29 SYN866-1 theorem 36.9 28 SYN867-1 non_thm 0.1 3 SYN868-1 non_thm 0.1 3 SYN869-1 theorem 0.1 23 SYN870-1 non_thm 0.1 3 SYN871-1 theorem 0.1 23 SYN872-1 non_thm 0.7 5 SYN873-1 theorem 0.1 23 SYN874-1 theorem 0.1 23 SYN875-1 theorem 0.1 3 SYN876-1 theorem 0.2 3 SYN877-1 theorem 0.1 23 SYN878-1 theorem 0.1 3 SYN879-1 theorem 0.1 23 SYN880-1 theorem 0.2 23 SYN881-1 theorem 0.2 3 SYN882-1 theorem 0.2 23 SYN883-1 theorem 0.2 23 SYN884-1 theorem 0.4 23 SYN885-1 theorem 0.4 23 SYN886-1 theorem 0.4 23 SYN887-1 theorem 0.4 23 SYN888-1 non_thm 1.1 23 SYN889-1 theorem 0.1 3 SYN890-1 theorem 0.1 23 SYN891-1 theorem 0.1 3 SYN892-1 theorem 0.1 23 SYN893-1 theorem 0.2 23 SYN894-1 theorem 0.2 23 SYN895-1 theorem 0.2 23 SYN896-1 theorem 0.3 23 SYN897-1 theorem 0.5 23 SYN898-1 theorem 0.5 23 SYN899-1 theorem 0.5 23 SYN900-1 theorem 0.5 23 SYN901-1 theorem 1.1 23 SYN902-1 non_thm 1.3 23 SYN903-1 timeout 300.0 23 SYN904-1 timeout 300.0 23 SYN905-1 timeout 300.0 23 SYN906-1 timeout 300.0 23 SYN907-1 timeout 300.0 23 SYN908-1 timeout 300.0 23 SYN909-1 timeout 300.0 23 SYN910-1 timeout 300.0 23 SYN911-1 timeout 300.0 23 SYN912-1 timeout 300.0 23 SYN913-1 timeout 300.0 23 TOP001-1 timeout 300.0 23 TOP001-2 theorem 0.0 23 TOP002-1 timeout 300.0 23 TOP002-2 theorem 0.0 23 TOP003-1 timeout 300.0 18 TOP003-2 timeout 300.0 23 TOP004-1 theorem 0.0 23 TOP004-2 theorem 0.0 23 TOP005-1 timeout 300.0 23 TOP005-2 theorem 21.7 23 TOP006-1 timeout 300.0 18 TOP007-1 timeout 300.0 23 TOP008-1 timeout 300.0 23 TOP009-1 timeout 300.0 23 TOP010-1 non_thm 0.1 23 TOP011-1 non_thm 0.1 3 TOP012-1 timeout 300.0 23 TOP013-1 timeout 300.0 23 TOP014-1 non_thm 0.1 23 TOP015-1 non_thm 0.1 23 TOP016-1 non_thm 0.1 3 TOP017-1 timeout 300.0 23 TOP018-1 non_thm 0.1 23 TOP019-1 non_thm 0.1 23