-------------------------------------------------------------------------------- Execute format string : ./eprover -s --tstp-format -xAuto -tAuto 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.1 3 ANA001-1 memory 120.5 499 ANA002-1 theorem 32.3 167 ANA002-2 theorem 22.7 116 ANA002-3 theorem 5.8 31 ANA002-4 theorem 3.0 20 ANA003-4 theorem 0.0 2 ANA004-4 theorem 0.0 2 ANA004-5 theorem 0.3 5 ANA005-4 memory 80.1 499 ANA005-5 memory 112.9 500 CAT007-3 theorem 0.0 2 COM002-2 theorem 0.0 2 COM003-1 theorem 0.1 3 COM003-2 theorem 0.0 2 COM005-1 timeout 300.0 63 COM006-1 timeout 300.0 270 FLD001-3 theorem 0.9 7 FLD002-3 theorem 0.2 4 FLD003-1 theorem 16.2 74 FLD004-1 memory 109.2 499 FLD005-1 theorem 0.6 6 FLD005-3 theorem 0.9 7 FLD006-1 theorem 0.1 3 FLD006-3 theorem 0.0 2 FLD007-1 memory 175.2 499 FLD007-3 theorem 0.3 4 FLD008-1 memory 108.3 499 FLD008-2 memory 138.9 499 FLD008-3 memory 225.1 499 FLD008-4 theorem 0.1 3 FLD009-1 theorem 1.2 10 FLD009-3 theorem 0.5 5 FLD010-1 theorem 0.1 3 FLD010-3 theorem 0.0 2 FLD010-5 theorem 2.1 8 FLD011-1 memory 191.2 499 FLD011-3 theorem 4.8 11 FLD012-1 memory 99.5 499 FLD012-2 memory 124.7 499 FLD012-3 memory 232.1 499 FLD012-4 theorem 31.1 72 FLD013-1 theorem 12.5 56 FLD013-2 theorem 0.2 4 FLD013-3 theorem 1.1 9 FLD013-4 theorem 0.1 3 FLD013-5 theorem 0.1 3 FLD014-1 memory 145.2 499 FLD014-3 theorem 0.2 4 FLD015-1 theorem 11.9 48 FLD015-3 theorem 0.0 3 FLD016-1 theorem 20.0 81 FLD016-3 theorem 0.1 3 FLD016-5 theorem 0.2 4 FLD017-1 theorem 0.1 3 FLD017-3 theorem 0.1 3 FLD018-1 theorem 0.2 4 FLD018-3 theorem 0.0 3 FLD019-1 theorem 0.1 3 FLD019-3 theorem 0.0 2 FLD020-1 theorem 14.8 63 FLD020-3 theorem 0.1 3 FLD021-1 theorem 0.2 4 FLD021-3 theorem 0.0 3 FLD022-1 theorem 23.6 113 FLD022-3 theorem 0.1 3 FLD023-1 theorem 0.1 3 FLD023-3 theorem 0.0 3 FLD024-1 theorem 11.1 51 FLD024-3 theorem 0.1 3 FLD025-1 theorem 14.8 62 FLD025-2 theorem 0.1 3 FLD025-3 theorem 0.1 3 FLD025-4 theorem 0.0 2 FLD025-5 theorem 0.0 3 FLD026-1 memory 151.1 499 FLD026-3 theorem 1.7 10 FLD027-1 memory 116.0 500 FLD027-3 theorem 0.1 3 FLD028-1 memory 125.5 499 FLD028-3 theorem 2.5 14 FLD029-1 memory 124.9 499 FLD029-3 theorem 1.0 7 FLD030-1 theorem 0.0 3 FLD030-2 theorem 0.0 3 FLD030-3 theorem 1.2 8 FLD030-4 theorem 0.0 2 FLD031-1 theorem 0.1 3 FLD031-3 theorem 0.0 3 FLD031-5 theorem 0.0 2 FLD032-1 theorem 2.3 13 FLD032-3 theorem 0.1 3 FLD033-1 theorem 69.4 263 FLD033-3 theorem 0.1 3 FLD034-1 theorem 0.1 3 FLD034-3 theorem 0.0 2 FLD035-1 memory 115.1 499 FLD035-3 theorem 2.0 12 FLD036-1 memory 115.3 498 FLD036-3 theorem 2.0 12 FLD037-1 theorem 0.1 3 FLD037-3 theorem 0.0 3 FLD038-1 memory 109.0 499 FLD038-3 theorem 0.1 3 FLD039-1 theorem 0.0 2 FLD039-3 theorem 0.0 2 FLD040-1 memory 123.2 499 FLD040-3 theorem 3.2 18 FLD040-5 theorem 3.2 17 FLD041-1 memory 113.5 499 FLD041-2 memory 155.6 499 FLD041-3 theorem 13.5 45 FLD041-4 theorem 92.2 240 FLD043-1 memory 189.1 500 FLD043-3 theorem 0.2 4 FLD043-5 theorem 33.1 44 FLD044-1 memory 108.4 499 FLD044-2 memory 128.1 499 FLD044-3 memory 227.9 499 FLD044-4 timeout 300.0 431 FLD045-1 memory 108.2 499 FLD045-2 memory 125.1 499 FLD045-3 memory 227.8 499 FLD045-4 memory 239.3 499 FLD046-1 memory 191.8 499 FLD046-3 timeout 300.0 385 FLD047-1 memory 101.6 500 FLD047-2 memory 149.2 499 FLD047-3 memory 226.2 499 FLD047-4 timeout 300.0 410 FLD048-1 memory 110.3 499 FLD048-2 memory 187.6 499 FLD048-3 memory 231.2 499 FLD048-4 timeout 300.0 406 FLD049-1 memory 110.3 499 FLD049-2 memory 131.7 499 FLD049-3 theorem 48.1 111 FLD049-4 theorem 0.9 7 FLD050-1 memory 113.9 499 FLD050-2 memory 131.9 499 FLD050-3 timeout 300.0 440 FLD050-4 theorem 2.1 11 FLD051-1 memory 110.3 499 FLD051-2 memory 182.0 499 FLD051-3 memory 225.6 499 FLD051-4 timeout 300.0 419 FLD052-1 memory 110.1 498 FLD052-2 memory 52.9 499 FLD052-3 memory 228.0 499 FLD052-4 memory 76.7 499 FLD053-1 memory 112.3 499 FLD053-2 memory 51.6 499 FLD053-3 memory 221.6 500 FLD053-4 memory 77.6 496 FLD054-1 memory 99.5 499 FLD054-2 memory 164.3 497 FLD054-3 memory 227.0 499 FLD054-4 timeout 300.0 433 FLD055-1 theorem 0.0 2 FLD055-3 theorem 0.0 2 FLD056-1 theorem 0.0 2 FLD056-3 theorem 0.0 2 FLD057-1 memory 154.3 499 FLD057-3 memory 292.9 499 FLD058-1 theorem 0.0 2 FLD058-3 theorem 0.0 2 FLD059-1 theorem 0.1 0 FLD059-2 theorem 0.1 3 FLD059-3 theorem 0.1 3 FLD059-4 theorem 0.0 2 FLD060-1 theorem 7.2 34 FLD060-2 theorem 0.1 3 FLD060-3 theorem 227.7 469 FLD060-4 theorem 0.3 2 FLD061-1 theorem 9.9 45 FLD061-2 theorem 0.1 3 FLD061-3 memory 236.9 499 FLD061-4 theorem 0.6 6 FLD062-1 memory 105.4 500 FLD062-3 theorem 19.5 64 FLD063-1 memory 107.6 499 FLD063-3 theorem 4.1 19 FLD064-1 theorem 3.8 21 FLD064-3 theorem 0.0 3 FLD065-1 theorem 0.0 3 FLD065-3 theorem 0.0 2 FLD066-1 theorem 54.4 228 FLD066-3 theorem 0.2 4 FLD067-1 theorem 0.0 3 FLD067-2 theorem 0.1 3 FLD067-3 theorem 0.5 6 FLD067-4 theorem 0.0 2 FLD068-1 memory 106.8 499 FLD068-2 theorem 25.9 95 FLD068-3 theorem 20.7 62 FLD068-4 theorem 0.1 3 FLD069-1 theorem 0.0 3 FLD069-3 theorem 0.0 2 FLD070-1 theorem 0.1 3 FLD070-2 theorem 0.0 3 FLD070-3 theorem 0.1 3 FLD070-4 theorem 0.0 2 FLD071-1 theorem 0.0 2 FLD071-2 theorem 0.0 3 FLD071-3 theorem 0.0 2 FLD071-4 theorem 0.0 2 FLD072-1 memory 147.2 499 FLD072-2 memory 155.8 499 FLD072-3 timeout 300.0 440 FLD072-4 timeout 300.0 273 FLD073-1 memory 147.3 499 FLD073-2 memory 184.1 499 FLD073-3 timeout 300.0 451 FLD073-4 timeout 300.0 316 FLD074-1 memory 118.2 499 FLD074-2 memory 145.5 499 FLD074-3 memory 282.2 499 FLD074-4 timeout 300.0 441 FLD075-1 memory 114.3 499 FLD075-2 memory 145.5 500 FLD075-3 memory 282.4 499 FLD075-4 timeout 300.0 434 FLD076-1 memory 116.5 499 FLD076-2 memory 146.1 500 FLD076-3 timeout 300.0 467 FLD076-4 timeout 300.0 382 FLD077-1 memory 115.2 499 FLD077-2 memory 145.4 499 FLD077-3 memory 280.6 499 FLD077-4 timeout 300.0 404 FLD078-1 memory 123.9 499 FLD078-2 memory 140.2 499 FLD078-3 timeout 300.0 458 FLD078-4 timeout 300.0 346 FLD079-1 memory 132.8 499 FLD079-2 memory 121.0 499 FLD079-3 timeout 300.0 400 FLD079-4 timeout 300.0 328 FLD080-1 memory 217.0 499 FLD080-2 memory 156.9 499 FLD080-3 timeout 300.0 380 FLD080-4 timeout 300.0 403 FLD081-1 memory 141.1 499 FLD081-2 memory 165.8 499 FLD081-3 timeout 300.0 463 FLD081-4 timeout 300.0 241 FLD082-1 memory 132.6 499 FLD082-3 timeout 300.0 393 FLD083-1 memory 147.8 499 FLD083-3 timeout 300.0 440 FLD084-1 memory 108.5 499 FLD084-3 memory 269.0 499 FLD085-1 memory 113.2 500 FLD085-3 memory 271.4 499 FLD086-1 memory 114.0 499 FLD086-3 timeout 300.0 477 FLD087-1 memory 103.9 499 FLD087-3 memory 242.7 499 FLD088-1 memory 121.0 499 FLD088-3 memory 294.9 500 FLD089-1 memory 127.6 499 FLD089-3 timeout 300.0 455 FLD090-1 memory 183.2 499 FLD090-3 memory 233.4 499 FLD091-1 memory 107.6 500 FLD091-3 memory 243.0 499 FLD092-1 memory 106.4 499 FLD092-3 memory 253.9 499 FLD093-1 memory 108.2 499 FLD093-3 memory 241.1 499 FLD094-1 memory 110.1 498 FLD094-3 memory 258.2 499 FLD095-1 memory 144.7 499 FLD095-2 memory 54.1 499 FLD095-3 timeout 300.0 407 FLD095-4 memory 67.7 499 FLD096-1 memory 132.4 499 FLD096-2 memory 54.9 499 FLD096-3 timeout 300.0 407 FLD096-4 memory 70.4 499 FLD097-1 memory 126.2 499 FLD097-2 memory 164.2 499 FLD097-3 timeout 300.0 412 FLD097-4 timeout 300.0 333 FLD098-1 memory 128.1 499 FLD098-2 memory 172.5 499 FLD098-3 timeout 300.0 404 FLD098-4 timeout 300.0 332 FLD099-1 memory 133.9 499 FLD099-2 memory 180.7 499 FLD099-3 timeout 300.0 423 FLD099-4 timeout 300.0 269 FLD100-1 memory 146.4 499 FLD100-2 memory 163.8 499 FLD100-3 timeout 300.0 450 FLD100-4 timeout 300.0 410 GRA001-1 theorem 0.0 2 GRP025-3 memory 147.0 499 GRP026-3 memory 208.7 499 GRP027-2 memory 93.1 499 GRP039-6 theorem 1.1 8 GRP123-1.003 theorem 0.0 2 GRP123-1.005 timeout 300.0 233 GRP123-2.003 theorem 0.0 2 GRP123-2.005 timeout 300.0 84 GRP123-3.003 theorem 0.0 2 GRP123-3.004 non_thm 0.6 3 GRP123-4.003 theorem 0.0 2 GRP123-4.004 non_thm 2.8 4 GRP123-6.003 theorem 0.0 2 GRP123-6.005 timeout 300.0 263 GRP123-7.003 theorem 0.0 2 GRP123-7.005 timeout 300.0 294 GRP123-8.003 theorem 0.0 2 GRP123-8.004 non_thm 1.3 3 GRP123-9.003 theorem 0.0 2 GRP123-9.004 non_thm 1.5 3 GRP124-1.004 theorem 0.2 3 GRP124-1.005 timeout 300.0 451 GRP124-2.004 theorem 0.0 2 GRP124-2.005 timeout 300.0 268 GRP124-3.004 theorem 0.1 3 GRP124-3.005 timeout 300.0 254 GRP124-4.004 theorem 0.1 2 GRP124-4.005 memory 192.2 499 GRP124-6.004 theorem 0.1 3 GRP124-6.005 timeout 300.0 221 GRP124-7.004 theorem 0.0 3 GRP124-7.005 timeout 300.0 241 GRP124-8.004 theorem 0.1 3 GRP124-8.005 timeout 300.0 245 GRP124-9.004 theorem 0.1 3 GRP124-9.005 timeout 300.0 223 GRP125-1.003 theorem 0.0 2 GRP125-1.004 non_thm 0.8 3 GRP125-2.004 non_thm 0.1 2 GRP125-2.005 theorem 5.0 13 GRP125-3.004 non_thm 0.2 3 GRP125-3.005 theorem 13.7 25 GRP125-4.003 theorem 0.0 2 GRP125-4.004 non_thm 2.9 5 GRP126-1.004 theorem 0.1 3 GRP126-1.005 memory 197.6 499 GRP126-2.004 theorem 0.0 2 GRP126-2.005 timeout 300.0 204 GRP126-3.004 theorem 0.1 3 GRP126-3.005 timeout 300.0 208 GRP126-4.004 theorem 0.1 3 GRP126-4.005 memory 197.2 499 GRP127-1.004 theorem 0.1 2 GRP127-1.005 timeout 300.0 338 GRP127-2.005 non_thm 1.0 4 GRP127-2.006 theorem 19.1 41 GRP127-3.004 theorem 0.1 3 GRP127-3.005 timeout 300.0 124 GRP127-4.004 theorem 0.0 3 GRP127-4.005 memory 179.5 497 GRP128-1.003 theorem 0.1 2 GRP128-1.004 non_thm 9.1 4 GRP128-2.004 non_thm 0.4 3 GRP128-2.006 timeout 300.0 219 GRP128-3.004 non_thm 0.5 3 GRP128-3.005 theorem 3.8 6 GRP128-4.003 theorem 0.1 3 GRP128-4.004 non_thm 3.9 5 GRP129-1.003 theorem 0.1 3 GRP129-1.005 memory 272.3 499 GRP129-2.004 theorem 0.3 3 GRP129-2.005 timeout 300.0 237 GRP129-3.004 theorem 1.0 4 GRP129-3.005 timeout 300.0 415 GRP129-4.004 theorem 0.4 3 GRP129-4.005 memory 170.3 499 GRP130-1.003 theorem 0.4 3 GRP130-1.005 timeout 300.0 464 GRP130-2.003 theorem 0.1 3 GRP130-2.005 non_thm 9.6 12 GRP130-3.003 theorem 0.1 3 GRP130-3.004 non_thm 3.3 7 GRP130-4.003 theorem 0.2 3 GRP130-4.004 non_thm 8.9 6 GRP131-1.002 theorem 0.0 2 GRP131-1.005 memory 151.1 499 GRP131-2.002 theorem 0.0 2 GRP131-2.005 memory 276.5 499 GRP132-1.002 theorem 0.0 2 GRP132-1.005 memory 127.7 499 GRP132-2.002 theorem 0.0 2 GRP132-2.005 memory 187.1 499 GRP133-1.003 theorem 0.2 3 GRP133-1.004 timeout 300.0 249 GRP133-2.003 theorem 0.1 3 GRP133-2.004 timeout 300.0 112 GRP134-1.003 theorem 0.2 3 GRP134-1.005 memory 140.5 499 GRP134-2.003 theorem 0.1 3 GRP134-2.005 memory 158.0 499 GRP135-1.002 theorem 0.0 2 GRP135-1.005 timeout 300.0 411 GRP135-2.002 theorem 0.0 2 GRP135-2.005 non_thm 194.3 211 HWV003-3 theorem 0.0 2 HWV005-1 theorem 0.0 3 HWV005-2 theorem 0.0 2 HWV006-1 theorem 1.1 5 HWV006-2 theorem 0.1 3 HWV007-1 theorem 0.8 4 HWV007-2 theorem 0.1 3 HWV008-1.001 theorem 0.3 3 HWV008-1.002 theorem 0.4 3 HWV008-2.001 theorem 0.0 3 HWV008-2.002 theorem 0.1 3 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.2 3 KRS009-1 non_thm 0.0 2 KRS010-1 theorem 0.0 2 KRS011-1 non_thm 0.1 3 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.0 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.0 2 MGT036-1 theorem 0.0 2 MGT036-2 theorem 0.0 2 MGT041-2 theorem 0.0 2 MSC001-1 theorem 0.6 4 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 4 MSC008-1.002 theorem 0.2 3 MSC008-1.010 memory 273.9 499 MSC008-2.002 theorem 0.3 3 MSC009-1 non_thm 0.0 2 NLP026-1 timeout 300.0 339 NLP027-1 timeout 300.0 374 NLP028-1 memory 226.5 499 NLP029-1 timeout 300.0 290 NLP030-1 memory 261.3 499 NLP031-1 timeout 300.0 328 NLP032-1 timeout 300.0 341 NLP033-1 timeout 300.0 221 NLP034-1 timeout 300.0 454 NLP035-1 timeout 300.0 349 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 24.7 27 NLP060-1 timeout 300.0 239 NLP061-1 timeout 300.0 310 NLP062-1 timeout 300.0 214 NLP063-1 timeout 300.0 252 NLP064-1 non_thm 1.4 3 NLP065-1 timeout 300.0 173 NLP066-1 non_thm 0.0 2 NLP067-1 non_thm 0.1 2 NLP068-1 non_thm 0.0 2 NLP079-1 theorem 0.0 2 NLP080-1 theorem 0.0 2 NLP081-1 theorem 0.0 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 435 NLP161-1 timeout 300.0 427 NLP162-1 timeout 300.0 441 NLP163-1 timeout 300.0 434 NLP164-1 timeout 300.0 417 NLP165-1 timeout 300.0 434 NLP166-1 timeout 300.0 340 NLP167-1 timeout 300.0 444 NLP168-1 timeout 300.0 434 NLP169-1 timeout 300.0 361 NLP190-1 timeout 300.0 306 NLP191-1 timeout 300.0 267 NLP192-1 timeout 300.0 370 NLP193-1 timeout 300.0 191 NLP194-1 timeout 300.0 326 NLP195-1 timeout 300.0 322 NLP196-1 timeout 300.0 270 NLP197-1 timeout 300.0 351 NLP198-1 timeout 300.0 348 NLP199-1 timeout 300.0 346 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.2 3 NLP231-1 non_thm 0.2 3 NLP232-1 non_thm 0.2 3 NLP233-1 non_thm 0.4 3 NLP234-1 non_thm 1.0 3 NLP235-1 non_thm 0.3 2 NLP236-1 non_thm 0.3 3 NLP237-1 non_thm 0.4 3 NLP238-1 non_thm 0.2 3 NLP239-1 non_thm 0.3 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 223 PLA002-1 theorem 0.0 2 PLA002-2 theorem 0.4 4 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 25.7 9 PUZ012-1 theorem 0.0 2 PUZ013-1 theorem 0.0 2 PUZ014-1 theorem 0.0 2 PUZ015-2.006 theorem 0.7 3 PUZ016-2.004 non_thm 0.0 2 PUZ016-2.005 theorem 0.0 2 PUZ017-1 theorem 0.3 3 PUZ018-1 theorem 0.1 3 PUZ018-2 timeout 300.0 334 PUZ019-1 theorem 0.0 2 PUZ021-1 theorem 0.1 3 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.1 2 PUZ028-3 non_thm 15.3 5 PUZ028-4 non_thm 16.5 5 PUZ028-5 theorem 0.2 3 PUZ028-6 theorem 1.1 5 PUZ029-1 theorem 0.0 2 PUZ030-1 theorem 0.1 3 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 38 PUZ034-1.004 theorem 32.0 10 PUZ035-1 theorem 0.0 2 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.2 3 SET006-1 theorem 0.0 2 SET007-1 theorem 2.1 7 SET008-1 theorem 0.0 2 SET009-1 theorem 0.0 2 SET010-1 theorem 22.2 15 SET011-1 theorem 0.4 3 SET012-1 theorem 0.1 3 SET012-2 theorem 0.2 3 SET013-1 theorem 2.3 19 SET013-2 theorem 14.0 46 SET014-2 theorem 45.9 147 SET015-1 theorem 3.7 29 SET015-2 theorem 40.6 107 SET043-5 theorem 0.0 2 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.0 3 SET055-7 theorem 0.0 3 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 memory 90.1 500 SET786-1 theorem 0.0 2 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 2 SYN008-1 theorem 0.0 2 SYN009-1 theorem 0.0 2 SYN009-2 theorem 0.0 2 SYN009-3 theorem 0.0 2 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 0.0 2 SYN028-1 theorem 0.0 2 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 15.0 5 SYN036-2 non_thm 22.8 5 SYN036-3 theorem 0.0 2 SYN036-4 theorem 0.1 3 SYN037-1 theorem 0.0 2 SYN037-2 theorem 0.0 2 SYN038-1 theorem 0.0 2 SYN039-1 theorem 0.2 3 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 6.4 6 SYN067-2 theorem 27.7 33 SYN067-3 theorem 1.9 5 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 7 SYN308-1 non_thm 0.0 2 SYN309-1 non_thm 0.0 2 SYN313-1.001.002 theorem 0.1 3 SYN314-1.002.001 timeout 300.0 336 SYN315-1 theorem 0.0 2 SYN316-1 non_thm 0.0 2 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 2 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 2 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 2 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.1 2 SYN352-1 theorem 0.0 2 SYN353-1 theorem 0.0 2 SYN354-1 theorem 0.0 2 SYN418-1 timeout 300.0 128 SYN419-1 non_thm 3.7 4 SYN420-1 non_thm 12.3 5 SYN421-1 non_thm 52.7 7 SYN422-1 non_thm 164.7 16 SYN423-1 non_thm 45.5 7 SYN424-1 timeout 300.0 163 SYN425-1 timeout 300.0 23 SYN426-1 timeout 300.0 145 SYN427-1 timeout 300.0 128 SYN428-1 timeout 300.0 91 SYN429-1 timeout 300.0 142 SYN430-1 non_thm 0.2 3 SYN431-1 non_thm 2.1 3 SYN432-1 non_thm 41.4 22 SYN433-1 non_thm 29.8 15 SYN434-1 memory 190.6 499 SYN435-1 timeout 300.0 393 SYN436-1 theorem 28.8 7 SYN437-1 timeout 300.0 416 SYN438-1 timeout 300.0 123 SYN439-1 memory 278.5 499 SYN440-1 timeout 300.0 280 SYN441-1 memory 167.0 499 SYN442-1 theorem 25.6 11 SYN443-1 theorem 40.4 32 SYN444-1 theorem 8.1 7 SYN445-1 theorem 9.0 7 SYN446-1 non_thm 69.0 52 SYN447-1 memory 293.4 499 SYN448-1 theorem 17.8 10 SYN449-1 timeout 300.0 267 SYN450-1 theorem 55.1 25 SYN451-1 theorem 5.0 7 SYN452-1 theorem 58.7 25 SYN453-1 timeout 300.0 448 SYN454-1 theorem 7.0 7 SYN455-1 theorem 28.8 8 SYN456-1 timeout 300.0 155 SYN457-1 timeout 300.0 476 SYN458-1 theorem 8.3 8 SYN459-1 theorem 9.2 8 SYN460-1 timeout 300.0 435 SYN461-1 theorem 12.2 12 SYN462-1 theorem 22.6 16 SYN463-1 non_thm 7.0 8 SYN464-1 timeout 300.0 460 SYN465-1 theorem 18.7 12 SYN466-1 theorem 30.9 18 SYN467-1 theorem 84.7 43 SYN468-1 theorem 26.9 17 SYN469-1 theorem 12.5 10 SYN470-1 theorem 203.3 77 SYN471-1 theorem 20.6 16 SYN472-1 theorem 70.5 30 SYN473-1 theorem 127.8 65 SYN474-1 theorem 49.5 23 SYN475-1 theorem 9.5 10 SYN476-1 theorem 111.7 75 SYN477-1 theorem 20.2 13 SYN478-1 theorem 28.7 16 SYN479-1 theorem 37.1 20 SYN480-1 theorem 62.9 43 SYN481-1 theorem 117.1 81 SYN482-1 theorem 39.5 24 SYN483-1 theorem 12.5 10 SYN484-1 theorem 11.1 11 SYN485-1 theorem 7.5 9 SYN486-1 theorem 9.9 9 SYN487-1 theorem 58.3 25 SYN488-1 theorem 52.2 24 SYN489-1 theorem 187.6 155 SYN490-1 non_thm 0.1 2 SYN491-1 non_thm 0.0 2 SYN492-1 non_thm 0.0 2 SYN493-1 non_thm 0.1 3 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 16.7 12 SYN499-1 theorem 17.3 8 SYN500-1 theorem 33.4 22 SYN501-1 theorem 18.1 11 SYN502-1 theorem 18.9 20 SYN503-1 theorem 34.9 26 SYN504-1 theorem 40.0 34 SYN505-1 theorem 27.0 19 SYN506-1 theorem 13.3 9 SYN507-1 theorem 91.1 33 SYN508-1 theorem 43.5 28 SYN509-1 theorem 25.5 18 SYN510-1 theorem 152.5 113 SYN511-1 theorem 6.8 9 SYN512-1 theorem 23.2 16 SYN513-1 non_thm 15.5 6 SYN514-1 timeout 300.0 364 SYN515-1 non_thm 0.1 3 SYN516-1 non_thm 0.0 2 SYN517-1 non_thm 0.0 2 SYN518-1 timeout 300.0 53 SYN519-1 timeout 300.0 390 SYN520-1 timeout 300.0 166 SYN521-1 non_thm 0.0 2 SYN522-1 non_thm 0.2 3 SYN523-1 non_thm 0.0 2 SYN524-1 non_thm 0.1 3 SYN525-1 non_thm 0.1 2 SYN526-1 non_thm 0.0 3 SYN527-1 non_thm 0.0 2 SYN528-1 non_thm 0.1 3 SYN529-1 non_thm 0.0 3 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 timeout 300.0 183 SYN539-1 non_thm 0.9 3 SYN540-1 non_thm 0.1 3 SYN541-1 non_thm 19.0 20 SYN542-1 timeout 300.0 451 SYN543-1 timeout 300.0 425 SYN544-1 non_thm 184.0 42 SYN545-1 timeout 300.0 119 SYN546-1 non_thm 185.1 14 SYN547-1 memory 260.5 499 SYN554-1 theorem 0.0 2 SYN560-1 theorem 3.8 48 SYN567-1 theorem 0.0 2 SYN568-1 theorem 0.0 2 SYN571-1 theorem 0.4 4 SYN573-1 theorem 0.7 6 SYN574-1 theorem 0.4 4 SYN575-1 theorem 0.4 4 SYN576-1 theorem 35.1 113 SYN578-1 theorem 0.2 3 SYN579-1 theorem 0.1 3 SYN580-1 theorem 0.6 5 SYN581-1 theorem 0.0 2 SYN582-1 theorem 0.0 2 SYN583-1 theorem 0.1 3 SYN585-1 theorem 0.0 3 SYN586-1 theorem 28.4 184 SYN587-1 theorem 27.7 184 SYN591-1 theorem 9.5 80 SYN592-1 theorem 10.5 88 SYN593-1 theorem 0.0 2 SYN594-1 theorem 0.0 3 SYN595-1 theorem 0.0 2 SYN604-1 theorem 0.6 6 SYN605-1 theorem 3.1 11 SYN606-1 theorem 3.7 13 SYN607-1 theorem 3.2 11 SYN608-1 theorem 1.6 7 SYN609-1 theorem 3.2 11 SYN610-1 theorem 1.6 7 SYN611-1 theorem 3.1 11 SYN612-1 theorem 3.7 13 SYN613-1 theorem 0.2 3 SYN619-1 theorem 0.0 2 SYN620-1 theorem 14.6 59 SYN621-1 theorem 0.2 4 SYN622-1 theorem 0.3 4 SYN623-1 theorem 0.4 4 SYN624-1 theorem 41.0 164 SYN625-1 theorem 0.2 3 SYN626-1 theorem 0.4 5 SYN627-1 theorem 0.0 2 SYN630-1 theorem 0.1 3 SYN633-1 theorem 0.1 3 SYN634-1 theorem 0.1 3 SYN635-1 theorem 0.0 3 SYN636-1 theorem 0.1 3 SYN641-1 theorem 0.4 4 SYN642-1 theorem 0.3 4 SYN643-1 theorem 0.6 5 SYN644-1 theorem 0.3 6 SYN645-1 theorem 3.1 25 SYN648-1 theorem 0.0 2 SYN650-1 theorem 0.1 3 SYN656-1 theorem 0.2 3 SYN657-1 theorem 0.1 3 SYN658-1 theorem 4.0 14 SYN659-1 theorem 0.2 3 SYN660-1 theorem 0.2 3 SYN661-1 theorem 0.2 3 SYN662-1 theorem 0.1 3 SYN663-1 theorem 0.1 3 SYN664-1 theorem 0.3 3 SYN665-1 theorem 0.3 3 SYN666-1 theorem 3.0 3 SYN667-1 theorem 3.0 3 SYN668-1 theorem 3.0 3 SYN669-1 theorem 3.0 3 SYN670-1 theorem 1.2 3 SYN671-1 theorem 1.2 3 SYN672-1 theorem 7.1 23 SYN673-1 theorem 0.6 6 SYN674-1 theorem 0.2 3 SYN675-1 theorem 0.2 3 SYN676-1 theorem 0.1 3 SYN677-1 theorem 0.1 3 SYN678-1 theorem 0.2 3 SYN679-1 theorem 0.2 3 SYN680-1 theorem 0.2 3 SYN681-1 theorem 0.2 3 SYN682-1 theorem 0.2 3 SYN683-1 theorem 0.2 3 SYN684-1 theorem 0.1 3 SYN685-1 theorem 0.1 3 SYN686-1 theorem 0.5 5 SYN687-1 theorem 6.9 7 SYN690-1 theorem 0.0 3 SYN692-1 theorem 0.8 5 SYN693-1 theorem 0.7 5 SYN694-1 theorem 1.3 8 SYN695-1 theorem 1.8 9 SYN696-1 theorem 1.2 7 SYN697-1 theorem 1.4 7 SYN698-1 theorem 1.3 8 SYN699-1 theorem 1.2 7 SYN700-1 theorem 1.3 8 SYN701-1 theorem 1.7 9 SYN710-1 theorem 0.4 4 SYN713-1 theorem 40.4 153 SYN714-1 theorem 0.0 3 SYN717-1 theorem 0.1 3 SYN718-1 theorem 31.1 94 SYN724-1 theorem 0.0 2 SYN726-1 theorem 0.0 2 SYN728-1 theorem 0.0 2 SYN734-1 non_thm 0.0 2 SYN735-1 non_thm 0.0 2 SYN736-1 non_thm 0.1 2 SYN737-1 non_thm 0.1 2 SYN738-1 non_thm 0.0 2 SYN739-1 non_thm 0.0 2 SYN740-1 non_thm 0.0 2 SYN741-1 non_thm 0.1 3 SYN742-1 non_thm 0.1 2 SYN743-1 non_thm 0.0 2 SYN744-1 non_thm 0.0 2 SYN745-1 non_thm 0.2 3 SYN746-1 non_thm 0.7 3 SYN747-1 non_thm 1.0 3 SYN748-1 non_thm 1.0 3 SYN749-1 non_thm 0.1 2 SYN750-1 non_thm 9.7 5 SYN751-1 non_thm 6.9 4 SYN752-1 non_thm 2.4 4 SYN753-1 non_thm 16.7 7 SYN754-1 non_thm 0.2 3 SYN755-1 theorem 0.1 2 SYN756-1 non_thm 0.0 2 SYN757-1 non_thm 0.0 2 SYN758-1 theorem 2.4 4 SYN759-1 theorem 4.3 4 SYN760-1 non_thm 1.3 4 SYN761-1 non_thm 26.5 7 SYN762-1 theorem 0.6 3 SYN763-1 non_thm 0.3 3 SYN764-1 memory 286.7 499 SYN765-1 timeout 300.0 416 SYN766-1 timeout 300.0 198 SYN767-1 timeout 300.0 381 SYN768-1 non_thm 0.3 3 SYN769-1 timeout 300.0 193 SYN770-1 timeout 300.0 156 SYN771-1 timeout 300.0 213 SYN772-1 non_thm 0.1 3 SYN773-1 timeout 300.0 62 SYN774-1 non_thm 1.1 3 SYN775-1 non_thm 0.2 3 SYN776-1 timeout 300.0 481 SYN777-1 timeout 300.0 422 SYN778-1 timeout 300.0 447 SYN779-1 timeout 300.0 447 SYN780-1 timeout 300.0 198 SYN781-1 timeout 300.0 299 SYN782-1 timeout 300.0 274 SYN783-1 timeout 300.0 398 SYN784-1 theorem 0.5 3 SYN785-1 non_thm 0.1 3 SYN786-1 timeout 300.0 149 SYN787-1 timeout 300.0 209 SYN788-1 timeout 300.0 320 SYN789-1 timeout 300.0 454 SYN790-1 timeout 300.0 23 SYN791-1 timeout 300.0 220 SYN792-1 timeout 300.0 479 SYN793-1 memory 245.3 499 SYN794-1 non_thm 0.2 3 SYN795-1 timeout 300.0 157 SYN796-1 theorem 0.1 3 SYN797-1 non_thm 0.1 3 SYN798-1 non_thm 7.8 7 SYN799-1 non_thm 27.7 13 SYN800-1 non_thm 18.0 12 SYN801-1 non_thm 41.2 17 SYN802-1 theorem 5.6 6 SYN803-1 timeout 300.0 217 SYN804-1 timeout 300.0 152 SYN805-1 timeout 300.0 209 SYN806-1 timeout 300.0 459 SYN807-1 timeout 300.0 390 SYN808-1 memory 291.6 499 SYN809-1 timeout 300.0 452 SYN810-1 timeout 300.0 403 SYN811-1 non_thm 1.0 4 SYN812-1 non_thm 7.9 15 SYN813-1 theorem 3.5 3 SYN814-1 non_thm 2.8 5 SYN815-1 non_thm 6.8 9 SYN816-1 non_thm 7.0 8 SYN817-1 non_thm 6.5 9 SYN818-1 non_thm 25.3 19 SYN819-1 theorem 0.6 3 SYN820-1 theorem 0.5 3 SYN821-1 timeout 300.0 11 SYN822-1 timeout 300.0 13 SYN823-1 non_thm 0.2 3 SYN824-1 non_thm 1.8 6 SYN825-1 non_thm 6.3 14 SYN826-1 non_thm 7.1 15 SYN827-1 non_thm 0.3 3 SYN828-1 non_thm 3.0 8 SYN829-1 non_thm 11.1 18 SYN830-1 non_thm 11.7 20 SYN831-1 non_thm 11.4 19 SYN832-1 non_thm 9.4 17 SYN833-1 theorem 0.4 3 SYN834-1 theorem 0.4 3 SYN835-1 non_thm 0.4 3 SYN836-1 theorem 0.4 3 SYN837-1 theorem 1.2 5 SYN838-1 non_thm 5.3 9 SYN839-1 non_thm 14.8 21 SYN840-1 non_thm 14.0 21 SYN841-1 non_thm 14.8 21 SYN842-1 non_thm 17.4 23 SYN843-1 theorem 0.4 3 SYN844-1 theorem 0.4 3 SYN845-1 theorem 0.4 3 SYN846-1 theorem 1.3 5 SYN847-1 theorem 1.1 5 SYN848-1 theorem 1.2 5 SYN849-1 theorem 1.1 5 SYN850-1 theorem 4.9 10 SYN851-1 non_thm 4.8 10 SYN852-1 non_thm 18.2 23 SYN853-1 non_thm 19.0 24 SYN854-1 non_thm 18.9 23 SYN855-1 non_thm 16.6 22 SYN856-1 theorem 0.5 3 SYN857-1 theorem 0.5 4 SYN858-1 theorem 1.3 5 SYN859-1 theorem 1.3 5 SYN860-1 theorem 1.6 5 SYN861-1 theorem 5.2 10 SYN862-1 theorem 5.3 10 SYN863-1 non_thm 6.4 10 SYN864-1 non_thm 5.5 10 SYN865-1 theorem 5.4 10 SYN866-1 theorem 4.9 10 SYN867-1 non_thm 0.0 3 SYN868-1 non_thm 0.0 3 SYN869-1 theorem 0.0 3 SYN870-1 non_thm 0.0 2 SYN871-1 theorem 0.0 3 SYN872-1 non_thm 0.3 4 SYN873-1 theorem 0.1 3 SYN874-1 theorem 0.1 3 SYN875-1 theorem 0.1 3 SYN876-1 theorem 0.1 3 SYN877-1 theorem 0.1 3 SYN878-1 theorem 0.1 3 SYN879-1 theorem 0.1 3 SYN880-1 theorem 0.1 3 SYN881-1 theorem 0.1 3 SYN882-1 theorem 0.1 3 SYN883-1 theorem 0.1 3 SYN884-1 theorem 0.2 3 SYN885-1 theorem 0.2 3 SYN886-1 theorem 0.2 3 SYN887-1 theorem 0.2 3 SYN888-1 non_thm 0.4 4 SYN889-1 theorem 0.1 3 SYN890-1 theorem 0.0 2 SYN891-1 theorem 0.0 3 SYN892-1 theorem 0.1 3 SYN893-1 theorem 0.1 3 SYN894-1 theorem 0.1 3 SYN895-1 theorem 0.1 3 SYN896-1 theorem 0.1 3 SYN897-1 theorem 0.2 3 SYN898-1 theorem 0.2 3 SYN899-1 theorem 0.2 3 SYN900-1 theorem 0.2 3 SYN901-1 theorem 0.4 4 SYN902-1 non_thm 0.4 4 SYN903-1 timeout 300.0 82 SYN904-1 timeout 300.0 104 SYN905-1 timeout 300.0 120 SYN906-1 timeout 300.0 60 SYN907-1 timeout 300.0 76 SYN908-1 timeout 300.0 165 SYN909-1 timeout 300.0 82 SYN910-1 timeout 300.0 121 SYN911-1 timeout 300.0 89 SYN912-1 timeout 300.0 124 SYN913-1 timeout 300.0 58 TOP001-1 timeout 300.0 373 TOP001-2 theorem 0.0 2 TOP002-1 timeout 300.0 388 TOP002-2 theorem 0.0 2 TOP003-1 timeout 300.0 391 TOP003-2 non_thm 0.0 2 TOP004-1 theorem 0.0 2 TOP004-2 theorem 0.0 2 TOP005-1 timeout 300.0 290 TOP005-2 theorem 0.0 3 TOP006-1 timeout 300.0 372 TOP007-1 timeout 300.0 213 TOP008-1 timeout 300.0 325 TOP009-1 timeout 300.0 179 TOP010-1 timeout 300.0 287 TOP011-1 timeout 300.0 384 TOP012-1 timeout 300.0 316 TOP013-1 timeout 300.0 324 TOP014-1 timeout 300.0 300 TOP015-1 timeout 300.0 321 TOP016-1 timeout 300.0 323 TOP017-1 timeout 300.0 308 TOP018-1 timeout 300.0 5 TOP019-1 timeout 300.0 160