-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true -ubj false 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 2 1 45 0 4 0 0 0 3 45 280 101 0 ANA001-1 timeout 300.0 54 ANA002-1 timeout 300.0 36 ANA002-2 timeout 300.0 36 ANA002-3 timeout 300.0 14 ANA002-4 timeout 300.0 16 ANA003-4 timeout 300.0 195 ANA004-4 timeout 300.0 196 ANA004-5 timeout 300.0 28 ANA005-4 timeout 300.0 30 ANA005-5 timeout 300.0 67 CAT007-3 theorem 0.0 2 1 5 0 5 0 0 0 2 5 12 6 0 COM002-2 theorem 0.0 2 1 26 0 15 0 0 0 2 26 47 9 0 COM003-1 timeout 300.0 20 COM003-2 theorem 0.0 2 1 12 0 17 13 1 0 2 12 24 22 0 FLD001-3 theorem 0.0 2 1 62 0 7 0 0 0 2 62 283 2000 0 FLD002-3 theorem 0.0 2 1 63 0 7 0 0 0 2 63 300 2005 0 FLD003-1 timeout 300.0 16 FLD004-1 timeout 300.0 16 FLD005-1 timeout 300.0 16 FLD005-3 theorem 0.0 2 1 91 0 6 0 0 0 2 91 629 2082 0 FLD006-1 theorem 27.7 4 1 154 0 4 0 0 0 3 154 1362 16646 0 FLD006-3 theorem 0.0 2 1 5 0 4 0 0 0 2 5 31 32 0 FLD007-1 timeout 300.0 12 FLD007-3 timeout 300.0 57 FLD008-1 timeout 300.0 16 FLD008-2 timeout 300.0 20 FLD008-3 timeout 300.0 43 FLD008-4 theorem 0.1 2 1 145 0 10 0 0 0 2 145 804 7875 0 FLD009-1 timeout 300.0 17 FLD009-3 theorem 0.1 2 1 112 0 7 0 0 0 2 112 907 2094 0 FLD010-1 theorem 34.3 5 1 168 0 5 0 0 0 3 168 1396 18973 0 FLD010-3 theorem 0.0 2 1 6 0 5 0 0 0 2 6 35 34 0 FLD010-5 theorem 0.0 2 1 54 0 5 0 0 0 2 54 658 341 0 FLD011-1 timeout 300.0 12 FLD011-3 timeout 300.0 52 FLD012-1 timeout 300.0 17 FLD012-2 timeout 300.0 22 FLD012-3 timeout 300.0 60 FLD012-4 theorem 0.2 3 1 270 0 12 0 0 0 2 270 3112 8519 0 FLD013-1 theorem 7.0 3 1 272 0 10 0 0 0 2 272 1327 8600 0 FLD013-2 theorem 16.1 3 1 345 0 12 0 0 0 2 345 1638 14448 0 FLD013-3 theorem 0.5 0 1 324 0 10 0 0 0 2 324 6414 9245 0 FLD013-4 theorem 0.0 2 1 29 0 12 0 0 0 2 29 315 509 0 FLD013-5 theorem 0.0 2 1 27 0 14 0 0 0 2 27 334 599 0 FLD014-1 timeout 300.0 16 FLD014-3 theorem 0.2 2 1 192 0 7 0 0 0 2 192 3602 2729 0 FLD015-1 timeout 300.0 16 FLD015-3 theorem 0.1 2 1 93 0 7 0 0 0 2 93 636 2018 0 FLD016-1 timeout 300.0 21 FLD016-3 theorem 0.1 2 1 151 0 10 0 0 0 2 151 851 7883 0 FLD016-5 theorem 0.2 3 1 204 0 12 0 0 0 2 204 1500 13874 0 FLD017-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 310 460 0 FLD017-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 187 219 0 FLD018-1 timeout 300.0 12 FLD018-3 theorem 0.0 2 1 73 0 6 0 0 0 2 73 1562 1180 0 FLD019-1 timeout 300.0 12 FLD019-3 theorem 0.0 2 1 14 0 6 0 0 0 2 14 96 133 0 FLD020-1 timeout 300.0 16 FLD020-3 theorem 0.0 2 1 83 0 7 0 0 0 2 83 518 2102 0 FLD021-1 theorem 0.8 2 1 55 0 7 0 0 0 2 55 216 1950 0 FLD021-3 theorem 0.0 2 1 14 0 7 0 0 0 2 14 104 171 0 FLD022-1 timeout 300.0 15 FLD022-3 theorem 0.1 2 1 149 0 10 0 0 0 2 149 827 7875 0 FLD023-1 theorem 89.9 12 1 212 0 7 0 0 0 3 212 10330 36163 0 FLD023-3 theorem 0.0 2 1 86 0 7 0 0 0 2 86 738 2163 0 FLD024-1 timeout 300.0 16 FLD024-3 theorem 0.0 2 1 57 0 7 0 0 0 2 57 227 1951 0 FLD025-1 theorem 7.0 3 1 284 0 10 0 0 0 2 284 1371 8644 0 FLD025-2 theorem 34.0 4 1 460 0 14 0 0 0 2 460 2232 23137 0 FLD025-3 theorem 0.5 3 1 324 0 10 0 0 0 2 324 6414 9245 0 FLD025-4 theorem 0.0 2 1 36 0 12 0 0 0 2 36 336 530 0 FLD025-5 theorem 0.0 2 1 35 0 14 0 0 0 2 35 362 623 0 FLD026-1 timeout 300.0 17 FLD026-3 theorem 0.5 3 1 410 0 8 0 0 0 2 410 12031 3013 0 FLD027-1 timeout 300.0 17 FLD027-3 theorem 0.1 2 1 149 0 9 0 0 0 2 149 1648 2240 0 FLD028-1 timeout 300.0 15 FLD028-3 theorem 0.1 3 1 181 0 11 0 0 0 2 181 1229 8064 0 FLD029-1 timeout 300.0 15 FLD029-3 theorem 0.5 3 1 589 0 11 0 0 0 2 589 8391 8884 0 FLD030-1 theorem 0.0 2 1 9 0 8 0 0 0 2 9 149 167 0 FLD030-2 theorem 0.0 2 1 24 0 10 0 0 0 2 24 310 460 0 FLD030-3 theorem 0.0 2 1 25 0 8 0 0 0 2 25 188 291 0 FLD030-4 theorem 0.0 2 1 11 0 10 0 0 0 2 11 187 219 0 FLD031-1 timeout 300.0 13 FLD031-3 theorem 0.0 2 1 83 0 7 0 0 0 2 83 2127 1244 0 FLD031-5 theorem 0.1 2 1 100 0 7 0 0 0 2 100 2896 1342 0 FLD032-1 timeout 300.0 12 FLD032-3 theorem 0.0 2 1 18 0 7 0 0 0 2 18 110 139 0 FLD033-1 timeout 300.0 17 FLD033-3 theorem 0.1 2 1 126 0 8 0 0 0 2 126 1084 2200 0 FLD034-1 theorem 0.8 2 1 60 0 7 0 0 0 2 60 233 2047 0 FLD034-3 theorem 0.0 2 1 18 0 7 0 0 0 2 18 120 183 0 FLD035-1 timeout 300.0 15 FLD035-3 theorem 0.1 3 1 181 0 11 0 0 0 2 181 1229 8064 0 FLD036-1 timeout 300.0 15 FLD036-3 theorem 0.1 3 1 181 0 11 0 0 0 2 181 1229 8064 0 FLD037-1 theorem 133.5 14 1 275 0 8 0 0 0 3 275 11553 51689 0 FLD037-3 theorem 0.1 2 1 128 0 8 0 0 0 2 128 1883 2362 0 FLD038-1 timeout 300.0 17 FLD038-3 theorem 0.0 2 1 64 0 8 0 0 0 2 64 277 2055 0 FLD039-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 65 71 0 FLD039-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 81 126 0 FLD040-1 timeout 300.0 12 FLD040-3 theorem 0.0 2 1 67 0 6 0 0 0 2 67 537 907 0 FLD040-5 theorem 0.0 2 1 68 0 6 0 0 0 2 68 601 904 0 FLD041-1 timeout 300.0 17 FLD041-2 timeout 300.0 16 FLD041-3 theorem 0.1 2 1 188 0 8 0 0 0 2 188 2588 2269 0 FLD041-4 theorem 0.4 3 1 343 0 10 0 0 0 2 343 10802 5214 0 FLD042-1 timeout 300.0 17 FLD042-3 theorem 0.1 2 1 188 0 8 0 0 0 2 188 2588 2269 0 FLD043-1 timeout 300.0 12 FLD043-3 theorem 0.0 2 1 107 0 7 0 0 0 2 107 851 2223 0 FLD043-5 theorem 9.7 12 1 684 0 5 0 0 0 2 684 101318 13914 0 FLD044-1 timeout 300.0 16 FLD044-2 timeout 300.0 31 FLD044-3 timeout 300.0 43 FLD044-4 timeout 300.0 47 FLD045-1 timeout 300.0 16 FLD045-2 timeout 300.0 19 FLD045-3 timeout 300.0 43 FLD045-4 timeout 300.0 44 FLD046-1 timeout 300.0 12 FLD046-3 timeout 300.0 51 FLD047-1 timeout 300.0 15 FLD047-2 timeout 300.0 21 FLD047-3 timeout 300.0 55 FLD047-4 theorem 0.5 4 1 441 0 15 0 0 0 2 441 5200 22960 0 FLD048-1 timeout 300.0 16 FLD048-2 timeout 300.0 21 FLD048-3 timeout 300.0 53 FLD048-4 theorem 252.9 30 1 2432 0 20 0 0 0 2 2432 157881 113120 0 FLD049-1 timeout 300.0 15 FLD049-2 timeout 300.0 21 FLD049-3 timeout 300.0 53 FLD049-4 theorem 0.3 3 1 295 0 15 0 0 0 2 295 1927 22696 0 FLD050-1 timeout 300.0 15 FLD050-2 timeout 300.0 19 FLD050-3 timeout 300.0 53 FLD050-4 theorem 0.3 3 1 298 0 15 0 0 0 2 298 1974 22714 0 FLD051-1 timeout 300.0 17 FLD051-2 timeout 300.0 21 FLD051-3 timeout 300.0 61 FLD051-4 timeout 300.0 31 FLD052-1 timeout 300.0 16 FLD052-2 timeout 300.0 11 FLD052-3 timeout 300.0 53 FLD052-4 theorem 3.4 13 1 932 0 25 0 0 0 2 932 9605 182444 0 FLD053-1 timeout 300.0 16 FLD053-2 timeout 300.0 11 FLD053-3 timeout 300.0 53 FLD053-4 timeout 300.0 29 FLD054-1 timeout 300.0 17 FLD054-2 timeout 300.0 18 FLD054-3 timeout 300.0 63 FLD054-4 theorem 0.4 4 1 419 0 14 0 0 0 2 419 5923 14352 0 FLD055-1 theorem 0.0 2 1 27 0 9 0 0 0 2 27 278 396 0 FLD055-3 theorem 0.0 2 1 20 0 9 0 0 0 2 20 154 259 0 FLD056-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 57 64 0 FLD056-3 theorem 0.0 2 1 4 0 4 0 0 0 2 4 57 64 0 FLD057-1 timeout 300.0 11 FLD057-3 timeout 300.0 88 FLD058-1 theorem 0.0 2 1 25 0 9 0 0 0 2 25 213 275 0 FLD058-3 theorem 0.0 2 1 21 0 9 0 0 0 2 21 131 199 0 FLD059-1 theorem 0.2 2 1 40 0 6 0 0 0 2 40 141 791 0 FLD059-2 theorem 0.8 2 1 177 0 8 0 0 0 2 177 908 2480 0 FLD059-3 theorem 0.0 2 1 54 0 6 0 0 0 2 54 322 833 0 FLD059-4 theorem 0.0 2 1 14 0 8 0 0 0 2 14 107 173 0 FLD060-1 theorem 0.8 2 1 133 0 7 0 0 0 2 133 517 2165 0 FLD060-2 theorem 6.9 3 1 267 0 11 0 0 0 2 267 1054 8300 0 FLD060-3 theorem 32.5 17 1 996 0 7 0 0 0 2 996 145733 26815 0 FLD060-4 theorem 0.3 3 1 313 0 11 0 0 0 2 313 3407 8487 0 FLD061-1 theorem 6.8 3 1 245 0 10 0 0 0 2 245 889 8166 0 FLD061-2 theorem 33.9 4 1 421 0 14 0 0 0 2 421 1571 22732 0 FLD061-3 theorem 189.7 35 1 1854 0 10 0 0 0 2 1854 290812 57117 0 FLD061-4 theorem 0.8 4 1 471 0 14 0 0 0 2 471 5072 22973 0 FLD062-1 timeout 300.0 16 FLD062-3 theorem 88.6 32 1 1101 0 7 0 0 0 2 1101 276678 85188 0 FLD063-1 timeout 300.0 16 FLD063-3 theorem 23.9 14 1 818 0 7 0 0 0 2 818 111768 25639 0 FLD064-1 timeout 300.0 12 FLD064-3 theorem 0.0 2 1 87 0 6 0 0 0 2 87 1933 1305 0 FLD065-1 timeout 300.0 12 FLD065-3 theorem 0.0 2 1 12 0 6 0 0 0 2 12 67 105 0 FLD066-1 timeout 300.0 15 FLD066-3 theorem 0.2 3 1 207 0 12 0 0 0 2 207 1580 13965 0 FLD067-1 theorem 86.1 12 1 202 0 7 0 0 0 3 202 9543 35389 0 FLD067-2 timeout 300.0 18 FLD067-3 timeout 300.0 44 FLD067-4 theorem 0.1 2 1 107 0 9 0 0 0 2 107 531 4188 0 FLD068-1 timeout 300.0 16 FLD068-2 timeout 300.0 17 FLD068-3 timeout 300.0 44 FLD068-4 theorem 0.1 2 1 87 0 9 0 0 0 2 87 372 4172 0 FLD069-1 theorem 0.8 2 1 98 0 9 0 0 0 2 98 401 2130 0 FLD069-3 theorem 0.0 2 1 16 0 9 0 0 0 2 16 110 194 0 FLD070-1 theorem 0.8 2 1 60 0 8 0 0 0 2 60 220 1955 0 FLD070-2 theorem 2.6 2 1 266 0 10 0 0 0 2 266 1401 5021 0 FLD070-3 theorem 0.1 2 1 80 0 8 0 0 0 2 80 453 2008 0 FLD070-4 theorem 0.0 2 1 17 0 10 0 0 0 2 17 155 255 0 FLD071-1 theorem 0.0 2 1 8 0 8 0 0 0 2 8 103 116 0 FLD071-2 theorem 2.5 2 1 100 0 10 0 0 0 2 100 376 4176 0 FLD071-3 theorem 0.0 2 1 9 0 8 0 0 0 2 9 98 104 0 FLD071-4 theorem 0.0 2 1 9 0 9 0 0 0 2 9 141 157 0 FLD072-1 timeout 300.0 16 FLD072-2 timeout 300.0 16 FLD072-3 timeout 300.0 49 FLD072-4 timeout 300.0 68 FLD073-1 timeout 300.0 16 FLD073-2 timeout 300.0 15 FLD073-3 timeout 300.0 44 FLD073-4 timeout 300.0 76 FLD074-1 timeout 300.0 16 FLD074-2 timeout 300.0 32 FLD074-3 timeout 300.0 45 FLD074-4 timeout 300.0 37 FLD075-1 timeout 300.0 18 FLD075-2 timeout 300.0 24 FLD075-3 timeout 300.0 45 FLD075-4 timeout 300.0 39 FLD076-1 timeout 300.0 16 FLD076-2 timeout 300.0 22 FLD076-3 timeout 300.0 55 FLD076-4 timeout 300.0 45 FLD077-1 timeout 300.0 15 FLD077-2 timeout 300.0 20 FLD077-3 timeout 300.0 57 FLD077-4 timeout 300.0 45 FLD078-1 timeout 300.0 17 FLD078-2 timeout 300.0 15 FLD078-3 timeout 300.0 55 FLD078-4 timeout 300.0 51 FLD079-1 timeout 300.0 17 FLD079-2 timeout 300.0 16 FLD079-3 timeout 300.0 69 FLD079-4 timeout 300.0 69 FLD080-1 timeout 300.0 12 FLD080-2 timeout 300.0 16 FLD080-3 timeout 300.0 55 FLD080-4 timeout 300.0 63 FLD081-1 timeout 300.0 29 FLD081-2 timeout 300.0 33 FLD081-3 timeout 300.0 46 FLD081-4 timeout 300.0 49 FLD082-1 timeout 300.0 17 FLD082-3 timeout 300.0 69 FLD083-1 timeout 300.0 17 FLD083-3 timeout 300.0 69 FLD084-1 timeout 300.0 17 FLD084-3 timeout 300.0 63 FLD085-1 timeout 300.0 17 FLD085-3 timeout 300.0 63 FLD086-1 timeout 300.0 12 FLD086-3 timeout 300.0 54 FLD087-1 timeout 300.0 12 FLD087-3 timeout 300.0 54 FLD088-1 timeout 300.0 12 FLD088-3 timeout 300.0 54 FLD089-1 timeout 300.0 12 FLD089-3 timeout 300.0 54 FLD090-1 timeout 300.0 12 FLD090-3 timeout 300.0 52 FLD091-1 timeout 300.0 12 FLD091-3 timeout 300.0 52 FLD092-1 timeout 300.0 12 FLD092-3 timeout 300.0 52 FLD093-1 timeout 300.0 12 FLD093-3 timeout 300.0 52 FLD094-1 timeout 300.0 12 FLD094-3 timeout 300.0 52 FLD095-1 timeout 300.0 15 FLD095-2 timeout 300.0 21 FLD095-3 timeout 300.0 58 FLD095-4 timeout 300.0 36 FLD096-1 timeout 300.0 20 FLD096-2 timeout 300.0 23 FLD096-3 timeout 300.0 58 FLD096-4 timeout 300.0 36 FLD097-1 timeout 300.0 17 FLD097-2 timeout 300.0 25 FLD097-3 timeout 300.0 44 FLD097-4 timeout 300.0 38 FLD098-1 timeout 300.0 16 FLD098-2 timeout 300.0 26 FLD098-3 timeout 300.0 45 FLD098-4 timeout 300.0 38 FLD099-1 timeout 300.0 12 FLD099-2 timeout 300.0 19 FLD099-3 timeout 300.0 52 FLD099-4 timeout 300.0 81 FLD100-1 timeout 300.0 16 FLD100-2 timeout 300.0 23 FLD100-3 timeout 300.0 44 FLD100-4 timeout 300.0 36 GRA001-1 theorem 0.0 2 4 10 3 16 28 0 1 2 5 22 10 0 GRP025-3 timeout 300.0 63 GRP026-3 timeout 300.0 81 GRP027-2 timeout 300.0 25 GRP039-6 theorem 14.0 4 20 1644 23 9 0 1 26271 2 640 199863 28775 0 GRP123-1.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 87 44 0 GRP123-1.005 non_thm 0.0 2 0 143 4 26 0 0 256 2 0 1556 505 0 GRP123-2.003 theorem 0.0 2 1 37 0 15 0 0 0 2 37 94 44 0 GRP123-2.005 non_thm 0.1 2 1 189 2 40 0 0 259 2 152 1815 595 0 GRP123-3.003 theorem 0.0 2 1 51 0 20 0 0 0 2 51 111 53 0 GRP123-3.004 non_thm 0.0 2 1 143 1 32 0 0 155 2 95 951 257 0 GRP123-4.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 105 116 0 GRP123-4.004 non_thm 0.0 2 0 77 1 17 0 0 244 2 0 802 449 0 GRP123-6.003 theorem 0.0 2 1 50 0 11 0 0 0 2 50 143 82 0 GRP123-6.005 non_thm 0.1 2 0 264 4 27 0 0 453 2 0 1624 947 0 GRP123-7.003 theorem 0.0 2 1 56 0 16 0 0 0 2 56 149 82 0 GRP123-7.005 non_thm 0.1 2 0 284 4 41 0 0 453 2 0 1644 947 0 GRP123-8.003 theorem 0.0 2 1 62 0 21 0 0 0 2 62 156 87 0 GRP123-8.004 non_thm 0.0 2 0 177 2 33 0 0 234 2 0 879 372 0 GRP123-9.003 theorem 0.0 2 1 50 0 11 0 0 0 2 50 143 100 0 GRP123-9.004 non_thm 0.0 2 0 138 29 18 0 0 214 2 0 813 379 0 GRP124-1.004 theorem 0.0 2 2 72 1 17 0 0 20 2 64 392 155 0 GRP124-1.005 non_thm 0.1 2 0 142 5 26 0 0 255 2 0 1556 505 0 GRP124-2.004 theorem 0.0 2 1 75 0 26 0 0 0 2 75 182 111 0 GRP124-2.005 non_thm 0.1 2 0 173 2 40 0 0 258 2 0 1590 505 0 GRP124-3.004 theorem 0.0 2 2 117 1 32 0 0 31 2 106 337 171 0 GRP124-3.005 non_thm 0.1 2 2 244 4 47 0 0 331 2 176 1899 670 0 GRP124-4.004 theorem 0.0 2 2 66 1 17 0 0 50 2 62 293 350 0 GRP124-4.005 non_thm 0.1 2 0 143 4 26 0 0 566 2 0 1606 1305 0 GRP124-6.004 theorem 0.0 2 2 109 1 18 0 0 37 2 101 424 234 0 GRP124-6.005 non_thm 0.1 2 0 263 5 27 0 0 452 2 0 1624 947 0 GRP124-7.004 theorem 0.0 2 2 121 1 27 0 0 37 2 113 436 234 0 GRP124-7.005 non_thm 0.1 2 0 283 5 41 0 0 452 2 0 1644 947 0 GRP124-8.004 theorem 0.0 2 2 148 2 33 0 0 56 2 141 490 259 0 GRP124-8.005 non_thm 0.1 2 0 322 6 48 0 0 513 2 0 1739 1009 0 GRP124-9.004 theorem 0.0 2 2 109 1 18 0 0 37 2 101 424 266 0 GRP124-9.005 non_thm 0.1 2 0 263 50 27 0 0 457 2 0 1624 997 0 GRP125-1.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 94 43 0 GRP125-1.004 non_thm 0.0 2 0 77 1 17 0 0 111 2 0 469 180 0 GRP125-2.004 non_thm 0.0 2 0 96 0 26 0 0 112 2 0 490 180 0 GRP125-2.005 theorem 0.0 2 3 184 2 40 0 0 58 2 157 800 479 0 GRP125-3.004 non_thm 0.0 2 1 143 1 32 0 0 142 2 95 669 247 0 GRP125-3.005 theorem 0.1 2 5 280 4 47 0 0 131 2 219 1294 748 0 GRP125-4.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 146 117 0 GRP125-4.004 non_thm 0.0 2 0 77 1 17 0 0 257 2 0 719 462 0 GRP126-1.004 theorem 0.0 2 2 69 1 17 0 0 19 2 63 316 141 0 GRP126-1.005 non_thm 0.0 2 0 143 4 26 0 0 235 2 0 935 484 0 GRP126-2.004 theorem 0.0 2 1 75 0 26 0 0 0 2 75 224 111 0 GRP126-2.005 non_thm 0.0 2 0 173 2 40 0 0 237 2 0 969 484 0 GRP126-3.004 theorem 0.0 2 2 117 1 32 0 0 30 2 106 371 171 0 GRP126-3.005 non_thm 0.1 2 2 244 4 47 0 0 310 2 174 1271 649 0 GRP126-4.004 theorem 0.0 2 2 67 1 17 0 0 51 2 63 403 367 0 GRP126-4.005 non_thm 0.1 2 0 144 3 26 0 0 588 2 0 1427 1326 0 GRP127-1.004 theorem 0.0 2 2 72 1 17 0 0 19 2 64 352 151 0 GRP127-1.005 non_thm 0.0 2 0 145 2 26 0 0 237 2 0 935 484 0 GRP127-2.005 non_thm 0.0 2 1 187 1 40 0 0 239 2 130 1050 542 0 GRP127-2.006 theorem 0.1 2 3 313 2 57 0 0 85 2 253 1328 1321 0 GRP127-3.004 theorem 0.0 2 2 117 1 32 0 0 30 2 106 347 170 0 GRP127-3.005 non_thm 0.1 2 2 271 2 47 0 0 296 2 181 1407 744 0 GRP127-4.004 theorem 0.0 2 2 68 1 17 0 0 51 2 63 429 368 0 GRP127-4.005 non_thm 0.1 2 0 145 2 26 0 0 589 2 0 1427 1326 0 GRP128-1.003 theorem 0.0 2 4 59 3 9 0 0 5 2 32 200 90 0 GRP128-1.004 non_thm 0.0 2 7 171 8 16 0 0 143 2 48 925 392 0 GRP128-2.004 non_thm 0.0 2 1 100 3 25 0 0 122 2 40 537 198 0 GRP128-2.006 theorem 0.1 2 8 428 7 56 0 0 173 2 251 1751 1545 0 GRP128-3.004 non_thm 0.0 2 3 212 4 31 0 0 156 2 92 876 345 0 GRP128-3.005 theorem 0.1 2 7 395 6 46 0 0 78 2 207 1467 858 0 GRP128-4.003 theorem 0.0 2 4 28 3 9 0 0 9 2 28 193 108 0 GRP128-4.004 non_thm 0.0 2 5 83 6 16 0 0 275 2 54 884 512 0 GRP129-1.003 theorem 0.0 2 4 59 3 9 0 0 5 2 29 238 92 0 GRP129-1.005 non_thm 0.1 2 24 686 28 25 0 0 429 2 85 3378 2149 0 GRP129-2.004 theorem 0.0 2 7 164 7 25 0 0 47 2 78 599 258 0 GRP129-2.005 non_thm 0.1 2 10 316 15 39 0 0 300 2 122 1745 820 0 GRP129-3.004 theorem 0.0 2 7 236 7 31 0 0 140 2 115 783 344 0 GRP129-3.005 non_thm 0.1 2 7 390 9 46 0 0 519 2 171 1914 992 0 GRP129-4.004 theorem 0.0 2 9 116 8 16 0 0 35 2 51 665 526 0 GRP129-4.005 non_thm 0.1 2 13 234 16 25 0 0 658 2 49 2184 1880 0 GRP130-1.003 theorem 0.0 2 4 71 3 9 0 0 5 2 36 316 123 0 GRP130-1.005 non_thm 0.1 2 15 393 18 25 0 0 321 2 125 2174 1188 0 GRP130-2.003 theorem 0.0 2 3 68 2 14 0 0 6 2 43 282 104 0 GRP130-2.005 non_thm 0.0 2 3 248 4 39 0 0 254 2 136 1296 688 0 GRP130-3.003 theorem 0.0 2 2 94 1 19 0 0 2 2 68 289 108 0 GRP130-3.004 non_thm 0.0 2 2 202 2 31 0 0 154 2 83 826 334 0 GRP130-4.003 theorem 0.0 2 4 43 3 9 0 0 9 2 25 177 143 0 GRP130-4.004 non_thm 0.0 2 5 120 6 16 0 0 291 2 40 911 650 0 GRP131-1.002 theorem 0.0 2 2 20 1 4 0 0 0 2 14 81 32 0 GRP131-1.005 non_thm 0.1 2 0 147 8 25 0 0 272 2 0 1575 525 0 GRP131-2.002 theorem 0.0 2 2 22 1 6 0 0 0 2 16 84 32 0 GRP131-2.005 non_thm 0.7 2 80 1612 88 39 0 0 1489 2 172 16728 7868 0 GRP132-1.002 theorem 0.0 2 2 20 1 4 0 0 0 2 14 81 32 0 GRP132-1.005 non_thm 0.1 2 0 147 8 25 0 0 272 2 0 1575 525 0 GRP132-2.002 theorem 0.0 2 2 22 1 6 0 0 0 2 16 84 32 0 GRP132-2.005 non_thm 1.0 2 92 2522 99 39 0 0 1228 2 174 29511 12989 0 GRP133-1.003 theorem 0.0 2 4 80 3 9 0 0 5 2 33 340 139 0 GRP133-1.004 non_thm 0.0 0 1 87 3 16 0 0 122 2 52 530 211 0 GRP133-2.003 theorem 0.0 2 3 69 2 14 0 0 6 2 43 251 97 0 GRP133-2.004 non_thm 0.0 2 2 121 5 25 0 0 121 2 79 613 250 0 GRP134-1.003 theorem 0.0 2 4 92 3 9 0 0 5 2 34 434 169 0 GRP134-1.005 non_thm 0.1 2 6 219 10 25 0 0 256 2 138 1724 855 0 GRP134-2.003 theorem 0.0 2 3 86 2 14 0 0 6 2 44 352 127 0 GRP134-2.005 non_thm 0.1 2 6 456 11 39 0 0 368 2 171 3295 1717 0 GRP135-1.002 theorem 0.0 2 2 19 1 4 0 0 0 2 14 61 25 0 GRP135-1.005 non_thm 0.4 2 60 1853 64 25 0 0 1360 2 133 12748 6877 0 GRP135-2.002 theorem 0.0 2 2 21 1 6 0 0 0 2 16 63 25 0 GRP135-2.005 non_thm 0.2 2 20 828 21 39 0 0 545 2 168 5153 2994 0 HWV005-1 theorem 0.0 2 1 96 0 10 0 0 0 3 96 323 60 0 HWV005-2 unsound 0.0 2 0 160 1 8 0 0 43 3 0 305 46 0 HWV006-1 theorem 0.1 2 1 356 0 15 1 4 0 4 356 1440 162 0 HWV006-2 unsound 0.1 2 0 864 3 13 0 0 118 4 0 1699 124 0 HWV007-1 theorem 0.1 2 1 352 0 13 1 6 0 4 352 941 144 0 HWV007-2 unsound 0.1 2 0 707 2 11 1 0 117 4 0 1387 121 0 HWV008-1.001 theorem 0.1 2 1 215 0 11 0 0 0 5 215 653 133 0 HWV008-1.002 theorem 0.1 2 1 324 0 14 0 0 0 5 324 934 210 0 HWV008-2.001 theorem 0.1 2 1 215 0 9 0 0 0 5 215 601 100 0 HWV008-2.002 theorem 0.1 2 1 326 0 12 0 0 0 5 326 866 162 0 HWV034-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 HWV034-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 HWV035-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 HWV035-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 HWV036-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 HWV036-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 KRS001-1 theorem 0.0 2 1 8 0 1 0 0 0 2 8 16 19 0 KRS002-1 theorem 0.0 2 1 9 0 1 0 0 0 3 9 16 20 0 KRS003-1 theorem 0.0 2 1 9 0 2 0 0 0 2 9 16 18 0 KRS005-1 non_thm 0.0 2 0 8 0 1 0 0 36 2 0 8 36 0 KRS006-1 non_thm 0.0 2 0 20 3 5 0 0 64 3 0 31 71 0 KRS007-1 non_thm 0.0 2 0 27 2 2 0 0 74 3 0 37 85 0 KRS008-1 non_thm 0.1 2 0 42 34 2 0 0 528 3 0 72 810 0 KRS009-1 non_thm 0.0 2 0 43 8 1 0 0 229 3 0 65 237 0 KRS010-1 theorem 0.0 2 2 21 1 2 0 0 77 2 18 38 95 0 KRS011-1 non_thm 0.0 2 0 36 3 2 0 0 37 2 0 44 49 0 KRS012-1 theorem 0.0 2 1 5 0 2 0 0 0 2 5 10 5 0 KRS013-1 theorem 0.0 2 1 17 0 2 0 0 0 3 17 27 45 0 KRS014-1 non_thm 0.0 2 0 14 2 1 0 0 30 2 0 17 32 0 KRS015-1 theorem 0.0 2 1 10 0 1 0 0 0 3 10 18 22 0 KRS016-1 non_thm 0.0 2 0 4 4 2 0 0 10 2 0 4 14 0 KRS017-1 theorem 0.0 2 1 3 0 2 0 0 0 2 3 7 3 0 LCL181-2 theorem 0.0 2 1 2 0 4 2 0 0 2 2 4 2 0 LCL230-2 theorem 0.0 2 1 3 0 3 3 0 0 2 3 6 1 0 MGT004-1 theorem 0.0 2 1 15 0 9 0 0 0 2 15 26 12 0 MGT007-1 theorem 0.0 2 1 17 0 9 0 0 0 2 17 28 14 0 MGT016-1 theorem 0.0 2 1 16 0 13 0 0 0 2 16 26 3 0 MGT018-1 theorem 0.0 2 1 16 0 13 0 0 0 2 16 26 3 0 MGT022-1 theorem 0.0 2 2 8 1 7 3 0 0 3 7 19 6 0 MGT022-2 theorem 0.0 2 2 8 1 7 3 0 0 3 7 19 6 0 MGT028-1 theorem 0.0 2 2 13 1 2 0 0 1 4 11 27 15 0 MGT030-1 theorem 0.0 1 6 23 8 2 0 0 4 4 14 80 45 0 MGT036-1 theorem 0.0 0 1 9 0 4 0 0 0 2 9 15 10 0 MGT036-2 theorem 0.0 2 1 9 0 4 0 0 0 2 9 16 11 0 MGT041-2 theorem 0.0 0 1 7 0 4 0 0 0 2 7 9 3 0 MSC001-1 theorem 0.0 2 1 65 0 5 1 2 0 5 65 235 99 0 MSC002-1 theorem 0.0 2 1 22 0 3 1 0 0 4 22 42 36 0 MSC002-2 theorem 0.0 2 1 22 0 3 1 0 0 4 22 42 36 0 MSC003-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 9 5 0 MSC004-1 theorem 0.0 2 6 20 11 2 0 0 4 3 14 38 49 0 MSC006-1 theorem 0.0 2 6 47 22 2 0 0 196 2 30 193 537 0 MSC007-1.008 theorem 2.9 2 5040 55182 5039 65260 78952 0 3513 2 56 105582 27398 0 MSC008-1.002 timeout 300.0 5 MSC008-1.010 timeout 300.1 451 MSC008-2.002 timeout 300.0 4 MSC009-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 NLP001-1 theorem 0.0 2 2 28 1 28 5 0 0 2 19 32 30 0 NLP026-1 non_thm 0.0 2 0 4 5 5 3 0 5 2 0 4 10 0 NLP027-1 non_thm 0.0 2 0 4 5 5 4 0 7 2 0 4 12 0 NLP028-1 non_thm 0.0 2 0 5 5 6 4 0 8 2 0 5 13 0 NLP029-1 non_thm 0.0 2 0 4 5 5 4 0 5 2 0 4 10 0 NLP030-1 non_thm 0.0 2 0 5 5 6 4 0 7 2 0 5 12 0 NLP031-1 non_thm 0.0 2 6 38 12 12 5 0 17 4 20 77 99 0 NLP032-1 timeout 300.0 9 NLP033-1 non_thm 0.0 2 7 40 12 11 4 0 12 5 21 88 105 0 NLP034-1 timeout 300.0 34 NLP035-1 timeout 300.0 13 NLP043-1 non_thm 0.0 2 0 17 2 18 3 0 30 2 0 17 32 0 NLP044-1 non_thm 0.0 2 0 17 2 18 3 0 30 2 0 17 32 0 NLP045-1 non_thm 0.0 2 0 17 2 18 3 0 30 2 0 17 32 0 NLP046-1 non_thm 0.0 2 0 17 2 18 3 0 30 2 0 17 32 0 NLP047-1 non_thm 0.0 2 0 17 2 18 3 0 30 2 0 17 32 0 NLP048-1 non_thm 0.0 2 0 17 2 18 3 0 30 2 0 17 32 0 NLP059-1 non_thm 0.0 2 0 10 4 7 3 0 25 2 0 10 29 0 NLP060-1 non_thm 0.0 2 0 9 10 7 3 0 20 2 0 11 30 0 NLP061-1 non_thm 0.0 2 0 10 4 7 3 0 25 2 0 10 29 0 NLP062-1 non_thm 0.0 2 0 10 4 7 3 0 23 2 0 10 27 0 NLP063-1 non_thm 0.0 2 0 8 14 7 3 0 25 2 0 8 39 0 NLP064-1 non_thm 0.0 2 1 20 10 7 3 3 28 3 27 25 58 0 NLP065-1 non_thm 0.0 2 0 8 14 7 3 0 24 2 0 8 38 0 NLP066-1 non_thm 0.0 2 0 12 4 7 3 0 27 2 0 12 31 0 NLP067-1 non_thm 0.0 2 0 10 4 7 3 0 25 2 0 10 29 0 NLP068-1 non_thm 0.0 2 0 5 3 6 3 0 13 2 0 5 16 0 NLP079-1 theorem 0.0 2 2 40 1 38 4 0 0 2 22 82 54 0 NLP080-1 theorem 0.0 2 2 40 1 38 4 0 0 2 22 80 54 0 NLP081-1 theorem 0.0 2 2 38 1 36 4 0 0 2 21 76 51 0 NLP094-1 theorem 0.0 2 2 41 1 30 4 0 0 2 23 50 44 0 NLP095-1 non_thm 0.0 2 0 2 1 3 3 0 6 2 0 2 7 0 NLP096-1 non_thm 0.0 2 0 2 1 3 3 0 6 2 0 2 7 0 NLP097-1 non_thm 0.0 2 0 2 1 3 2 0 7 2 0 2 8 0 NLP098-1 non_thm 0.0 2 0 2 1 3 2 0 7 2 0 2 8 0 NLP099-1 non_thm 0.0 2 0 3 1 4 3 0 2 2 0 3 3 0 NLP100-1 non_thm 0.0 2 0 2 1 3 3 0 14 2 0 2 15 0 NLP101-1 non_thm 0.0 2 0 2 1 3 3 0 14 2 0 2 15 0 NLP102-1 non_thm 0.0 2 0 3 1 4 4 0 9 2 0 3 10 0 NLP103-1 non_thm 0.0 2 0 4 1 5 4 0 10 2 0 4 11 0 NLP114-1 non_thm 0.0 2 0 18 1 19 2 0 31 2 0 18 32 0 NLP115-1 non_thm 0.0 2 0 18 1 19 2 0 31 2 0 18 32 0 NLP116-1 non_thm 0.0 2 0 18 1 19 2 0 31 2 0 18 32 0 NLP117-1 theorem 0.0 2 2 34 1 34 5 0 0 2 19 38 48 0 NLP118-1 non_thm 0.0 2 1 34 1 35 4 0 16 2 19 36 48 0 NLP119-1 non_thm 0.0 2 1 34 1 35 4 0 16 2 19 36 48 0 NLP120-1 non_thm 0.0 2 0 18 1 19 2 0 31 2 0 18 32 0 NLP121-1 non_thm 0.0 2 0 18 1 19 2 0 31 2 0 18 32 0 NLP122-1 theorem 0.0 2 2 34 1 34 5 0 0 2 19 38 48 0 NLP123-1 non_thm 0.0 2 0 18 1 19 2 0 31 2 0 18 32 0 NLP130-1 non_thm 0.0 2 0 24 4 22 4 0 46 2 0 24 50 0 NLP131-1 non_thm 0.0 2 0 21 2 22 4 0 39 2 0 21 41 0 NLP132-1 non_thm 0.0 2 0 21 3 22 4 0 39 2 0 21 42 0 NLP133-1 non_thm 0.0 2 0 21 3 22 4 0 39 2 0 21 42 0 NLP134-1 non_thm 0.0 2 0 21 2 22 4 0 38 2 0 21 40 0 NLP135-1 non_thm 0.0 2 0 24 4 22 4 0 46 2 0 24 50 0 NLP136-1 non_thm 0.0 2 1 43 2 42 5 0 20 2 25 46 62 0 NLP137-1 non_thm 0.0 2 0 30 4 22 4 0 50 3 0 30 58 0 NLP138-1 non_thm 0.0 2 1 43 2 42 5 0 20 2 25 46 62 0 NLP139-1 non_thm 0.0 2 0 30 4 22 4 0 50 3 0 30 58 0 NLP160-1 non_thm 0.0 2 0 26 4 27 4 0 87 2 0 26 91 0 NLP161-1 non_thm 0.0 2 0 26 4 27 4 0 87 2 0 26 91 0 NLP162-1 non_thm 0.0 2 0 26 4 27 4 0 87 2 0 26 91 0 NLP163-1 non_thm 0.0 2 1 54 4 52 5 0 25 2 31 57 80 0 NLP164-1 non_thm 0.0 2 1 54 4 52 5 0 25 2 31 57 80 0 NLP165-1 non_thm 0.0 2 1 54 4 52 5 0 25 2 31 57 80 0 NLP166-1 non_thm 0.0 2 0 26 4 27 4 0 87 2 0 26 91 0 NLP167-1 non_thm 0.0 2 0 26 4 27 4 0 87 2 0 26 91 0 NLP168-1 non_thm 0.0 0 0 26 4 27 4 0 87 2 0 26 91 0 NLP169-1 non_thm 0.0 2 0 26 4 27 4 0 87 2 0 26 91 0 NLP190-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP191-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP192-1 non_thm 0.0 1 0 33 4 34 4 0 73 2 0 33 77 0 NLP193-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP194-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP195-1 non_thm 0.0 1 0 33 4 34 4 0 73 2 0 33 77 0 NLP196-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP197-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP198-1 non_thm 0.0 1 0 33 4 34 4 0 73 2 0 33 77 0 NLP199-1 non_thm 0.0 2 0 33 4 34 4 0 73 2 0 33 77 0 NLP221-1 non_thm 0.0 2 0 20 1 21 4 0 34 2 0 20 35 0 NLP222-1 non_thm 0.0 2 0 20 1 21 4 0 34 2 0 20 35 0 NLP223-1 non_thm 0.0 2 0 19 1 20 4 0 33 2 0 19 34 0 NLP230-1 non_thm 0.1 2 1 78 1 78 5 0 36 3 43 83 113 0 NLP231-1 non_thm 0.0 2 0 37 1 38 4 0 69 2 0 37 70 0 NLP232-1 non_thm 0.0 1 0 38 1 39 4 0 70 2 0 38 71 0 NLP233-1 non_thm 0.0 2 0 39 1 38 4 0 70 2 0 39 71 0 NLP234-1 non_thm 0.0 2 0 38 1 39 4 0 70 2 0 38 71 0 NLP235-1 non_thm 0.0 2 0 37 1 38 4 0 69 2 0 37 70 0 NLP236-1 non_thm 0.0 2 0 37 1 38 4 0 69 2 0 37 70 0 NLP237-1 non_thm 0.0 2 0 38 1 39 4 0 70 2 0 38 71 0 NLP238-1 non_thm 0.0 2 0 37 1 38 4 0 69 2 0 37 70 0 NLP239-1 non_thm 0.0 2 0 37 1 38 4 0 69 2 0 37 70 0 NUM014-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 11 4 0 NUM015-1 theorem 0.0 1 1 11 0 2 0 0 0 3 11 21 14 0 NUM016-1 theorem 0.0 2 1 14 0 4 0 0 0 3 14 36 12 0 NUM016-2 theorem 0.0 2 1 12 0 2 0 0 0 3 12 18 8 0 NUM021-1 theorem 0.0 2 1 80 0 9 0 0 0 3 80 405 210 0 NUM022-1 theorem 0.0 2 1 9 0 3 0 0 0 3 9 14 5 0 NUM025-2 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 8 0 NUM027-1 theorem 0.0 2 1 49 0 10 0 0 0 2 49 247 142 0 NUM285-1 non_thm 0.0 2 0 16 5 23 44 0 12 2 0 16 17 0 NUM288-1 timeout 300.0 21 PLA002-1 theorem 0.0 2 1 7 0 6 8 0 0 2 7 10 3 0 PLA002-2 theorem 4.2 32 1 1994 0 2 0 0 0 5 1994 2625 611529 0 PUZ001-1 theorem 0.0 2 1 17 0 5 2 0 0 2 17 20 8 0 PUZ001-3 non_thm 0.0 2 0 19 0 6 2 0 10 2 0 22 11 0 PUZ002-1 theorem 0.0 2 1 11 0 2 0 0 0 2 11 13 5 0 PUZ004-1 theorem 0.0 2 1 10 0 10 11 0 0 2 10 12 3 0 PUZ005-1 theorem 0.0 2 2 26 1 3 0 0 0 2 21 83 164 0 PUZ009-1 theorem 0.0 2 1 5 0 6 11 0 0 2 5 11 11 0 PUZ010-1 theorem 1.2 2 344 6918 359 1227 446 0 4981 2 204 20149 27734 0 PUZ012-1 theorem 0.0 2 1 20 0 13 1 0 0 2 20 36 20 0 PUZ013-1 theorem 0.0 2 1 7 0 10 10 0 0 2 7 12 10 0 PUZ014-1 theorem 0.0 2 2 16 1 21 22 0 10 2 13 22 17 0 PUZ015-2.006 theorem 0.1 2 162 2673 165 3003 5888 0 256 2 59 3942 3040 0 PUZ016-2.004 non_thm 0.0 2 0 22 2 29 39 0 22 2 0 27 35 0 PUZ016-2.005 theorem 0.0 2 26 362 25 417 789 0 28 2 40 522 408 0 PUZ017-1 theorem 0.0 2 5 302 4 85 1 5 403 2 231 1159 1598 0 PUZ018-1 theorem 0.0 2 1 53 0 41 6 0 0 2 53 84 891 0 PUZ018-2 non_thm 0.1 2 2 89 22 40 6 0 1971 2 109 163 3101 0 PUZ019-1 theorem 0.0 2 1 116 0 44 1 3 0 2 116 333 577 0 PUZ021-1 theorem 0.1 2 13 195 66 0 0 6 339 3 55 877 3786 0 PUZ023-1 theorem 0.0 2 2 10 2 8 6 0 4 2 11 30 16 0 PUZ024-1 theorem 0.0 2 1 7 0 9 7 0 0 2 7 19 7 0 PUZ025-1 theorem 0.0 2 8 37 9 7 4 0 40 2 22 223 184 0 PUZ026-1 theorem 0.0 2 3 29 2 12 5 3 10 2 18 99 61 0 PUZ027-1 theorem 0.0 2 3 18 2 13 14 0 1 2 12 73 40 0 PUZ028-1 non_thm 0.0 2 0 31 15 11 0 0 20 2 0 91 35 0 PUZ028-2 non_thm 0.0 2 0 70 18 36 0 0 16 2 0 190 46 0 PUZ028-3 non_thm 0.0 2 0 70 18 88 154 0 16 2 0 190 46 0 PUZ028-4 non_thm 0.0 2 0 28 18 46 106 0 16 2 0 136 46 0 PUZ028-5 theorem 0.1 2 30 742 29 11 0 0 97 2 90 1674 246 0 PUZ028-6 theorem 0.0 2 20 376 19 36 0 0 102 2 82 1298 292 0 PUZ029-1 theorem 0.0 2 1 13 0 4 0 0 0 2 13 17 14 0 PUZ030-1 theorem 0.0 2 24 327 24 363 397 0 115 2 28 887 1001 0 PUZ030-2 theorem 0.0 2 9 35 8 51 173 0 11 2 10 96 96 0 PUZ031-1 theorem 0.0 2 1 33 0 6 0 0 0 2 33 56 30 0 PUZ032-1 theorem 0.0 2 2 16 1 4 0 0 6 3 16 54 17 0 PUZ033-1 theorem 0.0 2 1 11 0 11 17 0 0 2 11 15 8 0 PUZ034-1.003 timeout 300.0 59 PUZ034-1.004 timeout 300.0 58 PUZ035-1 theorem 0.0 2 4 16 3 13 17 0 1 2 9 41 14 0 PUZ035-2 theorem 0.0 2 4 25 3 20 30 1 6 2 12 55 30 0 PUZ035-3 theorem 0.0 2 4 12 3 6 8 0 2 2 8 27 6 0 PUZ035-4 theorem 0.0 2 4 12 3 6 8 0 2 2 8 27 6 0 PUZ035-5 theorem 0.0 2 4 7 4 5 0 0 0 2 6 27 20 0 PUZ035-6 theorem 0.0 2 4 5 4 5 0 0 7 2 6 20 31 0 PUZ035-7 theorem 0.1 2 12 217 32 8 0 0 366 3 81 882 2294 0 PUZ044-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 PUZ045-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 SET001-1 theorem 0.0 2 1 4 0 3 0 0 0 2 4 8 3 0 SET002-1 theorem 0.0 2 3 9 3 2 0 0 0 2 8 21 22 0 SET003-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 9 6 0 SET004-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 8 5 0 SET005-1 theorem 0.0 2 2 135 1 4 0 0 0 2 131 378 143 0 SET006-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 10 7 0 SET007-1 theorem 0.1 2 3 578 2 5 0 38 0 2 339 2353 722 0 SET008-1 theorem 0.0 2 1 10 0 3 0 0 0 2 10 34 21 0 SET009-1 theorem 0.0 2 1 22 0 4 0 0 0 2 22 41 17 0 SET010-1 theorem 0.1 2 3 835 2 5 0 61 0 2 486 3402 997 0 SET011-1 theorem 0.0 2 2 73 1 3 0 0 0 2 67 239 94 0 SET012-1 timeout 300.0 54 SET012-2 theorem 0.1 2 3 131 2 6 0 0 510 2 102 1735 1045 0 SET013-1 timeout 300.0 70 SET013-2 theorem 0.2 3 3 609 2 6 0 0 510 2 336 6941 2910 0 SET014-2 timeout 300.0 26 SET015-1 timeout 300.0 63 SET015-2 theorem 0.1 2 3 381 2 6 0 0 510 2 222 4397 1954 0 SET043-5 theorem 0.0 2 4 0 3 0 0 0 0 2 2 8 9 0 SET044-5 theorem 0.0 2 8 8 13 0 0 0 18 2 6 32 79 0 SET045-5 theorem 0.0 2 6 2 6 1 0 0 8 2 6 15 34 0 SET046-5 theorem 0.0 2 4 4 3 0 0 0 1 2 4 18 19 0 SET047-5 theorem 0.0 2 4 6 3 4 4 0 1 2 4 24 15 0 SET055-6 theorem 112.3 10 51 17443 108 30 0 204 273966 2 5353 370551 283070 0 SET055-7 theorem 0.0 2 1 5 0 5 0 0 0 2 5 47 15 0 SET777-1 non_thm 0.0 2 0 0 2 0 0 0 2 2 0 0 4 0 SET778-1 non_thm 0.0 2 0 0 3 0 0 0 2 2 0 0 5 0 SET779-1 non_thm 0.0 2 0 0 3 0 0 0 3 2 0 0 6 0 SET780-1 non_thm 0.0 2 0 0 3 0 0 0 2 2 0 0 5 0 SET781-1 timeout 300.0 28 SET786-1 theorem 0.0 2 4 4 3 0 0 0 1 2 4 16 18 0 SWV001-1 theorem 0.0 2 2 10 1 2 0 0 5 2 9 39 21 0 SWV009-1 theorem 0.0 2 1 9 0 5 0 0 0 2 9 12 4 0 SYN001-1.005 theorem 0.0 2 16 16 15 46 118 0 0 2 5 96 31 0 SYN002-1.007.008 theorem 0.1 2 2 0 37 0 0 0 234 23 22 0 309 0 SYN006-1 theorem 0.0 2 1 6 0 4 1 0 0 3 6 7 2 0 SYN008-1 theorem 0.0 2 1 3 0 3 4 0 0 2 3 6 4 0 SYN009-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 18 48 0 SYN009-2 theorem 0.0 2 1 7 0 4 0 0 0 2 7 9 30 0 SYN009-3 theorem 0.0 2 1 9 0 5 1 0 0 2 9 11 31 0 SYN009-4 theorem 0.0 2 1 8 0 4 0 0 0 2 8 10 58 0 SYN011-1 theorem 0.0 2 2 9 1 11 13 0 0 2 7 13 9 0 SYN012-1 theorem 0.0 2 9 0 37 0 0 0 111 5 16 0 182 0 SYN014-2 theorem 0.0 2 1 8 0 7 0 0 0 2 8 36 22 0 SYN015-2 theorem 0.0 2 1 33 0 7 0 0 0 2 33 149 81 0 SYN028-1 theorem 0.0 2 1 5 0 5 7 0 0 2 5 7 4 0 SYN029-1 theorem 0.0 2 2 3 1 5 7 0 0 2 3 7 3 0 SYN030-1 theorem 0.0 2 2 5 1 7 11 0 0 2 5 10 6 0 SYN031-1 theorem 0.0 2 3 5 2 0 0 0 0 2 4 19 20 0 SYN032-1 theorem 0.0 2 3 7 2 11 14 0 0 2 5 13 9 0 SYN034-1 theorem 0.0 2 4 4 3 0 0 0 1 2 4 16 18 0 SYN036-1 theorem 6.4 10 46 118 45 196 350 3 28018 2 18 238903 374388 0 SYN036-2 non_thm 0.0 2 0 0 1 16 44 0 0 2 0 0 1 0 SYN036-3 theorem 0.0 2 10 67 9 95 142 5 22 2 17 111 79 0 SYN036-4 theorem 0.0 2 8 9 7 46 98 6 1 2 5 61 56 0 SYN037-1 theorem 0.0 2 9 71 8 101 166 11 20 2 17 113 80 0 SYN037-2 theorem 0.0 2 12 22 15 68 87 8 20 2 11 78 71 0 SYN038-1 theorem 0.0 2 9 0 37 0 0 0 111 5 16 0 182 0 SYN039-1 theorem 0.2 2 17 20 53 62 0 12 1377 4 16 106 3001 0 SYN044-1 theorem 0.0 2 2 4 1 6 9 0 0 2 3 8 4 0 SYN045-1 theorem 0.0 2 1 3 0 3 3 0 0 2 3 5 4 0 SYN047-1 theorem 0.0 2 1 4 0 4 6 0 0 2 4 7 2 0 SYN051-1 theorem 0.0 2 2 2 1 6 6 0 0 2 2 6 3 0 SYN052-1 theorem 0.0 2 2 2 1 3 5 0 0 2 2 7 3 0 SYN053-1 theorem 0.0 2 2 1 1 4 4 0 0 2 2 8 6 0 SYN054-1 theorem 0.0 2 2 5 1 2 1 0 0 2 4 9 6 0 SYN055-1 theorem 0.0 2 1 9 0 3 0 0 0 2 9 12 9 0 SYN056-1 non_thm 0.0 2 0 2 2 4 0 0 2 2 0 2 4 0 SYN059-1 non_thm 0.0 2 0 5 7 7 11 0 92 2 0 24 99 0 SYN060-1 theorem 0.0 2 1 3 0 1 0 0 0 2 3 5 6 0 SYN061-1 theorem 0.0 2 1 5 0 2 0 0 0 2 5 7 2 0 SYN063-1 theorem 0.0 2 1 2 0 2 5 0 0 2 2 6 0 0 SYN066-1 theorem 0.0 2 1 4 0 5 3 1 0 2 4 6 2 0 SYN067-1 theorem 16.1 3 375 3049 395 547 853 0 42808 2 41 14501 387750 0 SYN067-2 theorem 45.2 3 1030 9078 1055 1673 1909 0 149394 2 52 49149 1115044 0 SYN067-3 theorem 4.0 2 278 3043 313 481 483 0 33468 2 42 9936 188724 0 SYN069-1 theorem 0.0 2 1 9 0 1 0 0 0 2 9 16 13 0 SYN070-1 theorem 0.0 2 1 15 0 4 0 0 0 2 15 37 78 0 SYN081-1 theorem 0.0 2 2 0 4 0 0 0 4 3 3 0 10 0 SYN082-1 theorem 0.0 2 3 3 2 4 5 0 0 3 3 18 11 0 SYN084-1 non_thm 0.0 2 0 1 1 7 14 1 0 2 0 1 1 0 SYN084-2 theorem 0.0 2 4 17 4 11 19 0 5 3 9 29 39 0 SYN091-1.003 non_thm 0.0 2 0 2 4 6 6 0 3 2 0 3 7 0 SYN092-1.003 non_thm 0.0 2 0 0 9 9 7 0 6 2 0 0 15 0 SYN093-1.002 theorem 0.0 2 2 10 1 12 15 0 0 2 8 16 8 0 SYN094-1.005 theorem 5.6 2 16384 68034 18882 103299 127999 0 40441 2 45 133570 108485 0 SYN097-1.002 theorem 0.0 2 2 14 1 16 20 0 3 2 12 20 13 0 SYN098-1.002 theorem 0.0 2 32 147 47 225 260 0 73 2 31 275 230 0 SYN099-1.003 theorem 0.0 2 1 16 0 14 2 0 0 2 16 35 12 0 SYN100-1.005 theorem 0.0 2 1 42 0 8 0 0 0 2 42 83 37 0 SYN304-1 non_thm 0.0 2 0 6 1 6 0 0 3 2 0 9 4 0 SYN306-1 timeout 300.0 5 SYN307-1 non_thm 0.0 2 0 2 1 2 0 0 5 2 0 4 6 0 SYN308-1 non_thm 0.0 2 0 1 2 2 0 0 0 3 0 1 2 0 SYN309-1 non_thm 0.0 2 0 2 2 4 0 0 0 2 0 2 2 0 SYN313-1.001.002 theorem 6.5 3 1035 4805 2361 0 0 4 9206 29 58 6015 28745 0 SYN314-1.002.001 timeout 300.0 10 SYN315-1 theorem 0.0 2 2 2 1 4 4 0 0 2 2 6 3 0 SYN316-1 timeout 300.0 2 SYN317-1 non_thm 0.0 2 0 2 0 3 3 0 0 2 0 2 0 0 SYN319-1 theorem 0.0 2 1 3 0 3 1 0 0 2 3 5 2 0 SYN320-1 non_thm 0.0 2 0 2 1 2 0 0 0 2 0 2 1 0 SYN321-1 theorem 0.0 2 2 2 1 3 3 0 0 2 2 7 3 0 SYN323-1 theorem 0.0 2 3 2 3 0 0 0 0 2 3 6 7 0 SYN324-1 timeout 300.0 2 SYN325-1 theorem 0.0 2 1 2 0 1 1 0 0 2 2 3 3 0 SYN326-1 theorem 0.0 2 1 4 0 3 3 0 0 2 4 6 4 0 SYN327-1 theorem 0.0 2 4 4 3 0 0 0 0 2 4 22 25 0 SYN328-1 theorem 0.0 2 18 0 74 0 0 0 408 6 17 0 624 0 SYN330-1 timeout 300.0 27 SYN331-1 theorem 0.0 2 1 6 0 4 0 0 0 4 6 15 7 0 SYN332-1 theorem 0.7 2 3 0 98 0 0 0 2065 5 96 0 2739 0 SYN334-1 theorem 0.0 2 9 0 37 0 0 0 111 5 16 0 182 0 SYN335-1 timeout 300.0 51 SYN343-1 theorem 0.0 2 2 1 1 3 2 0 0 2 2 5 2 0 SYN344-1 non_thm 0.0 2 0 0 2 2 0 0 0 2 0 0 2 0 SYN345-1 theorem 0.0 2 4 6 3 11 14 0 0 2 4 19 12 0 SYN347-1 theorem 0.0 2 12 10 14 4 4 0 23 2 8 64 82 0 SYN348-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 SYN349-1 theorem 0.0 2 17 0 29 0 0 0 109 3 9 0 373 0 SYN350-1 theorem 0.0 2 5 4 6 0 0 0 19 3 8 20 57 0 SYN351-1 timeout 300.0 30 SYN352-1 theorem 0.0 2 4 5 7 1 0 0 44 3 11 8 85 0 SYN353-1 timeout 300.0 9 SYN354-1 theorem 0.0 2 3 2 2 2 0 0 0 2 4 15 6 0 SYN418-1 non_thm 0.1 2 0 59 57 89 95 0 276 2 0 77 352 0 SYN419-1 non_thm 0.0 2 0 47 43 75 103 0 215 2 0 54 276 0 SYN420-1 non_thm 0.1 2 1 80 106 111 136 0 1223 2 90 116 1449 0 SYN421-1 non_thm 0.0 2 0 45 61 80 97 0 265 2 0 54 341 0 SYN422-1 non_thm 0.1 2 0 47 63 66 107 0 247 2 0 57 358 0 SYN423-1 non_thm 0.1 2 0 140 83 133 132 0 496 2 0 156 619 0 SYN424-1 non_thm 0.1 3 0 115 114 131 149 0 1176 2 0 128 1460 0 SYN425-1 non_thm 0.1 2 0 140 97 114 124 0 1028 2 0 164 1326 0 SYN426-1 non_thm 0.2 3 1 140 161 180 204 4 1413 2 4 174 1680 0 SYN427-1 non_thm 0.2 3 0 165 90 172 151 0 1449 2 0 177 1553 0 SYN428-1 non_thm 0.8 4 2 222 252 154 176 0 9998 2 422 299 13589 0 SYN429-1 non_thm 0.1 2 1 107 55 117 147 0 369 2 66 153 459 0 SYN430-1 non_thm 0.0 2 0 36 11 45 15 0 150 2 0 41 218 0 SYN431-1 non_thm 0.0 2 1 45 13 57 19 0 166 2 13 50 217 0 SYN432-1 non_thm 0.0 2 0 54 16 69 21 0 548 2 0 56 628 0 SYN433-1 non_thm 0.9 4 2 58 19 65 26 0 17464 2 61 147 36506 0 SYN434-1 non_thm 5.3 10 3 125 30 133 43 0 110723 2 126 913 170631 0 SYN435-1 non_thm 0.2 2 0 91 27 113 32 0 4102 2 0 173 4361 0 SYN436-1 theorem 10.8 4 155 2420 169 2157 965 0 155551 2 82 7784 785873 0 SYN437-1 non_thm 0.9 3 18 280 36 276 106 0 12455 2 91 1969 46685 0 SYN438-1 non_thm 0.8 3 20 174 31 180 100 0 18669 2 55 974 43052 0 SYN439-1 theorem 4.7 3 276 5688 300 5168 2107 0 24076 2 92 15814 269376 0 SYN440-1 timeout 300.0 8 SYN441-1 non_thm 7.9 4 64 1250 91 1155 419 0 94010 2 110 10769 306655 0 SYN442-1 theorem 24.1 6 187 3127 215 2817 1237 0 362360 2 100 12688 1273397 0 SYN443-1 theorem 2.0 4 65 1031 65 963 487 0 18221 2 78 3224 172214 0 SYN444-1 theorem 1.1 2 82 1143 83 1046 479 0 10263 2 77 5263 66729 0 SYN445-1 theorem 4.0 4 49 942 52 849 374 0 51895 2 93 3383 279924 0 SYN446-1 non_thm 0.7 3 13 261 22 245 110 0 9716 2 83 1400 39281 0 SYN447-1 theorem 103.3 17 457 9695 498 8215 3795 0 858035 2 130 37227 7372493 0 SYN448-1 theorem 5.3 3 179 2678 198 2469 1242 0 45453 2 88 8473 375481 0 SYN449-1 non_thm 6.2 3 217 3235 230 2870 1424 0 57177 2 89 14292 357543 0 SYN450-1 theorem 0.5 2 54 688 55 641 327 0 6033 2 72 2264 29567 0 SYN451-1 theorem 1.0 2 59 768 69 726 367 0 12740 2 61 2621 52599 0 SYN452-1 theorem 1.5 3 81 934 91 879 426 0 21197 2 81 3285 86421 0 SYN453-1 non_thm 6.3 11 58 1502 83 1337 482 0 72109 2 139 7286 199615 0 SYN454-1 theorem 1.8 3 69 1107 71 1003 481 0 14576 2 69 3635 121783 0 SYN455-1 theorem 19.0 4 151 2232 201 2095 1030 0 363267 2 96 10627 969590 0 SYN456-1 non_thm 9.6 9 273 2954 307 2766 1464 0 172249 2 77 16121 517518 0 SYN457-1 timeout 300.0 8 SYN458-1 theorem 1.0 2 36 759 37 708 317 0 3538 2 85 2146 84352 0 SYN459-1 theorem 2.2 3 80 1222 85 1103 548 0 21145 2 74 4603 184295 0 SYN460-1 theorem 4.1 3 121 2500 133 2281 942 0 10864 2 84 9219 330230 0 SYN461-1 theorem 0.9 3 78 913 80 862 473 0 10628 2 58 3143 59260 0 SYN462-1 theorem 2.0 3 60 938 64 858 421 0 32534 2 67 3915 151631 0 SYN463-1 non_thm 0.3 2 3 75 14 81 37 0 5707 2 65 167 8845 0 SYN464-1 non_thm 25.8 8 77 1348 125 1315 526 0 389099 2 133 12439 1318769 0 SYN465-1 theorem 1.9 3 73 1208 75 1056 501 0 20007 2 70 5074 118020 0 SYN466-1 theorem 1.8 3 82 1257 88 1160 550 0 18647 2 85 5946 94411 0 SYN467-1 theorem 0.7 3 40 657 41 604 295 0 5653 2 60 2448 47886 0 SYN468-1 theorem 2.0 3 120 1808 131 1656 862 0 12051 2 110 7658 118224 0 SYN469-1 theorem 3.9 3 145 2261 149 2004 1005 0 42323 2 64 8031 327055 0 SYN470-1 theorem 4.0 3 139 2671 145 2399 1064 0 25050 2 95 9250 252092 0 SYN471-1 theorem 5.8 5 56 652 57 617 320 0 118950 2 80 3929 331204 0 SYN472-1 theorem 5.6 3 141 1843 151 1690 863 0 76102 2 66 9969 443102 0 SYN473-1 theorem 3.0 3 91 1423 92 1249 645 0 22384 2 76 6440 260700 0 SYN474-1 theorem 4.0 3 139 2238 143 2015 1050 0 33740 2 72 8370 306127 0 SYN475-1 theorem 3.5 3 80 1273 81 1161 608 0 44624 2 65 4571 302466 0 SYN476-1 theorem 1.8 3 124 1999 129 1811 926 0 11779 2 84 7377 91167 0 SYN477-1 theorem 1.2 3 57 621 62 590 332 0 18903 2 55 2914 95528 0 SYN478-1 theorem 4.6 4 142 2166 144 2014 1096 0 43904 2 67 7654 335716 0 SYN479-1 theorem 1.2 3 40 588 43 551 324 0 9658 2 79 2277 119341 0 SYN480-1 theorem 2.0 3 74 1009 76 911 496 0 25997 2 62 3980 144682 0 SYN481-1 theorem 4.6 3 126 1763 130 1564 846 0 53446 2 73 7292 366443 0 SYN482-1 theorem 1.8 3 94 1240 101 1129 602 0 22128 2 74 7091 79523 0 SYN483-1 theorem 1.3 3 66 1143 65 1034 544 0 9226 2 66 3845 85414 0 SYN484-1 theorem 0.7 3 32 507 32 465 228 0 4942 2 54 1887 63805 0 SYN485-1 theorem 1.5 3 41 717 40 661 326 0 15446 2 81 2442 118120 0 SYN486-1 theorem 1.3 3 76 1035 75 956 525 0 12432 2 58 4277 117983 0 SYN487-1 theorem 5.0 3 142 2467 161 2252 1139 0 58459 2 101 10776 219600 0 SYN488-1 theorem 6.1 4 168 2893 182 2599 1286 0 52463 2 82 12235 369476 0 SYN489-1 theorem 0.7 3 43 950 44 861 412 0 3221 2 76 3031 37252 0 SYN490-1 non_thm 0.0 2 0 13 4 17 6 0 15 2 0 14 19 0 SYN491-1 non_thm 0.0 2 0 10 3 13 7 0 18 2 0 11 21 0 SYN492-1 non_thm 0.0 2 0 7 2 9 6 0 7 2 0 7 9 0 SYN493-1 non_thm 0.0 2 0 10 3 13 7 0 8 2 0 10 11 0 SYN494-1 non_thm 0.0 2 0 7 2 9 5 0 12 2 0 7 14 0 SYN495-1 non_thm 0.0 2 0 25 8 33 10 0 42 2 0 27 50 0 SYN496-1 non_thm 0.0 2 0 7 2 9 6 0 5 2 0 8 7 0 SYN497-1 non_thm 0.0 2 0 13 4 17 6 0 12 2 0 14 16 0 SYN498-1 theorem 3.3 4 92 1438 93 1338 704 0 30610 2 76 5327 278183 0 SYN499-1 theorem 7.7 4 86 1231 90 1131 600 0 102811 2 85 9744 447168 0 SYN500-1 theorem 1.9 3 73 985 74 889 468 0 17718 2 62 4381 192180 0 SYN501-1 theorem 0.8 3 25 390 24 356 184 0 6196 2 63 1488 62545 0 SYN502-1 theorem 5.4 4 112 2491 117 2184 987 0 37407 2 79 11088 417679 0 SYN503-1 theorem 0.9 3 56 658 58 623 356 0 11697 2 66 3451 60444 0 SYN504-1 theorem 2.9 3 42 532 63 517 274 0 44829 2 75 4107 184741 0 SYN505-1 theorem 1.0 3 80 920 86 883 537 0 15141 2 72 3107 69327 0 SYN506-1 theorem 0.4 3 21 431 21 398 191 0 2390 2 69 1456 21725 0 SYN507-1 theorem 3.4 3 85 1465 84 1324 636 0 40780 2 89 5187 206958 0 SYN508-1 theorem 7.6 3 120 1443 128 1366 767 0 144439 2 84 10685 366278 0 SYN509-1 theorem 0.6 2 54 682 54 635 383 0 5370 2 54 2453 45739 0 SYN510-1 theorem 1.9 3 131 1906 141 1781 907 0 17555 2 77 6806 122006 0 SYN511-1 theorem 1.1 3 60 803 63 738 409 0 8691 2 80 4566 37402 0 SYN512-1 theorem 1.5 3 66 1626 68 1488 683 0 10077 2 86 4118 82821 0 SYN513-1 non_thm 0.1 2 3 103 79 76 107 0 1352 2 141 174 2228 0 SYN514-1 non_thm 0.1 2 1 73 36 65 79 0 460 2 5 94 581 0 SYN515-1 non_thm 0.0 2 0 7 11 14 22 0 26 2 0 8 37 0 SYN516-1 non_thm 0.0 2 0 0 6 6 12 0 14 2 0 0 20 0 SYN517-1 non_thm 0.0 2 1 15 7 21 24 0 33 2 18 23 49 0 SYN518-1 non_thm 0.3 3 0 143 67 129 98 0 2137 2 0 158 4152 0 SYN519-1 timeout 300.0 180 SYN520-1 timeout 300.0 347 SYN521-1 non_thm 0.0 2 0 16 11 24 16 0 82 2 0 18 93 0 SYN522-1 non_thm 0.0 2 0 13 17 17 29 0 66 2 0 15 83 0 SYN523-1 non_thm 0.0 2 0 2 10 11 13 0 16 2 0 2 26 0 SYN524-1 non_thm 0.0 2 0 10 10 17 25 0 34 2 0 11 47 0 SYN525-1 non_thm 0.0 2 0 8 14 18 27 0 36 2 0 11 50 0 SYN526-1 non_thm 0.0 2 0 9 10 17 28 0 27 2 0 11 37 0 SYN527-1 non_thm 0.0 2 0 12 9 17 24 0 22 2 0 14 36 0 SYN528-1 non_thm 0.0 2 0 6 14 11 21 0 37 2 0 7 51 0 SYN529-1 non_thm 0.0 2 0 24 16 35 33 0 84 2 0 30 128 0 SYN530-1 non_thm 0.0 2 0 7 12 10 20 0 35 2 0 8 48 0 SYN531-1 non_thm 0.0 2 0 16 18 24 28 0 45 2 0 17 71 0 SYN532-1 non_thm 0.0 2 0 20 11 25 34 0 59 2 0 24 75 0 SYN533-1 non_thm 0.0 2 0 13 12 22 20 0 45 2 0 15 57 0 SYN534-1 non_thm 0.0 2 0 12 10 20 26 0 26 2 0 14 42 0 SYN535-1 non_thm 0.0 2 0 5 11 15 26 0 27 2 0 6 39 0 SYN536-1 non_thm 0.0 2 0 15 9 24 25 0 35 2 0 17 44 0 SYN537-1 non_thm 0.0 2 0 28 11 27 36 0 48 2 0 31 82 0 SYN538-1 non_thm 0.0 2 0 2 13 10 27 0 24 2 0 3 37 0 SYN539-1 non_thm 0.0 2 0 7 12 14 31 0 30 2 0 9 45 0 SYN540-1 non_thm 0.0 2 3 27 16 39 60 0 55 2 30 58 111 0 SYN541-1 non_thm 0.0 2 0 22 21 33 39 0 80 2 0 22 102 0 SYN542-1 non_thm 7.4 13 0 133 75 141 41 0 164627 2 0 664 201357 0 SYN543-1 non_thm 8.3 14 0 132 68 133 38 0 154890 2 0 1066 209617 0 SYN544-1 non_thm 0.1 2 2 140 79 94 85 0 1746 2 174 177 1926 0 SYN545-1 non_thm 0.1 2 3 63 70 76 105 0 482 2 112 124 696 0 SYN546-1 non_thm 0.1 2 0 92 78 104 107 0 826 2 0 110 1065 0 SYN547-1 non_thm 0.1 2 1 75 60 79 116 0 402 2 6 106 561 0 SYN554-1 theorem 0.0 2 1 10 0 4 0 0 0 2 10 43 22 0 SYN560-1 theorem 0.6 3 1 39 0 6 0 0 0 5 39 1011 987 0 SYN567-1 theorem 0.0 2 1 8 0 7 0 0 0 4 8 25 11 0 SYN568-1 theorem 0.0 2 1 8 0 6 0 0 0 5 8 29 16 0 SYN571-1 theorem 0.0 2 1 23 0 6 0 0 0 3 23 74 45 0 SYN573-1 theorem 0.0 2 1 8 0 5 0 0 0 2 8 23 13 0 SYN574-1 theorem 0.0 2 2 18 1 8 0 0 28 3 17 63 36 0 SYN575-1 theorem 0.0 2 2 18 1 8 0 0 28 3 17 63 36 0 SYN576-1 theorem 0.5 3 1 118 0 8 0 0 0 4 118 2989 2971 0 SYN578-1 theorem 0.0 2 2 54 1 9 0 0 258 3 53 298 269 0 SYN579-1 theorem 0.0 2 2 54 1 9 0 0 258 3 53 298 269 0 SYN580-1 theorem 0.0 2 1 21 0 8 0 0 0 2 21 65 31 0 SYN581-1 theorem 0.0 2 1 34 0 9 0 0 0 3 34 205 156 0 SYN582-1 theorem 0.0 2 1 28 0 9 0 0 0 3 28 157 105 0 SYN583-1 theorem 0.0 2 1 27 0 9 0 0 0 3 27 236 223 0 SYN585-1 timeout 300.0 38 SYN586-1 theorem 0.0 2 1 42 0 9 0 0 0 3 42 205 203 0 SYN587-1 theorem 0.0 2 1 23 0 9 0 0 0 2 23 78 66 0 SYN591-1 theorem 0.0 2 1 29 0 13 0 0 0 3 29 98 72 0 SYN592-1 theorem 0.0 2 1 25 0 13 0 0 0 3 25 79 54 0 SYN593-1 theorem 0.0 2 1 10 0 10 0 0 0 2 10 31 34 0 SYN594-1 theorem 0.0 2 1 20 0 8 0 0 0 5 20 62 25 0 SYN595-1 theorem 108.8 25 1 52 0 8 0 0 0 5 52 1141 878 0 SYN604-1 theorem 248.8 30 1 441 0 11 0 0 0 6 441 12872 11842 0 SYN605-1 theorem 0.4 4 1 131 0 12 1 0 0 4 131 2980 2958 0 SYN606-1 timeout 300.0 20 SYN607-1 timeout 300.0 20 SYN608-1 theorem 0.5 4 1 153 0 12 1 0 0 4 153 3412 3390 0 SYN609-1 timeout 300.0 21 SYN610-1 timeout 300.0 20 SYN611-1 timeout 300.0 21 SYN612-1 timeout 300.0 20 SYN613-1 theorem 0.0 2 1 14 0 10 0 0 0 3 14 47 28 0 SYN619-1 theorem 0.0 2 1 23 0 8 0 0 0 4 23 115 88 0 SYN620-1 theorem 0.0 2 1 67 0 13 0 0 0 4 67 283 267 0 SYN621-1 timeout 300.0 78 SYN622-1 theorem 0.0 2 1 17 0 12 0 0 0 4 17 107 87 0 SYN623-1 theorem 1.3 5 1 513 0 15 0 0 0 4 513 13804 13608 0 SYN624-1 theorem 117.1 16 1 30 0 14 0 0 0 6 30 198 167 0 SYN625-1 theorem 0.0 2 1 23 0 8 0 0 0 5 23 73 35 0 SYN626-1 theorem 0.0 2 1 24 0 10 0 0 0 5 24 83 60 0 SYN627-1 theorem 0.2 2 1 36 0 10 0 0 0 3 36 215 162 0 SYN630-1 theorem 0.0 2 1 9 0 9 0 0 0 2 9 28 19 0 SYN633-1 timeout 300.0 10 SYN634-1 timeout 300.0 10 SYN635-1 timeout 300.0 10 SYN636-1 timeout 300.0 10 SYN641-1 theorem 0.2 2 1 178 0 15 0 0 0 4 178 1115 2509 0 SYN642-1 theorem 0.2 2 1 170 0 15 0 0 0 4 170 1091 2485 0 SYN643-1 theorem 0.2 2 1 174 0 15 0 0 0 4 174 1103 2497 0 SYN644-1 timeout 300.0 40 SYN645-1 timeout 300.0 40 SYN648-1 timeout 300.0 161 SYN650-1 timeout 300.0 40 SYN656-1 theorem 0.0 2 1 38 0 18 0 0 0 5 38 120 38 0 SYN657-1 timeout 300.0 10 SYN658-1 timeout 300.0 10 SYN659-1 theorem 3.2 5 1 221 0 22 0 0 0 4 221 2111 2074 0 SYN660-1 theorem 0.1 2 1 91 0 23 0 0 0 3 91 466 401 0 SYN661-1 theorem 0.0 2 1 82 0 23 0 0 0 3 82 434 401 0 SYN662-1 theorem 0.0 2 1 59 0 23 0 0 0 3 59 214 153 0 SYN663-1 theorem 0.0 2 1 50 0 23 0 0 0 3 50 184 153 0 SYN664-1 theorem 0.1 2 1 91 0 23 0 0 0 3 91 466 401 0 SYN665-1 theorem 0.1 2 1 82 0 23 0 0 0 3 82 434 401 0 SYN666-1 theorem 0.0 2 1 61 0 23 0 0 0 3 61 249 202 0 SYN667-1 theorem 0.0 2 1 56 0 23 0 0 0 3 56 235 202 0 SYN668-1 theorem 0.0 2 1 61 0 23 0 0 0 3 61 249 202 0 SYN669-1 theorem 0.0 2 1 56 0 23 0 0 0 3 56 235 202 0 SYN670-1 theorem 0.0 2 1 33 0 23 0 0 0 3 33 85 42 0 SYN671-1 theorem 0.0 2 1 28 0 23 0 0 0 3 28 73 42 0 SYN672-1 theorem 0.0 2 1 30 0 22 0 0 0 4 30 90 54 0 SYN673-1 theorem 7.1 7 1 558 0 19 0 0 0 6 558 14487 10362 0 SYN674-1 theorem 0.0 2 1 92 0 24 0 0 0 3 92 467 401 0 SYN675-1 theorem 0.1 2 1 83 0 24 0 0 0 3 83 435 401 0 SYN676-1 theorem 0.0 2 1 60 0 24 0 0 0 3 60 215 153 0 SYN677-1 theorem 0.0 2 1 51 0 24 0 0 0 3 51 185 153 0 SYN678-1 theorem 0.1 2 1 92 0 24 0 0 0 3 92 467 401 0 SYN679-1 theorem 0.0 2 1 83 0 24 0 0 0 3 83 435 401 0 SYN680-1 theorem 0.0 2 1 92 0 24 0 0 0 3 92 467 401 0 SYN681-1 theorem 0.1 2 1 83 0 24 0 0 0 3 83 435 401 0 SYN682-1 theorem 0.0 2 1 92 0 24 0 0 0 3 92 467 401 0 SYN683-1 theorem 0.1 2 1 83 0 24 0 0 0 3 83 435 401 0 SYN684-1 theorem 0.0 2 1 60 0 24 0 0 0 3 60 215 153 0 SYN685-1 theorem 0.0 2 1 51 0 24 0 0 0 3 51 185 153 0 SYN686-1 theorem 0.2 3 1 64 0 22 0 0 0 4 64 521 506 0 SYN687-1 theorem 3.9 3 1 41 0 20 0 0 0 7 41 128 48 0 SYN690-1 timeout 300.0 9 SYN692-1 timeout 300.0 287 SYN693-1 timeout 300.0 286 SYN694-1 timeout 300.0 217 SYN695-1 timeout 300.0 255 SYN696-1 timeout 300.0 249 SYN697-1 timeout 300.0 278 SYN698-1 timeout 300.0 222 SYN699-1 timeout 300.0 253 SYN700-1 timeout 300.0 248 SYN701-1 timeout 300.0 284 SYN710-1 theorem 0.0 2 1 53 0 26 0 0 0 4 53 154 97 0 SYN713-1 theorem 0.0 2 1 60 0 40 0 0 0 4 60 200 154 0 SYN714-1 theorem 0.0 2 1 38 0 31 0 0 0 3 38 136 96 0 SYN717-1 theorem 0.0 2 1 50 0 46 0 0 0 2 50 131 84 0 SYN718-1 theorem 1.1 3 1 144 0 43 0 0 0 4 144 672 580 0 SYN724-1 theorem 0.0 2 2 5 1 5 6 0 0 2 4 9 6 0 SYN726-1 theorem 0.0 2 6 47 22 2 0 0 196 2 30 193 537 0 SYN728-1 theorem 0.0 2 3 3 6 3 3 0 1 5 6 9 11 0 SYN734-1 non_thm 0.0 2 0 1 1 1 0 0 0 2 0 1 1 0 SYN735-1 non_thm 0.0 2 0 1 2 1 0 0 4 2 0 1 6 0 SYN736-1 non_thm 0.0 2 0 1 1 1 0 0 1 2 0 1 2 0 SYN737-1 non_thm 0.0 2 0 1 11 1 0 0 198 5 0 1 238 0 SYN738-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 SYN739-1 non_thm 0.0 2 0 1 5 1 0 0 2 2 0 1 7 0 SYN740-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 SYN741-1 timeout 300.0 4 SYN742-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 SYN743-1 non_thm 0.0 2 0 1 7 1 0 0 12 2 0 1 19 0 SYN744-1 non_thm 0.0 2 0 1 2 1 0 0 1 2 0 1 3 0 SYN745-1 non_thm 0.0 2 0 1 3 1 0 0 5 3 0 1 8 0 SYN746-1 non_thm 0.0 2 0 1 1 1 0 0 5 2 0 1 6 0 SYN747-1 timeout 300.0 4 SYN748-1 non_thm 0.0 2 0 1 5 1 0 0 61 4 0 1 68 0 SYN749-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 SYN750-1 non_thm 73.5 4 16 1 116 1 0 0 81074 18 94 1 118198 0 SYN751-1 non_thm 0.0 2 0 1 12 1 0 0 75 5 0 1 94 0 SYN752-1 non_thm 0.0 2 0 1 1 1 0 0 2 2 0 1 3 0 SYN753-1 non_thm 0.1 2 0 1 21 1 0 0 408 6 0 1 451 0 SYN754-1 non_thm 0.0 2 0 1 6 1 0 0 13 5 0 1 19 0 SYN755-1 theorem 2.4 2 146 1 366 1 0 0 34607 5 21 1 60249 0 SYN756-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 SYN757-1 non_thm 0.0 2 0 1 3 1 0 0 26 2 0 1 29 0 SYN758-1 theorem 22.5 2 301 1 945 1 0 0 180432 9 27 1 291113 0 SYN759-1 theorem 31.8 2 356 1 1125 1 0 0 264671 8 32 1 420170 0 SYN760-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 SYN761-1 timeout 300.0 7 SYN762-1 theorem 20.7 2 232 1 853 1 0 0 191992 8 30 1 296175 0 SYN763-1 non_thm 0.0 2 0 1 9 1 0 0 55 3 0 1 65 0 SYN764-1 non_thm 0.0 2 0 1 6 1 0 0 18 4 0 1 24 0 SYN765-1 timeout 300.0 7 SYN766-1 non_thm 20.7 3 13 1 92 1 0 0 35217 13 72 1 51611 0 SYN767-1 non_thm 0.0 2 0 1 6 1 0 0 23 3 0 1 29 0 SYN768-1 non_thm 0.0 2 0 2 1 2 0 0 5 2 0 2 6 0 SYN769-1 non_thm 0.0 2 0 2 1 2 0 0 16 3 0 2 17 0 SYN770-1 non_thm 0.0 2 0 2 1 2 0 0 13 2 0 2 14 0 SYN771-1 non_thm 0.0 2 0 2 1 2 0 0 27 3 0 2 28 0 SYN772-1 non_thm 0.0 2 0 2 7 2 0 0 37 3 0 2 44 0 SYN773-1 non_thm 0.0 2 0 2 1 2 0 0 9 2 0 2 10 0 SYN774-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 SYN775-1 timeout 300.0 8 SYN776-1 non_thm 0.0 2 0 2 2 2 0 0 122 3 0 2 124 0 SYN777-1 timeout 300.0 22 SYN778-1 non_thm 0.1 2 0 2 6 2 0 0 344 4 0 2 351 0 SYN779-1 timeout 300.0 19 SYN780-1 non_thm 0.0 2 0 2 1 2 0 0 8 2 0 2 9 0 SYN781-1 non_thm 0.0 2 0 2 5 2 0 0 26 5 0 2 31 0 SYN782-1 timeout 300.0 25 SYN783-1 non_thm 0.0 2 0 2 3 2 0 0 63 4 0 2 66 0 SYN784-1 theorem 3.3 2 82 2 340 2 0 0 34461 4 23 2 55259 0 SYN785-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 SYN786-1 non_thm 0.1 2 0 2 4 2 0 0 322 3 0 2 326 0 SYN787-1 timeout 300.0 7 SYN788-1 timeout 300.0 16 SYN789-1 timeout 300.0 32 SYN790-1 timeout 300.0 32 SYN791-1 non_thm 0.0 2 0 2 1 2 0 0 7 2 0 2 8 0 SYN792-1 timeout 300.0 16 SYN793-1 non_thm 0.0 2 0 2 2 2 0 0 27 3 0 2 29 0 SYN794-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 SYN795-1 non_thm 0.4 2 0 2 24 2 0 0 1066 7 0 2 1139 0 SYN796-1 theorem 0.8 2 43 2 146 2 0 0 11343 3 16 2 20487 0 SYN797-1 non_thm 0.0 2 0 2 1 2 0 0 20 2 0 2 21 0 SYN798-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 SYN799-1 timeout 300.0 7 SYN800-1 timeout 300.0 11 SYN801-1 timeout 300.0 7 SYN802-1 timeout 300.0 8 SYN803-1 non_thm 0.0 2 0 2 1 2 0 0 10 2 0 2 11 0 SYN804-1 non_thm 0.0 2 0 2 7 2 0 0 107 3 0 2 114 0 SYN805-1 timeout 300.0 10 SYN806-1 timeout 300.0 16 SYN807-1 non_thm 0.0 2 0 2 5 2 0 0 227 3 0 2 232 0 SYN808-1 timeout 300.0 18 SYN809-1 timeout 300.0 9 SYN810-1 timeout 300.0 17 SYN811-1 non_thm 1.3 5 0 376 86 52 489 29 451 2 0 712 537 0 SYN812-1 non_thm 15.0 19 0 936 186 86 1708 3 1090 2 0 1801 1276 0 SYN813-1 theorem 1.2 4 12 188 535 36 269 133 684 2 335 360 1365 0 SYN814-1 non_thm 5.9 9 0 376 908 52 489 254 2299 2 0 712 3417 0 SYN815-1 non_thm 5.5 12 0 674 193 70 939 24 843 2 0 1293 1036 0 SYN816-1 non_thm 5.0 11 0 590 170 66 939 32 772 2 0 1127 942 0 SYN817-1 non_thm 6.1 12 0 626 207 68 939 11 854 2 0 1198 1061 0 SYN818-1 non_thm 23.7 26 0 1374 465 102 1763 107 1824 2 0 2669 2289 0 SYN819-1 theorem 2.1 5 18 188 958 36 269 136 1415 2 356 366 2810 0 SYN820-1 theorem 1.5 5 12 188 604 36 269 95 1127 2 389 360 2053 0 SYN821-1 non_thm 6.0 12 0 696 172 72 899 19 856 2 0 1336 1028 0 SYN822-1 non_thm 10.8 16 0 696 871 72 939 177 1816 2 0 1336 2695 0 SYN823-1 non_thm 0.4 3 0 160 86 32 249 0 230 2 0 288 316 0 SYN824-1 non_thm 3.3 9 0 515 126 65 896 0 624 2 0 965 750 0 SYN825-1 non_thm 11.5 18 0 945 117 85 1649 0 1033 2 0 1805 1150 0 SYN826-1 non_thm 11.1 17 0 858 25 84 1763 0 867 2 0 1632 892 0 SYN827-1 non_thm 0.8 4 3 188 140 36 269 0 488 2 319 343 671 0 SYN828-1 non_thm 5.5 12 0 646 277 68 899 1 984 2 0 1224 1271 0 SYN829-1 non_thm 16.3 25 0 1177 145 95 1704 0 1273 2 0 2259 1418 0 SYN830-1 non_thm 17.0 24 0 1214 64 98 1763 0 1232 2 0 2330 1296 0 SYN831-1 non_thm 18.2 24 0 1268 334 96 1763 1 1589 2 0 2440 1926 0 SYN832-1 non_thm 15.3 21 0 1033 218 93 1704 0 1225 2 0 1973 1443 0 SYN833-1 theorem 0.8 4 13 188 221 36 269 1 407 2 271 353 719 0 SYN834-1 theorem 1.2 5 30 188 582 36 269 1 862 2 353 370 1687 0 SYN835-1 non_thm 0.9 4 4 188 237 36 269 4 572 2 375 344 849 0 SYN836-1 theorem 0.7 4 7 188 216 36 269 5 408 2 325 347 760 0 SYN837-1 theorem 164.0 11 626 376 33955 52 489 796 58281 2 895 1326 107448 0 SYN838-1 non_thm 6.9 14 0 634 367 70 939 0 991 2 0 1198 1358 0 SYN839-1 non_thm 21.8 28 0 1336 410 102 1763 0 1711 2 0 2570 2121 0 SYN840-1 non_thm 34.3 30 5 1150 742 96 1763 5 2423 2 1746 2209 3361 0 SYN841-1 non_thm 28.9 31 1 1330 718 102 1763 1 2178 2 1891 2559 2905 0 SYN842-1 non_thm 27.4 32 0 1400 591 102 1763 0 1968 2 0 2698 2559 0 SYN843-1 theorem 0.6 4 7 188 138 36 269 1 341 2 286 347 571 0 SYN844-1 theorem 3.4 5 40 188 1241 36 269 29 2242 2 388 380 4392 0 SYN845-1 theorem 2.5 5 41 188 1110 36 269 14 2185 2 368 381 4192 0 SYN846-1 timeout 300.0 17 SYN847-1 theorem 258.7 14 1119 376 41211 52 489 664 94140 2 913 1820 156882 0 SYN848-1 theorem 4.1 8 25 376 991 52 489 3 1506 2 622 725 2990 0 SYN849-1 theorem 5.3 8 33 376 1119 52 489 8 1837 2 585 733 3669 0 SYN850-1 theorem 55.3 17 103 696 6351 72 939 89 9941 2 1179 1423 18512 0 SYN851-1 non_thm 7.5 14 4 696 537 72 939 0 1254 2 1084 1324 1821 0 SYN852-1 non_thm 30.3 33 0 1396 863 102 1763 0 2267 2 0 2690 3134 0 SYN853-1 non_thm 65.0 35 44 1424 2855 104 1763 14 4938 2 2106 2788 8255 0 SYN854-1 timeout 300.0 39 SYN855-1 non_thm 28.8 33 0 1424 887 104 1763 0 2410 2 0 2744 3297 0 SYN856-1 theorem 0.9 4 10 188 258 36 269 0 498 2 314 350 972 0 SYN857-1 theorem 1.7 5 19 188 628 36 269 12 1058 2 369 359 2265 0 SYN858-1 theorem 29.0 10 123 376 5943 52 489 159 10002 2 789 823 21454 0 SYN859-1 theorem 10.8 9 60 376 2007 52 489 2 3904 2 748 760 7061 0 SYN860-1 timeout 300.0 16 SYN861-1 theorem 22.1 17 45 696 2436 72 939 18 3824 2 1134 1365 7300 0 SYN862-1 theorem 159.0 20 300 696 13467 72 939 156 22340 2 1414 1620 42845 0 SYN863-1 non_thm 10.5 16 5 696 856 72 939 0 1802 2 1372 1325 2703 0 SYN864-1 non_thm 16.1 17 21 696 1841 72 939 12 2823 2 1281 1341 4827 0 SYN865-1 theorem 77.8 18 137 696 5631 72 939 49 10755 2 1373 1461 19644 0 SYN866-1 theorem 121.8 19 481 696 16633 72 939 116 20179 2 1135 1801 40963 0 SYN867-1 non_thm 0.1 2 0 48 12 48 458 0 40 2 0 48 52 0 SYN868-1 non_thm 0.1 2 0 45 6 45 433 0 37 2 0 45 43 0 SYN869-1 theorem 0.1 2 3 36 10 36 266 0 37 2 42 39 74 0 SYN870-1 non_thm 0.1 2 0 36 12 36 262 0 48 2 0 36 63 0 SYN871-1 theorem 0.4 2 20 36 113 36 256 0 295 2 58 57 556 0 SYN872-1 non_thm 0.5 4 0 94 4 94 1717 0 74 2 0 94 78 0 SYN873-1 theorem 0.2 2 12 36 57 36 269 0 90 2 50 48 218 0 SYN874-1 theorem 0.1 2 6 36 21 36 269 0 31 2 45 42 105 0 SYN875-1 theorem 0.1 2 4 36 18 36 265 0 36 2 44 40 112 0 SYN876-1 theorem 3.1 3 36 52 222 52 487 2 981 2 95 88 1765 0 SYN877-1 theorem 0.1 2 3 36 12 36 268 0 43 2 43 39 108 0 SYN878-1 theorem 0.1 3 4 36 16 36 271 0 36 2 44 40 103 0 SYN879-1 theorem 0.1 2 4 36 14 36 271 0 36 2 44 40 132 0 SYN880-1 theorem 0.2 2 2 52 12 52 488 0 42 2 62 54 95 0 SYN881-1 theorem 2.2 3 67 52 308 52 490 0 881 2 88 121 1889 0 SYN882-1 theorem 0.6 3 15 52 82 52 485 0 185 2 96 67 416 0 SYN883-1 theorem 0.4 3 8 52 38 52 491 0 106 2 69 60 240 0 SYN884-1 theorem 0.4 3 6 70 18 70 932 0 67 2 80 76 125 0 SYN885-1 timeout 300.0 11 SYN886-1 theorem 0.3 3 2 72 8 72 909 0 56 2 77 74 89 0 SYN887-1 theorem 0.4 3 5 72 17 72 938 0 60 2 81 77 130 0 SYN888-1 non_thm 1.2 5 4 102 24 102 1760 0 93 2 120 106 134 0 SYN889-1 theorem 0.1 2 2 36 4 36 271 0 29 2 39 38 81 0 SYN890-1 theorem 0.1 2 2 36 8 36 273 0 33 2 41 38 84 0 SYN891-1 theorem 0.1 2 2 36 4 36 259 0 29 2 39 38 75 0 SYN892-1 theorem 0.1 2 2 36 10 36 273 0 33 2 45 38 110 0 SYN893-1 theorem 0.2 2 3 52 16 52 485 0 47 2 62 55 125 0 SYN894-1 theorem 0.2 3 2 52 7 52 489 0 42 2 57 54 80 0 SYN895-1 theorem 0.3 2 4 52 16 52 479 0 55 2 64 56 130 0 SYN896-1 theorem 0.3 2 6 52 31 52 492 0 85 2 70 58 216 0 SYN897-1 timeout 300.0 7 SYN898-1 timeout 300.0 9 SYN899-1 theorem 1.4 4 18 72 118 72 931 0 143 2 105 90 473 0 SYN900-1 theorem 1.8 4 24 72 85 72 923 0 216 2 112 96 509 0 SYN901-1 theorem 1.5 5 11 101 46 101 1680 0 122 2 130 112 224 0 SYN902-1 non_thm 14.8 7 12 102 177 102 1757 12 1210 2 246 114 2090 0 SYN903-1 timeout 300.0 15 SYN904-1 timeout 300.0 18 SYN905-1 timeout 300.0 12 SYN906-1 timeout 300.0 26 SYN907-1 timeout 300.0 24 SYN908-1 timeout 300.0 27 SYN909-1 timeout 300.0 35 SYN910-1 timeout 300.0 39 SYN911-1 timeout 300.0 46 SYN912-1 timeout 300.0 51 SYN913-1 timeout 300.0 42 TOP001-1 timeout 300.0 35 TOP001-2 timeout 300.0 43 TOP002-1 timeout 300.0 15 TOP002-2 theorem 0.0 2 1 2 0 2 0 0 0 2 2 4 2 0 TOP003-1 timeout 300.0 18 TOP003-2 non_thm 0.0 2 0 12 24 3 0 0 54 4 0 20 78 0 TOP004-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 2 0 TOP004-2 theorem 0.0 2 1 1 0 0 0 0 0 2 1 5 1 0 TOP005-1 timeout 300.0 16 TOP005-2 timeout 300.0 26 TOP006-1 timeout 300.0 16 TOP007-1 timeout 300.0 59 TOP008-1 memory 245.8 499 TOP009-1 timeout 300.0 80 TOP010-1 timeout 300.0 21 TOP011-1 timeout 300.0 38 TOP012-1 timeout 300.0 41 TOP013-1 timeout 300.0 43 TOP014-1 timeout 300.0 190 TOP015-1 timeout 300.0 40 TOP016-1 timeout 300.0 41 TOP017-1 timeout 300.0 195 TOP018-1 timeout 300.0 119 TOP019-1 timeout 300.0 108