-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true -us false Problems list file : nne-problems Output file : nne-output Summary file : nne-summary Time limit : 300 s Memory limit : 500 MB -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug [0.00] ALG002-1 theorem 0.0 2 1 45 0 0 0 0 0 3 45 280 101 0 [0.00] CAT007-3 theorem 0.0 2 1 5 0 0 0 0 0 2 5 12 6 0 [0.00] COM002-2 theorem 0.0 2 1 26 0 0 0 0 0 2 26 47 9 0 [0.00] COM003-2 theorem 0.0 2 1 12 0 0 13 1 0 2 12 26 24 0 [0.00] FLD001-3 theorem 0.0 2 1 62 0 0 0 0 0 2 62 283 2000 0 [0.00] FLD005-3 theorem 0.0 2 1 91 0 0 0 0 0 2 91 629 2082 0 [0.00] FLD006-1 theorem 27.7 4 1 154 0 0 0 0 0 3 154 1362 16646 0 [0.00] FLD006-3 theorem 0.0 2 1 5 0 0 0 0 0 2 5 31 32 0 [0.00] FLD009-3 theorem 0.1 2 1 112 0 0 0 0 0 2 112 907 2094 0 [0.00] FLD010-1 theorem 34.8 5 1 168 0 0 0 0 0 3 168 1396 18973 0 [0.00] FLD010-3 theorem 0.0 2 1 6 0 0 0 0 0 2 6 35 34 0 [0.00] FLD013-1 theorem 6.9 3 1 272 0 0 0 0 0 2 272 1327 8600 0 [0.00] FLD013-2 theorem 16.1 3 1 345 0 0 0 0 0 2 345 1638 14448 0 [0.00] FLD013-3 theorem 0.5 3 1 324 0 0 0 0 0 2 324 6414 9245 0 [0.00] FLD013-4 theorem 0.0 2 1 29 0 0 0 0 0 2 29 315 509 0 [0.00] FLD013-5 theorem 0.0 2 1 27 0 0 0 0 0 2 27 334 599 0 [0.00] FLD015-3 theorem 0.0 2 1 93 0 0 0 0 0 2 93 636 2018 0 [0.00] FLD016-3 theorem 0.1 2 1 151 0 0 0 0 0 2 151 851 7883 0 [0.00] FLD016-5 theorem 0.2 3 1 204 0 0 0 0 0 2 204 1500 13874 0 [0.00] FLD017-1 theorem 0.0 2 1 24 0 0 0 0 0 2 24 310 460 0 [0.00] FLD017-3 theorem 0.0 2 1 11 0 0 0 0 0 2 11 187 219 0 [0.00] FLD018-3 theorem 0.0 2 1 73 0 0 0 0 0 2 73 1562 1180 0 [0.00] FLD019-3 theorem 0.0 2 1 14 0 0 0 0 0 2 14 96 133 0 [0.00] FLD020-3 theorem 0.0 2 1 83 0 0 0 0 0 2 83 518 2102 0 [0.00] FLD021-1 theorem 0.8 2 1 55 0 0 0 0 0 2 55 216 1950 0 [0.00] FLD021-3 theorem 0.0 2 1 14 0 0 0 0 0 2 14 104 171 0 [0.00] FLD022-3 theorem 0.1 2 1 149 0 0 0 0 0 2 149 827 7875 0 [0.00] FLD023-3 theorem 0.0 2 1 86 0 0 0 0 0 2 86 738 2163 0 [0.00] FLD024-3 theorem 0.0 2 1 57 0 0 0 0 0 2 57 227 1951 0 [0.00] FLD025-1 theorem 6.9 3 1 284 0 0 0 0 0 2 284 1371 8644 0 [0.00] FLD025-3 theorem 0.5 3 1 324 0 0 0 0 0 2 324 6414 9245 0 [0.00] FLD025-4 theorem 0.0 2 1 36 0 0 0 0 0 2 36 336 530 0 [0.00] FLD025-5 theorem 0.0 2 1 35 0 0 0 0 0 2 35 362 623 0 [0.00] FLD027-3 theorem 0.1 2 1 149 0 0 0 0 0 2 149 1648 2240 0 [0.00] FLD028-3 theorem 0.1 3 1 181 0 0 0 0 0 2 181 1229 8064 0 [0.00] FLD030-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 149 167 0 [0.00] FLD030-2 theorem 0.0 2 1 24 0 0 0 0 0 2 24 310 460 0 [0.00] FLD030-3 theorem 0.0 2 1 25 0 0 0 0 0 2 25 188 291 0 [0.00] FLD030-4 theorem 0.0 2 1 11 0 0 0 0 0 2 11 187 219 0 [0.00] FLD031-3 theorem 0.0 2 1 83 0 0 0 0 0 2 83 2127 1244 0 [0.00] FLD031-5 theorem 0.1 2 1 100 0 0 0 0 0 2 100 2896 1342 0 [0.00] FLD032-3 theorem 0.0 2 1 18 0 0 0 0 0 2 18 110 139 0 [0.00] FLD033-3 theorem 0.0 2 1 126 0 0 0 0 0 2 126 1084 2200 0 [0.00] FLD034-1 theorem 0.8 2 1 60 0 0 0 0 0 2 60 233 2047 0 [0.00] FLD034-3 theorem 0.0 2 1 18 0 0 0 0 0 2 18 120 183 0 [0.00] FLD035-3 theorem 0.1 3 1 181 0 0 0 0 0 2 181 1229 8064 0 [0.00] FLD036-3 theorem 0.1 3 1 181 0 0 0 0 0 2 181 1229 8064 0 [0.00] FLD037-3 theorem 0.1 2 1 128 0 0 0 0 0 2 128 1883 2362 0 [0.00] FLD038-3 theorem 0.0 2 1 64 0 0 0 0 0 2 64 277 2055 0 [0.00] FLD039-1 theorem 0.0 2 1 6 0 0 0 0 0 2 6 65 71 0 [0.00] FLD039-3 theorem 0.0 2 1 15 0 0 0 0 0 2 15 81 126 0 [0.00] FLD043-3 theorem 0.0 2 1 107 0 0 0 0 0 2 107 851 2223 0 [0.00] FLD055-1 theorem 0.0 2 1 27 0 0 0 0 0 2 27 278 396 0 [0.00] FLD055-3 theorem 0.0 2 1 20 0 0 0 0 0 2 20 154 259 0 [0.00] FLD056-1 theorem 0.0 2 1 4 0 0 0 0 0 2 4 57 64 0 [0.00] FLD056-3 theorem 0.0 2 1 4 0 0 0 0 0 2 4 57 64 0 [0.00] FLD058-1 theorem 0.0 2 1 25 0 0 0 0 0 2 25 213 275 0 [0.00] FLD058-3 theorem 0.0 2 1 21 0 0 0 0 0 2 21 131 199 0 [0.00] FLD059-1 theorem 0.2 2 1 40 0 0 0 0 0 2 40 141 791 0 [0.00] FLD059-2 theorem 0.8 2 1 177 0 0 0 0 0 2 177 908 2480 0 [0.00] FLD059-3 theorem 0.0 2 1 54 0 0 0 0 0 2 54 322 833 0 [0.00] FLD059-4 theorem 0.0 2 1 14 0 0 0 0 0 2 14 107 173 0 [0.00] FLD060-1 theorem 0.8 2 1 133 0 0 0 0 0 2 133 517 2165 0 [0.00] FLD060-2 theorem 6.9 3 1 267 0 0 0 0 0 2 267 1054 8300 0 [0.00] FLD060-4 theorem 0.3 3 1 313 0 0 0 0 0 2 313 3407 8487 0 [0.00] FLD061-1 theorem 6.9 3 1 245 0 0 0 0 0 2 245 889 8166 0 [0.00] FLD061-4 theorem 0.7 4 1 471 0 0 0 0 0 2 471 5072 22973 0 [0.00] FLD064-3 theorem 0.1 2 1 87 0 0 0 0 0 2 87 1933 1305 0 [0.00] FLD065-3 theorem 0.0 2 1 12 0 0 0 0 0 2 12 67 105 0 [0.00] FLD067-4 theorem 0.1 2 1 107 0 0 0 0 0 2 107 531 4188 0 [0.00] FLD068-4 theorem 0.1 2 1 87 0 0 0 0 0 2 87 372 4172 0 [0.00] FLD069-1 theorem 0.8 2 1 98 0 0 0 0 0 2 98 401 2130 0 [0.00] FLD069-3 theorem 0.0 2 1 16 0 0 0 0 0 2 16 110 194 0 [0.00] FLD070-1 theorem 0.8 2 1 60 0 0 0 0 0 2 60 220 1955 0 [0.00] FLD070-2 theorem 2.6 3 1 266 0 0 0 0 0 2 266 1401 5021 0 [0.00] FLD070-3 theorem 0.0 2 1 80 0 0 0 0 0 2 80 453 2008 0 [0.00] FLD070-4 theorem 0.0 2 1 17 0 0 0 0 0 2 17 155 255 0 [0.00] FLD071-1 theorem 0.0 2 1 8 0 0 0 0 0 2 8 103 116 0 [0.00] FLD071-2 theorem 2.6 2 1 100 0 0 0 0 0 2 100 376 4176 0 [0.00] FLD071-3 theorem 0.0 2 1 9 0 0 0 0 0 2 9 98 104 0 [0.00] FLD071-4 theorem 0.0 2 1 9 0 0 0 0 0 2 9 141 157 0 [0.00] GRA001-1 theorem 0.0 2 4 10 3 0 28 0 2 2 5 32 17 0 [0.00] GRP123-1.003 theorem 0.0 2 1 31 0 0 0 0 0 2 31 87 44 0 [0.00] GRP123-2.003 theorem 0.0 2 1 37 0 0 0 0 0 2 37 94 44 0 [0.00] GRP123-3.003 theorem 0.0 2 1 51 0 0 0 0 0 2 51 111 53 0 [0.00] GRP123-4.003 theorem 0.0 2 1 31 0 0 0 0 0 2 31 105 116 0 [0.00] GRP123-6.003 theorem 0.0 2 1 50 0 0 0 0 0 2 50 143 82 0 [0.00] GRP123-7.003 theorem 0.0 2 1 56 0 0 0 0 0 2 56 149 82 0 [0.00] GRP123-8.003 theorem 0.0 2 1 62 0 0 0 0 0 2 62 156 87 0 [0.00] GRP123-9.003 theorem 0.0 2 1 50 0 0 0 0 0 2 50 143 100 0 [0.00] GRP124-1.004 theorem 0.0 2 2 72 1 0 0 0 20 2 64 392 155 0 [0.00] GRP124-2.004 theorem 0.0 2 1 75 0 0 0 0 0 2 75 182 111 0 [0.00] GRP124-3.004 theorem 0.0 2 2 117 1 0 0 0 31 2 106 337 171 0 [0.00] GRP124-4.004 theorem 0.0 2 2 66 1 0 0 0 50 2 62 293 350 0 [0.00] GRP124-6.004 theorem 0.0 2 2 109 1 0 0 0 37 2 101 424 234 0 [0.00] GRP124-7.004 theorem 0.0 2 2 121 1 0 0 0 37 2 113 436 234 0 [0.00] GRP124-8.004 theorem 0.0 2 2 148 2 0 0 0 56 2 141 490 259 0 [0.00] GRP124-9.004 theorem 0.0 2 2 109 1 0 0 0 37 2 101 424 266 0 [0.00] GRP125-1.003 theorem 0.0 2 1 31 0 0 0 0 0 2 31 94 43 0 [0.00] GRP125-2.005 theorem 0.0 2 3 184 2 0 0 0 58 2 157 800 479 0 [0.00] GRP125-3.005 theorem 0.0 2 5 280 4 0 0 0 131 2 219 1294 748 0 [0.00] GRP125-4.003 theorem 0.0 2 1 31 0 0 0 0 0 2 31 146 117 0 [0.00] GRP126-1.004 theorem 0.0 2 2 69 1 0 0 0 19 2 63 316 141 0 [0.00] GRP126-2.004 theorem 0.0 2 1 75 0 0 0 0 0 2 75 224 111 0 [0.00] GRP126-3.004 theorem 0.0 2 2 117 1 0 0 0 30 2 106 371 171 0 [0.00] GRP127-1.004 theorem 0.0 2 2 72 1 0 0 0 19 2 64 352 151 0 [0.00] GRP127-3.004 theorem 0.0 2 2 117 1 0 0 0 30 2 106 347 170 0 [0.00] GRP128-1.003 theorem 0.0 2 4 59 3 0 0 0 5 2 32 200 90 0 [0.00] GRP128-4.003 theorem 0.0 2 4 28 3 0 0 0 9 2 28 193 108 0 [0.00] GRP129-1.003 theorem 0.0 2 4 59 3 0 0 0 5 2 29 238 92 0 [0.00] GRP129-2.004 theorem 0.0 2 7 164 7 0 0 0 47 2 78 599 258 0 [0.00] GRP129-3.004 theorem 0.0 2 7 236 7 0 0 0 140 2 115 783 344 0 [0.00] GRP130-1.003 theorem 0.0 2 4 71 3 0 0 0 5 2 36 316 123 0 [0.00] GRP130-2.003 theorem 0.0 2 3 68 2 0 0 0 6 2 43 282 104 0 [0.00] GRP130-3.003 theorem 0.0 2 2 94 1 0 0 0 2 2 68 289 108 0 [0.00] GRP130-4.003 theorem 0.0 2 4 43 3 0 0 0 9 2 25 177 143 0 [0.00] GRP131-1.002 theorem 0.0 2 2 20 1 0 0 0 0 2 14 81 32 0 [0.00] GRP131-2.002 theorem 0.0 2 2 22 1 0 0 0 0 2 16 84 32 0 [0.00] GRP132-1.002 theorem 0.0 2 2 20 1 0 0 0 0 2 14 81 32 0 [0.00] GRP132-2.002 theorem 0.0 2 2 22 1 0 0 0 0 2 16 84 32 0 [0.00] GRP133-1.003 theorem 0.0 2 4 80 3 0 0 0 5 2 33 340 139 0 [0.00] GRP133-2.003 theorem 0.0 2 3 69 2 0 0 0 6 2 43 251 97 0 [0.00] GRP134-1.003 theorem 0.0 2 4 92 3 0 0 0 5 2 34 434 169 0 [0.00] GRP134-2.003 theorem 0.0 2 3 86 2 0 0 0 6 2 44 352 127 0 [0.00] GRP135-1.002 theorem 0.0 2 2 19 1 0 0 0 0 2 14 61 25 0 [0.00] GRP135-2.002 theorem 0.0 2 2 21 1 0 0 0 0 2 16 63 25 0 [0.00] HWV005-1 theorem 0.0 2 1 96 0 0 0 0 0 3 96 323 60 0 [0.00] HWV005-2 unsound 0.0 2 0 160 1 0 0 0 43 3 0 305 46 0 [0.00] HWV007-1 theorem 0.1 2 1 352 0 0 1 6 0 4 352 941 144 0 [0.00] HWV007-2 unsound 0.1 2 0 707 2 0 1 0 117 4 0 1387 121 0 [0.00] HWV034-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.00] HWV034-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] KRS001-1 theorem 0.0 2 1 8 0 0 0 0 0 2 8 16 19 0 [0.00] KRS002-1 theorem 0.0 2 1 9 0 0 0 0 0 3 9 16 20 0 [0.00] KRS003-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 16 18 0 [0.00] KRS005-1 non_thm 0.0 2 0 8 0 0 0 0 36 2 0 8 36 0 [0.00] KRS006-1 non_thm 0.0 2 0 20 3 0 0 0 64 3 0 31 71 0 [0.00] KRS007-1 non_thm 0.0 2 0 27 2 0 0 0 74 3 0 37 85 0 [0.00] KRS008-1 non_thm 0.1 2 0 42 34 0 0 0 528 3 0 72 810 0 [0.00] KRS009-1 non_thm 0.0 2 0 43 8 0 0 0 229 3 0 65 237 0 [0.00] KRS010-1 theorem 0.0 2 2 21 1 0 0 0 77 2 18 38 95 0 [0.00] KRS011-1 non_thm 0.0 2 0 36 3 0 0 0 37 2 0 44 49 0 [0.00] KRS012-1 theorem 0.0 2 1 5 0 0 0 0 0 2 5 10 5 0 [0.00] KRS013-1 theorem 0.0 2 1 17 0 0 0 0 0 3 17 27 45 0 [0.00] KRS014-1 non_thm 0.0 2 0 14 2 0 0 0 30 2 0 17 32 0 [0.00] KRS015-1 theorem 0.0 2 1 10 0 0 0 0 0 3 10 18 22 0 [0.00] KRS016-1 non_thm 0.0 2 0 4 4 0 0 0 10 2 0 4 14 0 [0.00] KRS017-1 theorem 0.0 2 1 3 0 0 0 0 0 2 3 7 3 0 [0.00] LCL181-2 theorem 0.0 2 1 2 0 0 2 0 0 2 2 4 2 0 [0.00] LCL230-2 theorem 0.0 2 1 3 0 0 3 0 0 2 3 6 1 0 [0.00] MGT004-1 theorem 0.0 2 1 15 0 0 0 0 0 2 15 26 12 0 [0.00] MGT007-1 theorem 0.0 2 1 17 0 0 0 0 0 2 17 28 14 0 [0.00] MGT016-1 theorem 0.0 2 1 16 0 0 0 0 0 2 16 26 3 0 [0.00] MGT018-1 theorem 0.0 2 1 16 0 0 0 0 0 2 16 26 3 0 [0.00] MGT022-1 theorem 0.0 2 2 8 1 0 3 0 0 3 7 20 7 0 [0.00] MGT022-2 theorem 0.0 2 2 8 1 0 3 0 0 3 7 20 7 0 [0.00] MGT028-1 theorem 0.0 2 2 13 1 0 0 0 1 4 11 27 15 0 [0.00] MGT030-1 theorem 0.0 2 6 23 8 0 0 0 4 4 14 80 45 0 [0.00] MGT036-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 15 10 0 [0.00] MGT036-2 theorem 0.0 2 1 9 0 0 0 0 0 2 9 16 11 0 [0.00] MGT041-2 theorem 0.0 2 1 7 0 0 0 0 0 2 7 9 3 0 [0.00] MSC001-1 theorem 0.0 2 1 65 0 0 1 2 0 5 65 235 99 0 [0.00] MSC002-1 theorem 0.0 2 1 22 0 0 1 0 0 4 22 42 36 0 [0.00] MSC002-2 theorem 0.0 2 1 22 0 0 1 0 0 4 22 42 36 0 [0.00] MSC003-1 theorem 0.0 2 1 6 0 0 0 0 0 2 6 9 5 0 [0.00] MSC004-1 theorem 0.0 2 6 20 11 0 0 0 4 3 14 38 49 0 [0.00] MSC006-1 theorem 0.0 2 6 47 22 0 0 0 196 2 30 193 537 0 [0.00] MSC009-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 [0.00] NLP001-1 theorem 0.0 2 2 28 1 0 5 0 0 2 19 32 30 0 [0.00] NLP043-1 non_thm 0.0 2 0 17 2 0 3 0 31 2 0 17 33 0 [0.00] NLP044-1 non_thm 0.0 2 0 17 2 0 3 0 31 2 0 17 33 0 [0.00] NLP045-1 non_thm 0.0 2 0 17 2 0 3 0 31 2 0 17 33 0 [0.00] NLP046-1 non_thm 0.0 2 0 17 2 0 3 0 31 2 0 17 33 0 [0.00] NLP047-1 non_thm 0.0 2 0 17 2 0 3 0 31 2 0 17 33 0 [0.00] NLP048-1 non_thm 0.0 2 0 17 2 0 3 0 31 2 0 17 33 0 [0.00] NLP066-1 non_thm 0.0 2 0 12 4 0 3 0 28 2 0 12 32 0 [0.00] NLP067-1 non_thm 0.0 2 0 10 4 0 3 0 26 2 0 10 30 0 [0.00] NLP068-1 non_thm 0.0 2 0 5 3 0 3 0 14 2 0 5 17 0 [0.00] NLP095-1 non_thm 0.0 2 0 2 1 0 3 0 6 2 0 2 7 0 [0.00] NLP096-1 non_thm 0.0 2 0 2 1 0 3 0 6 2 0 2 7 0 [0.00] NLP097-1 non_thm 0.0 2 0 2 1 0 2 0 7 2 0 2 8 0 [0.00] NLP098-1 non_thm 0.0 2 0 2 1 0 2 0 7 2 0 2 8 0 [0.00] NLP099-1 non_thm 0.0 2 0 3 1 0 3 0 5 2 0 3 6 0 [0.00] NLP100-1 non_thm 0.0 2 0 2 1 0 3 0 14 2 0 2 15 0 [0.00] NLP101-1 non_thm 0.0 2 0 2 1 0 3 0 14 2 0 2 15 0 [0.00] NLP102-1 non_thm 0.0 2 0 3 1 0 4 0 12 2 0 3 13 0 [0.00] NLP103-1 non_thm 0.0 2 0 4 1 0 4 0 12 2 0 4 13 0 [0.00] NLP114-1 non_thm 0.0 2 0 18 1 0 2 0 32 2 0 19 33 0 [0.00] NLP115-1 non_thm 0.0 2 0 18 1 0 2 0 32 2 0 19 33 0 [0.00] NLP116-1 non_thm 0.0 2 0 18 1 0 2 0 32 2 0 19 33 0 [0.00] NLP117-1 theorem 0.0 2 2 34 1 0 5 0 0 2 19 38 48 0 [0.00] NLP118-1 non_thm 0.0 2 1 34 1 0 4 0 16 2 19 37 48 0 [0.00] NLP119-1 non_thm 0.0 2 1 34 1 0 4 0 16 2 19 37 48 0 [0.00] NLP120-1 non_thm 0.0 2 0 18 1 0 2 0 32 2 0 19 33 0 [0.00] NLP121-1 non_thm 0.0 2 0 18 1 0 2 0 32 2 0 19 33 0 [0.00] NLP122-1 theorem 0.0 2 2 34 1 0 5 0 0 2 19 38 48 0 [0.00] NLP123-1 non_thm 0.0 2 0 18 1 0 2 0 32 2 0 19 33 0 [0.00] NLP130-1 non_thm 0.0 2 0 24 4 0 4 0 47 2 0 24 51 0 [0.00] NLP131-1 non_thm 0.0 2 0 21 2 0 4 0 40 2 0 21 42 0 [0.00] NLP132-1 non_thm 0.0 2 0 21 3 0 4 0 40 2 0 21 43 0 [0.00] NLP133-1 non_thm 0.0 2 0 21 3 0 4 0 40 2 0 21 43 0 [0.00] NLP134-1 non_thm 0.0 2 0 21 2 0 4 0 39 2 0 21 41 0 [0.00] NLP135-1 non_thm 0.0 2 0 24 4 0 4 0 47 2 0 24 51 0 [0.00] NLP136-1 non_thm 0.0 2 1 43 2 0 5 0 20 2 25 46 63 0 [0.00] NLP137-1 non_thm 0.0 2 0 30 4 0 4 0 51 3 0 30 59 0 [0.00] NLP138-1 non_thm 0.0 2 1 43 2 0 5 0 20 2 25 46 63 0 [0.00] NLP139-1 non_thm 0.0 2 0 30 4 0 4 0 51 3 0 30 59 0 [0.00] NLP221-1 non_thm 0.0 2 0 20 1 0 4 0 35 2 0 20 36 0 [0.00] NLP222-1 non_thm 0.0 2 0 20 1 0 4 0 35 2 0 20 36 0 [0.00] NLP223-1 non_thm 0.0 2 0 19 1 0 4 0 34 2 0 19 35 0 [0.00] NLP230-1 non_thm 0.0 2 1 78 1 0 5 0 36 3 43 83 115 0 [0.00] NLP231-1 non_thm 0.0 2 0 37 1 0 4 0 71 2 0 37 72 0 [0.00] NLP232-1 non_thm 0.0 2 0 38 1 0 4 0 72 2 0 38 73 0 [0.00] NLP233-1 non_thm 0.0 2 0 39 1 0 4 0 72 2 0 39 73 0 [0.00] NLP235-1 non_thm 0.0 2 0 37 1 0 4 0 73 2 0 37 74 0 [0.00] NLP236-1 non_thm 0.0 2 0 37 1 0 4 0 71 2 0 37 72 0 [0.00] NLP238-1 non_thm 0.0 2 0 37 1 0 4 0 73 2 0 37 74 0 [0.00] NLP239-1 non_thm 0.0 0 0 37 1 0 4 0 70 2 0 37 71 0 [0.00] NUM014-1 theorem 0.0 2 1 5 0 0 0 0 0 2 5 11 4 0 [0.00] NUM015-1 theorem 0.0 2 1 11 0 0 0 0 0 3 11 21 14 0 [0.00] NUM016-1 theorem 0.0 2 1 14 0 0 0 0 0 3 14 36 12 0 [0.00] NUM016-2 theorem 0.0 2 1 12 0 0 0 0 0 3 12 18 8 0 [0.00] NUM021-1 theorem 0.0 2 1 80 0 0 0 0 0 3 80 405 210 0 [0.00] NUM022-1 theorem 0.0 2 1 9 0 0 0 0 0 3 9 14 5 0 [0.00] NUM025-2 theorem 0.0 2 1 4 0 0 0 0 0 2 4 17 8 0 [0.00] NUM027-1 theorem 0.0 2 1 49 0 0 0 0 0 2 49 247 142 0 [0.00] NUM285-1 non_thm 0.0 2 0 16 5 0 44 0 30 2 0 31 35 0 [0.00] PLA002-1 theorem 0.0 2 1 7 0 0 8 0 0 2 7 12 3 0 [0.00] PLA002-2 theorem 4.2 32 1 1994 0 0 0 0 0 5 1994 2625 611529 0 [0.00] PUZ001-1 theorem 0.0 2 1 17 0 0 2 0 0 2 17 20 8 0 [0.00] PUZ001-3 non_thm 0.0 2 0 19 0 0 2 0 10 2 0 22 11 0 [0.00] PUZ002-1 theorem 0.0 2 1 11 0 0 0 0 0 2 11 13 5 0 [0.00] PUZ004-1 theorem 0.0 2 1 10 0 0 11 0 0 2 10 13 3 0 [0.00] PUZ005-1 theorem 0.0 2 2 26 1 0 0 0 0 2 21 83 164 0 [0.00] PUZ009-1 theorem 0.0 2 1 5 0 0 11 0 0 2 5 14 13 0 [0.00] PUZ012-1 theorem 0.0 2 1 20 0 0 1 0 0 2 20 36 20 0 [0.00] PUZ013-1 theorem 0.0 2 1 7 0 0 10 0 0 2 7 13 11 0 [0.00] PUZ014-1 theorem 0.0 2 2 16 1 0 22 0 10 2 13 26 21 0 [0.00] PUZ015-2.006 theorem 0.1 2 143 2384 150 0 5261 0 701 2 59 6902 3383 0 [0.00] PUZ016-2.004 non_thm 0.0 2 0 22 2 0 39 0 27 2 0 48 42 0 [0.00] PUZ016-2.005 theorem 0.0 2 26 362 25 0 789 0 99 2 40 1038 520 0 [0.00] PUZ021-1 theorem 0.1 2 13 195 66 0 0 6 339 3 55 877 3786 0 [0.00] PUZ023-1 theorem 0.0 2 2 10 2 0 6 0 4 2 11 30 16 0 [0.00] PUZ024-1 theorem 0.0 2 1 7 0 0 7 0 0 2 7 20 7 0 [0.00] PUZ025-1 theorem 0.0 2 8 37 9 0 4 0 40 2 22 223 180 0 [0.00] PUZ026-1 theorem 0.0 2 3 29 2 0 5 3 10 2 18 99 61 0 [0.00] PUZ027-1 theorem 0.0 2 3 18 2 0 14 0 1 2 12 76 40 0 [0.00] PUZ028-1 non_thm 0.0 2 0 31 15 0 0 0 20 2 0 91 35 0 [0.00] PUZ028-2 non_thm 0.0 2 0 70 18 0 0 0 16 2 0 190 46 0 [0.00] PUZ028-3 non_thm 0.0 2 0 70 18 0 154 0 16 2 0 190 46 0 [0.00] PUZ028-4 non_thm 0.0 2 0 28 18 0 106 0 16 2 0 136 46 0 [0.00] PUZ028-5 theorem 0.1 2 30 742 29 0 0 0 97 2 90 1674 246 0 [0.00] PUZ029-1 theorem 0.0 2 1 13 0 0 0 0 0 2 13 17 14 0 [0.00] PUZ030-1 theorem 0.0 2 24 327 24 0 397 0 129 2 28 1047 1103 0 [0.00] PUZ030-2 theorem 0.0 2 9 35 8 0 173 0 19 2 10 164 167 0 [0.00] PUZ031-1 theorem 0.0 2 1 33 0 0 0 0 0 2 33 56 30 0 [0.00] PUZ032-1 theorem 0.0 2 2 16 1 0 0 0 6 3 16 54 17 0 [0.00] PUZ033-1 theorem 0.0 2 1 11 0 0 17 0 0 2 11 15 8 0 [0.00] PUZ035-1 theorem 0.0 2 4 16 3 0 17 0 1 2 9 41 14 0 [0.00] PUZ035-2 theorem 0.0 2 4 25 3 0 30 1 6 2 12 64 36 0 [0.00] PUZ035-3 theorem 0.0 2 4 12 3 0 8 0 2 2 8 27 6 0 [0.00] PUZ035-5 theorem 0.0 2 4 7 4 0 0 0 0 2 6 27 20 0 [0.00] PUZ035-6 theorem 0.0 2 4 5 4 0 0 0 7 2 6 20 31 0 [0.00] PUZ035-7 theorem 0.1 2 12 217 32 0 0 0 366 3 81 882 2294 0 [0.00] PUZ044-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 [0.00] PUZ045-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 [0.00] SET001-1 theorem 0.0 2 1 4 0 0 0 0 0 2 4 8 3 0 [0.00] SET002-1 theorem 0.0 2 3 9 3 0 0 0 0 2 8 21 22 0 [0.00] SET003-1 theorem 0.0 2 1 6 0 0 0 0 0 2 6 9 6 0 [0.00] SET004-1 theorem 0.0 2 1 6 0 0 0 0 0 2 6 8 5 0 [0.00] SET005-1 theorem 0.0 2 2 135 1 0 0 0 0 2 131 378 143 0 [0.00] SET006-1 theorem 0.0 2 1 6 0 0 0 0 0 2 6 10 7 0 [0.00] SET007-1 theorem 0.1 2 3 578 2 0 0 38 0 2 339 2353 722 0 [0.00] SET008-1 theorem 0.0 2 1 10 0 0 0 0 0 2 10 34 21 0 [0.00] SET009-1 theorem 0.0 2 1 22 0 0 0 0 0 2 22 41 17 0 [0.00] SET011-1 theorem 0.0 2 2 73 1 0 0 0 0 2 67 239 94 0 [0.00] SET014-2 timeout 300.0 18 [0.00] SET043-5 theorem 0.0 2 4 0 3 0 0 0 0 2 2 8 9 0 [0.00] SET044-5 theorem 0.0 2 8 8 13 0 0 0 18 2 6 32 79 0 [0.00] SET045-5 theorem 0.0 2 6 2 6 0 0 0 8 2 6 15 34 0 [0.00] SET046-5 theorem 0.0 2 4 4 3 0 0 0 1 2 4 18 19 0 [0.00] SET047-5 theorem 0.0 2 4 6 3 0 4 0 2 2 4 26 16 0 [0.00] SET055-6 theorem 119.8 10 51 17443 108 0 0 204 273966 2 5353 370551 283070 0 [0.00] SET055-7 theorem 0.0 2 1 5 0 0 0 0 0 2 5 47 15 0 [0.00] SET777-1 non_thm 0.0 2 0 0 2 0 0 0 2 2 0 0 4 0 [0.00] SET778-1 non_thm 0.0 2 0 0 3 0 0 0 2 2 0 0 5 0 [0.00] SET779-1 non_thm 0.0 2 0 0 3 0 0 0 3 2 0 0 6 0 [0.00] SET780-1 non_thm 0.0 2 0 0 3 0 0 0 2 2 0 0 5 0 [0.00] SET786-1 theorem 0.0 2 4 4 3 0 0 0 1 2 4 16 18 0 [0.00] SWV001-1 theorem 0.0 2 2 10 1 0 0 0 5 2 9 39 21 0 [0.00] SWV009-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 12 4 0 [0.00] SYN001-1.005 theorem 0.0 2 16 16 15 0 118 0 12 2 5 120 100 0 [0.00] SYN006-1 theorem 0.0 2 1 6 0 0 1 0 0 3 6 7 2 0 [0.00] SYN008-1 theorem 0.0 2 1 3 0 0 4 0 0 2 3 6 4 0 [0.00] SYN009-1 theorem 0.0 2 1 6 0 0 0 0 0 2 6 18 48 0 [0.00] SYN009-2 theorem 0.0 2 1 7 0 0 0 0 0 2 7 9 30 0 [0.00] SYN009-3 theorem 0.0 2 1 9 0 0 1 0 0 2 9 11 31 0 [0.00] SYN009-4 theorem 0.0 2 1 8 0 0 0 0 0 2 8 10 58 0 [0.00] SYN011-1 theorem 0.0 2 2 9 1 0 13 0 0 2 7 13 9 0 [0.00] SYN012-1 theorem 0.0 2 9 0 37 0 0 0 111 5 16 0 182 0 [0.00] SYN014-2 theorem 0.0 2 1 8 0 0 0 0 0 2 8 36 22 0 [0.00] SYN015-2 theorem 0.0 2 1 33 0 0 0 0 0 2 33 149 81 0 [0.00] SYN028-1 theorem 0.0 2 1 5 0 0 7 0 0 2 5 7 4 0 [0.00] SYN029-1 theorem 0.0 2 2 3 1 0 7 0 0 2 3 8 4 0 [0.00] SYN030-1 theorem 0.0 2 2 5 1 0 11 0 0 2 5 13 9 0 [0.00] SYN031-1 theorem 0.0 2 3 5 2 0 0 0 0 2 4 19 20 0 [0.00] SYN032-1 theorem 0.0 2 3 7 2 0 14 0 0 2 5 13 9 0 [0.00] SYN034-1 theorem 0.0 2 4 4 3 0 0 0 1 2 4 16 18 0 [0.00] SYN036-2 non_thm 0.0 2 0 0 1 0 44 0 15 2 0 0 16 0 [0.00] SYN038-1 theorem 0.0 2 9 0 37 0 0 0 111 5 16 0 182 0 [0.00] SYN044-1 theorem 0.0 2 2 4 1 0 9 0 0 2 3 9 5 0 [0.00] SYN045-1 theorem 0.0 2 1 3 0 0 3 0 0 2 3 5 4 0 [0.00] SYN047-1 theorem 0.0 2 1 4 0 0 6 0 0 2 4 7 2 0 [0.00] SYN051-1 theorem 0.0 2 2 2 1 0 6 0 0 2 2 8 4 0 [0.00] SYN052-1 theorem 0.0 2 2 2 1 0 5 0 0 2 2 9 5 0 [0.00] SYN053-1 theorem 0.0 2 2 1 1 0 4 0 0 2 2 9 7 0 [0.00] SYN054-1 theorem 0.0 2 2 5 1 0 1 0 0 2 4 9 6 0 [0.00] SYN055-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 12 10 0 [0.00] SYN056-1 non_thm 0.0 2 0 2 2 0 0 0 7 2 0 4 9 0 [0.00] SYN059-1 non_thm 0.0 2 0 5 7 0 11 0 119 2 0 28 126 0 [0.00] SYN060-1 theorem 0.0 2 1 3 0 0 0 0 0 2 3 5 6 0 [0.00] SYN061-1 theorem 0.0 2 1 5 0 0 0 0 0 2 5 7 2 0 [0.00] SYN063-1 theorem 0.0 2 1 2 0 0 5 0 0 2 2 6 0 0 [0.00] SYN066-1 theorem 0.0 2 1 4 0 0 3 1 0 2 4 6 2 0 [0.00] SYN069-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 16 13 0 [0.00] SYN070-1 theorem 0.0 2 1 15 0 0 0 0 0 2 15 43 84 0 [0.00] SYN081-1 theorem 0.0 2 2 0 4 0 0 0 4 3 3 0 10 0 [0.00] SYN082-1 theorem 0.0 2 3 3 2 0 5 0 1 3 3 19 14 0 [0.00] SYN084-1 non_thm 0.0 2 0 1 1 0 14 1 11 3 0 5 12 0 [0.00] SYN084-2 theorem 0.0 2 4 17 4 0 19 0 5 3 9 29 42 0 [0.00] SYN091-1.003 non_thm 0.0 2 0 2 4 0 6 0 4 2 0 4 8 0 [0.00] SYN092-1.003 non_thm 0.0 2 0 0 9 0 7 0 6 2 0 0 15 0 [0.00] SYN093-1.002 theorem 0.0 2 2 10 1 0 15 0 0 2 8 16 8 0 [0.00] SYN094-1.005 theorem 5.5 6 16384 75927 26775 0 143799 0 53270 2 45 141463 128438 0 [0.00] SYN097-1.002 theorem 0.0 2 2 14 1 0 20 0 3 2 12 20 13 0 [0.00] SYN098-1.002 theorem 0.0 2 32 264 127 0 472 0 230 2 31 392 481 0 [0.00] SYN099-1.003 theorem 0.0 2 1 16 0 0 2 0 0 2 16 35 12 0 [0.00] SYN100-1.005 theorem 0.0 2 1 42 0 0 0 0 0 2 42 83 37 0 [0.00] SYN304-1 non_thm 0.0 2 0 6 1 0 0 0 3 2 0 9 4 0 [0.00] SYN306-1 timeout 300.0 5 [0.00] SYN308-1 non_thm 0.0 2 0 1 2 0 0 0 0 3 0 1 2 0 [0.00] SYN309-1 non_thm 0.0 2 0 2 2 0 0 0 0 2 0 2 2 0 [0.00] SYN315-1 theorem 0.0 2 2 2 1 0 4 0 0 2 2 8 4 0 [0.00] SYN316-1 timeout 300.0 2 [0.00] SYN317-1 non_thm 0.0 2 0 2 0 0 3 0 1 2 0 3 1 0 [0.00] SYN319-1 theorem 0.0 2 1 3 0 0 1 0 0 2 3 5 2 0 [0.00] SYN320-1 non_thm 0.0 2 0 2 1 0 0 0 0 2 0 2 1 0 [0.00] SYN321-1 theorem 0.0 2 2 2 1 0 3 0 0 2 2 8 4 0 [0.00] SYN323-1 theorem 0.0 2 3 2 3 0 0 0 0 2 3 6 7 0 [0.00] SYN324-1 timeout 300.0 2 [0.00] SYN325-1 theorem 0.0 2 1 2 0 0 1 0 0 2 2 3 3 0 [0.00] SYN326-1 theorem 0.0 2 1 4 0 0 3 0 0 2 4 6 4 0 [0.00] SYN327-1 theorem 0.0 2 4 4 3 0 0 0 0 2 4 22 25 0 [0.00] SYN328-1 theorem 0.0 2 18 0 74 0 0 0 408 6 17 0 624 0 [0.00] SYN330-1 timeout 300.0 26 [0.00] SYN331-1 theorem 0.0 2 1 6 0 0 0 0 0 4 6 15 7 0 [0.00] SYN332-1 theorem 0.7 2 3 0 98 0 0 0 2065 5 96 0 2739 0 [0.00] SYN334-1 theorem 0.0 2 9 0 37 0 0 0 111 5 16 0 182 0 [0.00] SYN335-1 timeout 300.0 50 [0.00] SYN343-1 theorem 0.0 2 2 1 1 0 2 0 0 2 2 5 2 0 [0.00] SYN344-1 non_thm 0.0 2 0 0 2 0 0 0 0 2 0 0 2 0 [0.00] SYN345-1 theorem 0.0 2 4 6 3 0 14 0 0 2 4 22 15 0 [0.00] SYN347-1 theorem 0.0 2 12 10 14 0 4 0 23 2 8 68 88 0 [0.00] SYN348-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 [0.00] SYN349-1 theorem 0.0 2 17 0 29 0 0 0 109 3 9 0 373 0 [0.00] SYN350-1 theorem 0.0 2 5 4 6 0 0 0 19 3 8 20 57 0 [0.00] SYN351-1 timeout 300.0 27 [0.00] SYN352-1 theorem 0.0 2 4 5 7 0 0 0 44 3 11 8 85 0 [0.00] SYN354-1 theorem 0.0 2 3 2 2 0 0 0 0 2 4 15 6 0 [0.00] SYN419-1 non_thm 0.0 2 0 47 43 0 103 0 244 2 0 63 305 0 [0.00] SYN422-1 non_thm 0.1 2 0 47 63 0 107 0 264 2 0 61 341 0 [0.00] SYN425-1 non_thm 0.1 2 0 140 97 0 124 0 1047 2 0 173 1309 0 [0.00] SYN430-1 non_thm 0.0 2 0 36 11 0 15 0 176 2 0 50 244 0 [0.00] SYN431-1 non_thm 0.0 2 1 45 13 0 19 0 204 2 13 60 254 0 [0.00] SYN432-1 non_thm 0.0 2 0 54 16 0 21 0 759 2 0 70 839 0 [0.00] SYN433-1 non_thm 0.9 4 2 58 19 0 26 0 17630 2 61 168 36708 0 [0.00] SYN445-1 theorem 4.3 4 49 958 54 0 378 0 60673 2 93 4038 302906 0 [0.00] SYN462-1 theorem 2.1 3 60 946 66 0 423 0 38588 2 67 4580 167046 0 [0.00] SYN490-1 non_thm 0.0 2 0 13 4 0 6 0 30 2 0 16 34 0 [0.00] SYN491-1 non_thm 0.0 2 0 10 3 0 7 0 19 2 0 12 22 0 [0.00] SYN492-1 non_thm 0.0 2 0 7 2 0 6 0 9 2 0 8 11 0 [0.00] SYN493-1 non_thm 0.0 2 0 10 3 0 7 0 17 2 0 12 20 0 [0.00] SYN494-1 non_thm 0.0 2 0 7 2 0 5 0 15 2 0 8 17 0 [0.00] SYN495-1 non_thm 0.0 2 0 25 8 0 10 0 55 2 0 32 63 0 [0.00] SYN496-1 non_thm 0.0 2 0 7 2 0 6 0 5 2 0 8 7 0 [0.00] SYN497-1 non_thm 0.0 2 0 13 4 0 6 0 14 2 0 16 18 0 [0.00] SYN515-1 non_thm 0.0 2 0 7 11 0 22 0 27 2 0 9 38 0 [0.00] SYN516-1 non_thm 0.0 2 0 0 6 0 12 0 14 2 0 0 20 0 [0.00] SYN517-1 non_thm 0.0 2 1 15 7 0 24 0 40 2 18 23 62 0 [0.00] SYN521-1 non_thm 0.0 2 0 16 11 0 16 0 86 2 0 18 97 0 [0.00] SYN522-1 non_thm 0.0 2 0 13 17 0 29 0 68 2 0 16 85 0 [0.00] SYN523-1 non_thm 0.0 2 0 2 10 0 13 0 18 2 0 3 28 0 [0.00] SYN524-1 non_thm 0.0 2 0 10 10 0 25 0 36 2 0 13 47 0 [0.00] SYN525-1 non_thm 0.0 2 0 8 14 0 27 0 36 2 0 11 50 0 [0.00] SYN526-1 non_thm 0.0 2 0 9 10 0 28 0 29 2 0 12 39 0 [0.00] SYN527-1 non_thm 0.0 2 0 12 9 0 24 0 31 2 0 16 43 0 [0.00] SYN528-1 non_thm 0.0 2 0 6 14 0 21 0 39 2 0 7 53 0 [0.00] SYN529-1 non_thm 0.0 2 0 24 16 0 33 0 82 2 0 30 110 0 [0.00] SYN530-1 non_thm 0.0 2 0 7 12 0 20 0 39 2 0 8 52 0 [0.00] SYN531-1 non_thm 0.0 2 0 16 18 0 28 0 57 2 0 18 81 0 [0.00] SYN532-1 non_thm 0.0 2 0 20 11 0 34 0 65 2 0 26 80 0 [0.00] SYN533-1 non_thm 0.0 2 0 13 12 0 20 0 46 2 0 16 58 0 [0.00] SYN534-1 non_thm 0.0 2 0 12 10 0 26 0 26 2 0 15 36 0 [0.00] SYN535-1 non_thm 0.0 2 0 5 11 0 26 0 30 2 0 8 42 0 [0.00] SYN536-1 non_thm 0.0 2 0 15 9 0 25 0 39 2 0 17 48 0 [0.00] SYN537-1 non_thm 0.0 2 0 28 11 0 36 0 52 2 0 31 78 0 [0.00] SYN538-1 non_thm 0.0 2 0 2 13 0 27 0 24 2 0 3 37 0 [0.00] SYN539-1 non_thm 0.0 2 0 7 12 0 31 0 33 2 0 10 48 0 [0.00] SYN540-1 non_thm 0.0 2 3 27 16 0 60 0 58 2 30 60 99 0 [0.00] SYN541-1 non_thm 0.0 2 0 22 21 0 39 0 95 2 0 24 116 0 [0.00] SYN554-1 theorem 0.0 2 1 10 0 0 0 0 0 2 10 43 22 0 [0.00] SYN567-1 theorem 0.0 2 1 8 0 0 0 0 0 4 8 25 11 0 [0.00] SYN568-1 theorem 0.0 2 1 8 0 0 0 0 0 5 8 29 16 0 [0.00] SYN571-1 theorem 0.0 2 1 23 0 0 0 0 0 3 23 74 45 0 [0.00] SYN573-1 theorem 0.0 2 1 8 0 0 0 0 0 2 8 23 13 0 [0.00] SYN574-1 theorem 0.0 2 2 18 1 0 0 0 28 3 17 63 36 0 [0.00] SYN575-1 theorem 0.0 2 2 18 1 0 0 0 28 3 17 63 36 0 [0.00] SYN576-1 theorem 0.5 3 1 118 0 0 0 0 0 4 118 2989 2971 0 [0.00] SYN578-1 theorem 0.0 2 2 54 1 0 0 0 258 3 53 298 269 0 [0.00] SYN579-1 theorem 0.0 2 2 54 1 0 0 0 258 3 53 298 269 0 [0.00] SYN580-1 theorem 0.0 2 1 21 0 0 0 0 0 2 21 65 31 0 [0.00] SYN581-1 theorem 0.0 2 1 34 0 0 0 0 0 3 34 205 156 0 [0.00] SYN582-1 theorem 0.0 2 1 28 0 0 0 0 0 3 28 157 105 0 [0.00] SYN583-1 theorem 0.0 2 1 27 0 0 0 0 0 3 27 236 223 0 [0.00] SYN585-1 timeout 300.0 37 [0.00] SYN586-1 theorem 0.0 2 1 42 0 0 0 0 0 3 42 205 203 0 [0.00] SYN587-1 theorem 0.0 2 1 23 0 0 0 0 0 2 23 78 66 0 [0.00] SYN591-1 theorem 0.0 2 1 29 0 0 0 0 0 3 29 98 72 0 [0.00] SYN592-1 theorem 0.0 2 1 25 0 0 0 0 0 3 25 79 54 0 [0.00] SYN593-1 theorem 0.0 2 1 10 0 0 0 0 0 2 10 31 34 0 [0.00] SYN594-1 theorem 0.0 2 1 20 0 0 0 0 0 5 20 62 25 0 [0.00] SYN595-1 theorem 108.6 25 1 52 0 0 0 0 0 5 52 1141 878 0 [0.00] SYN604-1 theorem 238.5 10 1 441 0 0 0 0 0 6 441 12872 11842 0 [0.00] SYN605-1 theorem 0.4 4 1 131 0 0 1 0 0 4 131 2980 2958 0 [0.00] SYN606-1 timeout 300.0 20 [0.00] SYN608-1 theorem 0.5 4 1 153 0 0 1 0 0 4 153 3412 3390 0 [0.00] SYN613-1 theorem 0.0 2 1 14 0 0 0 0 0 3 14 47 28 0 [0.00] SYN619-1 theorem 0.0 2 1 23 0 0 0 0 0 4 23 115 88 0 [0.00] SYN620-1 theorem 0.0 2 1 67 0 0 0 0 0 4 67 283 267 0 [0.00] SYN621-1 timeout 300.0 79 [0.00] SYN622-1 theorem 0.0 2 1 17 0 0 0 0 0 4 17 107 87 0 [0.00] SYN623-1 theorem 1.4 5 1 513 0 0 0 0 0 4 513 13804 13608 0 [0.00] SYN624-1 theorem 117.4 17 1 30 0 0 0 0 0 6 30 198 167 0 [0.00] SYN625-1 theorem 0.0 2 1 23 0 0 0 0 0 5 23 73 35 0 [0.00] SYN626-1 theorem 0.0 2 1 24 0 0 0 0 0 5 24 83 60 0 [0.00] SYN627-1 theorem 0.2 2 1 36 0 0 0 0 0 3 36 215 162 0 [0.00] SYN633-1 timeout 300.0 10 [0.00] SYN641-1 theorem 0.2 2 1 178 0 0 0 0 0 4 178 1115 2509 0 [0.00] SYN642-1 theorem 0.2 2 1 170 0 0 0 0 0 4 170 1091 2485 0 [0.00] SYN643-1 theorem 0.2 2 1 174 0 0 0 0 0 4 174 1103 2497 0 [0.00] SYN644-1 timeout 300.0 40 [0.00] SYN656-1 theorem 0.0 2 1 38 0 0 0 0 0 5 38 120 38 0 [0.00] SYN657-1 timeout 300.0 10 [0.00] SYN658-1 timeout 300.0 10 [0.00] SYN659-1 theorem 3.2 5 1 221 0 0 0 0 0 4 221 2111 2074 0 [0.00] SYN660-1 theorem 0.1 2 1 91 0 0 0 0 0 3 91 466 401 0 [0.00] SYN661-1 theorem 0.0 2 1 82 0 0 0 0 0 3 82 434 401 0 [0.00] SYN662-1 theorem 0.0 2 1 59 0 0 0 0 0 3 59 214 153 0 [0.00] SYN663-1 theorem 0.0 2 1 50 0 0 0 0 0 3 50 184 153 0 [0.00] SYN664-1 theorem 0.1 2 1 91 0 0 0 0 0 3 91 466 401 0 [0.00] SYN665-1 theorem 0.1 2 1 82 0 0 0 0 0 3 82 434 401 0 [0.00] SYN666-1 theorem 0.0 2 1 61 0 0 0 0 0 3 61 249 202 0 [0.00] SYN667-1 theorem 0.0 2 1 56 0 0 0 0 0 3 56 235 202 0 [0.00] SYN668-1 theorem 0.0 2 1 61 0 0 0 0 0 3 61 249 202 0 [0.00] SYN669-1 theorem 0.0 2 1 56 0 0 0 0 0 3 56 235 202 0 [0.00] SYN670-1 theorem 0.0 2 1 33 0 0 0 0 0 3 33 85 42 0 [0.00] SYN671-1 theorem 0.0 2 1 28 0 0 0 0 0 3 28 73 42 0 [0.00] SYN672-1 theorem 0.0 2 1 30 0 0 0 0 0 4 30 90 54 0 [0.00] SYN674-1 theorem 0.1 2 1 92 0 0 0 0 0 3 92 467 401 0 [0.00] SYN675-1 theorem 0.0 2 1 83 0 0 0 0 0 3 83 435 401 0 [0.00] SYN676-1 theorem 0.0 2 1 60 0 0 0 0 0 3 60 215 153 0 [0.00] SYN677-1 theorem 0.0 2 1 51 0 0 0 0 0 3 51 185 153 0 [0.00] SYN678-1 theorem 0.1 2 1 92 0 0 0 0 0 3 92 467 401 0 [0.00] SYN679-1 theorem 0.0 2 1 83 0 0 0 0 0 3 83 435 401 0 [0.00] SYN680-1 theorem 0.0 2 1 92 0 0 0 0 0 3 92 467 401 0 [0.00] SYN681-1 theorem 0.0 2 1 83 0 0 0 0 0 3 83 435 401 0 [0.00] SYN682-1 theorem 0.0 2 1 92 0 0 0 0 0 3 92 467 401 0 [0.00] SYN683-1 theorem 0.0 2 1 83 0 0 0 0 0 3 83 435 401 0 [0.00] SYN684-1 theorem 0.0 2 1 60 0 0 0 0 0 3 60 215 153 0 [0.00] SYN685-1 theorem 0.0 2 1 51 0 0 0 0 0 3 51 185 153 0 [0.00] SYN686-1 theorem 0.2 3 1 64 0 0 0 0 0 4 64 521 506 0 [0.00] SYN692-1 timeout 300.0 283 [0.00] SYN693-1 timeout 300.0 300 [0.00] SYN694-1 timeout 300.0 221 [0.00] SYN695-1 timeout 300.0 256 [0.00] SYN696-1 timeout 300.0 250 [0.00] SYN697-1 timeout 300.0 292 [0.00] SYN698-1 timeout 300.0 221 [0.00] SYN699-1 timeout 300.0 240 [0.00] SYN700-1 timeout 300.0 253 [0.00] SYN701-1 timeout 300.0 283 [0.00] SYN710-1 theorem 0.0 2 1 53 0 0 0 0 0 4 53 154 97 0 [0.00] SYN713-1 theorem 0.0 2 1 60 0 0 0 0 0 4 60 200 154 0 [0.00] SYN714-1 theorem 0.0 2 1 38 0 0 0 0 0 3 38 136 96 0 [0.00] SYN717-1 theorem 0.0 2 1 50 0 0 0 0 0 2 50 131 84 0 [0.00] SYN718-1 theorem 1.1 3 1 144 0 0 0 0 0 4 144 672 580 0 [0.00] SYN724-1 theorem 0.0 2 2 5 1 0 6 0 0 2 4 9 6 0 [0.00] SYN726-1 theorem 0.0 2 6 47 22 0 0 0 196 2 30 193 537 0 [0.00] SYN728-1 theorem 0.0 2 3 3 6 0 3 0 1 5 6 9 11 0 [0.00] SYN734-1 non_thm 0.0 2 0 1 1 0 0 0 0 2 0 1 1 0 [0.00] SYN735-1 non_thm 0.0 2 0 1 2 0 0 0 4 2 0 1 6 0 [0.00] SYN738-1 non_thm 0.0 2 0 1 0 0 0 0 0 2 0 1 0 0 [0.00] SYN740-1 non_thm 0.0 2 0 1 0 0 0 0 0 2 0 1 0 0 [0.00] SYN743-1 non_thm 0.0 2 0 1 7 0 0 0 12 2 0 1 19 0 [0.00] SYN744-1 non_thm 0.0 2 0 1 2 0 0 0 1 2 0 1 3 0 [0.00] SYN756-1 non_thm 0.0 2 0 1 0 0 0 0 0 2 0 1 0 0 [0.00] SYN772-1 non_thm 0.0 2 0 2 7 0 0 0 37 3 0 2 44 0 [0.00] SYN811-1 non_thm 1.2 5 0 376 86 0 489 29 451 2 0 712 537 0 [0.00] SYN819-1 theorem 1.8 5 18 188 959 0 269 136 1420 2 356 366 2797 0 [0.00] SYN823-1 non_thm 0.3 3 0 160 86 0 249 0 230 2 0 288 316 0 [0.00] SYN824-1 non_thm 3.3 9 0 515 126 0 896 0 624 2 0 965 750 0 [0.00] SYN827-1 non_thm 0.7 4 3 188 140 0 269 0 493 2 319 343 676 0 [0.00] SYN833-1 theorem 0.7 4 13 188 223 0 269 1 410 2 271 353 722 0 [0.00] SYN834-1 theorem 1.1 4 30 188 582 0 269 1 864 2 353 370 1689 0 [0.00] SYN835-1 non_thm 0.8 4 4 188 285 0 269 5 635 2 375 344 959 0 [0.00] SYN836-1 theorem 0.7 4 7 188 250 0 269 5 436 2 325 347 821 0 [0.00] SYN837-1 theorem 59.2 10 346 376 17974 0 489 372 31503 2 824 1046 57044 0 [0.00] SYN844-1 theorem 1.9 5 26 188 809 0 269 16 1375 2 343 366 2848 0 [0.00] SYN845-1 theorem 1.0 4 17 188 405 0 269 9 729 2 293 357 1477 0 [0.00] SYN847-1 theorem 28.5 10 204 376 7476 0 489 104 14286 2 906 904 25698 0 [0.00] SYN848-1 theorem 3.7 8 21 376 979 0 489 3 1523 2 644 721 2949 0 [0.00] SYN849-1 theorem 4.8 8 33 376 1180 0 489 8 1922 2 585 733 3797 0 [0.00] SYN856-1 theorem 0.9 4 10 188 283 0 269 0 521 2 314 350 1017 0 [0.00] SYN857-1 theorem 1.5 5 19 188 628 0 269 12 1060 2 369 359 2263 0 [0.00] SYN858-1 theorem 12.2 9 70 376 3135 0 489 72 4867 2 764 770 11091 0 [0.00] SYN859-1 theorem 4.8 8 30 376 1050 0 489 0 1987 2 622 730 3625 0 [0.00] SYN860-1 theorem 85.6 13 366 376 18616 0 489 365 36392 2 931 1066 75544 0 [0.00] SYN867-1 non_thm 0.1 2 0 48 12 0 458 0 44 2 0 48 56 0 [0.00] SYN868-1 non_thm 0.1 2 0 45 6 0 433 0 39 2 0 45 45 0 [0.00] SYN869-1 theorem 0.1 2 3 36 10 0 266 0 37 2 42 39 74 0 [0.00] SYN870-1 non_thm 0.1 2 0 36 12 0 262 0 51 2 0 36 66 0 [0.00] SYN871-1 theorem 0.3 2 20 36 114 0 256 0 317 2 58 56 578 0 [0.00] SYN872-1 non_thm 0.6 4 0 94 4 0 1717 0 76 2 0 94 80 0 [0.00] SYN873-1 theorem 0.2 2 10 36 52 0 269 0 83 2 50 46 202 0 [0.00] SYN874-1 theorem 0.1 2 6 36 21 0 269 0 31 2 45 42 105 0 [0.00] SYN876-1 theorem 1.1 3 17 52 122 0 487 1 443 2 91 69 774 0 [0.00] SYN877-1 theorem 0.1 3 3 36 12 0 268 0 43 2 43 39 108 0 [0.00] SYN878-1 theorem 0.1 2 4 36 16 0 271 0 36 2 44 40 103 0 [0.00] SYN879-1 theorem 0.1 2 4 36 14 0 271 0 36 2 44 40 132 0 [0.00] SYN881-1 theorem 2.3 3 78 52 404 0 490 0 1225 2 88 130 2465 0 [0.00] SYN882-1 theorem 0.5 3 15 52 87 0 485 0 205 2 96 67 445 0 [0.00] SYN884-1 theorem 0.4 3 6 70 18 0 932 0 68 2 80 76 126 0 [0.00] SYN885-1 theorem 4.9 4 56 72 367 0 908 0 856 2 155 128 1974 0 [0.00] SYN886-1 theorem 0.3 3 2 72 8 0 909 0 56 2 77 74 89 0 [0.00] SYN887-1 theorem 0.4 3 5 72 18 0 938 0 61 2 81 77 130 0 [0.00] SYN888-1 non_thm 1.1 5 4 102 30 0 1760 0 101 2 120 106 145 0 [0.00] SYN889-1 theorem 0.1 2 2 36 4 0 271 0 29 2 39 38 81 0 [0.00] SYN890-1 theorem 0.1 2 2 36 8 0 273 0 33 2 41 38 84 0 [0.00] SYN892-1 theorem 0.1 2 2 36 10 0 273 0 33 2 45 38 110 0 [0.00] SYN893-1 theorem 0.2 2 3 52 16 0 485 0 47 2 62 55 125 0 [0.00] SYN894-1 theorem 0.2 2 2 52 7 0 489 0 42 2 57 54 80 0 [0.00] SYN895-1 theorem 0.2 2 4 52 16 0 479 0 55 2 64 56 130 0 [0.00] SYN896-1 theorem 0.3 3 6 52 33 0 492 0 90 2 70 58 220 0 [0.00] SYN897-1 timeout 300.0 10 [0.00] SYN898-1 theorem 8.7 5 110 72 905 0 941 8 1593 2 154 182 4395 0 [0.00] SYN899-1 theorem 1.0 4 14 72 95 0 931 0 132 2 105 86 389 0 [0.00] SYN900-1 theorem 1.4 4 24 72 91 0 923 0 236 2 112 96 535 0 [0.00] SYN902-1 non_thm 10.4 6 12 102 177 0 1757 12 1231 2 246 114 2108 0 [0.00] TOP002-2 theorem 0.0 2 1 2 0 0 0 0 0 2 2 4 2 0 [0.00] TOP004-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 2 0 [0.00] TOP004-2 theorem 0.0 2 1 1 0 0 0 0 0 2 1 5 1 0 [0.12] ANA002-4 timeout 300.0 14 [0.12] ANA003-4 timeout 300.0 196 [0.12] FLD002-3 theorem 0.0 2 1 63 0 0 0 0 0 2 63 300 2005 0 [0.12] FLD007-3 timeout 300.0 57 [0.12] FLD008-4 theorem 0.1 2 1 145 0 0 0 0 0 2 145 804 7875 0 [0.12] FLD010-5 theorem 0.0 2 1 54 0 0 0 0 0 2 54 658 341 0 [0.12] FLD014-3 theorem 0.2 2 1 192 0 0 0 0 0 2 192 3602 2729 0 [0.12] FLD018-1 timeout 300.0 12 [0.12] FLD019-1 timeout 300.0 12 [0.12] FLD023-1 theorem 87.6 12 1 212 0 0 0 0 0 3 212 10330 36163 0 [0.12] FLD025-2 theorem 33.9 4 1 460 0 0 0 0 0 2 460 2232 23137 0 [0.12] FLD026-3 theorem 0.5 3 1 410 0 0 0 0 0 2 410 12031 3013 0 [0.12] FLD029-3 theorem 0.5 3 1 589 0 0 0 0 0 2 589 8391 8884 0 [0.12] FLD031-1 timeout 300.0 13 [0.12] FLD032-1 timeout 300.0 12 [0.12] FLD037-1 theorem 134.3 14 1 275 0 0 0 0 0 3 275 11553 51689 0 [0.12] FLD040-3 theorem 0.0 2 1 67 0 0 0 0 0 2 67 537 907 0 [0.12] FLD040-5 theorem 0.0 2 1 68 0 0 0 0 0 2 68 601 904 0 [0.12] FLD041-3 theorem 0.1 2 1 188 0 0 0 0 0 2 188 2588 2269 0 [0.12] FLD042-3 theorem 0.1 2 1 188 0 0 0 0 0 2 188 2588 2269 0 [0.12] FLD060-3 theorem 32.1 17 1 996 0 0 0 0 0 2 996 145733 26815 0 [0.12] FLD061-2 theorem 33.9 4 1 421 0 0 0 0 0 2 421 1571 22732 0 [0.12] FLD061-3 theorem 188.5 35 1 1854 0 0 0 0 0 2 1854 290812 57117 0 [0.12] FLD063-3 theorem 23.9 15 1 818 0 0 0 0 0 2 818 111768 25639 0 [0.12] FLD064-1 timeout 300.0 12 [0.12] FLD065-1 timeout 300.0 12 [0.12] FLD066-3 theorem 0.2 3 1 207 0 0 0 0 0 2 207 1580 13965 0 [0.12] FLD067-1 theorem 86.7 12 1 202 0 0 0 0 0 3 202 9543 35389 0 [0.12] FLD067-2 timeout 300.0 17 [0.12] FLD067-3 timeout 300.0 43 [0.12] FLD068-3 timeout 300.0 44 [0.12] HWV006-1 theorem 0.1 2 1 356 0 0 1 4 0 4 356 1440 162 0 [0.12] HWV006-2 unsound 0.1 3 0 864 3 0 0 0 118 4 0 1699 124 0 [0.12] HWV008-1.001 theorem 0.1 2 1 215 0 0 0 0 0 5 215 653 133 0 [0.12] HWV008-1.002 theorem 0.1 2 1 324 0 0 0 0 0 5 324 934 210 0 [0.12] HWV008-2.001 theorem 0.0 2 1 215 0 0 0 0 0 5 215 601 100 0 [0.12] HWV008-2.002 theorem 0.1 2 1 326 0 0 0 0 0 5 326 866 162 0 [0.12] NLP079-1 theorem 0.0 2 2 40 1 0 4 0 0 2 22 82 55 0 [0.12] NLP080-1 theorem 0.0 2 2 40 1 0 4 0 0 2 22 80 55 0 [0.12] NLP081-1 theorem 0.0 2 2 38 1 0 4 0 0 2 21 76 52 0 [0.12] NLP094-1 theorem 0.0 2 2 41 1 0 4 0 0 2 23 50 44 0 [0.12] PUZ035-4 theorem 0.0 2 4 12 3 0 8 0 2 2 8 27 6 0 [0.12] SET010-1 theorem 0.1 2 3 835 2 0 0 61 0 2 486 3402 997 0 [0.12] SYN002-1.007.008 theorem 0.1 2 2 0 37 0 0 0 234 23 22 0 309 0 [0.12] SYN036-4 theorem 0.0 2 8 9 7 0 98 6 7 2 5 77 173 0 [0.12] SYN039-1 theorem 0.2 2 17 20 53 0 0 11 1390 4 16 125 3150 0 [0.12] SYN560-1 theorem 0.6 3 1 39 0 0 0 0 0 5 39 1011 987 0 [0.12] SYN607-1 timeout 300.0 20 [0.12] SYN609-1 timeout 300.0 20 [0.12] SYN610-1 timeout 300.0 20 [0.12] SYN611-1 timeout 300.0 21 [0.12] SYN612-1 timeout 300.0 20 [0.12] SYN630-1 theorem 0.0 2 1 9 0 0 0 0 0 2 9 28 19 0 [0.12] SYN634-1 timeout 300.0 10 [0.12] SYN635-1 timeout 300.0 10 [0.12] SYN636-1 timeout 300.0 10 [0.12] SYN645-1 timeout 300.0 39 [0.12] SYN648-1 timeout 300.0 164 [0.12] SYN687-1 theorem 3.9 2 1 41 0 0 0 0 0 7 41 128 48 0 [0.12] TOP001-2 timeout 300.0 30 [0.12] TOP005-2 timeout 300.0 19 [0.17] GRP126-4.004 theorem 0.0 2 2 67 1 0 0 0 51 2 63 403 367 0 [0.17] GRP127-4.004 theorem 0.0 2 2 68 1 0 0 0 51 2 63 429 368 0 [0.17] GRP128-3.005 theorem 0.1 2 7 395 6 0 0 0 78 2 207 1467 858 0 [0.17] GRP129-4.004 theorem 0.0 2 9 116 8 0 0 0 35 2 51 665 526 0 [0.17] MSC008-1.002 theorem 0.2 2 32 155 53 0 0 0 2400 2 23 1364 9005 0 [0.17] MSC008-2.002 theorem 0.2 2 32 155 53 0 0 0 2640 2 23 1188 7397 0 [0.17] PUZ010-1 theorem 1.0 2 344 6918 359 0 446 0 4981 2 204 20149 27734 0 [0.17] PUZ017-1 theorem 0.1 2 5 302 4 0 1 5 403 2 231 1159 1598 0 [0.17] PUZ018-1 theorem 0.0 2 1 53 0 0 6 0 0 2 53 84 891 0 [0.17] PUZ019-1 theorem 0.0 2 1 116 0 0 1 3 0 2 116 333 577 0 [0.17] PUZ028-6 theorem 0.0 2 20 376 19 0 0 0 102 2 82 1298 292 0 [0.17] SYN444-1 theorem 1.1 3 74 1039 78 0 444 0 14120 2 77 5187 73372 0 [0.17] SYN461-1 theorem 0.9 3 77 900 81 0 468 0 12051 2 58 3429 67880 0 [0.17] SYN471-1 theorem 5.6 4 53 610 55 0 298 0 119917 2 80 4018 330058 0 [0.17] SYN480-1 theorem 2.0 3 73 999 76 0 492 0 27970 2 62 4510 153883 0 [0.17] SYN484-1 theorem 0.7 3 32 507 32 0 228 0 5298 2 54 2132 67599 0 [0.17] SYN501-1 theorem 0.8 3 25 390 24 0 184 0 7069 2 63 1729 67583 0 [0.17] SYN510-1 theorem 1.9 3 124 1840 139 0 867 0 20351 2 77 7230 132401 0 [0.17] SYN813-1 theorem 1.1 4 12 188 562 0 269 137 704 2 335 360 1413 0 [0.17] SYN820-1 theorem 1.3 5 12 188 628 0 269 95 1150 2 389 360 2090 0 [0.17] SYN843-1 theorem 0.6 4 7 188 138 0 269 1 343 2 286 347 573 0 [0.17] SYN846-1 theorem 75.1 13 606 376 19373 0 489 154 28766 2 951 1306 56954 0 [0.17] SYN862-1 theorem 22.0 17 51 696 2907 0 939 24 4445 2 1202 1371 8219 0 [0.17] SYN875-1 theorem 0.1 2 4 36 18 0 265 0 36 2 44 40 112 0 [0.17] SYN880-1 theorem 0.2 2 2 52 12 0 488 0 42 2 62 54 95 0 [0.17] SYN883-1 theorem 0.3 3 8 52 38 0 491 0 108 2 69 60 242 0 [0.17] SYN891-1 theorem 0.1 2 2 36 4 0 259 0 29 2 39 38 75 0 [0.17] SYN901-1 theorem 1.3 5 11 101 46 0 1680 0 125 2 130 112 227 0 [0.20] HWV035-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.20] HWV035-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.20] HWV036-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.20] NLP059-1 non_thm 0.0 2 0 10 4 0 3 0 26 2 0 10 30 0 [0.20] NLP064-1 non_thm 0.0 2 1 20 10 0 3 3 29 3 27 25 59 0 [0.20] NLP234-1 non_thm 0.0 2 0 38 1 0 4 0 72 2 0 38 73 0 [0.20] NLP237-1 non_thm 0.0 2 0 38 1 0 4 0 72 2 0 38 73 0 [0.20] SYN737-1 non_thm 0.0 2 0 1 11 0 0 0 198 5 0 1 238 0 [0.20] SYN739-1 non_thm 0.0 2 0 1 5 0 0 0 2 2 0 1 7 0 [0.20] SYN741-1 timeout 300.0 4 [0.20] SYN742-1 non_thm 0.0 2 0 1 0 0 0 0 0 2 0 1 0 0 [0.20] SYN748-1 non_thm 0.0 2 0 1 5 0 0 0 61 4 0 1 68 0 [0.20] SYN749-1 non_thm 0.0 2 0 1 0 0 0 0 0 2 0 1 0 0 [0.20] SYN754-1 non_thm 0.0 2 0 1 6 0 0 0 13 5 0 1 19 0 [0.20] SYN757-1 non_thm 0.0 2 0 1 3 0 0 0 26 2 0 1 29 0 [0.20] SYN760-1 non_thm 0.0 2 0 1 0 0 0 0 0 2 0 1 0 0 [0.20] SYN774-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.20] SYN785-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.20] SYN798-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.25] ANA002-2 timeout 300.0 36 [0.25] ANA004-4 timeout 300.0 200 [0.25] FLD003-1 timeout 300.0 16 [0.25] FLD004-1 timeout 300.0 16 [0.25] FLD005-1 timeout 300.0 16 [0.25] FLD009-1 timeout 300.0 16 [0.25] FLD049-4 theorem 0.4 3 1 295 0 0 0 0 0 2 295 1927 22696 0 [0.25] FLD050-4 theorem 0.4 3 1 298 0 0 0 0 0 2 298 1974 22714 0 [0.25] GRP123-3.004 non_thm 0.0 2 1 143 1 0 0 0 155 2 95 951 257 0 [0.25] GRP123-4.004 non_thm 0.0 2 0 77 1 0 0 0 244 2 0 802 449 0 [0.25] GRP123-8.004 non_thm 0.0 2 0 177 2 0 0 0 234 2 0 879 372 0 [0.25] GRP123-9.004 non_thm 0.0 2 0 138 29 0 0 0 214 2 0 813 379 0 [0.25] GRP125-1.004 non_thm 0.0 2 0 77 1 0 0 0 111 2 0 469 180 0 [0.25] GRP125-2.004 non_thm 0.0 2 0 96 0 0 0 0 112 2 0 490 180 0 [0.25] GRP125-3.004 non_thm 0.0 2 1 143 1 0 0 0 142 2 95 669 247 0 [0.25] GRP125-4.004 non_thm 0.0 2 0 77 1 0 0 0 257 2 0 719 462 0 [0.25] GRP127-2.005 non_thm 0.0 2 1 187 1 0 0 0 239 2 130 1050 542 0 [0.25] GRP127-3.005 non_thm 0.1 2 2 271 2 0 0 0 296 2 181 1407 744 0 [0.25] GRP128-1.004 non_thm 0.0 2 7 171 8 0 0 0 143 2 48 925 392 0 [0.25] GRP128-2.004 non_thm 0.0 2 1 100 3 0 0 0 122 2 40 537 198 0 [0.25] GRP128-3.004 non_thm 0.0 2 3 212 4 0 0 0 156 2 92 876 345 0 [0.25] GRP128-4.004 non_thm 0.0 2 5 83 6 0 0 0 275 2 54 884 512 0 [0.25] GRP130-2.005 non_thm 0.0 2 3 248 4 0 0 0 254 2 136 1296 688 0 [0.25] GRP130-3.004 non_thm 0.0 2 2 202 2 0 0 0 154 2 83 826 334 0 [0.25] GRP130-4.004 non_thm 0.0 2 5 120 6 0 0 0 291 2 40 911 650 0 [0.25] SET012-1 timeout 300.0 52 [0.25] SET012-2 theorem 0.1 2 3 131 2 0 0 0 510 2 102 1735 1045 0 [0.25] SET013-1 timeout 300.0 72 [0.25] SET015-1 timeout 300.0 62 [0.25] SYN036-3 theorem 0.0 2 10 67 9 0 142 5 50 2 17 213 144 0 [0.25] SYN037-1 theorem 0.0 2 9 71 8 0 166 11 39 2 17 224 158 0 [0.25] SYN037-2 theorem 0.0 2 12 22 15 0 87 8 48 2 11 116 146 0 [0.25] SYN313-1.001.002 theorem 6.1 3 951 4505 2066 0 0 4 8248 29 58 5619 26413 0 [0.25] SYN418-1 non_thm 0.1 2 0 59 57 0 95 0 299 2 0 86 367 0 [0.25] SYN420-1 non_thm 0.1 2 1 80 106 0 136 0 1304 2 90 124 1483 0 [0.25] SYN421-1 non_thm 0.1 2 0 45 61 0 97 0 280 2 0 55 343 0 [0.25] SYN423-1 non_thm 0.1 2 0 140 83 0 132 0 599 2 0 166 694 0 [0.25] SYN424-1 non_thm 0.1 3 0 115 114 0 149 0 1441 2 0 138 1677 0 [0.25] SYN426-1 non_thm 0.2 3 1 140 157 0 203 4 1756 2 4 200 2024 0 [0.25] SYN427-1 non_thm 0.2 3 0 165 90 0 151 0 1507 2 0 177 1605 0 [0.25] SYN428-1 non_thm 0.7 3 2 222 252 0 176 0 10437 2 422 316 13755 0 [0.25] SYN429-1 non_thm 0.1 2 1 107 55 0 147 0 426 2 66 159 527 0 [0.25] SYN434-1 non_thm 5.4 9 3 125 30 0 43 0 121598 2 126 1106 182065 0 [0.25] SYN435-1 non_thm 0.3 2 0 91 27 0 32 0 5195 2 0 200 5454 0 [0.25] SYN437-1 non_thm 1.0 3 18 291 39 0 109 0 17162 2 91 2208 52261 0 [0.25] SYN438-1 non_thm 0.8 3 20 174 31 0 100 0 19026 2 55 1021 43369 0 [0.25] SYN446-1 non_thm 0.8 3 13 261 22 0 110 0 12143 2 83 1606 44049 0 [0.25] SYN449-1 non_thm 5.8 3 199 3030 220 0 1339 0 62248 2 89 14805 363070 0 [0.25] SYN456-1 non_thm 8.4 6 225 2444 264 0 1200 0 177007 2 77 13753 491897 0 [0.25] SYN463-1 non_thm 0.3 2 3 75 14 0 37 0 7700 2 65 211 11068 0 [0.25] SYN513-1 non_thm 0.2 2 3 103 79 0 107 0 2025 2 141 183 2801 0 [0.25] SYN518-1 non_thm 0.2 2 0 143 67 0 98 0 2164 2 0 168 2717 0 [0.25] SYN520-1 timeout 300.0 354 [0.25] SYN542-1 non_thm 7.4 10 0 133 75 0 41 0 172369 2 0 806 209099 0 [0.25] SYN543-1 non_thm 8.2 7 0 132 68 0 38 0 159908 2 0 1135 214635 0 [0.25] SYN544-1 non_thm 0.1 2 2 140 79 0 85 0 1890 2 174 181 2042 0 [0.25] SYN546-1 non_thm 0.1 2 0 92 78 0 107 0 852 2 0 115 1072 0 [0.25] SYN547-1 non_thm 0.1 2 1 75 60 0 116 0 570 2 6 115 695 0 [0.25] SYN650-1 timeout 300.0 40 [0.25] SYN690-1 timeout 300.0 8 [0.25] SYN815-1 non_thm 5.3 12 0 674 193 0 939 24 843 2 0 1293 1036 0 [0.25] SYN817-1 non_thm 5.8 12 0 626 207 0 939 11 856 2 0 1198 1063 0 [0.25] SYN828-1 non_thm 5.3 12 0 646 277 0 899 1 986 2 0 1224 1273 0 [0.25] SYN838-1 non_thm 6.8 14 0 634 367 0 939 0 992 2 0 1198 1359 0 [0.25] SYN851-1 non_thm 7.2 14 4 696 537 0 939 0 1254 2 1084 1324 1821 0 [0.25] SYN863-1 non_thm 9.4 16 5 696 856 0 939 0 1809 2 1372 1325 2710 0 [0.25] SYN864-1 non_thm 16.3 17 21 696 2216 0 939 12 3161 2 1281 1341 5540 0 [0.33] GRP127-2.006 theorem 0.1 2 3 313 2 0 0 0 85 2 253 1328 1321 0 [0.33] SYN448-1 theorem 5.6 3 179 2699 201 0 1248 0 53348 2 88 9854 428818 0 [0.33] SYN451-1 theorem 1.0 3 58 758 69 0 363 0 14765 2 61 2933 62397 0 [0.33] SYN454-1 theorem 1.8 3 65 1044 69 0 452 0 16890 2 69 3913 126295 0 [0.33] SYN458-1 theorem 1.1 4 36 759 37 0 317 0 4459 2 85 2535 95403 0 [0.33] SYN459-1 theorem 2.2 3 80 1222 85 0 548 0 24372 2 74 5261 200483 0 [0.33] SYN469-1 theorem 3.8 3 137 2149 148 0 950 0 46563 2 64 8817 332785 0 [0.33] SYN475-1 theorem 3.1 3 67 1051 71 0 506 0 42494 2 65 4467 272434 0 [0.33] SYN478-1 theorem 4.3 4 127 1952 142 0 968 0 46051 2 64 7638 325755 0 [0.33] SYN482-1 theorem 1.9 3 90 1200 99 0 578 0 30947 2 74 7489 101016 0 [0.33] SYN483-1 theorem 1.3 3 62 1091 62 0 520 0 11663 2 66 4195 101424 0 [0.33] SYN485-1 theorem 1.5 3 41 717 40 0 326 0 17423 2 81 2837 128707 0 [0.33] SYN504-1 theorem 2.1 3 33 422 48 0 219 0 36120 2 75 3371 145204 0 [0.33] SYN505-1 theorem 1.1 3 80 920 86 0 537 0 18207 2 72 3456 79254 0 [0.33] SYN506-1 theorem 0.4 3 17 406 18 0 173 0 2696 2 69 1575 30142 0 [0.33] SYN512-1 theorem 1.7 3 66 1629 69 0 684 0 12735 2 86 5202 121291 0 [0.33] SYN850-1 theorem 41.3 17 103 696 6442 0 939 89 9984 2 1179 1423 18566 0 [0.33] SYN861-1 theorem 11.5 16 21 696 1216 0 939 8 2112 2 1088 1341 3841 0 [0.33] SYN865-1 theorem 13.8 18 23 696 1478 0 939 6 2622 2 1268 1343 4468 0 [0.33] SYN866-1 theorem 57.7 18 244 696 9027 0 939 66 11760 2 1135 1564 23089 0 [0.38] ANA002-1 timeout 300.0 37 [0.38] ANA002-3 timeout 300.0 13 [0.38] COM003-1 theorem 4.1 4 673 6793 5147 0 192 0 43029 2 213 21373 169873 0 [0.38] FLD041-4 theorem 0.4 3 1 343 0 0 0 0 0 2 343 10802 5214 0 [0.38] FLD062-3 theorem 86.8 32 1 1101 0 0 0 0 0 2 1101 276678 85188 0 [0.38] GRP039-6 theorem 13.4 4 20 1644 23 0 0 1 26271 2 640 199863 28775 0 [0.38] SET013-2 theorem 0.2 2 3 609 2 0 0 0 510 2 336 6941 2910 0 [0.38] SYN036-1 theorem 7.7 9 46 118 45 0 350 3 45478 2 18 224220 533122 0 [0.38] SYN673-1 theorem 7.1 7 1 558 0 0 0 0 0 6 558 14487 10362 0 [0.38] SYN755-1 theorem 2.4 2 146 1 366 0 0 0 34607 5 21 1 60249 0 [0.38] SYN759-1 theorem 31.3 2 356 1 1125 0 0 0 264671 8 32 1 420170 0 [0.38] SYN784-1 theorem 3.3 2 82 2 340 0 0 0 34461 4 23 2 55259 0 [0.38] SYN796-1 theorem 0.8 2 43 2 146 0 0 0 11343 3 16 2 20487 0 [0.40] HWV036-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.40] NLP026-1 non_thm 0.0 2 0 4 5 0 3 0 6 2 0 4 11 0 [0.40] NLP031-1 non_thm 0.0 2 6 38 12 0 5 0 18 4 20 78 101 0 [0.40] NLP033-1 non_thm 0.1 2 7 40 12 0 4 0 13 5 21 90 108 0 [0.40] NLP063-1 non_thm 0.0 2 0 8 14 0 3 0 26 2 0 8 40 0 [0.40] NLP065-1 non_thm 0.0 2 0 8 14 0 3 0 25 2 0 8 39 0 [0.40] SYN736-1 non_thm 0.0 2 0 1 1 0 0 0 1 2 0 1 2 0 [0.40] SYN745-1 non_thm 0.0 2 0 1 3 0 0 0 5 3 0 1 8 0 [0.40] SYN746-1 non_thm 0.0 2 0 1 1 0 0 0 5 2 0 1 6 0 [0.40] SYN747-1 timeout 300.0 4 [0.40] SYN750-1 non_thm 72.5 3 16 1 116 0 0 0 81074 18 94 1 118198 0 [0.40] SYN751-1 non_thm 0.0 2 0 1 12 0 0 0 75 5 0 1 94 0 [0.40] SYN752-1 non_thm 0.0 2 0 1 1 0 0 0 2 2 0 1 3 0 [0.40] SYN753-1 non_thm 0.1 2 0 1 21 0 0 0 408 6 0 1 451 0 [0.40] SYN761-1 timeout 300.0 4 [0.40] SYN763-1 non_thm 0.0 2 0 1 9 0 0 0 55 3 0 1 65 0 [0.40] SYN766-1 non_thm 20.2 2 13 1 92 0 0 0 35217 13 72 1 51611 0 [0.40] SYN768-1 non_thm 0.0 2 0 2 1 0 0 0 5 2 0 2 6 0 [0.40] SYN775-1 timeout 300.0 5 [0.40] SYN790-1 timeout 300.0 8 [0.40] SYN797-1 non_thm 0.0 2 0 2 1 0 0 0 20 2 0 2 21 0 [0.40] TOP003-2 non_thm 0.0 2 0 12 24 0 0 0 54 4 0 20 78 0 [0.40] TOP010-1 timeout 300.0 12 [0.40] TOP011-1 timeout 300.0 18 [0.40] TOP014-1 timeout 300.0 148 [0.40] TOP016-1 timeout 300.0 31 [0.50] FLD011-3 timeout 300.0 52 [0.50] FLD020-1 timeout 300.0 16 [0.50] FLD047-4 theorem 0.5 4 1 441 0 0 0 0 0 2 441 5200 22960 0 [0.50] FLD049-3 timeout 300.0 53 [0.50] GRP123-1.005 non_thm 0.1 2 0 143 4 0 0 0 256 2 0 1556 505 0 [0.50] GRP123-2.005 non_thm 0.1 2 1 189 2 0 0 0 259 2 152 1815 595 0 [0.50] GRP123-6.005 non_thm 0.1 2 0 264 4 0 0 0 453 2 0 1624 947 0 [0.50] GRP123-7.005 non_thm 0.1 2 0 284 4 0 0 0 453 2 0 1644 947 0 [0.50] GRP124-1.005 non_thm 0.1 2 0 142 5 0 0 0 255 2 0 1556 505 0 [0.50] GRP124-2.005 non_thm 0.1 2 0 173 2 0 0 0 258 2 0 1590 505 0 [0.50] GRP124-3.005 non_thm 0.1 2 2 244 4 0 0 0 331 2 176 1899 670 0 [0.50] GRP124-4.005 non_thm 0.1 2 0 143 4 0 0 0 566 2 0 1606 1305 0 [0.50] GRP124-6.005 non_thm 0.1 2 0 263 5 0 0 0 452 2 0 1624 947 0 [0.50] GRP124-7.005 non_thm 0.1 2 0 283 5 0 0 0 452 2 0 1644 947 0 [0.50] GRP124-8.005 non_thm 0.1 2 0 322 6 0 0 0 513 2 0 1739 1009 0 [0.50] GRP124-9.005 non_thm 0.1 2 0 263 50 0 0 0 457 2 0 1624 997 0 [0.50] GRP126-1.005 non_thm 0.0 2 0 143 4 0 0 0 235 2 0 935 484 0 [0.50] GRP126-2.005 non_thm 0.1 2 0 173 2 0 0 0 237 2 0 969 484 0 [0.50] GRP126-3.005 non_thm 0.1 2 2 244 4 0 0 0 310 2 174 1271 649 0 [0.50] GRP126-4.005 non_thm 0.1 2 0 144 3 0 0 0 588 2 0 1427 1326 0 [0.50] GRP127-1.005 non_thm 0.0 2 0 145 2 0 0 0 237 2 0 935 484 0 [0.50] GRP127-4.005 non_thm 0.1 2 0 145 2 0 0 0 589 2 0 1427 1326 0 [0.50] GRP129-1.005 non_thm 0.1 2 24 686 28 0 0 0 429 2 85 3378 2149 0 [0.50] GRP129-2.005 non_thm 0.1 2 10 316 15 0 0 0 300 2 122 1745 820 0 [0.50] GRP129-3.005 non_thm 0.1 2 7 390 9 0 0 0 519 2 171 1914 992 0 [0.50] GRP129-4.005 non_thm 0.1 2 13 234 16 0 0 0 658 2 49 2184 1880 0 [0.50] GRP130-1.005 non_thm 0.1 2 15 393 18 0 0 0 321 2 125 2174 1188 0 [0.50] GRP131-1.005 non_thm 0.1 2 0 147 8 0 0 0 272 2 0 1575 525 0 [0.50] GRP131-2.005 non_thm 0.6 2 80 1612 88 0 0 0 1489 2 172 16728 7868 0 [0.50] GRP132-2.005 non_thm 1.0 2 92 2522 99 0 0 0 1228 2 174 29511 12989 0 [0.50] GRP133-1.004 non_thm 0.0 2 1 87 3 0 0 0 122 2 52 530 211 0 [0.50] GRP133-2.004 non_thm 0.0 2 2 121 5 0 0 0 121 2 79 613 250 0 [0.50] GRP134-1.005 non_thm 0.1 2 6 219 10 0 0 0 256 2 138 1724 855 0 [0.50] GRP134-2.005 non_thm 0.1 2 6 456 11 0 0 0 368 2 171 3295 1717 0 [0.50] GRP135-1.005 non_thm 0.4 2 60 1853 64 0 0 0 1360 2 133 12748 6877 0 [0.50] GRP135-2.005 non_thm 0.2 2 20 828 21 0 0 0 545 2 168 5153 2994 0 [0.50] MSC007-1.008 theorem 2.3 2 5040 55182 5039 0 78952 0 10044 2 56 145014 46529 0 [0.50] PUZ018-2 non_thm 0.1 2 2 89 22 0 6 0 1971 2 109 163 3101 0 [0.50] SET015-2 theorem 0.2 2 3 381 2 0 0 0 510 2 222 4397 1954 0 [0.50] SYN067-1 theorem 18.0 3 375 3049 399 0 853 0 54989 2 41 14838 436681 0 [0.50] SYN307-1 non_thm 0.0 2 0 2 1 0 0 0 5 2 0 4 6 0 [0.50] SYN353-1 timeout 300.0 8 [0.50] SYN436-1 theorem 10.7 4 155 2423 170 0 966 0 161626 2 82 8957 802484 0 [0.50] SYN441-1 non_thm 8.0 4 64 1253 92 0 420 0 104704 2 110 11713 324934 0 [0.50] SYN442-1 theorem 23.4 6 173 2966 208 0 1172 0 373210 2 100 13987 1254236 0 [0.50] SYN443-1 theorem 2.0 4 65 1031 65 0 487 0 20870 2 78 3694 188755 0 [0.50] SYN447-1 theorem 80.9 19 354 7741 423 0 3032 0 727236 2 130 38654 6003427 0 [0.50] SYN450-1 theorem 0.6 2 54 688 56 0 328 0 9387 2 72 2562 37796 0 [0.50] SYN452-1 theorem 1.6 3 78 906 90 0 412 0 27957 2 81 3692 97559 0 [0.50] SYN453-1 non_thm 6.6 10 58 1502 83 0 482 0 83707 2 139 8555 256089 0 [0.50] SYN455-1 theorem 16.5 3 126 1969 194 0 888 0 345967 2 96 10092 861323 0 [0.50] SYN460-1 theorem 4.0 4 115 2424 132 0 917 0 11081 2 84 10679 345343 0 [0.50] SYN464-1 non_thm 23.4 8 69 1329 124 0 501 0 388217 2 133 12786 1271899 0 [0.50] SYN465-1 theorem 1.7 3 67 1108 71 0 462 0 20328 2 70 5118 117012 0 [0.50] SYN466-1 theorem 1.9 3 80 1220 87 0 536 0 27673 2 85 6459 108987 0 [0.50] SYN467-1 theorem 0.6 2 40 657 41 0 295 0 6404 2 60 2671 52512 0 [0.50] SYN468-1 theorem 2.0 3 98 1531 109 0 726 0 20560 2 101 7459 130359 0 [0.50] SYN470-1 theorem 4.2 3 138 2632 145 0 1051 0 29661 2 95 10886 295637 0 [0.50] SYN472-1 theorem 5.4 3 136 1770 148 0 829 0 81727 2 66 10494 445792 0 [0.50] SYN473-1 theorem 2.9 3 89 1394 92 0 634 0 24267 2 76 7013 273036 0 [0.50] SYN474-1 theorem 4.2 3 139 2238 143 0 1050 0 40294 2 72 9846 351680 0 [0.50] SYN476-1 theorem 1.9 3 123 1982 131 0 919 0 15096 2 84 8479 119456 0 [0.50] SYN477-1 theorem 1.2 3 57 624 63 0 333 0 21181 2 55 3096 102515 0 [0.50] SYN479-1 theorem 1.3 3 40 588 43 0 324 0 12261 2 79 2559 129796 0 [0.50] SYN481-1 theorem 4.0 3 119 1665 127 0 805 0 54851 2 71 7375 338472 0 [0.50] SYN486-1 theorem 1.3 3 76 1035 75 0 525 0 13859 2 58 4801 129110 0 [0.50] SYN487-1 theorem 5.6 3 136 2429 157 0 1108 0 82907 2 101 12261 277892 0 [0.50] SYN488-1 theorem 6.3 4 167 2914 185 0 1290 0 62880 2 82 14068 409278 0 [0.50] SYN489-1 theorem 0.8 3 42 942 44 0 406 0 4881 2 76 3641 63313 0 [0.50] SYN498-1 theorem 3.1 5 85 1353 92 0 658 0 31780 2 76 5680 269050 0 [0.50] SYN499-1 theorem 7.4 4 83 1209 90 0 582 0 114341 2 85 10380 464791 0 [0.50] SYN500-1 theorem 1.9 3 73 985 74 0 468 0 18678 2 62 4773 198671 0 [0.50] SYN502-1 theorem 5.7 4 111 2466 117 0 979 0 43270 2 79 13092 485030 0 [0.50] SYN503-1 theorem 1.0 3 56 664 60 0 358 0 14197 2 66 3740 68211 0 [0.50] SYN507-1 theorem 3.5 3 80 1371 80 0 603 0 50205 2 89 5835 230014 0 [0.50] SYN508-1 theorem 7.5 3 120 1447 128 0 768 0 161876 2 84 11366 395809 0 [0.50] SYN509-1 theorem 0.6 2 53 665 54 0 374 0 6098 2 54 2657 49502 0 [0.50] SYN511-1 theorem 1.2 2 60 803 63 0 409 0 14311 2 80 5045 50959 0 [0.50] SYN514-1 non_thm 0.1 2 1 73 36 0 79 0 474 2 5 100 543 0 [0.50] SYN519-1 timeout 300.0 148 [0.50] SYN545-1 non_thm 0.1 2 3 63 70 0 105 0 577 2 112 132 813 0 [0.50] SYN814-1 non_thm 5.2 9 0 376 899 0 489 253 2278 2 0 712 3387 0 [0.50] SYN816-1 non_thm 4.8 11 0 590 170 0 939 32 772 2 0 1127 942 0 [0.50] SYN825-1 non_thm 11.2 18 0 945 117 0 1649 0 1033 2 0 1805 1150 0 [0.50] SYN826-1 non_thm 10.9 17 0 858 25 0 1763 0 867 2 0 1632 892 0 [0.50] SYN830-1 non_thm 16.8 24 0 1214 64 0 1763 0 1232 2 0 2330 1296 0 [0.50] SYN832-1 non_thm 15.1 22 0 1033 218 0 1704 0 1225 2 0 1973 1443 0 [0.50] SYN839-1 non_thm 21.2 29 0 1336 410 0 1763 0 1711 2 0 2570 2121 0 [0.50] SYN840-1 non_thm 29.8 30 6 1150 762 0 1763 5 2556 2 1746 2210 3516 0 [0.50] SYN841-1 non_thm 26.3 30 1 1330 718 0 1763 1 2181 2 1891 2559 2908 0 [0.50] SYN852-1 non_thm 29.4 33 0 1396 863 0 1763 0 2269 2 0 2690 3136 0 [0.50] SYN853-1 non_thm 56.9 35 40 1424 2854 0 1763 14 4812 2 2106 2784 8143 0 [0.50] SYN854-1 timeout 300.0 41 [0.50] SYN855-1 non_thm 28.0 33 0 1424 887 0 1763 0 2412 2 0 2744 3299 0 [0.60] NLP032-1 timeout 300.0 8 [0.60] NLP035-1 timeout 300.0 9 [0.60] NLP060-1 non_thm 0.0 2 0 9 10 0 3 0 21 2 0 11 31 0 [0.60] NLP061-1 non_thm 0.0 2 0 10 4 0 3 0 26 2 0 10 30 0 [0.60] NLP062-1 non_thm 0.0 2 0 10 4 0 3 0 24 2 0 10 28 0 [0.60] NLP160-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP161-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP162-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP163-1 non_thm 0.0 2 1 54 4 0 5 0 25 2 31 57 81 0 [0.60] NLP164-1 non_thm 0.0 2 1 54 4 0 5 0 25 2 31 57 81 0 [0.60] NLP165-1 non_thm 0.0 2 1 54 4 0 5 0 25 2 31 57 81 0 [0.60] NLP166-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP167-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP168-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP169-1 non_thm 0.0 2 0 26 4 0 4 0 88 2 0 26 92 0 [0.60] NLP190-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP191-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP192-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP193-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP194-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP195-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP196-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP197-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP198-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NLP199-1 non_thm 0.0 2 0 33 4 0 4 0 74 2 0 33 78 0 [0.60] NUM288-1 timeout 300.0 21 [0.60] SET781-1 timeout 300.0 20 [0.60] SYN769-1 non_thm 0.0 2 0 2 1 0 0 0 16 3 0 2 17 0 [0.60] SYN780-1 non_thm 0.0 2 0 2 1 0 0 0 8 2 0 2 9 0 [0.60] SYN786-1 non_thm 0.0 2 0 2 4 0 0 0 322 3 0 2 326 0 [0.60] SYN787-1 timeout 300.0 5 [0.60] SYN794-1 non_thm 0.0 2 0 2 0 0 0 0 0 2 0 2 0 0 [0.60] SYN799-1 timeout 300.0 5 [0.60] SYN800-1 timeout 300.0 5 [0.60] SYN801-1 timeout 300.0 5 [0.60] SYN903-1 timeout 300.0 15 [0.60] SYN904-1 timeout 300.0 17 [0.60] SYN905-1 timeout 300.0 12 [0.60] SYN907-1 timeout 300.0 25 [0.60] SYN908-1 timeout 300.0 28 [0.60] SYN909-1 timeout 300.0 36 [0.60] TOP015-1 timeout 300.0 32 [0.60] TOP018-1 timeout 300.0 31 [0.60] TOP019-1 timeout 300.0 47 [0.62] FLD012-4 theorem 0.2 3 1 270 0 0 0 0 0 2 270 3112 8519 0 [0.62] FLD033-1 timeout 300.0 17 [0.62] FLD038-1 timeout 300.0 16 [0.62] FLD043-5 theorem 9.6 12 1 684 0 0 0 0 0 2 684 101318 13914 0 [0.62] FLD054-4 theorem 0.4 4 1 419 0 0 0 0 0 2 419 5923 14352 0 [0.62] SYN067-2 theorem 45.6 2 997 8803 1028 0 1841 0 151413 2 52 47548 1104117 0 [0.62] SYN067-3 theorem 3.9 2 278 3043 317 0 483 0 33561 2 42 9955 189242 0 [0.62] SYN758-1 theorem 22.5 2 301 1 945 0 0 0 180432 9 27 1 291113 0 [0.62] SYN762-1 theorem 20.4 2 232 1 853 0 0 0 191992 8 30 1 296175 0 [0.67] GRP128-2.006 theorem 0.1 2 8 428 7 0 0 0 173 2 251 1751 1545 0 [0.67] SYN439-1 theorem 4.8 3 268 5487 299 0 2033 0 27984 2 92 18334 318663 0 [0.67] SYN440-1 theorem 279.2 7 1470 19600 1966 0 7221 0 3157487 2 126 44058013149643 0 [0.67] SYN457-1 theorem 229.1 8 999 21446 1481 0 6817 0 3142909 2 156 237811 7667913 0 [0.75] ANA004-5 timeout 300.0 26 [0.75] FLD015-1 timeout 300.0 16 [0.75] FLD024-1 timeout 300.0 16 [0.75] FLD027-1 timeout 300.0 17 [0.75] FLD028-1 timeout 300.0 14 [0.75] FLD063-1 timeout 300.0 16 [0.75] FLD068-1 timeout 300.0 16 [0.75] FLD068-2 timeout 300.0 17 [0.75] GRP132-1.005 non_thm 0.1 2 0 147 8 0 0 0 272 2 0 1575 525 0 [0.75] PUZ034-1.004 timeout 300.0 58 [0.75] SYN802-1 timeout 300.0 5 [0.75] SYN812-1 non_thm 13.9 19 0 936 186 0 1708 3 1090 2 0 1801 1276 0 [0.75] SYN818-1 non_thm 22.0 27 0 1374 465 0 1763 107 1824 2 0 2669 2289 0 [0.75] SYN821-1 non_thm 5.7 12 0 696 172 0 899 19 856 2 0 1336 1028 0 [0.75] SYN822-1 non_thm 9.8 16 0 696 871 0 939 177 1813 2 0 1336 2692 0 [0.75] SYN829-1 non_thm 16.2 25 0 1177 145 0 1704 0 1273 2 0 2259 1418 0 [0.75] SYN831-1 non_thm 17.9 24 0 1268 334 0 1763 1 1589 2 0 2440 1926 0 [0.75] SYN842-1 non_thm 26.1 32 0 1400 591 0 1763 0 1971 2 0 2698 2562 0 [0.80] GRP025-3 timeout 300.0 63 [0.80] GRP026-3 timeout 300.0 77 [0.80] GRP027-2 timeout 300.0 25 [0.80] NLP027-1 non_thm 0.0 2 0 4 5 0 4 0 8 2 0 4 13 0 [0.80] NLP028-1 non_thm 0.0 2 0 5 5 0 4 0 9 2 0 5 14 0 [0.80] NLP029-1 non_thm 0.0 2 0 4 5 0 4 0 6 2 0 4 11 0 [0.80] NLP030-1 non_thm 0.0 2 0 5 5 0 4 0 8 2 0 5 13 0 [0.80] NLP034-1 timeout 300.0 9 [0.80] PUZ034-1.003 timeout 300.0 60 [0.80] SYN764-1 non_thm 0.0 2 0 1 6 0 0 0 18 4 0 1 24 0 [0.80] SYN765-1 timeout 300.0 4 [0.80] SYN767-1 non_thm 0.0 2 0 1 6 0 0 0 23 3 0 1 29 0 [0.80] SYN770-1 non_thm 0.0 2 0 2 1 0 0 0 13 2 0 2 14 0 [0.80] SYN771-1 non_thm 0.0 2 0 2 1 0 0 0 27 3 0 2 28 0 [0.80] SYN773-1 non_thm 0.0 2 0 2 1 0 0 0 9 2 0 2 10 0 [0.80] SYN776-1 non_thm 0.0 2 0 2 2 0 0 0 122 3 0 2 124 0 [0.80] SYN777-1 timeout 300.0 5 [0.80] SYN778-1 non_thm 0.1 2 0 2 6 0 0 0 344 4 0 2 351 0 [0.80] SYN779-1 timeout 300.0 5 [0.80] SYN781-1 non_thm 0.0 2 0 2 5 0 0 0 26 5 0 2 31 0 [0.80] SYN782-1 timeout 300.0 7 [0.80] SYN783-1 non_thm 0.0 2 0 2 3 0 0 0 63 4 0 2 66 0 [0.80] SYN788-1 timeout 300.0 5 [0.80] SYN789-1 timeout 300.0 6 [0.80] SYN791-1 non_thm 0.0 2 0 2 1 0 0 0 7 2 0 2 8 0 [0.80] SYN792-1 timeout 300.0 6 [0.80] SYN793-1 non_thm 0.0 2 0 2 2 0 0 0 27 3 0 2 29 0 [0.80] SYN795-1 non_thm 0.4 2 0 2 24 0 0 0 1066 7 0 2 1139 0 [0.80] SYN803-1 non_thm 0.0 2 0 2 1 0 0 0 10 2 0 2 11 0 [0.80] SYN804-1 non_thm 0.0 2 0 2 7 0 0 0 107 3 0 2 114 0 [0.80] SYN805-1 timeout 300.0 9 [0.80] SYN806-1 timeout 300.0 7 [0.80] SYN807-1 non_thm 0.0 2 0 2 5 0 0 0 227 3 0 2 232 0 [0.80] SYN808-1 timeout 300.0 7 [0.80] SYN809-1 timeout 300.0 6 [0.80] SYN810-1 timeout 300.0 7 [0.80] SYN906-1 timeout 300.0 26 [0.80] SYN910-1 timeout 300.0 41 [0.80] SYN911-1 timeout 300.0 45 [0.80] SYN912-1 timeout 300.0 50 [0.80] SYN913-1 timeout 300.0 43 [0.80] TOP001-1 timeout 300.0 16 [0.80] TOP002-1 timeout 300.0 12 [0.80] TOP003-1 timeout 300.0 9 [0.80] TOP005-1 timeout 300.0 15 [0.80] TOP006-1 timeout 300.0 8 [0.80] TOP007-1 timeout 300.0 20 [0.80] TOP008-1 memory 247.3 499 [0.80] TOP009-1 timeout 300.0 30 [0.80] TOP012-1 timeout 300.0 20 [0.80] TOP013-1 timeout 300.0 32 [0.80] TOP017-1 timeout 300.0 145 [0.88] FLD007-1 timeout 300.0 12 [0.88] FLD008-3 timeout 300.0 44 [0.88] FLD016-1 timeout 300.0 21 [0.88] FLD022-1 timeout 300.0 15 [0.88] FLD035-1 timeout 300.0 15 [0.88] FLD036-1 timeout 300.0 15 [0.88] FLD048-4 theorem 247.0 31 1 2432 0 0 0 0 0 2 2432 157881 113120 0 [0.88] FLD050-3 timeout 300.0 53 [0.88] FLD052-4 theorem 3.4 13 1 932 0 0 0 0 0 2 932 9605 182444 0 [0.88] FLD057-3 timeout 300.0 90 [0.88] FLD066-1 timeout 300.0 15 [0.88] FLD072-4 timeout 300.0 68 [0.88] FLD086-3 timeout 300.0 54 [0.88] FLD090-3 timeout 300.0 53 [0.88] FLD097-4 timeout 300.0 37 [1.00] ANA001-1 timeout 300.0 55 [1.00] ANA005-4 timeout 300.0 28 [1.00] ANA005-5 timeout 300.0 69 [1.00] FLD008-1 timeout 300.0 16 [1.00] FLD008-2 timeout 300.0 22 [1.00] FLD011-1 timeout 300.0 12 [1.00] FLD012-1 timeout 300.0 17 [1.00] FLD012-2 timeout 300.0 21 [1.00] FLD012-3 timeout 300.0 60 [1.00] FLD014-1 timeout 300.0 16 [1.00] FLD026-1 timeout 300.0 17 [1.00] FLD029-1 timeout 300.0 17 [1.00] FLD040-1 timeout 300.0 12 [1.00] FLD041-1 timeout 300.0 17 [1.00] FLD041-2 timeout 300.0 16 [1.00] FLD042-1 timeout 300.0 17 [1.00] FLD043-1 timeout 300.0 12 [1.00] FLD044-1 timeout 300.0 16 [1.00] FLD044-2 timeout 300.0 31 [1.00] FLD044-3 timeout 300.0 43 [1.00] FLD044-4 timeout 300.0 47 [1.00] FLD045-1 timeout 300.0 16 [1.00] FLD045-2 timeout 300.0 18 [1.00] FLD045-3 timeout 300.0 44 [1.00] FLD045-4 timeout 300.0 45 [1.00] FLD046-1 timeout 300.0 12 [1.00] FLD046-3 timeout 300.0 52 [1.00] FLD047-1 timeout 300.0 15 [1.00] FLD047-2 timeout 300.0 21 [1.00] FLD047-3 timeout 300.0 56 [1.00] FLD048-1 timeout 300.0 17 [1.00] FLD048-2 timeout 300.0 22 [1.00] FLD048-3 timeout 300.0 53 [1.00] FLD049-1 timeout 300.0 16 [1.00] FLD049-2 timeout 300.0 21 [1.00] FLD050-1 timeout 300.0 15 [1.00] FLD050-2 timeout 300.0 20 [1.00] FLD051-1 timeout 300.0 16 [1.00] FLD051-2 timeout 300.0 21 [1.00] FLD051-3 timeout 300.0 61 [1.00] FLD051-4 timeout 300.0 32 [1.00] FLD052-1 timeout 300.0 17 [1.00] FLD052-2 timeout 300.0 11 [1.00] FLD052-3 timeout 300.0 53 [1.00] FLD053-1 timeout 300.0 16 [1.00] FLD053-2 timeout 300.0 11 [1.00] FLD053-3 timeout 300.0 53 [1.00] FLD053-4 timeout 300.0 29 [1.00] FLD054-1 timeout 300.0 17 [1.00] FLD054-2 timeout 300.0 17 [1.00] FLD054-3 timeout 300.0 60 [1.00] FLD057-1 timeout 300.0 11 [1.00] FLD062-1 timeout 300.0 16 [1.00] FLD072-1 timeout 300.0 16 [1.00] FLD072-2 timeout 300.0 16 [1.00] FLD072-3 timeout 300.0 49 [1.00] FLD073-1 timeout 300.0 16 [1.00] FLD073-2 timeout 300.0 15 [1.00] FLD073-3 timeout 300.0 44 [1.00] FLD073-4 timeout 300.0 79 [1.00] FLD074-1 timeout 300.0 16 [1.00] FLD074-2 timeout 300.0 32 [1.00] FLD074-3 timeout 300.0 46 [1.00] FLD074-4 timeout 300.0 39 [1.00] FLD075-1 timeout 300.0 17 [1.00] FLD075-2 timeout 300.0 24 [1.00] FLD075-3 timeout 300.0 46 [1.00] FLD075-4 timeout 300.0 39 [1.00] FLD076-1 timeout 300.0 16 [1.00] FLD076-2 timeout 300.0 23 [1.00] FLD076-3 timeout 300.0 56 [1.00] FLD076-4 timeout 300.0 45 [1.00] FLD077-1 timeout 300.0 15 [1.00] FLD077-2 timeout 300.0 20 [1.00] FLD077-3 timeout 300.0 56 [1.00] FLD077-4 timeout 300.0 44 [1.00] FLD078-1 timeout 300.0 17 [1.00] FLD078-2 timeout 300.0 15 [1.00] FLD078-3 timeout 300.0 54 [1.00] FLD078-4 timeout 300.0 51 [1.00] FLD079-1 timeout 300.0 17 [1.00] FLD079-2 timeout 300.0 16 [1.00] FLD079-3 timeout 300.0 68 [1.00] FLD079-4 timeout 300.0 71 [1.00] FLD080-1 timeout 300.0 12 [1.00] FLD080-2 timeout 300.0 16 [1.00] FLD080-3 timeout 300.0 56 [1.00] FLD080-4 timeout 300.0 61 [1.00] FLD081-1 timeout 300.0 29 [1.00] FLD081-2 timeout 300.0 33 [1.00] FLD081-3 timeout 300.0 46 [1.00] FLD081-4 timeout 300.0 48 [1.00] FLD082-1 timeout 300.0 17 [1.00] FLD082-3 timeout 300.0 69 [1.00] FLD083-1 timeout 300.0 17 [1.00] FLD083-3 timeout 300.0 68 [1.00] FLD084-1 timeout 300.0 17 [1.00] FLD084-3 timeout 300.0 63 [1.00] FLD085-1 timeout 300.0 17 [1.00] FLD085-3 timeout 300.0 63 [1.00] FLD086-1 timeout 300.0 12 [1.00] FLD087-1 timeout 300.0 12 [1.00] FLD087-3 timeout 300.0 54 [1.00] FLD088-1 timeout 300.0 12 [1.00] FLD088-3 timeout 300.0 54 [1.00] FLD089-1 timeout 300.0 12 [1.00] FLD089-3 timeout 300.0 54 [1.00] FLD090-1 timeout 300.0 12 [1.00] FLD091-1 timeout 300.0 12 [1.00] FLD091-3 timeout 300.0 52 [1.00] FLD092-1 timeout 300.0 12 [1.00] FLD092-3 timeout 300.0 51 [1.00] FLD093-1 timeout 300.0 12 [1.00] FLD093-3 timeout 300.0 52 [1.00] FLD094-1 timeout 300.0 12 [1.00] FLD094-3 timeout 300.0 51 [1.00] FLD095-1 timeout 300.0 14 [1.00] FLD095-2 timeout 300.0 22 [1.00] FLD095-3 timeout 300.0 57 [1.00] FLD095-4 timeout 300.0 38 [1.00] FLD096-1 timeout 300.0 19 [1.00] FLD096-2 timeout 300.0 24 [1.00] FLD096-3 timeout 300.0 58 [1.00] FLD096-4 timeout 300.0 36 [1.00] FLD097-1 timeout 300.0 16 [1.00] FLD097-2 timeout 300.0 24 [1.00] FLD097-3 timeout 300.0 44 [1.00] FLD098-1 timeout 300.0 16 [1.00] FLD098-2 timeout 300.0 25 [1.00] FLD098-3 timeout 300.0 44 [1.00] FLD098-4 timeout 300.0 38 [1.00] FLD099-1 timeout 300.0 12 [1.00] FLD099-2 timeout 300.0 19 [1.00] FLD099-3 timeout 300.0 51 [1.00] FLD099-4 timeout 300.0 86 [1.00] FLD100-1 timeout 300.0 16 [1.00] FLD100-2 timeout 300.0 23 [1.00] FLD100-3 timeout 300.0 45 [1.00] FLD100-4 timeout 300.0 36 [1.00] MSC008-1.010 timeout 300.0 130 [1.00] SYN314-1.002.001 timeout 300.0 5