-------------------------------------------------------------------------------- Execute format string : ./vampire.7.0 --mode casc-j2 -t 300 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 20 ANA001-1 timeout 300.0 69 ANA002-1 theorem 2.0 20 ANA002-2 theorem 14.7 36 ANA002-3 theorem 61.0 52 ANA002-4 theorem 1.0 20 ANA003-4 theorem 0.1 20 ANA004-4 theorem 0.2 20 ANA004-5 theorem 6.0 52 ANA005-4 timeout 300.0 117 ANA005-5 timeout 300.0 149 CAT007-3 theorem 0.0 20 COM002-2 theorem 0.0 20 COM003-1 theorem 0.1 20 COM003-2 theorem 0.0 20 COM005-1 theorem 77.7 38 COM006-1 timeout 300.0 100 FLD001-3 theorem 3.6 36 FLD002-3 theorem 3.3 36 FLD003-1 theorem 0.4 20 FLD004-1 theorem 0.5 20 FLD005-1 theorem 1.6 36 FLD005-3 theorem 0.3 20 FLD006-1 theorem 0.0 20 FLD006-3 theorem 0.0 20 FLD007-1 theorem 114.3 197 FLD007-3 theorem 0.0 20 FLD008-1 timeout 300.0 262 FLD008-2 timeout 300.0 245 FLD008-3 theorem 22.2 84 FLD008-4 theorem 3.7 36 FLD009-1 theorem 0.9 20 FLD009-3 theorem 0.2 20 FLD010-1 theorem 0.0 20 FLD010-3 theorem 0.0 20 FLD010-5 theorem 0.5 20 FLD011-1 timeout 300.0 245 FLD011-3 theorem 0.5 20 FLD012-1 timeout 300.0 247 FLD012-2 timeout 300.0 245 FLD012-3 theorem 180.8 213 FLD012-4 theorem 4.8 52 FLD013-1 theorem 0.5 20 FLD013-2 theorem 0.7 20 FLD013-3 theorem 3.5 36 FLD013-4 theorem 1.9 36 FLD013-5 theorem 3.2 36 FLD014-1 theorem 224.7 213 FLD014-3 theorem 1.6 20 FLD015-1 theorem 4.8 52 FLD015-3 theorem 0.5 20 FLD016-1 timeout 300.0 245 FLD016-3 theorem 3.3 36 FLD016-5 theorem 3.6 36 FLD017-1 theorem 0.1 20 FLD017-3 theorem 0.1 20 FLD018-1 theorem 0.4 20 FLD018-3 theorem 0.1 20 FLD019-1 theorem 0.3 20 FLD019-3 theorem 0.1 20 FLD020-1 theorem 4.2 52 FLD020-3 theorem 0.1 20 FLD021-1 theorem 0.1 20 FLD021-3 theorem 0.1 20 FLD022-1 theorem 6.6 68 FLD022-3 theorem 3.1 36 FLD023-1 theorem 0.1 20 FLD023-3 theorem 0.1 20 FLD024-1 theorem 3.9 52 FLD024-3 theorem 0.1 20 FLD025-1 theorem 0.5 20 FLD025-2 theorem 0.9 20 FLD025-3 theorem 3.4 36 FLD025-4 theorem 3.3 36 FLD025-5 theorem 3.5 36 FLD026-1 timeout 300.0 245 FLD026-3 theorem 3.4 36 FLD027-1 theorem 6.3 68 FLD027-3 theorem 1.9 36 FLD028-1 theorem 238.2 261 FLD028-3 theorem 3.3 36 FLD029-1 timeout 300.0 245 FLD029-3 theorem 3.4 36 FLD030-1 theorem 0.0 20 FLD030-2 theorem 0.1 20 FLD030-3 theorem 0.1 20 FLD030-4 theorem 0.1 2 FLD031-1 theorem 0.1 20 FLD031-3 theorem 0.1 20 FLD031-5 theorem 0.1 20 FLD032-1 theorem 0.3 20 FLD032-3 theorem 0.1 20 FLD033-1 theorem 3.7 52 FLD033-3 theorem 0.1 20 FLD034-1 theorem 0.1 20 FLD034-3 theorem 0.0 20 FLD035-1 theorem 24.5 100 FLD035-3 theorem 3.3 36 FLD036-1 theorem 24.3 100 FLD036-3 theorem 3.3 36 FLD037-1 theorem 0.1 20 FLD037-3 theorem 0.0 20 FLD038-1 theorem 4.4 52 FLD038-3 theorem 0.1 20 FLD039-1 theorem 0.0 20 FLD039-3 theorem 0.2 20 FLD040-1 theorem 39.6 100 FLD040-3 theorem 0.6 20 FLD040-5 theorem 0.7 20 FLD041-1 theorem 29.5 100 FLD041-2 timeout 300.0 229 FLD041-3 theorem 3.3 36 FLD041-4 theorem 4.1 36 FLD043-1 timeout 300.0 229 FLD043-3 theorem 0.1 20 FLD043-5 theorem 4.1 36 FLD044-1 timeout 300.0 229 FLD044-2 timeout 300.0 245 FLD044-3 timeout 300.0 278 FLD044-4 theorem 297.3 280 FLD045-1 timeout 300.0 245 FLD045-2 timeout 300.0 247 FLD045-3 timeout 300.0 247 FLD045-4 theorem 298.4 278 FLD046-1 timeout 300.0 245 FLD046-3 timeout 300.0 262 FLD047-1 timeout 300.0 261 FLD047-2 timeout 300.0 261 FLD047-3 theorem 186.8 229 FLD047-4 theorem 4.9 52 FLD048-1 timeout 300.0 262 FLD048-2 timeout 300.0 261 FLD048-3 timeout 300.0 229 FLD048-4 theorem 8.4 68 FLD049-1 timeout 300.0 246 FLD049-2 timeout 300.0 245 FLD049-3 theorem 4.7 52 FLD049-4 theorem 3.9 52 FLD050-1 timeout 300.0 262 FLD050-2 timeout 300.0 245 FLD050-3 theorem 4.0 52 FLD050-4 theorem 4.1 52 FLD051-1 timeout 300.0 261 FLD051-2 timeout 300.0 261 FLD051-3 timeout 300.0 229 FLD051-4 theorem 14.6 84 FLD052-1 timeout 300.0 262 FLD052-2 timeout 300.0 245 FLD052-3 timeout 300.0 229 FLD052-4 theorem 33.7 116 FLD053-1 timeout 300.0 262 FLD053-2 timeout 300.0 261 FLD053-3 timeout 300.0 229 FLD053-4 timeout 300.0 245 FLD054-1 timeout 300.0 245 FLD054-2 timeout 300.0 261 FLD054-3 timeout 300.0 246 FLD054-4 theorem 38.5 100 FLD055-1 theorem 0.1 20 FLD055-3 theorem 0.3 20 FLD056-1 theorem 0.0 20 FLD056-3 theorem 0.0 20 FLD057-1 timeout 300.0 214 FLD057-3 theorem 258.9 245 FLD058-1 theorem 0.1 20 FLD058-3 theorem 0.2 20 FLD059-1 theorem 0.2 20 FLD059-2 theorem 0.5 20 FLD059-3 theorem 0.1 20 FLD059-4 theorem 0.3 20 FLD060-1 theorem 1.9 36 FLD060-2 theorem 2.2 36 FLD060-3 theorem 1.1 20 FLD060-4 theorem 0.9 20 FLD061-1 theorem 0.3 20 FLD061-2 theorem 4.7 52 FLD061-3 theorem 3.3 36 FLD061-4 theorem 1.0 20 FLD062-1 timeout 300.0 229 FLD062-3 theorem 3.3 36 FLD063-1 theorem 6.7 68 FLD063-3 theorem 1.5 20 FLD064-1 theorem 0.9 20 FLD064-3 theorem 0.1 20 FLD065-1 theorem 0.4 20 FLD065-3 theorem 0.0 20 FLD066-1 theorem 15.4 84 FLD066-3 theorem 3.7 36 FLD067-1 theorem 0.1 20 FLD067-2 theorem 0.5 20 FLD067-3 theorem 0.0 20 FLD067-4 theorem 0.1 20 FLD068-1 theorem 4.8 52 FLD068-2 theorem 12.8 84 FLD068-3 theorem 1.6 20 FLD068-4 theorem 2.4 36 FLD069-1 theorem 0.5 20 FLD069-3 theorem 0.3 20 FLD070-1 theorem 0.4 20 FLD070-2 theorem 0.4 20 FLD070-3 theorem 0.2 20 FLD070-4 theorem 0.4 20 FLD071-1 theorem 0.0 20 FLD071-2 theorem 1.4 36 FLD071-3 theorem 0.0 20 FLD071-4 theorem 0.0 20 FLD072-1 timeout 300.0 213 FLD072-2 timeout 300.0 213 FLD072-3 theorem 16.4 84 FLD072-4 theorem 21.6 84 FLD073-1 timeout 300.0 245 FLD073-2 timeout 300.0 213 FLD073-3 timeout 300.0 245 FLD073-4 timeout 300.0 213 FLD074-1 timeout 300.0 229 FLD074-2 timeout 300.0 229 FLD074-3 theorem 132.2 229 FLD074-4 timeout 300.0 229 FLD075-1 timeout 300.0 229 FLD075-2 timeout 300.0 229 FLD075-3 timeout 300.0 245 FLD075-4 timeout 300.0 229 FLD076-1 timeout 300.0 245 FLD076-2 timeout 300.0 229 FLD076-3 timeout 300.0 213 FLD076-4 timeout 300.0 229 FLD077-1 timeout 300.0 229 FLD077-2 timeout 300.0 229 FLD077-3 timeout 300.0 213 FLD077-4 timeout 300.0 213 FLD078-1 timeout 300.0 197 FLD078-2 timeout 300.0 229 FLD078-3 timeout 300.0 197 FLD078-4 timeout 300.0 212 FLD079-1 timeout 300.0 181 FLD079-2 timeout 300.0 229 FLD079-3 timeout 300.0 213 FLD079-4 timeout 300.0 229 FLD080-1 timeout 300.0 197 FLD080-2 timeout 300.0 213 FLD080-3 timeout 300.0 214 FLD080-4 timeout 300.0 197 FLD081-1 timeout 300.0 197 FLD081-2 timeout 300.0 197 FLD081-3 timeout 300.0 213 FLD081-4 timeout 300.0 213 FLD082-1 timeout 300.0 214 FLD082-3 timeout 300.0 214 FLD083-1 timeout 300.0 181 FLD083-3 timeout 300.0 197 FLD084-1 timeout 300.0 181 FLD084-3 timeout 300.0 197 FLD085-1 timeout 300.0 133 FLD085-3 timeout 300.0 229 FLD086-1 timeout 300.0 181 FLD086-3 theorem 39.5 100 FLD087-1 timeout 300.0 165 FLD087-3 timeout 300.0 213 FLD088-1 timeout 300.0 165 FLD088-3 theorem 51.8 100 FLD089-1 timeout 300.0 165 FLD089-3 timeout 300.0 213 FLD090-1 timeout 300.0 181 FLD090-3 theorem 167.6 165 FLD091-1 timeout 300.0 230 FLD091-3 timeout 300.0 246 FLD092-1 timeout 300.0 245 FLD092-3 timeout 300.0 230 FLD093-1 timeout 300.0 166 FLD093-3 timeout 300.0 245 FLD094-1 timeout 300.0 246 FLD094-3 timeout 300.0 213 FLD095-1 timeout 300.0 197 FLD095-2 timeout 300.0 197 FLD095-3 timeout 300.0 229 FLD095-4 timeout 300.0 229 FLD096-1 timeout 300.0 229 FLD096-2 timeout 300.0 229 FLD096-3 timeout 300.0 213 FLD096-4 timeout 300.0 213 FLD097-1 timeout 300.0 229 FLD097-2 timeout 300.0 197 FLD097-3 timeout 300.0 264 FLD097-4 theorem 180.5 229 FLD098-1 timeout 300.0 197 FLD098-2 timeout 300.0 197 FLD098-3 timeout 300.0 277 FLD098-4 timeout 300.0 230 FLD099-1 timeout 300.0 165 FLD099-2 timeout 300.0 197 FLD099-3 timeout 300.0 214 FLD099-4 timeout 300.0 182 FLD100-1 timeout 300.0 229 FLD100-2 timeout 300.0 197 FLD100-3 timeout 300.0 279 FLD100-4 timeout 300.0 230 GRA001-1 theorem 0.0 20 GRP025-3 timeout 300.0 181 GRP026-3 timeout 300.0 197 GRP027-2 timeout 300.0 165 GRP039-6 theorem 0.2 20 GRP123-1.003 theorem 0.0 20 GRP123-1.005 timeout 300.0 100 GRP123-2.003 theorem 0.0 20 GRP123-2.005 timeout 300.0 84 GRP123-3.003 theorem 0.0 20 GRP123-3.004 timeout 300.0 68 GRP123-4.003 theorem 0.0 20 GRP123-4.004 timeout 300.0 84 GRP123-6.003 theorem 0.0 20 GRP123-6.005 timeout 300.0 68 GRP123-7.003 theorem 0.0 20 GRP123-7.005 timeout 300.0 68 GRP123-8.003 theorem 0.0 20 GRP123-8.004 timeout 300.0 84 GRP123-9.003 theorem 0.0 20 GRP123-9.004 timeout 300.0 84 GRP124-1.004 theorem 1.5 20 GRP124-1.005 timeout 300.0 68 GRP124-2.004 theorem 0.2 20 GRP124-2.005 timeout 300.0 52 GRP124-3.004 theorem 5.3 20 GRP124-3.005 timeout 300.0 100 GRP124-4.004 theorem 0.1 20 GRP124-4.005 timeout 300.0 84 GRP124-6.004 theorem 5.8 20 GRP124-6.005 timeout 300.0 116 GRP124-7.004 theorem 5.8 20 GRP124-7.005 timeout 300.0 116 GRP124-8.004 theorem 5.8 20 GRP124-8.005 timeout 300.0 116 GRP124-9.004 theorem 5.9 20 GRP124-9.005 timeout 300.0 116 GRP125-1.003 theorem 0.0 20 GRP125-1.004 timeout 300.0 52 GRP125-2.004 timeout 281.4 36 GRP125-2.005 timeout 300.0 36 GRP125-3.004 timeout 300.0 52 GRP125-3.005 timeout 300.0 52 GRP125-4.003 theorem 0.0 20 GRP125-4.004 timeout 300.0 68 GRP126-1.004 theorem 0.3 20 GRP126-1.005 timeout 300.0 68 GRP126-2.004 theorem 0.2 20 GRP126-2.005 timeout 300.0 36 GRP126-3.004 theorem 5.2 20 GRP126-3.005 timeout 300.0 52 GRP126-4.004 theorem 3.1 20 GRP126-4.005 timeout 300.0 68 GRP127-1.004 theorem 5.2 20 GRP127-1.005 timeout 300.0 52 GRP127-2.005 timeout 300.0 52 GRP127-2.006 timeout 300.0 52 GRP127-3.004 theorem 5.2 20 GRP127-3.005 timeout 300.0 52 GRP127-4.004 theorem 5.3 20 GRP127-4.005 timeout 300.0 52 GRP128-1.003 theorem 5.2 20 GRP128-1.004 timeout 300.0 52 GRP128-2.004 timeout 300.0 36 GRP128-2.006 timeout 300.0 100 GRP128-3.004 timeout 300.0 36 GRP128-3.005 timeout 300.0 84 GRP128-4.003 theorem 5.3 20 GRP128-4.004 timeout 300.0 68 GRP129-1.003 theorem 5.9 20 GRP129-1.005 timeout 300.0 68 GRP129-2.004 theorem 20.2 20 GRP129-2.005 timeout 300.0 68 GRP129-3.004 theorem 20.0 20 GRP129-3.005 timeout 300.0 68 GRP129-4.004 theorem 6.2 20 GRP129-4.005 timeout 300.0 68 GRP130-1.003 theorem 5.2 20 GRP130-1.005 timeout 300.0 68 GRP130-2.003 theorem 5.2 20 GRP130-2.005 timeout 300.0 52 GRP130-3.003 theorem 5.3 20 GRP130-3.004 timeout 300.0 52 GRP130-4.003 theorem 5.4 20 GRP130-4.004 timeout 300.0 68 GRP131-1.002 theorem 5.2 20 GRP131-1.005 timeout 300.0 116 GRP131-2.002 theorem 2.0 20 GRP131-2.005 timeout 300.0 84 GRP132-1.002 theorem 1.0 20 GRP132-1.005 timeout 300.0 84 GRP132-2.002 theorem 1.3 20 GRP132-2.005 timeout 300.0 68 GRP133-1.003 theorem 5.2 20 GRP133-1.004 timeout 300.0 68 GRP133-2.003 theorem 5.4 20 GRP133-2.004 timeout 300.0 36 GRP134-1.003 theorem 5.2 20 GRP134-1.005 timeout 300.0 84 GRP134-2.003 theorem 5.5 20 GRP134-2.005 timeout 300.0 68 GRP135-1.002 theorem 0.1 20 GRP135-1.005 timeout 300.0 68 GRP135-2.002 theorem 0.1 20 GRP135-2.005 timeout 300.0 52 HWV003-3 theorem 0.0 20 HWV005-1 theorem 0.0 20 HWV005-2 theorem 0.0 20 HWV006-1 theorem 0.1 20 HWV006-2 theorem 0.1 20 HWV007-1 theorem 0.1 20 HWV007-2 theorem 0.1 20 HWV008-1.001 theorem 0.1 20 HWV008-1.002 theorem 0.1 20 HWV008-2.001 theorem 0.0 20 HWV008-2.002 theorem 0.1 20 HWV034-1 non_thm 0.0 20 HWV034-2 non_thm 0.0 20 HWV035-1 non_thm 110.6 52 HWV035-2 non_thm 0.1 20 HWV036-1 non_thm 110.7 84 HWV036-2 non_thm 0.0 20 KRS001-1 theorem 0.0 20 KRS002-1 theorem 0.0 20 KRS003-1 theorem 0.0 20 KRS005-1 non_thm 57.3 20 KRS006-1 non_thm 93.4 36 KRS007-1 non_thm 93.3 20 KRS008-1 non_thm 251.4 100 KRS009-1 non_thm 0.1 20 KRS010-1 theorem 0.0 20 KRS011-1 non_thm 93.6 68 KRS012-1 theorem 0.0 20 KRS013-1 theorem 0.0 20 KRS014-1 non_thm 215.0 278 KRS015-1 theorem 0.0 20 KRS016-1 non_thm 0.1 20 KRS017-1 theorem 0.0 20 LCL181-2 theorem 0.0 20 LCL230-2 theorem 0.0 20 MGT004-1 theorem 0.0 20 MGT007-1 theorem 0.0 20 MGT016-1 theorem 0.0 20 MGT018-1 theorem 0.0 20 MGT022-1 theorem 0.0 20 MGT022-2 theorem 0.0 20 MGT028-1 theorem 0.0 20 MGT030-1 theorem 0.1 20 MGT036-1 theorem 0.0 20 MGT036-2 theorem 0.0 20 MGT041-2 theorem 0.0 20 MSC001-1 theorem 0.1 20 MSC002-1 theorem 0.0 20 MSC002-2 theorem 0.0 20 MSC003-1 theorem 0.0 20 MSC004-1 theorem 0.0 20 MSC006-1 theorem 0.0 20 MSC007-1.008 theorem 2.3 21 MSC008-1.002 theorem 0.1 20 MSC008-1.010 timeout 300.0 100 MSC008-2.002 theorem 0.1 20 MSC009-1 non_thm 0.1 20 NLP026-1 timeout 300.0 53 NLP027-1 timeout 300.0 69 NLP028-1 timeout 300.0 85 NLP029-1 timeout 300.0 53 NLP030-1 timeout 300.0 85 NLP031-1 timeout 300.0 52 NLP032-1 timeout 300.0 37 NLP033-1 timeout 300.0 85 NLP034-1 timeout 300.0 69 NLP035-1 timeout 300.0 52 NLP043-1 non_thm 0.2 20 NLP044-1 non_thm 0.3 20 NLP045-1 non_thm 0.3 20 NLP046-1 non_thm 0.2 20 NLP047-1 non_thm 0.2 20 NLP048-1 non_thm 0.2 20 NLP059-1 timeout 300.0 20 NLP060-1 timeout 300.0 20 NLP061-1 timeout 300.0 36 NLP062-1 timeout 300.0 20 NLP063-1 timeout 300.0 36 NLP064-1 timeout 300.0 36 NLP065-1 timeout 300.0 20 NLP066-1 non_thm 0.2 20 NLP067-1 non_thm 50.6 20 NLP068-1 non_thm 0.2 20 NLP079-1 theorem 0.1 20 NLP080-1 theorem 0.1 20 NLP081-1 theorem 0.1 20 NLP094-1 theorem 0.1 20 NLP095-1 non_thm 0.3 20 NLP096-1 non_thm 0.3 20 NLP097-1 non_thm 0.3 20 NLP098-1 non_thm 0.3 20 NLP099-1 non_thm 0.9 20 NLP100-1 non_thm 0.3 20 NLP101-1 non_thm 0.3 20 NLP102-1 non_thm 0.4 20 NLP103-1 non_thm 0.3 20 NLP114-1 non_thm 0.0 20 NLP115-1 non_thm 0.0 20 NLP116-1 non_thm 0.0 20 NLP117-1 theorem 0.0 20 NLP118-1 non_thm 0.0 20 NLP119-1 non_thm 0.0 20 NLP120-1 non_thm 0.0 20 NLP121-1 non_thm 0.0 20 NLP122-1 theorem 0.0 20 NLP123-1 non_thm 0.0 20 NLP130-1 non_thm 93.5 20 NLP131-1 non_thm 0.3 20 NLP132-1 non_thm 0.3 20 NLP133-1 non_thm 0.3 20 NLP134-1 non_thm 0.3 20 NLP135-1 non_thm 93.4 20 NLP136-1 non_thm 0.3 20 NLP137-1 non_thm 0.5 20 NLP138-1 non_thm 0.3 20 NLP139-1 non_thm 0.5 20 NLP160-1 timeout 300.0 36 NLP161-1 timeout 300.0 36 NLP162-1 timeout 300.0 36 NLP163-1 timeout 300.0 36 NLP164-1 timeout 300.0 36 NLP165-1 timeout 300.0 36 NLP166-1 timeout 300.0 36 NLP167-1 timeout 300.0 36 NLP168-1 timeout 300.0 36 NLP169-1 timeout 300.0 36 NLP190-1 timeout 300.0 52 NLP191-1 timeout 300.0 52 NLP192-1 timeout 300.0 52 NLP193-1 timeout 300.0 36 NLP194-1 timeout 300.0 36 NLP195-1 timeout 300.0 36 NLP196-1 timeout 300.0 36 NLP197-1 timeout 300.0 36 NLP198-1 timeout 300.0 36 NLP199-1 timeout 300.0 36 NLP221-1 non_thm 0.7 20 NLP222-1 non_thm 0.8 20 NLP223-1 non_thm 0.7 20 NLP230-1 non_thm 134.6 20 NLP231-1 non_thm 14.0 20 NLP232-1 non_thm 41.3 20 NLP233-1 non_thm 51.5 20 NLP234-1 non_thm 118.6 20 NLP235-1 non_thm 13.3 20 NLP236-1 non_thm 61.8 20 NLP237-1 non_thm 129.0 20 NLP238-1 non_thm 18.5 20 NLP239-1 non_thm 60.2 20 NUM014-1 theorem 0.0 20 NUM015-1 theorem 0.0 20 NUM016-1 theorem 0.0 20 NUM016-2 theorem 0.0 20 NUM021-1 theorem 0.0 20 NUM022-1 theorem 0.0 20 NUM025-2 theorem 0.0 20 NUM027-1 theorem 0.0 20 NUM285-1 non_thm 0.0 20 NUM288-1 timeout 77.1 116 PLA002-1 theorem 0.0 20 PLA002-2 theorem 0.0 20 PUZ001-1 theorem 0.0 20 PUZ001-3 non_thm 0.0 20 PUZ002-1 theorem 0.0 20 PUZ004-1 theorem 0.0 20 PUZ005-1 theorem 0.0 20 PUZ009-1 theorem 0.0 20 PUZ010-1 timeout 300.0 116 PUZ012-1 theorem 0.0 20 PUZ013-1 theorem 0.0 20 PUZ014-1 theorem 0.0 20 PUZ015-2.006 theorem 1.6 21 PUZ016-2.004 non_thm 0.0 20 PUZ016-2.005 theorem 0.1 20 PUZ017-1 theorem 0.1 20 PUZ018-1 theorem 3.6 20 PUZ018-2 timeout 300.0 52 PUZ019-1 theorem 0.0 20 PUZ021-1 theorem 0.0 20 PUZ023-1 theorem 0.0 20 PUZ024-1 theorem 0.0 20 PUZ025-1 theorem 0.0 20 PUZ026-1 theorem 0.0 20 PUZ027-1 theorem 0.0 20 PUZ028-1 non_thm 6.2 20 PUZ028-2 timeout 300.0 52 PUZ028-3 non_thm 0.1 20 PUZ028-4 non_thm 0.1 20 PUZ028-5 theorem 5.5 20 PUZ028-6 theorem 5.4 20 PUZ029-1 theorem 0.0 20 PUZ030-1 theorem 0.0 20 PUZ030-2 theorem 0.0 20 PUZ031-1 theorem 0.0 20 PUZ032-1 theorem 0.0 20 PUZ033-1 theorem 0.0 20 PUZ034-1.003 timeout 300.0 276 PUZ034-1.004 theorem 14.0 180 PUZ035-1 theorem 0.0 20 PUZ035-2 theorem 0.0 20 PUZ035-3 theorem 0.0 20 PUZ035-4 theorem 0.0 20 PUZ035-5 theorem 0.0 20 PUZ035-6 theorem 0.0 20 PUZ035-7 theorem 0.0 20 PUZ044-1 non_thm 94.3 20 PUZ045-1 non_thm 0.0 20 SET001-1 theorem 0.0 20 SET002-1 theorem 0.0 20 SET003-1 theorem 0.0 20 SET004-1 theorem 0.0 20 SET005-1 theorem 25.0 36 SET006-1 theorem 0.0 20 SET007-1 theorem 118.1 100 SET008-1 theorem 0.0 20 SET009-1 theorem 0.0 20 SET010-1 theorem 1.9 20 SET011-1 theorem 0.1 20 SET012-1 theorem 0.0 20 SET012-2 theorem 0.1 20 SET013-1 theorem 0.0 20 SET013-2 theorem 0.1 20 SET014-2 theorem 0.0 20 SET015-1 theorem 11.2 36 SET015-2 theorem 0.3 20 SET043-5 theorem 0.0 20 SET044-5 theorem 0.0 20 SET045-5 theorem 0.0 20 SET046-5 theorem 0.0 20 SET047-5 theorem 0.0 20 SET055-6 theorem 0.0 20 SET055-7 theorem 0.0 20 SET777-1 non_thm 17.3 20 SET778-1 non_thm 111.7 20 SET779-1 non_thm 113.6 20 SET780-1 non_thm 111.6 36 SET781-1 timeout 300.0 278 SET786-1 theorem 0.0 20 SWV001-1 theorem 0.0 20 SWV009-1 theorem 0.0 20 SYN001-1.005 theorem 0.0 20 SYN002-1.007.008 theorem 0.0 20 SYN006-1 theorem 0.0 20 SYN008-1 theorem 0.0 20 SYN009-1 theorem 0.0 20 SYN009-2 theorem 0.0 20 SYN009-3 theorem 0.0 20 SYN009-4 theorem 0.0 20 SYN011-1 theorem 0.0 20 SYN012-1 theorem 0.0 20 SYN014-2 theorem 0.0 20 SYN015-2 theorem 0.1 20 SYN028-1 theorem 0.0 20 SYN029-1 theorem 0.0 20 SYN030-1 theorem 0.0 20 SYN031-1 theorem 0.0 20 SYN032-1 theorem 0.0 20 SYN034-1 theorem 0.0 20 SYN036-1 theorem 0.1 20 SYN036-2 non_thm 0.5 20 SYN036-3 theorem 0.0 20 SYN036-4 theorem 0.0 20 SYN037-1 theorem 0.0 20 SYN037-2 theorem 0.0 20 SYN038-1 theorem 0.0 20 SYN039-1 theorem 0.6 20 SYN044-1 theorem 0.0 20 SYN045-1 theorem 0.0 20 SYN047-1 theorem 0.0 20 SYN051-1 theorem 0.0 20 SYN052-1 theorem 0.0 20 SYN053-1 theorem 0.0 20 SYN054-1 theorem 0.0 20 SYN055-1 theorem 0.0 20 SYN056-1 non_thm 0.0 20 SYN059-1 non_thm 0.0 20 SYN060-1 theorem 0.0 20 SYN061-1 theorem 0.0 20 SYN063-1 theorem 0.0 20 SYN066-1 theorem 0.0 20 SYN067-1 theorem 9.3 20 SYN067-2 theorem 61.9 36 SYN067-3 theorem 30.7 20 SYN069-1 theorem 0.0 20 SYN070-1 theorem 0.0 20 SYN081-1 theorem 0.0 20 SYN082-1 theorem 0.0 20 SYN084-1 non_thm 0.1 20 SYN084-2 theorem 0.0 20 SYN091-1.003 non_thm 0.0 20 SYN092-1.003 non_thm 0.0 20 SYN093-1.002 theorem 0.0 20 SYN094-1.005 theorem 0.0 20 SYN097-1.002 theorem 0.0 20 SYN098-1.002 theorem 0.0 20 SYN099-1.003 theorem 0.0 20 SYN100-1.005 theorem 0.0 20 SYN304-1 non_thm 0.0 20 SYN306-1 non_thm 0.0 20 SYN307-1 timeout 300.0 20 SYN308-1 non_thm 0.0 20 SYN309-1 non_thm 0.0 21 SYN313-1.001.002 theorem 0.2 20 SYN314-1.002.001 timeout 300.0 134 SYN315-1 theorem 0.0 20 SYN316-1 non_thm 0.0 20 SYN317-1 non_thm 0.0 20 SYN319-1 theorem 0.0 20 SYN320-1 non_thm 0.1 20 SYN321-1 theorem 0.0 20 SYN323-1 theorem 0.0 20 SYN324-1 non_thm 0.0 20 SYN325-1 theorem 0.0 20 SYN326-1 theorem 0.0 20 SYN327-1 theorem 0.0 20 SYN328-1 theorem 0.0 20 SYN330-1 non_thm 0.0 20 SYN331-1 theorem 0.0 4 SYN332-1 theorem 0.0 20 SYN334-1 theorem 0.0 20 SYN335-1 non_thm 225.1 158 SYN343-1 theorem 0.0 20 SYN344-1 non_thm 0.0 20 SYN345-1 theorem 0.0 20 SYN347-1 theorem 0.0 20 SYN348-1 non_thm 0.1 20 SYN349-1 theorem 0.0 20 SYN350-1 theorem 0.0 20 SYN351-1 non_thm 0.2 21 SYN352-1 theorem 0.0 20 SYN353-1 theorem 0.0 20 SYN354-1 theorem 0.0 20 SYN418-1 timeout 300.0 148 SYN419-1 timeout 300.0 132 SYN420-1 timeout 300.0 149 SYN421-1 timeout 300.0 148 SYN422-1 timeout 300.0 276 SYN423-1 timeout 300.0 277 SYN424-1 timeout 300.0 213 SYN425-1 timeout 300.0 149 SYN426-1 timeout 300.0 181 SYN427-1 timeout 300.0 133 SYN428-1 timeout 300.0 245 SYN429-1 timeout 300.0 245 SYN430-1 non_thm 0.1 20 SYN431-1 non_thm 0.1 20 SYN432-1 non_thm 0.4 20 SYN433-1 non_thm 3.9 20 SYN434-1 non_thm 5.7 20 SYN435-1 non_thm 6.7 20 SYN436-1 theorem 1.3 20 SYN437-1 non_thm 5.7 20 SYN438-1 non_thm 6.0 20 SYN439-1 theorem 1.5 20 SYN440-1 theorem 1.5 20 SYN441-1 non_thm 5.6 20 SYN442-1 theorem 1.1 20 SYN443-1 theorem 0.5 20 SYN444-1 theorem 0.7 20 SYN445-1 theorem 0.2 20 SYN446-1 non_thm 4.0 20 SYN447-1 theorem 0.4 20 SYN448-1 theorem 0.6 20 SYN449-1 non_thm 3.8 20 SYN450-1 theorem 0.7 20 SYN451-1 theorem 2.0 20 SYN452-1 theorem 1.4 20 SYN453-1 non_thm 5.6 20 SYN454-1 theorem 1.4 20 SYN455-1 theorem 0.3 20 SYN456-1 non_thm 5.7 20 SYN457-1 theorem 0.9 20 SYN458-1 theorem 1.8 20 SYN459-1 theorem 0.8 20 SYN460-1 theorem 0.5 20 SYN461-1 theorem 2.2 20 SYN462-1 theorem 0.3 20 SYN463-1 non_thm 4.5 20 SYN464-1 non_thm 5.8 20 SYN465-1 theorem 0.8 20 SYN466-1 theorem 0.9 20 SYN467-1 theorem 1.5 20 SYN468-1 theorem 1.7 20 SYN469-1 theorem 1.9 20 SYN470-1 theorem 1.1 20 SYN471-1 theorem 1.0 21 SYN472-1 theorem 0.5 20 SYN473-1 theorem 0.8 20 SYN474-1 theorem 0.9 20 SYN475-1 theorem 0.3 20 SYN476-1 theorem 1.5 21 SYN477-1 theorem 1.0 20 SYN478-1 theorem 0.6 20 SYN479-1 theorem 0.8 20 SYN480-1 theorem 0.5 20 SYN481-1 theorem 1.2 20 SYN482-1 theorem 0.8 20 SYN483-1 theorem 0.5 20 SYN484-1 theorem 0.4 20 SYN485-1 theorem 0.4 20 SYN486-1 theorem 0.7 20 SYN487-1 theorem 4.9 20 SYN488-1 theorem 1.3 21 SYN489-1 theorem 1.1 20 SYN490-1 non_thm 0.0 20 SYN491-1 non_thm 0.0 20 SYN492-1 non_thm 0.0 20 SYN493-1 non_thm 0.0 20 SYN494-1 non_thm 0.0 20 SYN495-1 non_thm 0.0 20 SYN496-1 non_thm 0.0 20 SYN497-1 non_thm 0.0 20 SYN498-1 theorem 0.4 20 SYN499-1 theorem 0.5 20 SYN500-1 theorem 1.0 21 SYN501-1 theorem 0.4 20 SYN502-1 theorem 0.6 20 SYN503-1 theorem 2.8 20 SYN504-1 theorem 1.1 20 SYN505-1 theorem 0.4 20 SYN506-1 theorem 0.9 20 SYN507-1 theorem 5.2 21 SYN508-1 theorem 1.0 20 SYN509-1 theorem 1.3 20 SYN510-1 theorem 0.7 20 SYN511-1 theorem 0.6 20 SYN512-1 theorem 0.6 20 SYN513-1 timeout 300.0 276 SYN514-1 timeout 300.0 276 SYN515-1 non_thm 0.0 20 SYN516-1 non_thm 0.0 20 SYN517-1 non_thm 0.0 20 SYN518-1 timeout 300.0 276 SYN519-1 timeout 300.0 276 SYN520-1 timeout 300.0 277 SYN521-1 non_thm 0.0 20 SYN522-1 non_thm 0.1 20 SYN523-1 non_thm 0.0 20 SYN524-1 non_thm 0.2 20 SYN525-1 non_thm 0.0 20 SYN526-1 non_thm 0.1 20 SYN527-1 non_thm 0.1 20 SYN528-1 non_thm 0.2 20 SYN529-1 non_thm 0.0 20 SYN530-1 non_thm 0.1 20 SYN531-1 non_thm 0.0 20 SYN532-1 non_thm 0.0 20 SYN533-1 non_thm 0.1 20 SYN534-1 non_thm 0.1 20 SYN535-1 non_thm 0.0 20 SYN536-1 non_thm 0.1 20 SYN537-1 non_thm 0.3 20 SYN538-1 non_thm 86.9 52 SYN539-1 non_thm 12.3 36 SYN540-1 non_thm 5.9 20 SYN541-1 timeout 300.0 84 SYN542-1 timeout 300.0 116 SYN543-1 timeout 300.0 116 SYN544-1 timeout 300.0 276 SYN545-1 timeout 300.0 148 SYN546-1 timeout 300.0 116 SYN547-1 timeout 300.0 276 SYN554-1 theorem 0.0 20 SYN560-1 theorem 14.3 36 SYN567-1 theorem 0.0 20 SYN568-1 theorem 0.0 20 SYN571-1 theorem 1.6 20 SYN573-1 theorem 0.8 20 SYN574-1 theorem 0.1 20 SYN575-1 theorem 0.1 20 SYN576-1 theorem 61.8 68 SYN578-1 theorem 1.0 20 SYN579-1 theorem 1.0 20 SYN580-1 theorem 0.1 20 SYN581-1 theorem 0.3 20 SYN582-1 theorem 0.3 20 SYN583-1 theorem 3.6 20 SYN585-1 theorem 0.0 20 SYN586-1 theorem 3.7 20 SYN587-1 theorem 2.1 20 SYN591-1 theorem 3.5 20 SYN592-1 theorem 3.6 20 SYN593-1 theorem 0.0 20 SYN594-1 theorem 0.0 20 SYN595-1 theorem 0.0 20 SYN604-1 theorem 0.0 20 SYN605-1 theorem 0.6 20 SYN606-1 theorem 0.7 20 SYN607-1 theorem 0.7 20 SYN608-1 theorem 0.7 20 SYN609-1 theorem 9.6 36 SYN610-1 theorem 10.4 36 SYN611-1 theorem 0.7 20 SYN612-1 theorem 0.7 20 SYN613-1 theorem 20.2 52 SYN619-1 theorem 0.0 20 SYN620-1 theorem 4.6 36 SYN621-1 theorem 0.2 20 SYN622-1 theorem 0.1 20 SYN623-1 theorem 0.2 20 SYN624-1 theorem 2.6 20 SYN625-1 theorem 67.3 52 SYN626-1 theorem 3.6 20 SYN627-1 theorem 2.3 20 SYN630-1 theorem 0.0 20 SYN633-1 theorem 0.0 20 SYN634-1 theorem 0.0 20 SYN635-1 theorem 0.0 20 SYN636-1 theorem 0.0 20 SYN641-1 theorem 0.2 20 SYN642-1 theorem 0.2 20 SYN643-1 theorem 0.1 20 SYN644-1 theorem 118.5 36 SYN645-1 theorem 124.2 36 SYN648-1 theorem 0.0 20 SYN650-1 theorem 199.0 52 SYN656-1 theorem 0.0 20 SYN657-1 theorem 0.0 20 SYN658-1 theorem 65.5 84 SYN659-1 theorem 0.0 20 SYN660-1 theorem 0.0 20 SYN661-1 theorem 0.1 20 SYN662-1 theorem 0.0 20 SYN663-1 theorem 0.1 20 SYN664-1 theorem 0.0 20 SYN665-1 theorem 0.1 20 SYN666-1 theorem 0.0 20 SYN667-1 theorem 0.1 20 SYN668-1 theorem 0.0 20 SYN669-1 theorem 0.0 20 SYN670-1 theorem 0.0 20 SYN671-1 theorem 0.0 20 SYN672-1 theorem 10.4 36 SYN673-1 theorem 6.1 36 SYN674-1 theorem 0.0 20 SYN675-1 theorem 0.0 20 SYN676-1 theorem 0.0 20 SYN677-1 theorem 0.0 20 SYN678-1 theorem 0.1 20 SYN679-1 theorem 0.0 20 SYN680-1 theorem 0.1 20 SYN681-1 theorem 0.0 20 SYN682-1 theorem 0.1 20 SYN683-1 theorem 0.0 20 SYN684-1 theorem 0.1 20 SYN685-1 theorem 0.0 20 SYN686-1 theorem 4.5 36 SYN687-1 theorem 0.2 20 SYN690-1 theorem 68.1 100 SYN692-1 theorem 0.3 20 SYN693-1 theorem 0.3 20 SYN694-1 theorem 0.4 20 SYN695-1 theorem 0.4 20 SYN696-1 theorem 0.4 20 SYN697-1 theorem 0.4 20 SYN698-1 theorem 0.4 20 SYN699-1 theorem 0.4 20 SYN700-1 theorem 0.4 20 SYN701-1 theorem 0.4 20 SYN710-1 theorem 0.1 20 SYN713-1 theorem 0.5 20 SYN714-1 theorem 0.1 20 SYN717-1 theorem 0.1 20 SYN718-1 theorem 1.5 20 SYN724-1 theorem 0.0 20 SYN726-1 theorem 0.0 20 SYN728-1 theorem 0.0 20 SYN734-1 non_thm 94.3 20 SYN735-1 non_thm 168.5 36 SYN736-1 timeout 300.0 68 SYN737-1 timeout 300.0 52 SYN738-1 non_thm 94.2 20 SYN739-1 non_thm 94.3 20 SYN740-1 non_thm 94.3 20 SYN741-1 timeout 300.0 52 SYN742-1 non_thm 169.4 20 SYN743-1 non_thm 0.1 20 SYN744-1 non_thm 0.1 20 SYN745-1 timeout 300.0 52 SYN746-1 timeout 300.0 52 SYN747-1 timeout 300.0 36 SYN748-1 timeout 300.0 52 SYN749-1 non_thm 95.4 20 SYN750-1 timeout 300.0 68 SYN751-1 timeout 300.0 68 SYN752-1 timeout 300.0 84 SYN753-1 timeout 300.0 84 SYN754-1 timeout 300.0 52 SYN755-1 theorem 0.2 20 SYN756-1 non_thm 94.3 20 SYN757-1 timeout 300.0 36 SYN758-1 theorem 61.4 36 SYN759-1 theorem 61.8 37 SYN760-1 non_thm 98.3 20 SYN761-1 timeout 300.0 36 SYN762-1 theorem 61.2 36 SYN763-1 timeout 300.0 68 SYN764-1 timeout 300.0 68 SYN765-1 timeout 300.0 68 SYN766-1 timeout 300.0 68 SYN767-1 timeout 300.0 68 SYN768-1 timeout 300.0 132 SYN769-1 timeout 300.0 116 SYN770-1 timeout 300.0 84 SYN771-1 timeout 300.0 100 SYN772-1 timeout 300.0 132 SYN773-1 timeout 300.0 148 SYN774-1 non_thm 95.6 20 SYN775-1 timeout 300.0 68 SYN776-1 timeout 300.0 100 SYN777-1 timeout 300.0 100 SYN778-1 timeout 300.0 84 SYN779-1 timeout 300.0 100 SYN780-1 timeout 300.0 132 SYN781-1 timeout 300.0 100 SYN782-1 timeout 300.0 132 SYN783-1 timeout 300.0 100 SYN784-1 theorem 14.6 36 SYN785-1 non_thm 95.5 37 SYN786-1 timeout 300.0 100 SYN787-1 timeout 300.0 116 SYN788-1 timeout 300.0 84 SYN789-1 timeout 300.0 100 SYN790-1 timeout 277.2 276 SYN791-1 timeout 300.0 100 SYN792-1 timeout 300.0 148 SYN793-1 timeout 300.0 116 SYN794-1 non_thm 169.6 68 SYN795-1 timeout 300.0 116 SYN796-1 theorem 4.2 20 SYN797-1 timeout 300.0 116 SYN798-1 non_thm 131.4 36 SYN799-1 timeout 300.0 84 SYN800-1 timeout 300.0 116 SYN801-1 timeout 300.0 84 SYN802-1 theorem 67.2 85 SYN803-1 timeout 300.0 100 SYN804-1 timeout 300.0 100 SYN805-1 timeout 300.0 132 SYN806-1 timeout 300.0 116 SYN807-1 timeout 300.0 148 SYN808-1 timeout 300.0 116 SYN809-1 timeout 300.0 116 SYN810-1 timeout 300.0 132 SYN811-1 non_thm 9.1 51 SYN812-1 timeout 53.7 391 SYN813-1 theorem 10.7 44 SYN814-1 non_thm 20.8 119 SYN815-1 non_thm 27.1 175 SYN816-1 non_thm 26.0 175 SYN817-1 non_thm 28.2 184 SYN818-1 timeout 26.5 290 SYN819-1 theorem 7.8 43 SYN820-1 theorem 7.4 43 SYN821-1 timeout 55.8 284 SYN822-1 timeout 54.8 289 SYN823-1 non_thm 0.8 30 SYN824-1 non_thm 8.2 164 SYN825-1 timeout 19.1 290 SYN826-1 timeout 20.0 290 SYN827-1 non_thm 1.0 33 SYN828-1 non_thm 12.3 230 SYN829-1 timeout 24.7 290 SYN830-1 timeout 26.2 274 SYN831-1 timeout 25.0 290 SYN832-1 timeout 23.0 290 SYN833-1 theorem 1.8 34 SYN834-1 theorem 2.3 34 SYN835-1 non_thm 1.1 34 SYN836-1 theorem 1.8 33 SYN837-1 theorem 7.7 74 SYN838-1 non_thm 14.9 268 SYN839-1 timeout 28.1 290 SYN840-1 timeout 28.1 290 SYN841-1 timeout 28.2 290 SYN842-1 timeout 30.6 280 SYN843-1 theorem 1.8 35 SYN844-1 theorem 1.8 35 SYN845-1 theorem 1.6 34 SYN846-1 theorem 6.4 76 SYN847-1 theorem 6.5 75 SYN848-1 theorem 6.4 75 SYN849-1 theorem 6.5 74 SYN850-1 theorem 22.7 278 SYN851-1 non_thm 15.5 270 SYN852-1 timeout 31.4 290 SYN853-1 timeout 31.2 290 SYN854-1 timeout 31.0 290 SYN855-1 timeout 30.2 290 SYN856-1 theorem 1.9 35 SYN857-1 theorem 2.5 36 SYN858-1 theorem 6.6 76 SYN859-1 theorem 7.4 76 SYN860-1 theorem 6.9 77 SYN861-1 theorem 28.5 279 SYN862-1 theorem 29.3 280 SYN863-1 non_thm 15.5 268 SYN864-1 non_thm 16.3 281 SYN865-1 theorem 23.2 282 SYN866-1 theorem 26.0 275 SYN867-1 non_thm 0.1 21 SYN868-1 non_thm 0.1 21 SYN869-1 theorem 0.4 21 SYN870-1 non_thm 0.1 21 SYN871-1 theorem 0.7 21 SYN872-1 non_thm 1.0 35 SYN873-1 theorem 0.8 22 SYN874-1 theorem 0.8 22 SYN875-1 theorem 0.6 22 SYN876-1 theorem 2.1 23 SYN877-1 theorem 0.6 22 SYN878-1 theorem 1.1 23 SYN879-1 theorem 0.9 23 SYN880-1 theorem 1.2 25 SYN881-1 theorem 1.8 25 SYN882-1 theorem 2.1 25 SYN883-1 theorem 2.3 26 SYN884-1 theorem 4.4 30 SYN885-1 theorem 7.6 32 SYN886-1 theorem 5.0 30 SYN887-1 theorem 6.6 31 SYN888-1 non_thm 1.3 37 SYN889-1 theorem 0.5 23 SYN890-1 theorem 0.8 23 SYN891-1 theorem 0.5 23 SYN892-1 theorem 0.6 23 SYN893-1 theorem 1.5 25 SYN894-1 theorem 1.5 25 SYN895-1 theorem 2.3 27 SYN896-1 theorem 2.5 26 SYN897-1 theorem 7.0 32 SYN898-1 theorem 6.6 34 SYN899-1 theorem 5.9 36 SYN900-1 theorem 5.2 35 SYN901-1 theorem 14.7 53 SYN902-1 non_thm 1.4 38 SYN903-1 timeout 214.7 325 SYN904-1 timeout 300.0 309 SYN905-1 timeout 300.0 309 SYN906-1 timeout 300.0 213 SYN907-1 timeout 300.0 309 SYN908-1 timeout 300.0 293 SYN909-1 timeout 300.0 277 SYN910-1 timeout 300.0 261 SYN911-1 timeout 300.0 277 SYN912-1 timeout 300.0 294 SYN913-1 timeout 300.0 277 TOP001-1 timeout 300.0 213 TOP001-2 theorem 0.0 21 TOP002-1 timeout 300.0 181 TOP002-2 theorem 0.0 21 TOP003-1 timeout 300.0 197 TOP003-2 timeout 218.7 86 TOP004-1 theorem 0.0 21 TOP004-2 theorem 0.0 20 TOP005-1 timeout 300.0 197 TOP005-2 theorem 0.0 21 TOP006-1 timeout 300.0 213 TOP007-1 timeout 300.0 181 TOP008-1 timeout 300.0 181 TOP009-1 timeout 300.0 181 TOP010-1 timeout 300.0 165 TOP011-1 timeout 300.0 149 TOP012-1 timeout 300.0 165 TOP013-1 timeout 300.0 181 TOP014-1 timeout 300.0 150 TOP015-1 timeout 300.0 149 TOP016-1 timeout 300.0 150 TOP017-1 timeout 300.0 149 TOP018-1 timeout 300.0 149 TOP019-1 timeout 300.0 149