-------------------------------------------------------------------------------- Execute format string : ./darwin --lookahead-all true Problems list file : nne_lookahead-problems Output file : nne_lookahead-output Summary file : nne_lookahead-summary Time limit : 300 s Memory limit : 400 MB -------------------------------------------------------------------------------- Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. ALG002-1 theorem 0.0 4 1 45 0 4 0 0 0 3 45 320 2 ANA001-1 timeout 299.0 29 ANA002-1 timeout 299.0 48 ANA002-2 timeout 299.0 63 ANA002-3 timeout 298.9 22 ANA002-4 timeout 299.0 26 ANA003-4 memory 291.4 399 ANA004-4 memory 297.7 399 ANA004-5 timeout 298.9 37 ANA005-4 timeout 299.0 42 ANA005-5 timeout 299.0 48 CAT007-3 theorem 0.0 4 1 5 0 5 0 0 0 2 5 13 2 COM002-2 theorem 0.0 4 1 26 0 15 0 0 0 2 26 47 0 COM003-1 theorem 5.4 9 814 8399 5778 1707 210 12 43771 2 209 34119 172588 COM003-2 theorem 0.0 4 1 12 0 22 13 1 0 2 12 24 1 COM005-1 timeout 298.9 23 COM006-1 timeout 299.0 21 FLD001-3 theorem 0.2 5 1 62 0 7 0 0 0 2 62 7017 0 FLD002-3 theorem 0.2 5 1 63 0 7 0 0 0 2 63 7034 0 FLD003-1 timeout 299.0 88 FLD004-1 timeout 299.0 93 FLD005-1 timeout 299.0 96 FLD005-3 theorem 0.3 5 1 89 0 6 0 0 0 2 89 7670 0 FLD006-1 timeout 298.9 87 FLD006-3 theorem 0.0 4 1 5 0 4 0 0 0 2 5 31 0 FLD007-1 timeout 299.0 71 FLD007-3 timeout 299.0 43 FLD008-1 timeout 299.0 84 FLD008-2 timeout 299.0 334 FLD008-3 timeout 298.9 40 FLD008-4 theorem 1.1 14 1 145 0 10 0 0 0 2 145 29718 0 FLD009-1 timeout 299.0 93 FLD009-3 theorem 0.3 6 1 110 0 7 0 0 0 2 110 7952 0 FLD010-1 timeout 299.0 93 FLD010-3 theorem 0.0 4 1 6 0 5 0 0 0 2 6 35 0 FLD010-5 theorem 0.1 4 1 54 0 5 0 0 0 2 54 1342 0 FLD011-1 timeout 299.0 90 FLD011-3 timeout 299.0 46 FLD012-1 timeout 299.0 98 FLD012-2 timeout 299.0 358 FLD012-3 timeout 299.0 59 FLD012-4 theorem 1.3 14 1 270 0 12 0 0 0 2 270 34114 0 FLD013-1 theorem 94.5 54 1 272 0 10 0 0 0 2 272 1901567 0 FLD013-2 theorem 203.3 73 1 345 0 12 0 0 0 2 345 4428727 0 FLD013-3 theorem 1.5 14 1 324 0 10 0 0 0 2 324 35332 0 FLD013-4 theorem 0.0 4 1 29 0 12 0 0 0 2 29 917 0 FLD013-5 theorem 0.0 4 1 27 0 14 0 0 0 2 27 1118 0 FLD014-1 timeout 299.0 85 FLD014-3 theorem 0.4 6 1 192 0 7 0 0 0 2 192 10340 0 FLD015-1 timeout 299.0 99 FLD015-3 theorem 0.3 4 1 93 0 7 0 0 0 2 93 7372 0 FLD016-1 timeout 299.0 332 FLD016-3 theorem 1.1 14 1 151 0 10 0 0 0 2 151 29765 0 FLD016-5 theorem 2.0 18 1 204 0 12 0 0 0 2 204 52592 0 FLD017-1 theorem 0.3 6 1 24 0 10 0 0 0 2 24 6100 0 FLD017-3 theorem 0.0 4 1 11 0 10 0 0 0 2 11 187 0 FLD018-1 timeout 299.0 86 FLD018-3 theorem 0.1 4 1 73 0 6 0 0 0 2 73 4072 0 FLD019-1 timeout 299.0 80 FLD019-3 theorem 0.0 4 1 14 0 6 0 0 0 2 14 264 0 FLD020-1 timeout 299.0 96 FLD020-3 theorem 0.3 4 1 83 0 7 0 0 0 2 83 7586 0 FLD021-1 theorem 14.7 38 1 55 0 7 0 0 0 2 55 214400 0 FLD021-3 theorem 0.0 4 1 14 0 7 0 0 0 2 14 304 0 FLD022-1 timeout 299.0 168 FLD022-3 theorem 1.1 14 1 149 0 10 0 0 0 2 149 29741 0 FLD023-1 timeout 299.0 94 FLD023-3 theorem 0.2 4 1 86 0 7 0 0 0 2 86 7472 0 FLD024-1 timeout 299.0 89 FLD024-3 theorem 0.2 5 1 57 0 7 0 0 0 2 57 6961 0 FLD025-1 theorem 94.4 51 1 284 0 10 0 0 0 2 284 1903651 0 FLD025-2 timeout 299.0 91 FLD025-3 theorem 1.5 14 1 324 0 10 0 0 0 2 324 35332 0 FLD025-4 theorem 0.0 4 1 36 0 12 0 0 0 2 36 938 0 FLD025-5 theorem 0.0 4 1 35 0 14 0 0 0 2 35 1146 0 FLD026-1 timeout 299.0 93 FLD026-3 theorem 0.9 7 1 410 0 8 0 0 0 2 410 19453 0 FLD027-1 timeout 299.0 104 FLD027-3 theorem 0.3 6 1 149 0 9 0 0 0 2 149 9064 0 FLD028-1 timeout 299.0 352 FLD028-3 theorem 1.2 14 1 181 0 11 0 0 0 2 181 30829 0 FLD029-1 timeout 299.0 370 FLD029-3 theorem 1.8 15 1 589 0 11 0 0 0 2 589 40111 0 FLD030-1 theorem 0.0 4 1 9 0 8 0 0 0 2 9 529 0 FLD030-2 theorem 0.3 6 1 24 0 10 0 0 0 2 24 6100 0 FLD030-3 theorem 0.0 4 1 25 0 8 0 0 0 2 25 498 0 FLD030-4 theorem 0.0 4 1 11 0 10 0 0 0 2 11 187 0 FLD031-1 timeout 299.0 87 FLD031-3 theorem 0.2 4 1 83 0 7 0 0 0 2 83 4841 0 FLD031-5 theorem 0.2 4 1 100 0 7 0 0 0 2 100 5614 0 FLD032-1 timeout 299.0 82 FLD032-3 theorem 0.0 4 1 18 0 7 0 0 0 2 18 278 0 FLD033-1 timeout 299.0 92 FLD033-3 theorem 0.3 6 1 126 0 8 0 0 0 2 126 8494 0 FLD034-1 theorem 15.0 35 1 60 0 7 0 0 0 2 60 230607 0 FLD034-3 theorem 0.0 4 1 18 0 7 0 0 0 2 18 320 0 FLD035-1 timeout 299.0 165 FLD035-3 theorem 1.1 13 1 181 0 11 0 0 0 2 181 30829 0 FLD036-1 timeout 299.0 146 FLD036-3 theorem 1.2 14 1 181 0 11 0 0 0 2 181 30829 0 FLD037-1 timeout 299.0 88 FLD037-3 theorem 0.3 4 1 128 0 8 0 0 0 2 128 9293 0 FLD038-1 timeout 299.0 89 FLD038-3 theorem 0.2 5 1 64 0 8 0 0 0 2 64 7345 0 FLD039-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 150 0 FLD039-3 theorem 0.0 4 1 15 0 6 0 0 0 2 15 249 0 FLD040-1 timeout 299.0 91 FLD040-3 theorem 0.1 4 1 67 0 6 0 0 0 2 67 3251 0 FLD040-5 theorem 0.1 4 1 68 0 6 0 0 0 2 68 3315 0 FLD041-1 timeout 299.0 99 FLD041-2 timeout 299.0 149 FLD041-3 theorem 0.4 6 1 188 0 8 0 0 0 2 188 10004 0 FLD041-4 theorem 1.0 10 1 343 0 10 0 0 0 2 343 26700 0 FLD043-1 timeout 299.0 94 FLD043-3 theorem 0.3 6 1 107 0 7 0 0 0 2 107 8261 0 FLD043-5 theorem 10.7 13 1 684 0 5 0 0 0 2 684 103836 0 FLD044-1 timeout 299.0 93 FLD044-2 timeout 299.0 347 FLD044-3 timeout 299.0 40 FLD044-4 timeout 299.0 48 FLD045-1 timeout 299.0 101 FLD045-2 timeout 299.0 338 FLD045-3 timeout 298.9 40 FLD045-4 timeout 299.0 47 FLD046-1 timeout 299.0 98 FLD046-3 timeout 299.0 47 FLD047-1 timeout 299.0 154 FLD047-2 timeout 299.0 91 FLD047-3 timeout 299.0 60 FLD047-4 theorem 3.8 23 1 441 0 15 0 0 0 2 441 91664 0 FLD048-1 timeout 299.0 346 FLD048-2 timeout 299.0 95 FLD048-3 timeout 299.0 60 FLD048-4 theorem 193.9 47 1 2388 0 20 0 0 0 2 2388 428915 0 FLD049-1 timeout 299.0 360 FLD049-2 timeout 299.0 82 FLD049-3 timeout 299.0 60 FLD049-4 theorem 3.6 23 1 295 0 15 0 0 0 2 295 88385 0 FLD050-1 timeout 299.0 352 FLD050-2 timeout 299.0 102 FLD050-3 timeout 299.0 60 FLD050-4 theorem 3.5 22 1 298 0 15 0 0 0 2 298 88432 0 FLD051-1 timeout 299.0 348 FLD051-2 timeout 299.0 124 FLD051-3 timeout 299.0 65 FLD051-4 timeout 299.0 50 FLD052-1 timeout 299.0 340 FLD052-2 timeout 299.0 87 FLD052-3 timeout 299.0 61 FLD052-4 theorem 31.8 57 1 932 0 25 0 0 0 2 932 725361 0 FLD053-1 timeout 299.0 360 FLD053-2 timeout 299.0 127 FLD053-3 timeout 299.0 60 FLD053-4 timeout 299.0 55 FLD054-1 timeout 299.0 88 FLD054-2 memory 288.1 399 FLD054-3 timeout 299.0 58 FLD054-4 theorem 2.4 18 1 419 0 14 0 0 0 2 419 58849 0 FLD055-1 theorem 0.2 6 1 27 0 9 0 0 0 2 27 4793 0 FLD055-3 theorem 0.0 4 1 20 0 9 0 0 0 2 20 464 0 FLD056-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 141 0 FLD056-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 57 0 FLD057-1 timeout 299.0 107 FLD057-3 timeout 299.0 62 FLD058-1 theorem 0.1 4 1 25 0 9 0 0 0 2 25 2761 0 FLD058-3 theorem 0.0 4 1 21 0 9 0 0 0 2 21 401 0 FLD059-1 theorem 2.9 18 1 40 0 6 0 0 0 2 40 50026 0 FLD059-2 theorem 14.8 39 1 177 0 8 0 0 0 2 177 221851 0 FLD059-3 theorem 0.1 4 1 54 0 6 0 0 0 2 54 2830 0 FLD059-4 theorem 0.0 4 1 14 0 8 0 0 0 2 14 307 0 FLD060-1 theorem 14.5 38 1 133 0 7 0 0 0 2 133 220008 0 FLD060-2 theorem 90.6 57 1 267 0 11 0 0 0 2 267 1897159 0 FLD060-3 theorem 31.7 20 1 996 0 7 0 0 0 2 996 152477 0 FLD060-4 theorem 1.4 14 1 313 0 11 0 0 0 2 313 32325 0 FLD061-1 theorem 92.7 58 1 245 0 10 0 0 0 2 245 1895470 0 FLD061-2 timeout 299.0 105 FLD061-3 theorem 178.3 43 1 1854 0 10 0 0 0 2 1854 319736 0 FLD061-4 theorem 3.9 23 1 471 0 14 0 0 0 2 471 89194 0 FLD062-1 timeout 299.0 90 FLD062-3 theorem 85.1 30 1 1101 0 7 0 0 0 2 1101 283422 0 FLD063-1 timeout 299.0 83 FLD063-3 theorem 22.5 18 1 818 0 7 0 0 0 2 818 118512 0 FLD064-1 timeout 299.0 102 FLD064-3 theorem 0.1 4 1 87 0 6 0 0 0 2 87 4443 0 FLD065-1 timeout 299.0 81 FLD065-3 theorem 0.0 4 1 12 0 6 0 0 0 2 12 181 0 FLD066-1 timeout 299.0 139 FLD066-3 theorem 2.0 18 1 207 0 12 0 0 0 2 207 52672 0 FLD067-1 timeout 299.0 93 FLD067-2 timeout 299.0 149 FLD067-3 theorem 0.3 5 1 85 0 7 0 0 0 2 85 7277 0 FLD067-4 theorem 0.6 9 1 107 0 9 0 0 0 2 107 15427 0 FLD068-1 timeout 299.0 94 FLD068-2 timeout 299.0 156 FLD068-3 timeout 299.0 41 FLD068-4 theorem 0.5 9 1 87 0 9 0 0 0 2 87 15268 0 FLD069-1 theorem 15.7 38 1 98 0 9 0 0 0 2 98 232411 0 FLD069-3 theorem 0.0 4 1 16 0 9 0 0 0 2 16 380 0 FLD070-1 theorem 14.2 37 1 60 0 8 0 0 0 2 60 214822 0 FLD070-2 theorem 38.6 45 1 266 0 10 0 0 0 2 266 713852 0 FLD070-3 theorem 0.2 4 1 80 0 8 0 0 0 2 80 7187 0 FLD070-4 theorem 0.0 4 1 17 0 10 0 0 0 2 17 465 0 FLD071-1 theorem 0.0 4 1 8 0 8 0 0 0 2 8 299 0 FLD071-2 theorem 43.4 56 1 100 0 10 0 0 0 2 100 699157 0 FLD071-3 theorem 0.0 4 1 9 0 8 0 0 0 2 9 98 0 FLD071-4 theorem 0.0 4 1 9 0 9 0 0 0 2 9 141 0 FLD072-1 timeout 299.0 94 FLD072-2 timeout 299.0 170 FLD072-3 timeout 299.0 46 FLD072-4 timeout 299.0 74 FLD073-1 timeout 299.0 91 FLD073-2 timeout 299.0 171 FLD073-3 timeout 299.0 41 FLD073-4 timeout 299.0 77 FLD074-1 timeout 299.0 168 FLD074-2 memory 277.6 399 FLD074-3 timeout 299.0 47 FLD074-4 timeout 298.9 47 FLD075-1 timeout 299.0 157 FLD075-2 memory 280.4 399 FLD075-3 timeout 298.9 47 FLD075-4 timeout 299.0 47 FLD076-1 timeout 299.0 162 FLD076-2 memory 272.3 399 FLD076-3 timeout 299.0 58 FLD076-4 timeout 299.0 48 FLD077-1 timeout 299.0 155 FLD077-2 memory 282.3 399 FLD077-3 timeout 299.0 58 FLD077-4 timeout 299.0 49 FLD078-1 timeout 299.0 83 FLD078-2 timeout 298.9 155 FLD078-3 timeout 299.0 54 FLD078-4 timeout 298.9 58 FLD079-1 timeout 299.0 119 FLD079-2 timeout 299.0 178 FLD079-3 timeout 299.0 64 FLD079-4 timeout 299.0 74 FLD080-1 timeout 299.0 89 FLD080-2 timeout 299.0 86 FLD080-3 timeout 299.0 42 FLD080-4 timeout 299.0 58 FLD081-1 timeout 299.0 346 FLD081-2 timeout 299.0 94 FLD081-3 timeout 299.0 52 FLD081-4 timeout 299.0 57 FLD082-1 timeout 299.0 88 FLD082-3 timeout 299.0 64 FLD083-1 timeout 299.0 101 FLD083-3 timeout 299.0 65 FLD084-1 timeout 299.0 104 FLD084-3 timeout 299.0 58 FLD085-1 timeout 299.0 92 FLD085-3 timeout 299.0 58 FLD086-1 timeout 299.0 89 FLD086-3 timeout 299.0 48 FLD087-1 timeout 299.0 90 FLD087-3 timeout 299.0 48 FLD088-1 timeout 299.0 110 FLD088-3 timeout 298.9 48 FLD089-1 timeout 299.0 92 FLD089-3 timeout 299.0 48 FLD090-1 timeout 299.0 94 FLD090-3 timeout 299.0 43 FLD091-1 timeout 299.0 85 FLD091-3 timeout 299.0 47 FLD092-1 timeout 299.0 91 FLD092-3 timeout 299.0 47 FLD093-1 timeout 299.0 84 FLD093-3 timeout 299.0 47 FLD094-1 timeout 299.0 86 FLD094-3 timeout 299.0 47 FLD095-1 timeout 299.0 372 FLD095-2 timeout 299.0 103 FLD095-3 timeout 298.9 64 FLD095-4 timeout 299.0 47 FLD096-1 timeout 299.0 358 FLD096-2 timeout 299.0 105 FLD096-3 timeout 299.0 65 FLD096-4 timeout 299.0 47 FLD097-1 timeout 299.0 91 FLD097-2 timeout 299.0 88 FLD097-3 timeout 299.0 42 FLD097-4 timeout 299.0 46 FLD098-1 timeout 299.0 86 FLD098-2 timeout 299.0 113 FLD098-3 timeout 299.0 42 FLD098-4 timeout 299.0 47 FLD099-1 timeout 299.0 105 FLD099-2 timeout 299.0 162 FLD099-3 timeout 299.0 47 FLD099-4 timeout 299.0 84 FLD100-1 timeout 299.0 82 FLD100-2 timeout 299.0 91 FLD100-3 timeout 299.0 42 FLD100-4 timeout 298.9 47 GRA001-1 theorem 0.0 4 4 10 3 44 28 0 2 2 5 22 10 GRP025-3 timeout 299.0 38 GRP026-3 timeout 299.0 56 GRP027-2 timeout 299.0 21 GRP039-6 theorem 39.4 7 26 2492 27 9 0 2 45122 2 822 434590 65270 GRP123-1.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 87 0 GRP123-1.005 non_thm 0.1 4 0 143 4 26 0 0 465 2 147 1556 505 GRP123-2.003 theorem 0.0 4 1 37 0 15 0 0 0 2 37 94 0 GRP123-2.005 non_thm 0.1 4 1 189 2 40 0 0 493 2 175 1815 595 GRP123-3.003 theorem 0.0 4 1 51 0 20 0 0 0 2 51 111 0 GRP123-3.004 non_thm 0.0 4 1 143 1 32 0 0 219 2 132 951 257 GRP123-4.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 105 0 GRP123-4.004 non_thm 0.1 4 0 77 1 17 0 0 406 2 78 802 449 GRP123-6.003 theorem 0.0 4 1 50 0 11 0 0 0 2 50 143 0 GRP123-6.005 non_thm 0.1 4 0 264 4 27 0 0 879 2 268 1624 947 GRP123-7.003 theorem 0.0 4 1 56 0 16 0 0 0 2 56 149 0 GRP123-7.005 non_thm 0.1 4 0 284 4 41 0 0 879 2 288 1644 947 GRP123-8.003 theorem 0.0 4 1 62 0 21 0 0 0 2 62 156 0 GRP123-8.004 non_thm 0.0 4 0 177 2 33 0 0 342 2 179 879 372 GRP123-9.003 theorem 0.0 4 1 50 0 11 0 0 0 2 50 143 0 GRP123-9.004 non_thm 0.0 4 0 138 29 18 0 0 322 2 167 813 379 GRP124-1.004 theorem 0.0 4 2 72 1 17 0 0 37 2 64 392 155 GRP124-1.005 non_thm 0.1 4 0 142 5 26 0 0 458 2 147 1556 505 GRP124-2.004 theorem 0.0 4 1 75 0 26 0 0 0 2 75 182 0 GRP124-2.005 non_thm 0.1 4 0 173 2 40 0 0 460 2 175 1590 505 GRP124-3.004 theorem 0.0 4 2 117 1 32 0 0 48 2 106 337 171 GRP124-3.005 non_thm 0.1 4 2 244 4 47 0 0 551 2 223 1899 670 GRP124-4.004 theorem 0.0 4 2 66 1 17 0 0 101 2 62 293 350 GRP124-4.005 non_thm 0.1 4 0 143 4 26 0 0 1190 2 147 1606 1305 GRP124-6.004 theorem 0.0 4 2 109 1 18 0 0 71 2 101 424 234 GRP124-6.005 non_thm 0.1 4 0 263 5 27 0 0 877 2 268 1624 947 GRP124-7.004 theorem 0.0 4 2 121 1 27 0 0 71 2 113 436 234 GRP124-7.005 non_thm 0.1 4 0 283 5 41 0 0 877 2 288 1644 947 GRP124-8.004 theorem 0.0 4 2 148 2 33 0 0 90 2 141 490 259 GRP124-8.005 non_thm 0.1 4 0 322 6 48 0 0 938 2 328 1739 1009 GRP124-9.004 theorem 0.0 4 2 109 1 18 0 0 71 2 101 424 266 GRP124-9.005 non_thm 0.1 4 0 263 50 27 0 0 882 2 313 1624 997 GRP125-1.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 94 0 GRP125-1.004 non_thm 0.0 4 0 77 1 17 0 0 165 2 78 469 180 GRP125-2.004 non_thm 0.0 4 0 96 0 26 0 0 180 2 96 490 180 GRP125-2.005 theorem 0.0 4 3 184 2 40 0 0 137 2 157 800 479 GRP125-3.004 non_thm 0.0 4 1 143 1 32 0 0 206 2 132 669 247 GRP125-3.005 theorem 0.1 4 5 280 4 47 0 0 232 2 219 1294 748 GRP125-4.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 146 0 GRP125-4.004 non_thm 0.0 4 0 77 1 17 0 0 419 2 78 719 462 GRP126-1.004 theorem 0.0 4 2 69 1 17 0 0 36 2 63 316 141 GRP126-1.005 non_thm 0.1 4 0 143 4 26 0 0 443 2 147 935 484 GRP126-2.004 theorem 0.0 4 1 75 0 26 0 0 0 2 75 224 0 GRP126-2.005 non_thm 0.0 4 0 173 2 40 0 0 450 2 175 969 484 GRP126-3.004 theorem 0.0 4 2 117 1 32 0 0 47 2 106 371 171 GRP126-3.005 non_thm 0.1 4 2 244 4 47 0 0 536 2 223 1271 649 GRP126-4.004 theorem 0.0 4 2 67 1 17 0 0 102 2 63 403 367 GRP126-4.005 non_thm 0.1 4 0 144 3 26 0 0 1212 2 147 1427 1326 GRP127-1.004 theorem 0.0 4 2 72 1 17 0 0 36 2 64 352 151 GRP127-1.005 non_thm 0.1 4 0 145 2 26 0 0 456 2 147 935 484 GRP127-2.005 non_thm 0.0 4 1 187 1 40 0 0 447 2 175 1050 542 GRP127-2.006 theorem 0.1 4 3 313 2 57 0 0 251 2 253 1328 1321 GRP127-3.004 theorem 0.0 4 2 117 1 32 0 0 47 2 106 347 170 GRP127-3.005 non_thm 0.1 4 2 271 2 47 0 0 550 2 227 1407 744 GRP127-4.004 theorem 0.0 4 2 68 1 17 0 0 102 2 63 429 368 GRP127-4.005 non_thm 0.1 4 0 145 2 26 0 0 1244 2 147 1427 1326 GRP128-1.003 theorem 0.0 4 4 59 3 9 0 0 7 2 32 200 90 GRP128-1.004 non_thm 0.0 4 7 171 8 16 0 0 215 2 84 925 392 GRP128-2.004 non_thm 0.0 4 1 100 3 25 0 0 188 2 102 537 198 GRP128-2.006 theorem 0.1 4 8 428 7 56 0 0 379 2 251 1751 1545 GRP128-3.004 non_thm 0.0 4 3 212 4 31 0 0 232 2 139 876 345 GRP128-3.005 theorem 0.1 4 7 395 6 46 0 0 143 2 207 1467 858 GRP128-4.003 theorem 0.0 4 4 28 3 9 0 0 15 2 28 193 108 GRP128-4.004 non_thm 0.0 4 5 83 6 16 0 0 474 2 84 884 512 GRP129-1.003 theorem 0.0 4 4 59 3 9 0 0 7 2 29 238 92 GRP129-1.005 non_thm 0.2 4 24 686 28 25 0 0 737 2 155 3378 2149 GRP129-2.004 theorem 0.0 4 7 164 7 25 0 0 69 2 78 599 258 GRP129-2.005 non_thm 0.1 4 10 316 15 39 0 0 592 2 183 1745 820 GRP129-3.004 theorem 0.0 4 7 236 7 31 0 0 165 2 115 783 344 GRP129-3.005 non_thm 0.1 4 7 390 9 46 0 0 827 2 232 1914 992 GRP129-4.004 theorem 0.0 4 9 116 8 16 0 0 94 2 51 665 526 GRP129-4.005 non_thm 0.1 4 13 234 16 25 0 0 1454 2 155 2184 1880 GRP130-1.003 theorem 0.0 4 4 71 3 9 0 0 7 2 36 316 123 GRP130-1.005 non_thm 0.1 4 15 393 18 25 0 0 628 2 155 2174 1188 GRP130-2.003 theorem 0.0 4 3 68 2 14 0 0 6 2 43 282 104 GRP130-2.005 non_thm 0.1 4 3 248 4 39 0 0 484 2 183 1296 688 GRP130-3.003 theorem 0.0 4 2 94 1 19 0 0 2 2 68 289 108 GRP130-3.004 non_thm 0.0 4 2 202 2 31 0 0 232 2 139 826 334 GRP130-4.003 theorem 0.0 4 4 43 3 9 0 0 15 2 25 177 143 GRP130-4.004 non_thm 0.0 4 5 120 6 16 0 0 500 2 84 911 650 GRP131-1.002 theorem 0.0 4 2 20 1 4 0 0 0 2 14 81 32 GRP131-1.005 non_thm 0.1 4 0 147 8 25 0 0 484 2 155 1575 525 GRP131-2.002 theorem 0.0 4 2 22 1 6 0 0 0 2 16 84 32 GRP131-2.005 non_thm 0.8 4 80 1612 88 39 0 0 2453 2 183 16728 7868 GRP132-1.002 theorem 0.0 4 2 20 1 4 0 0 0 2 14 81 32 GRP132-1.005 non_thm 0.1 4 0 147 8 25 0 0 484 2 155 1575 525 GRP132-2.002 theorem 0.0 4 2 22 1 6 0 0 0 2 16 84 32 GRP132-2.005 non_thm 1.2 4 92 2522 99 39 0 0 1994 2 183 29511 12989 GRP133-1.003 theorem 0.0 4 4 80 3 9 0 0 7 2 33 340 139 GRP133-1.004 non_thm 0.0 4 1 87 3 16 0 0 186 2 84 530 211 GRP133-2.003 theorem 0.0 4 3 69 2 14 0 0 6 2 43 251 97 GRP133-2.004 non_thm 0.0 4 2 121 5 25 0 0 186 2 102 613 250 GRP134-1.003 theorem 0.0 4 4 92 3 9 0 0 7 2 34 434 169 GRP134-1.005 non_thm 0.1 4 6 219 10 25 0 0 471 2 155 1724 855 GRP134-2.003 theorem 0.0 4 3 86 2 14 0 0 6 2 44 352 127 GRP134-2.005 non_thm 0.1 4 6 456 11 39 0 0 640 2 183 3295 1717 GRP135-1.002 theorem 0.0 4 2 19 1 4 0 0 0 2 14 61 25 GRP135-1.005 non_thm 0.5 4 60 1853 64 25 0 0 2405 2 155 12748 6877 GRP135-2.002 theorem 0.0 4 2 21 1 6 0 0 0 2 16 63 25 GRP135-2.005 non_thm 0.2 4 20 828 21 39 0 0 1088 2 183 5153 2994 HWV003-3 theorem 0.0 4 8 105 7 353 218 0 62 2 22 131 92 HWV005-1 theorem 0.0 4 1 96 0 10 0 0 0 3 96 323 0 HWV005-2 theorem 0.0 4 1 96 0 8 0 0 0 3 96 296 0 HWV006-1 theorem 0.1 4 1 356 0 15 1 4 0 4 356 1440 0 HWV006-2 theorem 0.1 4 1 360 0 13 1 0 0 4 360 1354 0 HWV007-1 theorem 0.1 4 1 352 0 13 1 6 0 4 352 941 0 HWV007-2 theorem 0.1 4 1 364 0 11 1 0 0 4 364 898 0 HWV008-1.001 theorem 0.1 4 1 215 0 11 0 0 0 5 215 653 0 HWV008-1.002 theorem 0.1 4 1 324 0 14 0 0 0 5 324 934 0 HWV008-2.001 theorem 0.1 4 1 215 0 9 0 0 0 5 215 601 0 HWV008-2.002 theorem 0.1 4 1 326 0 12 0 0 0 5 326 866 0 HWV034-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 HWV034-2 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 HWV035-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 HWV035-2 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 HWV036-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 HWV036-2 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 KRS001-1 theorem 0.0 4 1 8 0 1 0 0 0 2 8 16 2 KRS002-1 theorem 0.0 4 1 9 0 1 0 0 0 3 9 16 2 KRS003-1 theorem 0.0 4 1 9 0 2 0 0 0 2 9 16 2 KRS005-1 non_thm 0.0 4 0 8 0 1 0 0 36 2 8 8 36 KRS006-1 non_thm 0.0 4 0 20 3 5 0 0 68 3 23 31 71 KRS007-1 non_thm 0.0 4 0 27 2 2 0 0 83 3 29 37 85 KRS008-1 non_thm 0.1 4 0 42 34 2 0 0 772 3 76 72 810 KRS009-1 non_thm 0.0 4 0 31 26 1 0 0 163 2 33 71 177 KRS010-1 theorem 0.0 4 2 21 1 2 0 0 77 2 18 38 95 KRS011-1 non_thm 0.0 4 0 36 3 2 0 0 46 2 39 44 49 KRS012-1 theorem 0.0 4 1 5 0 2 0 0 0 2 5 10 3 KRS013-1 theorem 0.0 4 1 17 0 2 0 0 0 3 17 27 7 KRS014-1 non_thm 0.0 4 0 14 2 1 0 0 30 2 16 17 32 KRS015-1 theorem 0.0 4 1 10 0 1 0 0 0 3 10 18 2 KRS016-1 non_thm 0.0 4 0 4 4 2 0 0 10 2 8 4 14 KRS017-1 theorem 0.0 4 1 3 0 2 0 0 0 2 3 7 0 LCL181-2 theorem 0.0 4 1 2 0 3 2 0 0 2 2 4 1 LCL230-2 theorem 0.0 4 1 3 0 3 3 0 0 2 3 6 0 MGT004-1 theorem 0.0 4 1 15 0 9 0 0 0 2 15 26 0 MGT007-1 theorem 0.0 4 1 17 0 9 0 0 0 2 17 28 0 MGT016-1 theorem 0.0 4 1 16 0 13 0 0 0 2 16 26 0 MGT018-1 theorem 0.0 4 1 16 0 13 0 0 0 2 16 26 0 MGT022-1 theorem 0.0 4 2 8 1 11 3 0 0 3 7 19 6 MGT022-2 theorem 0.0 4 2 8 1 11 3 0 0 3 7 19 6 MGT028-1 theorem 0.0 4 2 13 1 2 0 0 1 4 11 27 15 MGT030-1 theorem 0.0 4 6 23 8 2 0 0 4 4 14 80 45 MGT036-1 theorem 0.0 4 1 9 0 4 0 0 0 2 9 15 0 MGT036-2 theorem 0.0 4 1 9 0 4 0 0 0 2 9 16 0 MGT041-2 theorem 0.0 4 1 7 0 4 0 0 0 2 7 9 0 MSC001-1 theorem 0.0 4 1 65 0 5 1 2 0 5 65 330 0 MSC002-1 theorem 0.0 4 1 22 0 3 1 0 0 4 22 49 0 MSC002-2 theorem 0.0 4 1 22 0 3 1 0 0 4 22 49 0 MSC003-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 9 0 MSC004-1 theorem 0.0 4 6 20 11 2 0 0 4 3 14 38 49 MSC006-1 theorem 0.0 4 6 47 22 2 0 0 228 2 30 193 537 MSC007-1.008 theorem 4.2 15 5040 55182 5039 282303 78952 0 2779 2 56 105582 27398 MSC008-1.002 theorem 0.2 4 32 155 53 2 0 0 2806 2 23 1364 9005 MSC008-1.010 timeout 299.0 153 MSC008-2.002 theorem 0.2 4 32 155 53 2 0 0 3238 2 23 1188 7397 MSC009-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 NLP026-1 non_thm 0.0 4 0 4 5 10 3 0 4 2 9 4 9 NLP027-1 non_thm 0.0 4 0 14 12 12 4 0 100 2 23 26 112 NLP028-1 non_thm 0.0 4 0 15 13 13 4 0 101 2 25 29 115 NLP029-1 non_thm 0.0 4 0 4 5 11 4 0 4 2 9 4 9 NLP030-1 non_thm 0.0 4 0 5 6 12 4 0 5 2 11 5 11 NLP031-1 non_thm 0.0 4 8 127 41 26 5 3 204 2 44 318 530 NLP032-1 timeout 299.0 35 NLP033-1 non_thm 0.1 4 5 38 77 18 4 0 568 2 41 109 802 NLP034-1 non_thm 0.1 4 6 74 63 23 4 2 617 2 53 208 916 NLP035-1 non_thm 0.1 4 6 111 115 23 4 13 1243 2 59 361 1545 NLP043-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 NLP044-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 NLP045-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 NLP046-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 NLP047-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 NLP048-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 NLP059-1 non_thm 0.0 4 0 10 4 13 3 0 24 2 14 10 28 NLP060-1 non_thm 0.0 4 0 9 5 13 3 1 24 2 14 11 29 NLP061-1 non_thm 0.0 4 0 10 4 13 3 0 24 2 14 10 28 NLP062-1 non_thm 0.0 4 0 10 4 13 3 0 22 2 14 10 26 NLP063-1 non_thm 0.0 4 0 10 5 13 3 3 33 2 15 10 38 NLP064-1 non_thm 0.0 4 0 10 5 13 3 3 31 2 15 10 36 NLP065-1 non_thm 0.0 4 0 10 5 13 3 3 32 2 15 10 37 NLP066-1 non_thm 0.0 4 0 12 4 12 3 0 26 2 16 12 30 NLP067-1 non_thm 0.0 4 0 10 4 13 3 0 24 2 14 10 28 NLP068-1 non_thm 0.0 4 0 5 3 12 3 0 12 2 8 5 15 NLP079-1 theorem 0.0 4 2 40 1 76 4 0 0 2 22 82 54 NLP080-1 theorem 0.0 4 2 40 1 76 4 0 0 2 22 80 54 NLP081-1 theorem 0.0 4 2 38 1 72 4 0 0 2 21 76 51 NLP094-1 theorem 0.0 4 2 41 1 64 4 0 0 2 23 52 46 NLP095-1 non_thm 0.0 4 0 2 1 20 3 0 6 2 3 2 7 NLP096-1 non_thm 0.0 4 0 2 1 20 3 0 6 2 3 2 7 NLP097-1 non_thm 0.0 4 0 2 1 21 2 0 7 2 3 2 8 NLP098-1 non_thm 0.0 4 0 2 1 21 2 0 7 2 3 2 8 NLP099-1 non_thm 0.0 4 0 3 1 22 3 0 2 2 4 3 3 NLP100-1 non_thm 0.0 4 0 2 1 21 3 0 14 2 3 2 15 NLP101-1 non_thm 0.0 4 0 2 1 21 3 0 14 2 3 2 15 NLP102-1 non_thm 0.0 4 0 3 1 22 4 0 9 2 4 3 10 NLP103-1 non_thm 0.0 4 0 4 1 22 4 0 10 2 5 4 11 NLP114-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 NLP115-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 NLP116-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 NLP117-1 theorem 0.0 4 2 34 1 66 5 0 0 2 19 38 48 NLP118-1 non_thm 0.0 4 1 34 1 67 4 0 32 2 19 36 48 NLP119-1 non_thm 0.0 4 1 34 1 67 4 0 32 2 19 36 48 NLP120-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 NLP121-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 NLP122-1 theorem 0.0 4 2 34 1 66 5 0 0 2 19 38 48 NLP123-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 NLP130-1 non_thm 0.0 4 0 24 4 44 4 0 45 2 28 24 49 NLP131-1 non_thm 0.0 4 0 21 2 44 4 0 38 2 23 21 40 NLP132-1 non_thm 0.0 4 0 21 3 44 4 0 38 2 24 21 41 NLP133-1 non_thm 0.0 4 0 21 3 44 4 0 38 2 24 21 41 NLP134-1 non_thm 0.0 4 0 21 2 44 4 0 37 2 23 21 39 NLP135-1 non_thm 0.0 4 0 24 4 44 4 0 45 2 28 24 49 NLP136-1 non_thm 0.0 4 1 43 2 86 5 0 39 2 25 46 62 NLP137-1 non_thm 0.0 4 4 70 26 88 5 0 143 2 39 98 173 NLP138-1 non_thm 0.0 4 1 43 2 86 5 0 39 2 25 46 62 NLP139-1 non_thm 0.0 4 4 70 26 88 5 0 143 2 39 98 173 NLP160-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP161-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP162-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP163-1 non_thm 0.0 4 1 54 4 108 5 0 49 2 31 57 80 NLP164-1 non_thm 0.0 4 1 54 4 108 5 0 49 2 31 57 80 NLP165-1 non_thm 0.0 4 1 54 4 108 5 0 49 2 31 57 80 NLP166-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP167-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP168-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP169-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 NLP190-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP191-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP192-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP193-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP194-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP195-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP196-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP197-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP198-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP199-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 NLP221-1 non_thm 0.0 4 0 20 1 43 4 0 34 2 21 20 35 NLP222-1 non_thm 0.0 4 0 20 1 43 4 0 34 2 21 20 35 NLP223-1 non_thm 0.0 4 0 19 1 42 4 0 33 2 20 19 34 NLP230-1 non_thm 0.0 4 1 78 1 159 5 0 72 2 43 83 113 NLP231-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 NLP232-1 non_thm 0.0 4 0 38 1 79 4 0 70 2 39 38 71 NLP233-1 non_thm 0.0 4 0 39 1 78 4 0 70 2 40 39 71 NLP234-1 non_thm 0.0 4 0 38 1 79 4 0 70 2 39 38 71 NLP235-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 NLP236-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 NLP237-1 non_thm 0.0 4 0 38 1 79 4 0 70 2 39 38 71 NLP238-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 NLP239-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 NUM014-1 theorem 0.0 4 1 5 0 4 0 0 0 2 5 12 0 NUM015-1 theorem 0.0 4 1 11 0 2 0 0 0 3 11 21 3 NUM016-1 theorem 0.0 4 1 14 0 4 0 0 0 3 14 38 3 NUM016-2 theorem 0.0 4 1 12 0 2 0 0 0 3 12 19 3 NUM021-1 theorem 0.0 4 1 36 0 9 0 0 0 3 36 179 0 NUM022-1 theorem 0.0 4 1 8 0 3 0 0 0 3 8 13 0 NUM025-2 theorem 0.0 4 1 4 0 4 0 0 0 2 4 20 1 NUM027-1 theorem 0.0 4 1 49 0 10 0 0 0 2 49 376 1 NUM285-1 non_thm 0.0 4 0 16 5 67 44 0 10 2 21 16 15 NUM288-1 timeout 299.0 9 PLA002-1 theorem 0.0 4 1 7 0 12 8 0 0 2 7 12 1 PLA002-2 theorem 1.6 6 1 1994 0 2 0 0 0 5 1994 5750 0 PUZ001-1 theorem 0.0 4 1 17 0 5 2 0 0 2 17 20 1 PUZ001-3 non_thm 0.0 4 0 19 0 6 2 0 9 2 19 22 9 PUZ002-1 theorem 0.0 4 1 11 0 2 0 0 0 2 11 13 1 PUZ004-1 theorem 0.0 4 1 10 0 11 11 0 0 2 10 12 1 PUZ005-1 theorem 0.0 4 2 26 1 3 0 0 0 2 21 91 165 PUZ009-1 theorem 0.0 4 1 5 0 15 11 0 0 2 5 11 4 PUZ010-1 theorem 1.3 4 344 6918 359 576 446 0 9902 2 204 20149 27734 PUZ012-1 theorem 0.0 4 1 20 0 13 1 0 0 2 20 36 2 PUZ013-1 theorem 0.0 4 1 7 0 14 10 0 0 2 7 12 6 PUZ014-1 theorem 0.0 4 2 16 1 26 22 0 5 2 13 22 12 PUZ015-2.006 theorem 0.2 4 139 2414 148 10158 5318 0 1063 2 59 3244 1829 PUZ016-2.004 non_thm 0.0 4 0 22 2 75 39 0 24 2 24 24 28 PUZ016-2.005 theorem 0.0 4 31 418 30 1745 919 0 84 2 40 553 319 PUZ017-1 theorem 0.1 4 5 302 4 85 1 5 723 2 231 1159 1598 PUZ018-1 theorem 0.0 4 1 53 0 41 6 0 0 2 53 84 2 PUZ018-2 non_thm 0.1 4 0 89 19 40 6 0 1428 2 108 150 1519 PUZ019-1 theorem 0.0 4 1 116 0 44 1 3 0 2 116 333 3 PUZ021-1 theorem 0.1 4 13 195 66 0 0 6 354 3 55 1068 4073 PUZ023-1 theorem 0.0 4 2 10 2 10 6 0 4 2 11 51 16 PUZ024-1 theorem 0.0 4 1 7 0 13 7 0 0 2 7 21 1 PUZ025-1 theorem 0.0 4 8 37 9 7 4 0 46 2 22 299 180 PUZ026-1 theorem 0.0 4 3 29 2 18 5 3 10 2 18 159 61 PUZ027-1 theorem 0.0 4 3 18 2 27 14 0 1 2 12 102 40 PUZ028-1 non_thm 0.0 4 0 31 15 11 0 0 20 2 46 91 35 PUZ028-2 non_thm 0.0 4 0 70 18 36 0 0 28 2 88 190 46 PUZ028-3 non_thm 0.0 4 0 70 18 432 154 0 24 2 88 114 42 PUZ028-4 non_thm 0.0 4 0 28 18 222 106 0 24 2 46 60 42 PUZ028-5 theorem 0.1 4 30 742 29 11 0 0 173 2 90 1674 246 PUZ028-6 theorem 0.1 4 20 376 19 36 0 0 137 2 82 1298 292 PUZ029-1 theorem 0.0 4 1 13 0 4 0 0 0 2 13 17 2 PUZ030-1 theorem 0.0 4 24 327 24 509 397 0 130 2 28 875 982 PUZ030-2 theorem 0.0 4 9 35 8 429 173 0 7 2 10 94 89 PUZ031-1 theorem 0.0 4 1 33 0 6 0 0 0 2 33 56 0 PUZ032-1 theorem 0.0 4 2 12 1 4 0 0 4 2 11 68 14 PUZ033-1 theorem 0.0 4 1 11 0 12 17 0 0 2 11 15 0 PUZ034-1.003 timeout 299.0 103 PUZ034-1.004 timeout 299.0 101 PUZ035-1 theorem 0.0 4 4 15 3 21 17 0 2 2 8 40 14 PUZ035-2 theorem 0.0 4 4 21 3 21 17 0 2 2 10 52 24 PUZ035-3 theorem 0.0 4 4 12 3 6 8 0 3 2 8 61 11 PUZ035-4 theorem 0.0 4 4 12 3 6 8 0 3 2 8 61 11 PUZ035-5 theorem 0.0 4 4 7 4 5 0 0 0 2 6 48 34 PUZ035-6 theorem 0.0 4 4 5 4 5 0 0 5 2 6 44 63 PUZ035-7 theorem 0.1 4 13 217 23 8 0 0 389 3 73 1081 2429 PUZ044-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 PUZ045-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 SET001-1 theorem 0.0 4 1 4 0 3 0 0 0 2 4 8 1 SET002-1 theorem 0.0 4 3 9 3 2 0 0 0 2 8 21 22 SET003-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 9 2 SET004-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 8 2 SET005-1 theorem 0.0 4 2 135 1 4 0 0 0 2 131 378 143 SET006-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 10 3 SET007-1 theorem 0.1 4 3 578 2 5 0 38 0 2 339 2353 722 SET008-1 theorem 0.0 4 1 10 0 3 0 0 0 2 10 34 4 SET009-1 theorem 0.0 4 1 22 0 4 0 0 0 2 22 41 2 SET010-1 theorem 0.1 4 3 835 2 5 0 61 0 2 486 3402 997 SET011-1 theorem 0.0 4 2 73 1 3 0 0 0 2 67 239 94 SET012-1 timeout 299.0 76 SET012-2 theorem 0.1 4 3 131 2 6 0 0 521 2 102 1995 1221 SET013-1 timeout 299.0 80 SET013-2 theorem 0.3 4 3 609 2 6 0 0 521 2 336 7871 3466 SET014-2 theorem 183.8 27 1 294 0 6 0 0 0 3 294 12417 2 SET015-1 timeout 299.0 70 SET015-2 theorem 0.2 4 3 381 2 6 0 0 521 2 222 5095 2332 SET043-5 theorem 0.0 4 4 0 3 0 0 0 0 2 2 8 9 SET044-5 theorem 0.0 4 8 8 13 0 0 0 25 2 6 40 100 SET045-5 theorem 0.0 4 6 2 6 1 0 0 8 2 6 16 39 SET046-5 theorem 0.0 4 4 4 3 0 0 0 0 2 4 18 19 SET047-5 theorem 0.0 4 4 6 3 4 4 0 2 2 4 24 15 SET055-6 theorem 228.1 51 51 17443 108 30 0 204 275213 2 5353 1496683 1124979 SET055-7 theorem 0.0 4 1 5 0 5 0 0 0 2 5 48 3 SET777-1 non_thm 0.0 4 0 0 2 0 0 0 2 2 2 0 4 SET778-1 non_thm 0.0 4 0 0 3 0 0 0 2 2 3 0 5 SET779-1 non_thm 0.0 4 0 0 3 0 0 0 3 2 3 0 6 SET780-1 non_thm 0.0 4 0 0 3 0 0 0 2 2 3 0 5 SET781-1 timeout 299.0 35 SET786-1 theorem 0.0 4 4 4 3 0 0 0 0 2 4 16 18 SWV001-1 theorem 0.0 4 2 10 1 2 0 0 5 2 9 39 21 SWV009-1 theorem 0.0 4 1 9 0 5 0 0 0 2 9 12 1 SYN001-1.005 theorem 0.0 4 16 16 15 608 118 0 0 2 5 96 31 SYN002-1.007.008 theorem 0.1 4 2 0 37 0 0 0 325 23 22 0 408 SYN006-1 theorem 0.0 4 1 6 0 4 1 0 0 2 6 9 0 SYN008-1 theorem 0.0 4 1 3 0 3 4 0 0 2 3 6 0 SYN009-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 18 0 SYN009-2 theorem 0.0 4 1 7 0 4 0 0 0 2 7 9 0 SYN009-3 theorem 0.0 4 1 9 0 5 1 0 0 2 9 11 0 SYN009-4 theorem 0.0 4 1 8 0 4 0 0 0 2 8 10 0 SYN011-1 theorem 0.0 4 2 9 1 12 13 0 0 2 7 13 9 SYN012-1 theorem 0.0 4 9 0 37 0 0 0 136 5 16 0 209 SYN014-2 theorem 0.0 4 1 8 0 7 0 0 0 2 8 36 2 SYN015-2 theorem 0.0 4 1 33 0 7 0 0 0 2 33 153 2 SYN028-1 theorem 0.0 4 1 5 0 5 7 0 0 2 5 7 1 SYN029-1 theorem 0.0 4 2 3 1 7 7 0 0 2 3 7 3 SYN030-1 theorem 0.0 4 2 5 1 13 11 0 0 2 5 10 6 SYN031-1 theorem 0.0 4 3 5 2 0 0 0 0 2 4 19 20 SYN032-1 theorem 0.0 4 3 7 2 14 14 0 0 2 5 13 9 SYN034-1 theorem 0.0 4 4 4 3 0 0 0 0 2 4 16 18 SYN036-1 theorem 6.6 11 46 118 45 2320 350 3 51805 2 18 206224 352011 SYN036-2 non_thm 0.0 4 0 0 1 124 44 0 0 2 1 0 1 SYN036-3 theorem 0.0 4 10 67 9 220 142 5 29 2 17 113 77 SYN036-4 theorem 0.0 4 8 9 7 199 98 6 0 2 5 65 57 SYN037-1 theorem 0.0 4 9 71 8 232 166 11 19 2 17 114 78 SYN037-2 theorem 0.0 4 12 22 15 171 87 8 27 2 11 82 76 SYN038-1 theorem 0.0 4 9 0 37 0 0 0 136 5 16 0 209 SYN039-1 theorem 0.0 4 7 4 17 18 0 0 129 4 11 22 247 SYN044-1 theorem 0.0 4 2 4 1 10 9 0 0 2 3 8 4 SYN045-1 theorem 0.0 4 1 3 0 3 3 0 0 2 3 5 2 SYN047-1 theorem 0.0 4 1 4 0 4 6 0 0 2 4 7 0 SYN051-1 theorem 0.0 4 2 3 1 6 6 1 0 2 3 7 4 SYN052-1 theorem 0.0 4 2 2 1 6 5 0 0 2 2 7 3 SYN053-1 theorem 0.0 4 2 1 1 4 4 0 0 2 2 8 6 SYN054-1 theorem 0.0 4 2 5 1 2 1 0 0 2 4 9 6 SYN055-1 theorem 0.0 4 1 9 0 3 0 0 0 2 9 12 0 SYN056-1 non_thm 0.0 4 0 2 2 8 0 0 2 2 4 2 4 SYN059-1 non_thm 0.0 4 0 5 7 30 11 0 88 2 12 24 95 SYN060-1 theorem 0.0 4 1 3 0 1 0 0 0 2 3 5 4 SYN061-1 theorem 0.0 4 1 5 0 2 0 0 0 2 5 7 1 SYN063-1 theorem 0.0 4 1 2 0 2 5 0 0 2 2 6 0 SYN066-1 theorem 0.0 4 1 4 0 4 2 0 0 2 4 7 1 SYN067-1 theorem 16.6 4 375 3049 399 7438 853 0 85708 2 41 16089 409302 SYN067-2 theorem 47.4 6 997 8803 1028 11294 1841 0 277148 2 52 55000 1171942 SYN067-3 theorem 4.2 4 278 3043 317 1563 483 0 56556 2 42 11283 205082 SYN069-1 theorem 0.0 4 1 9 0 1 0 0 0 2 9 16 0 SYN070-1 theorem 0.0 4 1 15 0 4 0 0 0 2 15 43 0 SYN081-1 theorem 0.0 4 2 0 4 0 0 0 4 3 3 0 12 SYN082-1 theorem 0.0 4 3 3 2 9 5 0 0 2 3 18 11 SYN084-1 non_thm 0.0 4 0 1 1 13 14 1 0 2 2 1 1 SYN084-2 theorem 0.0 4 4 17 4 17 19 0 6 3 9 39 56 SYN091-1.003 non_thm 0.0 4 0 2 4 12 6 0 2 2 6 2 6 SYN092-1.003 non_thm 0.0 4 0 0 9 33 7 0 6 2 9 0 15 SYN093-1.002 theorem 0.0 4 2 10 1 20 15 0 0 2 8 16 8 SYN094-1.005 theorem 10.2 36 16384 75927 26775 203333 143799 0 67723 2 45 141463 127670 SYN097-1.002 theorem 0.0 4 2 14 1 26 20 0 0 2 12 20 10 SYN098-1.002 theorem 0.0 4 32 264 127 638 472 0 235 2 31 392 449 SYN099-1.003 theorem 0.0 4 1 16 0 14 2 0 0 2 16 35 0 SYN100-1.005 theorem 0.0 4 1 42 0 8 0 0 0 2 42 83 1 SYN304-1 non_thm 0.0 4 0 6 1 6 0 0 3 2 7 9 4 SYN306-1 timeout 298.9 5 SYN307-1 non_thm 0.0 4 0 2 1 2 0 0 5 2 3 4 6 SYN308-1 non_thm 0.0 4 0 1 2 2 0 0 0 3 3 1 2 SYN309-1 non_thm 0.0 4 0 2 2 5 0 0 0 2 4 2 2 SYN313-1.001.002 theorem 43.3 5 951 4505 2066 0 0 4 10031 29 58 5619 26413 SYN314-1.002.001 timeout 299.0 127 SYN315-1 theorem 0.0 4 2 2 1 5 3 0 0 2 2 7 3 SYN316-1 timeout 298.9 4 SYN317-1 non_thm 0.0 4 0 2 0 3 3 0 0 2 2 2 0 SYN319-1 theorem 0.0 4 1 3 0 3 1 0 0 2 3 6 1 SYN320-1 non_thm 0.0 4 0 2 1 2 0 0 0 2 3 2 1 SYN321-1 theorem 0.0 4 2 2 1 4 3 0 0 2 2 7 3 SYN323-1 theorem 0.0 4 3 2 3 0 0 0 0 2 3 6 7 SYN324-1 timeout 299.0 4 SYN325-1 theorem 0.0 4 1 2 0 1 1 0 0 2 2 4 2 SYN326-1 theorem 0.0 4 1 4 0 3 3 0 0 2 4 8 3 SYN327-1 theorem 0.0 4 4 4 3 0 0 0 0 2 4 24 27 SYN328-1 theorem 0.1 4 18 0 74 0 0 0 458 6 17 0 650 SYN330-1 timeout 299.0 46 SYN331-1 theorem 0.0 4 1 6 0 4 0 0 0 3 6 16 1 SYN332-1 theorem 0.8 4 3 0 98 0 0 0 2670 5 96 0 3049 SYN334-1 theorem 0.0 4 9 0 37 0 0 0 136 5 16 0 209 SYN335-1 timeout 299.0 198 SYN343-1 theorem 0.0 4 2 1 1 4 2 0 0 2 2 5 2 SYN344-1 non_thm 0.0 4 0 0 2 2 0 0 0 2 2 0 2 SYN345-1 theorem 0.0 4 4 6 3 28 14 0 0 2 4 19 12 SYN347-1 theorem 0.0 4 12 10 14 8 4 0 23 2 8 64 82 SYN348-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 SYN349-1 theorem 0.0 4 17 0 29 0 0 0 135 3 9 0 373 SYN350-1 theorem 0.0 4 8 6 9 0 0 0 34 3 8 36 108 SYN351-1 non_thm 0.6 4 7 271 234 1 0 0 2073 5 114 609 2400 SYN352-1 theorem 0.0 4 4 5 7 1 0 0 48 3 11 9 133 SYN353-1 timeout 299.0 119 SYN354-1 theorem 0.0 4 3 2 2 2 0 0 0 2 4 15 6 SYN418-1 non_thm 0.1 4 0 59 57 407 95 0 231 2 116 60 291 SYN419-1 non_thm 0.0 4 0 49 45 369 103 0 163 2 94 50 211 SYN420-1 non_thm 0.1 4 1 80 106 531 136 0 1042 2 184 103 1172 SYN421-1 non_thm 0.1 4 0 45 61 456 97 0 213 2 106 47 274 SYN422-1 non_thm 0.1 4 0 47 63 378 107 0 227 2 110 50 290 SYN423-1 non_thm 0.1 4 0 140 83 494 132 0 379 2 223 143 463 SYN424-1 non_thm 0.1 4 0 115 114 662 149 0 728 2 229 120 854 SYN425-1 non_thm 0.1 4 0 140 97 398 124 0 965 2 237 147 1073 SYN426-1 non_thm 0.2 4 1 136 157 691 203 0 878 2 292 146 1048 SYN427-1 non_thm 0.1 4 0 165 90 530 151 0 1231 2 255 172 1321 SYN428-1 non_thm 0.6 4 2 222 252 566 176 0 11692 2 447 290 12210 SYN429-1 non_thm 0.1 4 1 107 55 667 147 0 246 2 161 137 318 SYN430-1 non_thm 0.0 4 0 36 11 71 15 0 165 2 47 40 176 SYN431-1 non_thm 0.0 4 1 45 13 89 19 0 170 2 55 47 196 SYN432-1 non_thm 0.0 4 0 54 16 101 21 0 459 2 70 54 491 SYN433-1 non_thm 0.6 4 2 58 19 97 26 0 29975 2 62 137 34703 SYN434-1 non_thm 4.5 9 3 125 30 199 43 0 148785 2 146 889 170063 SYN435-1 non_thm 0.2 4 0 91 27 175 32 0 2182 2 118 159 2209 SYN436-1 theorem 8.2 5 155 2423 170 3211 966 0 242967 2 82 7677 782479 SYN437-1 non_thm 0.7 4 18 291 39 418 109 0 22669 2 91 1948 47429 SYN438-1 non_thm 0.6 4 20 174 31 348 100 0 26078 2 55 946 41517 SYN439-1 theorem 4.3 5 268 5487 299 6404 2033 0 24038 2 92 14706 247325 SYN440-1 theorem 246.2 15 1470 19600 1966 24176 7221 0 5971066 2 126 41714112282455 SYN441-1 non_thm 6.7 4 64 1253 92 1459 420 0 126720 2 136 10580 294666 SYN442-1 theorem 17.9 6 173 2966 208 4720 1172 0 604960 2 100 11714 1206041 SYN443-1 theorem 1.7 4 65 1031 65 1909 487 0 24113 2 78 3166 168269 SYN444-1 theorem 0.8 4 74 1039 78 1725 444 0 10143 2 77 4533 57454 SYN445-1 theorem 3.5 4 49 958 54 1513 378 0 95936 2 93 3373 288649 SYN446-1 non_thm 0.6 4 13 261 22 459 110 0 14622 2 83 1381 37841 SYN447-1 theorem 65.3 23 354 7741 423 9283 3032 0 867115 2 130 27326 5669521 SYN448-1 theorem 4.4 5 179 2699 201 4693 1248 0 54688 2 88 8162 353093 SYN449-1 non_thm 5.0 4 199 3030 220 5002 1339 0 70244 2 89 12938 322102 SYN450-1 theorem 0.5 4 54 688 56 1265 328 0 7491 2 72 2246 28302 SYN451-1 theorem 0.8 4 58 758 69 1394 363 0 14777 2 61 2519 49292 SYN452-1 theorem 1.3 4 78 906 90 1623 412 0 26268 2 81 3108 81217 SYN453-1 non_thm 5.4 10 58 1502 83 1747 482 0 101075 2 156 7041 184027 SYN454-1 theorem 1.5 4 65 1044 69 1903 452 0 21906 2 69 3401 113545 SYN455-1 theorem 12.0 4 126 1969 194 3353 888 0 459156 2 96 8900 825538 SYN456-1 non_thm 6.6 5 225 2444 264 4412 1200 0 216245 2 77 12369 450415 SYN457-1 theorem 184.3 19 999 21446 1481 23793 6817 0 4562905 2 156 203897 6609426 SYN458-1 theorem 1.0 4 36 759 37 1271 317 0 4495 2 85 2118 83408 SYN459-1 theorem 1.8 4 80 1222 85 2211 548 0 32743 2 74 4534 181353 SYN460-1 theorem 3.6 4 115 2424 132 3214 917 0 10867 2 84 8861 312766 SYN461-1 theorem 0.8 4 77 900 81 1716 468 0 12279 2 58 3040 56095 SYN462-1 theorem 1.7 4 60 946 66 1637 423 0 44025 2 67 3846 153293 SYN463-1 non_thm 0.2 4 3 75 14 169 37 0 5746 2 80 154 8067 SYN464-1 non_thm 18.4 7 69 1329 124 1757 501 0 590908 2 133 11574 1250174 SYN465-1 theorem 1.5 4 67 1108 71 1958 462 0 19112 2 70 4436 100623 SYN466-1 theorem 1.5 4 80 1220 87 2187 536 0 25230 2 85 5683 88129 SYN467-1 theorem 0.6 4 40 657 41 1128 295 0 6204 2 60 2414 46843 SYN468-1 theorem 1.5 4 98 1531 109 2911 726 0 11778 2 101 6370 90582 SYN469-1 theorem 3.1 4 137 2149 148 3986 950 0 54235 2 64 7564 300711 SYN470-1 theorem 3.5 4 138 2632 145 4358 1051 0 26585 2 95 8910 242356 SYN471-1 theorem 4.1 4 53 610 55 1208 298 0 175300 2 80 3711 323880 SYN472-1 theorem 4.4 4 136 1770 148 3201 829 0 105259 2 66 9420 414112 SYN473-1 theorem 2.5 4 89 1394 92 2407 634 0 26700 2 76 6183 247403 SYN474-1 theorem 3.4 4 139 2238 143 4011 1050 0 40656 2 72 8227 298411 SYN475-1 theorem 2.5 4 67 1051 71 1960 506 0 57714 2 65 3827 255975 SYN476-1 theorem 1.6 4 123 1982 131 3529 919 0 10959 2 84 7110 83103 SYN477-1 theorem 1.0 4 57 624 63 1256 333 0 22276 2 55 2793 92723 SYN478-1 theorem 3.5 5 127 1952 142 4032 968 0 46296 2 64 6399 285933 SYN479-1 theorem 1.0 4 40 588 43 1166 324 0 12984 2 79 2213 115338 SYN480-1 theorem 1.7 4 73 999 76 1935 492 0 34929 2 62 3866 141294 SYN481-1 theorem 3.3 4 119 1665 127 3325 805 0 60934 2 71 6479 311796 SYN482-1 theorem 1.6 4 90 1200 99 2147 578 0 27509 2 74 6693 71566 SYN483-1 theorem 1.1 4 62 1091 62 2169 520 0 8410 2 66 3550 76206 SYN484-1 theorem 0.6 4 32 507 32 965 228 0 6375 2 54 1873 63539 SYN485-1 theorem 1.3 4 41 717 40 1429 326 0 22086 2 81 2404 116507 SYN486-1 theorem 1.1 4 76 1035 75 2153 525 0 13495 2 58 4195 115142 SYN487-1 theorem 4.1 4 136 2429 157 4668 1108 0 71747 2 101 9894 196619 SYN488-1 theorem 5.5 5 167 2914 185 5455 1290 0 74054 2 82 11914 358354 SYN489-1 theorem 0.7 4 42 942 44 1648 406 0 2850 2 76 2937 33727 SYN490-1 non_thm 0.0 4 0 13 4 30 6 0 14 2 17 13 18 SYN491-1 non_thm 0.0 4 0 10 3 21 7 0 17 2 13 10 20 SYN492-1 non_thm 0.0 4 0 7 2 21 6 0 7 2 9 7 9 SYN493-1 non_thm 0.0 4 0 10 3 23 7 0 8 2 13 10 11 SYN494-1 non_thm 0.0 4 0 7 2 20 5 0 12 2 9 7 14 SYN495-1 non_thm 0.0 4 0 25 8 49 10 0 25 2 33 25 33 SYN496-1 non_thm 0.0 4 0 7 2 19 6 0 4 2 9 7 6 SYN497-1 non_thm 0.0 4 0 13 4 30 6 0 11 2 17 13 15 SYN498-1 theorem 2.6 5 85 1353 92 2751 658 0 41153 2 76 4938 256428 SYN499-1 theorem 5.7 4 83 1209 90 2382 582 0 157129 2 85 9465 434234 SYN500-1 theorem 1.7 4 73 985 74 1731 468 0 20216 2 62 4348 189946 SYN501-1 theorem 0.7 4 25 390 24 831 184 0 7592 2 63 1473 61962 SYN502-1 theorem 4.7 5 111 2466 117 4509 979 0 45224 2 79 10862 407213 SYN503-1 theorem 0.8 4 56 664 60 1348 358 0 14286 2 66 3374 57289 SYN504-1 theorem 1.7 4 33 422 48 845 219 0 40410 2 75 3037 134377 SYN505-1 theorem 0.8 4 80 920 86 1979 537 0 17476 2 72 3030 66506 SYN506-1 theorem 0.4 4 17 406 18 802 173 0 1967 2 69 1289 19104 SYN507-1 theorem 2.6 4 80 1371 80 2673 603 0 53797 2 89 4775 187253 SYN508-1 theorem 5.6 4 120 1447 128 3053 768 0 166563 2 84 10321 353972 SYN509-1 theorem 0.6 4 53 665 54 1407 374 0 6400 2 54 2357 42898 SYN510-1 theorem 1.7 4 124 1840 139 3911 867 0 21205 2 77 6315 112841 SYN511-1 theorem 1.0 4 60 803 63 1585 409 0 11862 2 80 4511 35254 SYN512-1 theorem 1.4 4 66 1629 69 3116 684 0 9265 2 86 4021 77044 SYN513-1 non_thm 0.1 4 3 103 79 375 107 0 1712 2 178 165 1892 SYN514-1 non_thm 0.0 4 1 73 36 284 79 0 426 2 107 86 468 SYN515-1 non_thm 0.0 4 0 7 11 54 22 0 24 2 18 7 35 SYN516-1 non_thm 0.0 4 0 0 6 41 12 0 12 2 6 0 18 SYN517-1 non_thm 0.0 4 1 15 7 70 24 0 26 2 18 19 38 SYN518-1 non_thm 0.2 4 0 143 67 395 98 0 2505 2 210 150 2604 SYN519-1 timeout 299.0 160 SYN520-1 timeout 299.0 364 SYN521-1 non_thm 0.0 4 0 16 11 89 16 0 51 2 27 16 62 SYN522-1 non_thm 0.0 4 0 13 17 69 29 0 55 2 30 13 72 SYN523-1 non_thm 0.0 4 0 2 10 33 13 0 15 2 12 2 25 SYN524-1 non_thm 0.0 4 0 10 10 68 25 0 29 2 20 10 39 SYN525-1 non_thm 0.0 4 0 8 14 89 27 0 28 2 22 8 42 SYN526-1 non_thm 0.0 4 0 9 10 64 28 0 25 2 19 9 35 SYN527-1 non_thm 0.0 4 0 12 9 70 24 0 20 2 21 12 29 SYN528-1 non_thm 0.0 4 0 6 14 84 21 0 28 2 20 6 42 SYN529-1 non_thm 0.0 4 0 24 16 121 33 0 82 2 40 24 98 SYN530-1 non_thm 0.0 4 0 7 12 70 20 0 29 2 19 7 41 SYN531-1 non_thm 0.0 4 0 16 18 55 28 0 42 2 34 16 61 SYN532-1 non_thm 0.0 4 0 20 11 88 34 0 45 2 31 20 56 SYN533-1 non_thm 0.0 4 0 13 12 93 20 0 32 2 25 13 44 SYN534-1 non_thm 0.0 4 0 12 10 73 26 0 18 2 22 12 28 SYN535-1 non_thm 0.0 4 0 5 11 87 26 0 24 2 16 5 36 SYN536-1 non_thm 0.0 4 0 15 9 74 25 0 32 2 24 15 41 SYN537-1 non_thm 0.0 4 0 28 11 84 36 0 57 2 39 29 68 SYN538-1 non_thm 0.0 4 0 2 13 74 27 0 19 2 15 2 32 SYN539-1 non_thm 0.0 4 0 7 12 77 31 0 30 2 19 7 42 SYN540-1 non_thm 0.0 4 3 27 16 204 60 0 57 2 38 51 87 SYN541-1 non_thm 0.0 4 0 22 21 118 39 0 58 2 43 22 79 SYN542-1 non_thm 5.6 9 0 133 75 214 41 0 195640 2 208 642 196945 SYN543-1 non_thm 6.4 8 0 132 68 210 38 0 203382 2 200 1015 204756 SYN544-1 non_thm 0.1 4 2 140 80 225 85 0 1575 2 216 174 1687 SYN545-1 non_thm 0.1 4 3 63 70 447 105 0 497 2 128 118 630 SYN546-1 non_thm 0.1 4 0 92 78 451 107 0 639 2 170 97 765 SYN547-1 non_thm 0.0 4 1 75 60 491 116 0 225 2 132 91 311 SYN554-1 theorem 0.0 4 1 10 0 4 0 0 0 2 10 51 1 SYN560-1 theorem 1.1 9 1 39 0 6 0 0 0 5 39 2513 1 SYN567-1 theorem 0.0 4 1 8 0 7 0 0 0 2 8 35 0 SYN568-1 theorem 0.0 4 1 8 0 6 0 0 0 2 8 29 1 SYN571-1 theorem 0.0 4 1 23 0 6 0 0 0 3 23 116 1 SYN573-1 theorem 0.0 4 1 8 0 5 0 0 0 2 8 29 0 SYN574-1 theorem 0.0 4 2 18 1 8 0 0 28 3 17 72 46 SYN575-1 theorem 0.0 4 2 18 1 8 0 0 28 3 17 72 46 SYN576-1 theorem 2.4 15 1 118 0 8 0 0 0 4 118 26605 1 SYN578-1 theorem 0.0 4 2 25 1 9 0 0 23 2 20 106 48 SYN579-1 theorem 0.0 4 2 25 1 9 0 0 23 2 20 106 48 SYN580-1 theorem 0.0 4 1 21 0 8 0 0 0 2 21 73 0 SYN581-1 theorem 0.0 4 1 34 0 9 0 0 0 2 34 209 0 SYN582-1 theorem 0.0 4 1 28 0 9 0 0 0 2 28 161 0 SYN583-1 theorem 0.0 4 1 27 0 9 0 0 0 2 27 240 0 SYN585-1 theorem 0.0 4 1 14 0 12 0 0 0 2 14 170 0 SYN586-1 theorem 0.0 4 1 17 0 9 0 0 0 2 17 97 1 SYN587-1 theorem 0.0 4 1 12 0 9 0 0 0 2 12 60 1 SYN591-1 theorem 0.0 4 1 29 0 13 0 0 0 3 29 146 0 SYN592-1 theorem 0.0 4 1 25 0 13 0 0 0 3 25 99 0 SYN593-1 theorem 0.0 4 1 10 0 10 0 0 0 2 10 42 1 SYN594-1 theorem 0.0 4 1 20 0 8 0 0 0 5 20 75 0 SYN595-1 timeout 299.0 174 SYN604-1 theorem 268.1 21 1 441 0 11 0 0 0 6 441 33278 1 SYN605-1 theorem 0.1 4 1 30 0 12 1 0 0 3 30 1252 0 SYN606-1 theorem 0.8 4 1 44 0 12 1 0 0 4 44 2983 0 SYN607-1 theorem 1.1 9 1 68 0 12 1 0 0 4 68 6800 0 SYN608-1 theorem 0.1 4 1 30 0 12 1 0 0 3 30 1250 0 SYN609-1 timeout 299.0 108 SYN610-1 timeout 299.0 102 SYN611-1 timeout 299.0 116 SYN612-1 timeout 299.0 102 SYN613-1 theorem 0.0 4 1 14 0 10 0 0 0 3 14 73 0 SYN619-1 theorem 0.0 4 2 20 1 8 0 0 22 2 20 111 85 SYN620-1 theorem 0.0 4 1 26 0 13 0 0 0 3 26 161 0 SYN621-1 timeout 299.0 117 SYN622-1 theorem 0.0 4 1 27 0 12 0 0 0 3 27 290 0 SYN623-1 theorem 1.6 8 1 513 0 15 0 0 0 4 513 16770 0 SYN624-1 theorem 0.0 4 1 27 0 14 0 0 0 3 27 178 0 SYN625-1 theorem 0.0 4 1 23 0 8 0 0 0 5 23 73 1 SYN626-1 theorem 0.0 4 1 24 0 10 0 0 0 5 24 105 0 SYN627-1 theorem 1.3 10 1 36 0 10 0 0 0 3 36 1047 1 SYN630-1 theorem 0.0 4 1 9 0 9 0 0 0 2 9 43 0 SYN633-1 theorem 0.0 4 1 18 0 9 0 0 0 4 18 97 4 SYN634-1 theorem 0.0 4 1 18 0 9 0 0 0 4 18 97 4 SYN635-1 theorem 0.0 4 1 18 0 9 0 0 0 4 18 97 4 SYN636-1 theorem 0.0 4 1 18 0 9 0 0 0 4 18 97 4 SYN641-1 theorem 1.2 17 1 178 0 15 0 0 0 4 178 17235 0 SYN642-1 theorem 1.2 17 1 170 0 15 0 0 0 4 170 16203 0 SYN643-1 theorem 1.2 17 1 174 0 15 0 0 0 4 174 16463 0 SYN644-1 memory 270.3 400 SYN645-1 timeout 299.0 72 SYN648-1 timeout 299.0 315 SYN650-1 memory 267.2 399 SYN656-1 theorem 0.0 4 1 38 0 18 0 0 0 4 38 130 1 SYN657-1 theorem 0.1 4 1 38 0 20 0 0 0 4 38 327 1 SYN658-1 theorem 0.1 4 1 40 0 20 0 0 0 4 40 334 1 SYN659-1 theorem 0.1 4 1 116 0 22 0 0 0 3 116 1255 0 SYN660-1 theorem 0.2 5 1 91 0 23 0 0 0 3 91 3173 0 SYN661-1 theorem 0.2 5 1 82 0 23 0 0 0 3 82 3141 0 SYN662-1 theorem 0.1 4 1 59 0 23 0 0 0 3 59 1040 0 SYN663-1 theorem 0.1 4 1 50 0 23 0 0 0 3 50 1010 0 SYN664-1 theorem 0.2 5 1 91 0 23 0 0 0 3 91 3173 0 SYN665-1 theorem 0.2 5 1 82 0 23 0 0 0 3 82 3141 0 SYN666-1 theorem 0.1 4 1 61 0 23 0 0 0 3 61 1124 0 SYN667-1 theorem 0.1 4 1 56 0 23 0 0 0 3 56 1110 0 SYN668-1 theorem 0.1 4 1 61 0 23 0 0 0 3 61 1124 0 SYN669-1 theorem 0.1 4 1 56 0 23 0 0 0 3 56 1110 0 SYN670-1 theorem 0.0 4 1 33 0 23 0 0 0 3 33 129 0 SYN671-1 theorem 0.0 4 1 28 0 23 0 0 0 3 28 117 0 SYN672-1 theorem 0.0 4 1 30 0 22 0 0 0 4 30 100 0 SYN673-1 theorem 14.6 13 2 880 1 19 0 0 3082 5 867 41408 10148 SYN674-1 theorem 0.2 4 1 92 0 24 0 0 0 3 92 3179 0 SYN675-1 theorem 0.2 5 1 83 0 24 0 0 0 3 83 3147 0 SYN676-1 theorem 0.1 4 1 60 0 24 0 0 0 3 60 1044 0 SYN677-1 theorem 0.1 4 1 51 0 24 0 0 0 3 51 1014 0 SYN678-1 theorem 0.2 5 1 92 0 24 0 0 0 3 92 3179 0 SYN679-1 theorem 0.2 5 1 83 0 24 0 0 0 3 83 3147 0 SYN680-1 theorem 0.2 5 1 92 0 24 0 0 0 3 92 3179 0 SYN681-1 theorem 0.2 4 1 83 0 24 0 0 0 3 83 3147 0 SYN682-1 theorem 0.2 5 1 92 0 24 0 0 0 3 92 3179 0 SYN683-1 theorem 0.2 5 1 83 0 24 0 0 0 3 83 3147 0 SYN684-1 theorem 0.1 4 1 60 0 24 0 0 0 3 60 1044 0 SYN685-1 theorem 0.1 4 1 51 0 24 0 0 0 3 51 1014 0 SYN686-1 theorem 0.0 4 1 64 0 22 0 0 0 3 64 521 0 SYN687-1 theorem 4.1 4 1 41 0 20 0 0 0 7 41 132 1 SYN690-1 timeout 299.0 230 SYN692-1 theorem 1.3 12 1 141 0 26 0 0 0 3 141 19571 0 SYN693-1 theorem 1.3 10 1 142 0 27 0 0 0 3 142 19573 0 SYN694-1 theorem 2.1 14 1 189 0 30 0 0 0 3 189 32766 0 SYN695-1 theorem 1.6 13 1 167 0 30 0 0 0 3 167 24136 0 SYN696-1 theorem 1.8 10 1 167 0 30 0 0 0 3 167 27428 0 SYN697-1 theorem 1.3 11 1 145 0 30 0 0 0 3 145 19580 0 SYN698-1 theorem 2.2 15 1 191 0 31 0 0 0 3 191 32763 0 SYN699-1 theorem 1.7 14 1 169 0 31 0 0 0 3 169 24133 0 SYN700-1 theorem 1.9 13 1 168 0 31 0 0 0 3 168 27430 0 SYN701-1 theorem 1.3 12 1 146 0 31 0 0 0 3 146 19582 0 SYN710-1 theorem 0.0 4 1 53 0 26 0 0 0 4 53 163 1 SYN713-1 theorem 0.0 4 1 60 0 40 0 0 0 4 60 202 0 SYN714-1 theorem 0.0 4 1 38 0 31 0 0 0 3 38 137 0 SYN717-1 theorem 0.0 4 1 50 0 46 0 0 0 2 50 149 0 SYN718-1 theorem 3.2 19 1 144 0 43 0 0 0 4 144 1063 1 SYN724-1 theorem 0.0 4 2 5 1 8 6 0 0 2 4 9 6 SYN726-1 theorem 0.0 4 6 47 22 2 0 0 228 2 30 193 537 SYN728-1 theorem 0.0 4 3 3 6 3 3 0 1 5 6 9 11 SYN734-1 non_thm 0.0 4 0 1 1 1 0 0 0 2 2 1 1 SYN735-1 non_thm 0.0 4 0 1 2 1 0 0 4 2 3 1 6 SYN736-1 non_thm 0.0 4 0 1 1 1 0 0 1 2 2 1 2 SYN737-1 non_thm 0.0 4 0 1 6 1 0 0 68 2 7 1 73 SYN738-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 SYN739-1 non_thm 0.0 4 0 1 5 1 0 0 2 2 6 1 7 SYN740-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 SYN741-1 timeout 298.9 8 SYN742-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 SYN743-1 non_thm 0.0 4 0 1 7 1 0 0 12 2 8 1 19 SYN744-1 non_thm 0.0 4 0 1 2 1 0 0 1 2 3 1 3 SYN745-1 non_thm 0.0 4 0 1 9 1 0 0 23 2 8 1 31 SYN746-1 non_thm 0.0 4 0 1 1 1 0 0 5 2 2 1 6 SYN747-1 timeout 298.9 5 SYN748-1 non_thm 0.1 4 1 1 28 1 0 0 725 2 9 1 866 SYN749-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 SYN750-1 non_thm 0.0 4 0 1 9 1 0 0 59 2 9 1 69 SYN751-1 non_thm 0.1 4 0 1 45 1 0 0 456 2 14 1 539 SYN752-1 non_thm 0.0 4 0 1 1 1 0 0 2 2 2 1 3 SYN753-1 non_thm 0.0 4 0 1 11 1 0 0 50 2 8 1 61 SYN754-1 non_thm 0.0 4 0 1 8 1 0 0 27 2 6 1 41 SYN755-1 theorem 3.7 4 146 1 366 1 0 0 50475 5 21 1 62718 SYN756-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 SYN757-1 non_thm 0.0 4 0 1 3 1 0 0 26 2 4 1 29 SYN758-1 theorem 59.1 4 302 1 943 1 0 0 231323 8 27 1 291454 SYN759-1 theorem 78.2 4 356 1 1123 1 0 0 354700 8 32 1 434892 SYN760-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 SYN761-1 timeout 298.9 5 SYN762-1 theorem 62.9 4 232 1 852 1 0 0 253427 8 30 1 298706 SYN763-1 non_thm 0.0 4 0 1 9 1 0 0 56 2 10 1 65 SYN764-1 non_thm 0.0 4 0 1 7 1 0 0 31 2 7 1 38 SYN765-1 non_thm 0.9 4 51 1 306 1 0 0 12002 3 23 1 14135 SYN766-1 non_thm 0.8 4 29 1 335 1 0 0 11886 3 24 1 13415 SYN767-1 non_thm 0.0 4 0 1 6 1 0 0 23 2 7 1 29 SYN768-1 non_thm 0.0 4 0 2 1 2 0 0 5 2 3 2 6 SYN769-1 non_thm 0.0 4 0 2 1 2 0 0 16 2 3 2 17 SYN770-1 non_thm 0.0 4 0 2 1 2 0 0 13 2 3 2 14 SYN771-1 non_thm 0.0 4 0 2 1 2 0 0 27 2 3 2 28 SYN772-1 non_thm 0.0 4 0 2 7 2 0 0 37 2 9 2 44 SYN773-1 non_thm 0.0 4 0 2 1 2 0 0 9 2 3 2 10 SYN774-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 SYN775-1 timeout 299.0 19 SYN776-1 non_thm 0.1 4 0 2 2 2 0 0 122 3 4 2 124 SYN777-1 non_thm 1.6 4 8 2 57 2 0 0 20094 3 30 2 23409 SYN778-1 non_thm 0.1 4 0 2 6 2 0 0 345 3 8 2 351 SYN779-1 non_thm 0.8 4 7 2 45 2 0 0 9880 3 26 2 12174 SYN780-1 non_thm 0.0 4 0 2 1 2 0 0 8 2 3 2 9 SYN781-1 non_thm 0.1 4 0 2 40 2 0 0 1731 3 21 2 1817 SYN782-1 non_thm 0.3 4 3 2 44 2 0 0 3804 3 43 2 4545 SYN783-1 non_thm 0.1 4 0 2 3 2 0 0 63 3 5 2 66 SYN784-1 theorem 4.9 4 82 2 339 2 0 0 40113 4 23 2 56018 SYN785-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 SYN786-1 non_thm 0.1 4 0 2 4 2 0 0 322 3 6 2 326 SYN787-1 non_thm 48.6 4 328 2 980 2 0 0 569598 4 62 2 740735 SYN788-1 timeout 299.0 8 SYN789-1 timeout 298.9 5 SYN790-1 non_thm 0.1 4 3 2 41 2 0 0 822 2 20 2 1020 SYN791-1 non_thm 0.0 4 0 2 1 2 0 0 7 2 3 2 8 SYN792-1 timeout 299.0 10 SYN793-1 non_thm 0.0 4 0 2 2 2 0 0 27 3 4 2 29 SYN794-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 SYN795-1 non_thm 0.1 4 0 2 29 2 0 0 1446 3 23 2 1491 SYN796-1 theorem 1.2 4 42 2 143 2 0 0 14239 3 16 2 21197 SYN797-1 non_thm 0.0 4 0 2 1 2 0 0 20 2 3 2 21 SYN798-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 SYN799-1 non_thm 291.1 6 911 2 2775 2 0 0 2563714 5 126 2 3183132 SYN800-1 timeout 299.0 6 SYN801-1 non_thm 3.9 4 29 2 127 2 0 0 56398 3 30 2 71428 SYN802-1 timeout 299.0 8 SYN803-1 non_thm 0.0 4 0 2 1 2 0 0 10 2 3 2 11 SYN804-1 non_thm 0.6 4 0 2 7 2 0 0 107 3 9 2 114 SYN805-1 non_thm 0.7 4 49 2 346 2 0 0 15773 2 25 2 20243 SYN806-1 non_thm 3.3 4 22 2 277 2 0 0 50183 3 57 2 57124 SYN807-1 non_thm 0.1 4 0 2 5 2 0 0 227 3 7 2 232 SYN808-1 non_thm 9.5 4 84 2 693 2 0 0 140976 3 58 2 162536 SYN809-1 timeout 299.0 17 SYN810-1 timeout 299.0 17 SYN811-1 non_thm 1.1 5 0 376 84 64 489 0 400 2 460 712 484 SYN812-1 non_thm 11.8 19 0 936 186 101 1708 0 1005 2 1122 1801 1191 SYN813-1 theorem 1.7 17 23 188 1068 44 269 0 1340 2 340 371 2847 SYN814-1 non_thm 3.2 17 0 376 726 64 489 0 1650 2 1102 712 2398 SYN815-1 non_thm 4.5 17 0 674 193 85 939 0 774 2 867 1293 967 SYN816-1 non_thm 4.3 17 0 590 184 79 939 0 720 2 774 1127 904 SYN817-1 non_thm 4.9 17 0 626 207 82 939 0 787 2 833 1198 994 SYN818-1 non_thm 17.9 26 0 1374 471 125 1763 0 1728 2 1845 2669 2199 SYN819-1 theorem 3.3 19 40 188 1635 44 269 0 2941 2 394 388 5995 SYN820-1 theorem 8.5 19 81 188 4034 44 269 0 11277 2 561 429 17724 SYN821-1 non_thm 5.1 19 0 696 177 88 899 0 788 2 873 1336 965 SYN822-1 non_thm 7.1 19 0 696 678 88 939 0 1449 2 1374 1336 2128 SYN823-1 non_thm 0.3 19 0 160 86 32 249 0 205 2 246 288 291 SYN824-1 non_thm 2.9 19 0 515 126 65 896 0 573 2 641 965 699 SYN825-1 non_thm 9.5 19 0 945 117 85 1649 0 964 2 1062 1805 1081 SYN826-1 non_thm 9.6 19 0 858 25 84 1763 0 798 2 883 1632 823 SYN827-1 non_thm 0.6 19 0 188 138 36 269 0 443 2 326 340 581 SYN828-1 non_thm 4.4 19 1 646 246 68 899 0 898 2 892 1225 1153 SYN829-1 non_thm 13.7 22 0 1177 145 95 1704 0 1199 2 1322 2259 1344 SYN830-1 non_thm 14.3 22 0 1214 64 98 1763 0 1156 2 1278 2330 1220 SYN831-1 non_thm 14.5 23 0 1268 295 96 1763 0 1474 2 1563 2440 1772 SYN832-1 non_thm 12.7 20 0 1033 218 93 1704 0 1152 2 1251 1973 1370 SYN833-1 theorem 0.4 20 3 188 93 36 269 0 230 2 236 343 374 SYN834-1 theorem 1.2 20 14 188 793 36 269 0 1217 2 363 354 2305 SYN835-1 non_thm 0.6 20 1 188 210 36 269 0 494 2 391 341 709 SYN836-1 theorem 0.5 20 2 188 133 36 269 0 274 2 272 342 526 SYN837-1 theorem 6.5 20 22 376 2246 52 489 0 2755 2 729 722 5875 SYN838-1 non_thm 5.7 20 0 634 351 70 939 0 929 2 985 1198 1280 SYN839-1 non_thm 17.8 27 0 1336 423 102 1763 0 1636 2 1759 2570 2059 SYN840-1 non_thm 20.0 29 2 1150 549 96 1763 0 1976 2 1660 2206 2573 SYN841-1 non_thm 20.1 29 0 1330 681 102 1763 0 2045 2 2011 2558 2727 SYN842-1 non_thm 21.9 31 0 1400 672 102 1763 0 2037 2 2072 2698 2709 SYN843-1 theorem 0.6 22 4 188 152 36 269 0 314 2 296 344 620 SYN844-1 theorem 0.5 22 4 188 125 36 269 0 254 2 249 344 478 SYN845-1 theorem 0.4 22 2 188 84 36 269 0 232 2 251 342 393 SYN846-1 theorem 14.1 22 57 376 3943 52 489 0 4644 2 755 757 11420 SYN847-1 theorem 2.0 22 4 376 454 52 489 0 743 2 626 704 1503 SYN848-1 theorem 1.5 22 3 376 191 52 489 0 485 2 488 703 820 SYN849-1 theorem 16.0 22 77 376 5851 52 489 0 10192 2 751 777 20341 SYN850-1 theorem 5.0 22 2 696 160 72 939 0 764 2 789 1322 1052 SYN851-1 non_thm 5.8 22 1 696 478 72 939 0 1145 2 1086 1321 1662 SYN852-1 non_thm 23.7 32 0 1396 846 102 1763 0 2165 2 2242 2690 3015 SYN853-1 non_thm 28.2 33 3 1424 1373 104 1763 0 2969 2 2099 2747 4535 SYN854-1 non_thm 46.2 38 5 1424 1828 104 1763 0 6541 2 2934 2749 8790 SYN855-1 non_thm 20.8 31 0 1424 717 104 1763 0 2199 2 2141 2744 2916 SYN856-1 theorem 0.6 22 3 188 153 36 269 0 312 2 284 343 620 SYN857-1 theorem 0.7 22 3 188 206 36 269 0 337 2 280 343 733 SYN858-1 theorem 1.8 22 3 376 258 52 489 0 595 2 492 703 1088 SYN859-1 theorem 2.2 22 6 376 462 52 489 0 889 2 538 706 1551 SYN860-1 theorem 3.6 22 15 376 637 52 489 0 1270 2 634 715 2720 SYN861-1 theorem 8.8 22 10 696 933 72 939 0 1844 2 1211 1330 3296 SYN862-1 theorem 134.1 35 308 696 24497 72 939 0 40378 2 1314 1628 70638 SYN863-1 non_thm 6.9 22 0 696 718 72 939 0 1622 2 1414 1320 2340 SYN864-1 non_thm 6.5 22 0 696 522 72 939 0 1225 2 1218 1320 1749 SYN865-1 theorem 6.3 22 3 696 559 72 939 0 1223 2 1106 1323 1962 SYN866-1 theorem 32.4 22 29 696 5161 72 939 0 8595 2 1201 1349 15603 SYN867-1 non_thm 0.1 22 0 48 11 48 458 0 1 2 59 48 12 SYN868-1 non_thm 0.1 22 0 45 6 45 433 0 2 2 51 45 8 SYN869-1 theorem 0.1 22 2 36 5 36 266 0 0 2 40 38 34 SYN870-1 non_thm 0.1 22 3 36 14 36 262 0 30 2 47 39 63 SYN871-1 theorem 0.2 22 15 36 82 36 256 0 254 2 58 51 441 SYN872-1 non_thm 0.5 22 0 94 4 94 1717 0 0 2 98 94 4 SYN873-1 theorem 0.2 22 13 36 65 36 269 0 62 2 52 49 225 SYN874-1 theorem 0.1 22 4 36 22 36 269 0 22 2 48 40 84 SYN875-1 theorem 0.1 22 4 36 14 36 265 0 4 2 43 40 63 SYN876-1 theorem 12.4 22 125 52 1053 52 487 0 16037 2 136 177 18731 SYN877-1 theorem 0.1 22 3 36 13 36 268 0 3 2 42 39 87 SYN878-1 theorem 0.1 22 3 36 14 36 271 0 18 2 45 39 72 SYN879-1 theorem 0.1 22 2 36 12 36 271 0 14 2 45 38 91 SYN880-1 theorem 0.1 22 2 52 9 52 488 0 3 2 60 54 46 SYN881-1 theorem 168.6 28 2655 52 15389 52 490 0 170019 2 150 2707 226151 SYN882-1 theorem 0.2 22 5 52 19 52 485 0 16 2 62 57 72 SYN883-1 theorem 0.2 22 6 52 24 52 491 0 48 2 67 58 117 SYN884-1 theorem 0.4 22 4 70 14 70 932 0 2 2 77 74 60 SYN885-1 theorem 3.4 22 40 72 311 72 908 0 600 2 111 112 1426 SYN886-1 theorem 0.3 22 2 72 6 72 909 0 0 2 77 74 33 SYN887-1 theorem 0.4 22 4 72 14 72 938 0 3 2 82 76 58 SYN888-1 non_thm 0.8 22 0 102 10 102 1760 0 13 2 112 102 23 SYN889-1 theorem 0.1 22 2 36 4 36 271 0 0 2 39 38 53 SYN890-1 theorem 0.1 22 2 36 8 36 273 0 2 2 42 38 56 SYN891-1 theorem 0.1 22 2 36 7 36 259 0 0 2 40 38 64 SYN892-1 theorem 0.1 22 2 36 10 36 273 0 4 2 42 38 94 SYN893-1 theorem 0.2 22 2 52 5 52 485 0 1 2 56 54 46 SYN894-1 theorem 0.2 22 3 52 9 52 489 0 4 2 58 55 45 SYN895-1 theorem 0.2 22 2 52 11 52 479 0 0 2 60 54 68 SYN896-1 theorem 0.4 22 13 52 48 52 492 0 36 2 75 65 251 SYN897-1 theorem 0.5 22 2 72 23 72 940 0 5 2 88 74 86 SYN898-1 theorem 0.5 22 7 72 29 72 941 0 13 2 85 79 101 SYN899-1 theorem 0.4 22 3 72 15 72 931 0 5 2 82 75 83 SYN900-1 theorem 0.4 22 4 72 27 72 923 0 8 2 93 76 71 SYN901-1 theorem 1.0 22 4 101 23 101 1680 0 25 2 120 105 88 SYN902-1 non_thm 2.0 22 4 102 90 102 1757 0 200 2 189 106 329 SYN903-1 timeout 298.9 22 SYN904-1 timeout 299.0 22 SYN905-1 timeout 299.0 22 SYN906-1 timeout 299.0 25 SYN907-1 timeout 299.0 23 SYN908-1 timeout 298.9 26 SYN909-1 timeout 299.0 33 SYN910-1 timeout 298.9 36 SYN911-1 timeout 299.0 42 SYN912-1 timeout 298.9 50 SYN913-1 timeout 299.0 39 TOP001-1 timeout 299.0 22 TOP001-2 theorem 0.0 22 1 34 0 3 0 0 0 6 34 65 1 TOP002-1 timeout 298.9 24 TOP002-2 theorem 0.0 22 1 2 0 2 0 0 0 2 2 4 1 TOP003-1 timeout 299.0 41 TOP003-2 non_thm 0.0 22 0 12 18 3 0 0 50 3 28 20 67 TOP004-1 theorem 0.0 22 1 1 0 0 0 0 0 2 1 4 2 TOP004-2 theorem 0.0 22 1 1 0 0 0 0 0 2 1 5 1 TOP005-1 timeout 299.0 36 TOP005-2 timeout 299.0 36 TOP006-1 timeout 299.0 96 TOP007-1 timeout 299.0 78 TOP008-1 timeout 299.0 272 TOP009-1 timeout 299.0 109 TOP010-1 timeout 299.0 82 TOP011-1 timeout 299.0 23 TOP012-1 timeout 299.0 124 TOP013-1 timeout 299.0 61 TOP014-1 timeout 299.0 64 TOP015-1 timeout 299.0 62 TOP016-1 timeout 299.0 61 TOP017-1 timeout 299.0 66 TOP018-1 timeout 299.0 57 TOP019-1 timeout 299.0 33