-------------------------------------------------------------------------------- Execute format string : ./darwin --iterative-deepening TermWeight Problems list file : nne_weight-problems Output file : nne_weight-output Summary file : nne_weight-summary Time limit : 300 s Memory limit : 400 MB -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. [0.00] ALG002-1 theorem 0.1 4 1 79 0 4 0 0 0 7 79 253 2 [0.00] CAT007-3 theorem 0.0 4 1 5 0 5 0 0 0 2 5 9 2 [0.00] COM002-2 theorem 0.0 4 1 26 0 15 0 0 0 3 26 43 0 [0.00] COM003-2 theorem 0.0 4 1 14 0 10 11 0 0 3 14 29 1 [0.00] FLD006-1 theorem 114.6 4 1 95 0 4 0 0 0 7 95 801 0 [0.00] FLD006-3 theorem 0.0 4 1 5 0 4 0 0 0 5 5 23 0 [0.00] FLD010-1 theorem 132.5 4 1 282 0 4 0 0 0 7 282 1347 0 [0.00] FLD010-3 theorem 0.0 4 1 6 0 5 0 0 0 5 6 27 0 [0.00] FLD018-3 theorem 0.1 4 1 51 0 6 0 0 0 5 51 1499 0 [0.00] FLD019-3 theorem 0.0 4 1 10 0 6 0 0 0 5 10 68 0 [0.00] FLD020-3 theorem 0.1 4 1 45 0 7 0 0 0 5 45 408 0 [0.00] FLD021-3 theorem 0.0 4 1 10 0 7 0 0 0 4 10 60 0 [0.00] FLD033-3 theorem 0.2 4 1 87 0 8 0 0 0 5 87 951 0 [0.00] FLD034-3 theorem 0.0 4 1 14 0 7 0 0 0 4 14 76 0 [0.00] FLD039-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 [0.00] FLD039-3 theorem 0.0 4 1 11 0 6 0 0 0 4 11 50 0 [0.00] FLD055-1 theorem 0.0 4 1 21 0 9 0 0 0 3 21 72 0 [0.00] FLD056-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 7 0 [0.00] FLD056-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 7 0 [0.00] FLD058-1 theorem 0.0 4 1 20 0 9 0 0 0 3 20 72 0 [0.00] FLD071-3 theorem 4.9 4 1 9 0 8 0 0 0 6 9 98 0 [0.00] FLD071-4 theorem 0.0 4 1 9 0 9 0 0 0 2 9 10 0 [0.00] GRA001-1 theorem 0.0 4 4 10 3 44 28 0 2 2 5 22 10 [0.00] GRP123-1.003 theorem 0.0 4 1 31 0 10 0 0 0 4 31 87 0 [0.00] GRP123-2.003 theorem 0.0 4 1 37 0 15 0 0 0 4 37 94 0 [0.00] GRP123-3.003 theorem 0.0 4 1 48 0 20 0 1 0 4 48 111 0 [0.00] GRP123-4.003 theorem 0.0 4 1 31 0 10 0 0 0 4 31 105 0 [0.00] GRP123-6.003 theorem 0.0 4 1 50 0 11 0 0 0 4 50 143 0 [0.00] GRP123-7.003 theorem 0.0 4 1 56 0 16 0 0 0 4 56 149 0 [0.00] GRP123-8.003 theorem 0.0 4 1 63 0 21 0 1 0 4 63 156 0 [0.00] GRP123-9.003 theorem 0.0 4 1 50 0 11 0 0 0 4 50 143 0 [0.00] GRP124-1.004 theorem 0.0 4 2 72 1 17 0 0 37 4 64 392 155 [0.00] GRP124-2.004 theorem 0.0 4 1 75 0 26 0 0 0 4 75 182 0 [0.00] GRP124-3.004 theorem 0.0 4 2 117 1 32 0 1 48 4 107 336 167 [0.00] GRP124-4.004 theorem 0.0 4 2 66 1 17 0 0 101 4 62 293 350 [0.00] GRP124-6.004 theorem 0.0 4 2 109 1 18 0 0 71 4 101 424 234 [0.00] GRP124-7.004 theorem 0.0 4 2 121 1 27 0 0 71 4 113 436 234 [0.00] GRP124-8.004 theorem 0.0 4 2 149 2 33 0 1 90 4 142 490 259 [0.00] GRP124-9.004 theorem 0.0 4 2 109 1 18 0 0 71 4 101 424 266 [0.00] GRP125-1.003 theorem 0.0 4 1 31 0 10 0 0 0 4 31 94 0 [0.00] GRP125-2.005 theorem 0.0 4 3 176 2 40 0 0 137 4 157 800 479 [0.00] GRP125-3.005 theorem 0.1 4 5 281 4 47 0 1 232 4 220 1294 748 [0.00] GRP125-4.003 theorem 0.0 4 1 31 0 10 0 0 0 4 31 146 0 [0.00] GRP126-1.004 theorem 0.0 4 2 69 1 17 0 0 36 4 63 316 141 [0.00] GRP126-2.004 theorem 0.0 4 1 75 0 26 0 0 0 4 75 224 0 [0.00] GRP126-3.004 theorem 0.0 4 2 117 1 32 0 1 47 4 107 370 167 [0.00] GRP126-4.004 theorem 0.0 4 2 67 1 17 0 0 102 4 63 403 367 [0.00] GRP127-1.004 theorem 0.0 4 2 72 1 17 0 0 36 4 64 352 151 [0.00] GRP127-2.006 theorem 0.1 4 3 313 2 57 0 0 251 4 253 1328 1321 [0.00] GRP127-3.004 theorem 0.0 4 2 117 1 32 0 1 47 4 107 346 166 [0.00] GRP127-4.004 theorem 0.0 4 2 68 1 17 0 0 102 4 63 429 368 [0.00] GRP128-1.003 theorem 0.0 4 4 59 3 9 0 0 7 4 32 200 90 [0.00] GRP128-4.003 theorem 0.0 4 4 28 3 9 0 0 15 4 28 193 108 [0.00] GRP129-1.003 theorem 0.0 4 4 58 3 9 0 0 7 4 29 238 92 [0.00] GRP129-2.004 theorem 0.0 4 7 164 7 25 0 0 69 4 78 599 258 [0.00] GRP129-3.004 theorem 0.1 4 7 236 7 31 0 0 165 4 115 783 344 [0.00] GRP129-4.004 theorem 0.0 4 9 116 8 16 0 0 94 4 51 665 526 [0.00] GRP130-1.003 theorem 0.0 4 4 70 3 9 0 0 7 4 36 316 123 [0.00] GRP130-2.003 theorem 0.0 4 3 67 2 14 0 0 6 4 43 282 104 [0.00] GRP130-3.003 theorem 0.0 4 2 89 1 19 0 0 2 4 63 289 108 [0.00] GRP130-4.003 theorem 0.0 4 4 41 3 9 0 0 15 4 25 177 143 [0.00] GRP131-1.002 theorem 0.0 4 2 20 1 4 0 0 0 4 14 81 32 [0.00] GRP131-2.002 theorem 0.0 4 2 22 1 6 0 0 0 4 16 84 32 [0.00] GRP132-1.002 theorem 0.0 4 2 20 1 4 0 0 0 4 14 81 32 [0.00] GRP132-2.002 theorem 0.0 4 2 22 1 6 0 0 0 4 16 84 32 [0.00] GRP133-1.003 theorem 0.0 4 4 79 3 9 0 0 7 4 33 340 139 [0.00] GRP133-2.003 theorem 0.0 4 3 68 2 14 0 0 6 4 43 251 97 [0.00] GRP134-1.003 theorem 0.0 4 4 92 3 9 0 0 7 4 34 434 169 [0.00] GRP134-2.003 theorem 0.0 4 3 84 2 14 0 0 6 4 43 352 127 [0.00] GRP135-1.002 theorem 0.0 4 2 19 1 4 0 0 0 4 14 61 25 [0.00] GRP135-2.002 theorem 0.0 4 2 21 1 6 0 0 0 4 16 63 25 [0.00] HWV003-3 theorem 0.0 4 8 105 7 353 218 0 62 2 22 131 92 [0.00] HWV005-1 theorem 0.0 4 1 119 0 10 0 0 0 9 119 301 0 [0.00] HWV005-2 theorem 0.0 4 1 119 0 8 0 0 0 7 119 274 0 [0.00] HWV006-1 theorem 0.2 4 1 657 0 15 1 84 0 11 657 1343 0 [0.00] HWV006-2 theorem 0.2 4 1 622 0 13 1 0 0 9 622 1256 0 [0.00] HWV007-1 theorem 0.2 4 1 432 0 13 1 46 0 11 432 968 0 [0.00] HWV007-2 theorem 0.2 4 1 422 0 11 1 0 0 9 422 929 0 [0.00] KRS001-1 theorem 0.0 4 1 8 0 1 0 0 0 5 8 14 2 [0.00] KRS002-1 theorem 0.0 4 1 9 0 1 0 0 0 7 9 14 2 [0.00] KRS003-1 theorem 0.0 4 1 9 0 2 0 0 0 5 9 14 2 [0.00] KRS010-1 theorem 0.0 4 2 23 1 2 0 0 77 5 19 38 95 [0.00] KRS012-1 theorem 0.0 4 1 5 0 2 0 0 0 4 5 10 3 [0.00] KRS013-1 theorem 0.0 4 1 18 0 2 0 0 0 7 18 27 7 [0.00] KRS015-1 theorem 0.0 4 1 10 0 1 0 0 0 7 10 16 2 [0.00] KRS017-1 theorem 0.0 4 1 3 0 2 0 0 0 4 3 7 0 [0.00] LCL181-2 theorem 0.0 4 1 2 0 3 2 0 0 2 2 4 1 [0.00] LCL230-2 theorem 0.0 4 1 3 0 3 3 0 0 2 3 6 0 [0.00] MGT004-1 theorem 0.0 4 1 15 0 9 0 0 0 7 15 26 0 [0.00] MGT007-1 theorem 0.0 4 1 17 0 9 0 0 0 7 17 28 0 [0.00] MGT016-1 theorem 0.0 4 1 16 0 13 0 0 0 7 16 26 0 [0.00] MGT018-1 theorem 0.0 4 1 16 0 13 0 0 0 7 16 26 0 [0.00] MGT022-1 theorem 0.0 4 2 8 1 11 3 0 0 8 7 19 6 [0.00] MGT022-2 theorem 0.0 4 2 8 1 11 3 0 0 8 7 19 6 [0.00] MGT028-1 theorem 0.0 4 2 12 1 2 0 0 1 8 10 27 15 [0.00] MGT030-1 theorem 0.0 4 3 17 3 2 0 0 5 13 13 37 29 [0.00] MGT036-1 theorem 0.0 4 1 9 0 4 0 0 0 5 9 15 0 [0.00] MGT036-2 theorem 0.0 4 1 9 0 4 0 0 0 5 9 16 0 [0.00] MGT041-2 theorem 0.0 4 1 7 0 4 0 0 0 4 7 11 0 [0.00] MSC001-1 theorem 2.1 4 1 86 0 5 1 7 0 11 86 230 0 [0.00] MSC002-1 theorem 0.0 4 1 22 0 3 1 0 0 7 22 42 0 [0.00] MSC002-2 theorem 0.0 4 1 22 0 3 1 0 0 7 22 42 0 [0.00] MSC003-1 theorem 0.0 4 1 6 0 2 0 0 0 9 6 9 0 [0.00] MSC004-1 theorem 0.1 4 6 20 11 2 0 0 5 11 15 38 52 [0.00] MSC006-1 theorem 0.0 4 6 47 22 2 0 0 227 3 30 193 537 [0.00] MSC008-1.002 theorem 2.0 4 116 407 270 2 0 0 24992 4 32 4319 65944 [0.00] MSC008-2.002 theorem 0.7 4 32 155 116 2 0 0 7379 4 30 1239 14875 [0.00] NLP114-1 non_thm 0.0 4 0 18 1 35 2 0 31 4 19 18 32 [0.00] NLP115-1 non_thm 0.0 4 0 18 1 35 2 0 31 4 19 18 32 [0.00] NLP116-1 non_thm 0.0 4 0 18 1 35 2 0 31 4 19 18 32 [0.00] NLP117-1 theorem 0.0 4 2 34 1 66 5 0 0 4 19 38 48 [0.00] NLP118-1 non_thm 0.0 4 1 34 1 67 4 0 32 4 19 36 48 [0.00] NLP119-1 non_thm 0.0 4 1 34 1 67 4 0 32 4 19 36 48 [0.00] NLP120-1 non_thm 0.0 4 0 18 1 35 2 0 31 4 19 18 32 [0.00] NLP121-1 non_thm 0.0 4 0 18 1 35 2 0 31 4 19 18 32 [0.00] NLP122-1 theorem 0.0 4 2 34 1 66 5 0 0 4 19 38 48 [0.00] NLP123-1 non_thm 0.0 4 0 18 1 35 2 0 31 4 19 18 32 [0.00] NUM014-1 theorem 0.0 4 1 5 0 4 0 0 0 4 5 10 0 [0.00] NUM015-1 theorem 0.0 4 1 10 0 2 0 0 0 6 10 20 3 [0.00] NUM016-1 theorem 0.0 4 1 14 0 4 0 0 0 6 14 33 3 [0.00] NUM016-2 theorem 0.0 4 1 11 0 2 0 0 0 6 11 15 3 [0.00] NUM021-1 theorem 0.0 4 1 88 0 9 0 0 0 5 88 320 0 [0.00] NUM022-1 theorem 0.0 4 1 9 0 3 0 0 0 5 9 14 0 [0.00] NUM025-2 theorem 0.0 4 1 4 0 4 0 0 0 2 4 12 1 [0.00] NUM027-1 timeout 299.0 17 [0.00] NUM285-1 non_thm 0.0 4 0 16 5 67 44 0 10 2 21 16 15 [0.00] PLA002-1 theorem 0.0 4 2 7 1 19 12 0 0 2 7 11 2 [0.00] PLA002-2 theorem 20.1 43 1 1369 0 2 0 0 0 7 1369 5746 0 [0.00] PUZ001-1 theorem 0.0 4 1 17 0 5 2 0 0 3 17 20 1 [0.00] PUZ001-3 non_thm 0.0 4 0 19 0 6 2 0 9 3 19 22 9 [0.00] PUZ002-1 theorem 0.0 4 1 11 0 2 0 0 0 2 11 13 1 [0.00] PUZ004-1 theorem 0.0 4 1 10 0 11 11 0 0 2 10 12 1 [0.00] PUZ005-1 theorem 0.1 4 2 29 1 3 0 0 0 5 24 93 169 [0.00] PUZ009-1 theorem 0.0 4 1 5 0 15 11 0 0 2 5 11 4 [0.00] PUZ012-1 theorem 0.0 4 1 20 0 13 1 0 0 3 20 36 2 [0.00] PUZ013-1 theorem 0.0 4 1 7 0 14 10 0 0 2 7 12 6 [0.00] PUZ014-1 theorem 0.0 4 2 16 1 26 22 0 5 2 13 22 12 [0.00] PUZ015-2.006 theorem 0.2 4 139 2414 148 10158 5318 0 1063 2 59 3244 1829 [0.00] PUZ016-2.004 non_thm 0.0 4 0 22 2 75 39 0 24 2 24 24 28 [0.00] PUZ016-2.005 theorem 0.0 4 31 418 30 1745 919 0 84 2 40 553 319 [0.00] PUZ019-1 theorem 0.0 4 1 116 0 44 1 3 0 3 116 333 3 [0.00] PUZ021-1 theorem 2.8 4 17 28 332 0 0 0 11533 7 223 57 13367 [0.00] PUZ023-1 theorem 0.0 4 2 10 2 10 6 0 4 3 11 25 14 [0.00] PUZ024-1 theorem 0.0 4 1 7 0 13 7 0 0 2 7 16 1 [0.00] PUZ025-1 theorem 0.0 4 8 42 9 7 4 0 46 4 20 200 184 [0.00] PUZ026-1 theorem 0.0 4 3 35 2 6 0 0 10 3 21 107 62 [0.00] PUZ027-1 theorem 0.0 4 3 20 2 29 15 0 1 3 12 59 40 [0.00] PUZ028-1 non_thm 0.0 4 0 31 15 11 0 0 20 3 46 91 35 [0.00] PUZ028-2 non_thm 0.0 4 0 70 18 36 0 0 28 3 88 190 46 [0.00] PUZ028-3 non_thm 0.0 4 0 70 18 432 154 0 24 3 88 114 42 [0.00] PUZ028-4 non_thm 0.0 4 0 28 18 222 106 0 24 3 46 60 42 [0.00] PUZ028-5 theorem 0.1 4 30 742 29 11 0 0 173 3 90 1674 246 [0.00] PUZ029-1 theorem 0.0 4 1 13 0 4 0 0 0 2 13 17 2 [0.00] PUZ030-1 theorem 0.0 4 24 327 24 509 397 0 130 2 28 875 982 [0.00] PUZ030-2 theorem 0.0 4 9 35 8 429 173 0 7 2 10 94 89 [0.00] PUZ031-1 theorem 0.0 4 1 30 0 6 0 0 0 4 30 55 0 [0.00] PUZ032-1 theorem 0.0 4 2 15 1 4 0 0 8 5 15 51 17 [0.00] PUZ033-1 theorem 0.0 4 1 11 0 12 17 0 0 2 11 15 0 [0.00] PUZ035-1 theorem 0.0 4 4 17 3 21 17 0 2 3 9 42 16 [0.00] PUZ035-2 theorem 0.0 4 4 17 3 21 17 0 2 3 9 44 20 [0.00] PUZ035-5 theorem 0.0 4 4 9 4 5 0 0 0 4 6 23 26 [0.00] PUZ035-6 theorem 0.0 4 4 6 4 5 0 0 5 4 6 21 44 [0.00] SET001-1 theorem 0.0 4 1 4 0 3 0 0 0 3 4 8 1 [0.00] SET002-1 theorem 0.0 4 3 9 3 2 0 0 0 5 8 21 22 [0.00] SET003-1 theorem 0.0 4 1 6 0 2 0 0 0 5 6 9 2 [0.00] SET004-1 theorem 0.0 4 1 6 0 2 0 0 0 5 6 8 2 [0.00] SET006-1 theorem 0.0 4 1 6 0 2 0 0 0 5 6 10 3 [0.00] SET008-1 theorem 0.0 4 1 10 0 3 0 0 0 6 10 34 4 [0.00] SET009-1 theorem 0.0 4 1 22 0 4 0 0 0 5 22 41 2 [0.00] SET011-1 theorem 0.0 4 2 22 1 3 0 0 0 6 16 63 32 [0.00] SET043-5 theorem 0.0 4 4 0 3 0 0 0 0 3 2 8 9 [0.00] SET044-5 theorem 0.0 4 8 8 19 0 0 0 43 5 9 32 119 [0.00] SET045-5 theorem 0.0 4 6 2 6 1 0 0 7 5 6 16 37 [0.00] SET046-5 theorem 0.0 4 4 4 3 0 0 0 0 4 4 18 19 [0.00] SET047-5 theorem 0.0 4 4 6 3 4 4 0 2 5 4 24 15 [0.00] SET055-7 theorem 0.0 4 1 5 0 5 0 0 0 2 5 36 3 [0.00] SET786-1 theorem 0.0 4 4 4 3 0 0 0 0 4 4 16 18 [0.00] SWV001-1 theorem 0.0 4 2 8 1 2 0 0 5 4 7 34 21 [0.00] SWV009-1 theorem 0.0 4 1 9 0 5 0 0 0 3 9 11 1 [0.00] SYN001-1.005 theorem 0.0 4 16 16 15 608 118 0 0 2 5 96 31 [0.00] SYN006-1 theorem 0.0 4 1 6 0 4 1 0 0 4 6 6 0 [0.00] SYN008-1 theorem 0.0 4 1 3 0 3 4 0 0 2 3 6 0 [0.00] SYN009-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 9 0 [0.00] SYN009-2 theorem 0.0 4 1 7 0 4 0 0 0 4 7 9 0 [0.00] SYN009-3 theorem 0.0 4 1 9 0 5 1 0 0 4 9 11 0 [0.00] SYN009-4 theorem 0.0 4 1 8 0 4 0 0 0 4 8 10 0 [0.00] SYN011-1 theorem 0.0 4 2 9 1 12 13 0 0 2 7 13 9 [0.00] SYN012-1 theorem 0.1 4 10 0 39 0 0 0 117 23 14 0 184 [0.00] SYN014-2 theorem 0.0 4 1 8 0 7 0 0 0 3 8 36 2 [0.00] SYN028-1 theorem 0.0 4 1 5 0 5 7 0 0 2 5 7 1 [0.00] SYN029-1 theorem 0.0 4 2 3 1 7 7 0 0 2 3 7 3 [0.00] SYN030-1 theorem 0.0 4 2 5 1 13 11 0 0 2 5 10 6 [0.00] SYN031-1 theorem 0.0 4 3 5 2 0 0 0 0 4 4 19 20 [0.00] SYN032-1 theorem 0.0 4 3 7 2 14 14 0 0 2 5 13 9 [0.00] SYN034-1 theorem 0.0 4 4 4 3 0 0 0 0 4 4 16 18 [0.00] SYN038-1 theorem 0.1 4 10 0 39 0 0 0 117 23 14 0 184 [0.00] SYN039-1 theorem 0.1 4 8 6 21 36 0 3 257 6 13 24 352 [0.00] SYN044-1 theorem 0.0 4 2 4 1 10 9 0 0 2 3 8 4 [0.00] SYN045-1 theorem 0.0 4 1 3 0 3 3 0 0 2 3 5 2 [0.00] SYN047-1 theorem 0.0 4 1 4 0 4 6 0 0 2 4 7 0 [0.00] SYN051-1 theorem 0.0 4 2 2 1 6 6 0 0 2 2 6 3 [0.00] SYN052-1 theorem 0.0 4 2 2 1 8 7 0 0 2 2 6 3 [0.00] SYN053-1 theorem 0.0 4 2 1 1 4 4 0 0 2 2 8 6 [0.00] SYN054-1 theorem 0.0 4 2 5 1 2 1 0 0 2 4 9 6 [0.00] SYN055-1 theorem 0.0 4 1 9 0 3 0 0 0 2 9 12 0 [0.00] SYN056-1 non_thm 0.0 4 0 2 2 8 0 0 2 2 4 2 4 [0.00] SYN059-1 non_thm 0.0 4 0 5 7 30 11 0 88 2 12 24 95 [0.00] SYN060-1 theorem 0.0 4 1 3 0 1 0 0 0 2 3 5 4 [0.00] SYN061-1 theorem 0.0 4 1 5 0 2 0 0 0 2 5 7 1 [0.00] SYN063-1 theorem 0.0 4 1 2 0 2 5 0 0 2 2 6 0 [0.00] SYN066-1 theorem 0.0 4 1 4 0 5 3 1 0 2 4 4 1 [0.00] SYN069-1 theorem 0.0 4 1 9 0 1 0 0 0 4 9 16 0 [0.00] SYN070-1 theorem 0.0 4 1 15 0 4 0 0 0 4 15 37 0 [0.00] SYN081-1 theorem 0.0 4 2 0 4 0 0 0 4 3 3 0 10 [0.00] SYN082-1 theorem 0.0 4 3 3 2 9 5 0 0 6 3 18 11 [0.00] SYN084-2 theorem 0.0 4 4 17 4 17 19 0 6 4 9 29 41 [0.00] SYN091-1.003 non_thm 0.0 4 0 2 4 12 6 0 2 2 6 2 6 [0.00] SYN092-1.003 non_thm 0.0 4 0 0 9 33 7 0 6 2 9 0 15 [0.00] SYN093-1.002 theorem 0.0 4 2 10 1 20 15 0 0 2 8 16 8 [0.00] SYN094-1.005 theorem 10.0 37 16384 75927 26775 203333 143799 0 67723 2 45 141463 127670 [0.00] SYN097-1.002 theorem 0.0 4 2 14 1 26 20 0 0 2 12 20 10 [0.00] SYN098-1.002 theorem 0.0 4 32 264 127 638 472 0 235 2 31 392 449 [0.00] SYN099-1.003 theorem 0.0 4 1 16 0 14 2 0 0 2 16 35 0 [0.00] SYN100-1.005 theorem 0.0 4 1 42 0 8 0 0 0 2 42 83 1 [0.00] SYN315-1 theorem 0.0 4 2 2 1 6 4 0 0 2 2 6 3 [0.00] SYN317-1 non_thm 0.0 4 0 2 0 3 3 0 0 2 2 2 0 [0.00] SYN319-1 theorem 0.0 4 1 3 0 3 1 0 0 2 3 5 1 [0.00] SYN321-1 theorem 0.0 4 2 2 1 4 3 0 0 3 2 7 3 [0.00] SYN323-1 theorem 0.0 4 3 2 3 0 0 0 0 3 3 6 7 [0.00] SYN325-1 theorem 0.0 4 1 2 0 1 1 0 0 3 2 3 2 [0.00] SYN326-1 theorem 0.0 4 1 4 0 3 3 0 0 2 4 6 3 [0.00] SYN327-1 theorem 0.0 4 4 4 3 0 0 0 0 4 4 22 25 [0.00] SYN328-1 theorem 0.1 4 18 0 74 0 0 0 443 6 17 0 624 [0.00] SYN331-1 theorem 0.0 4 1 6 0 4 0 0 0 11 6 15 1 [0.00] SYN332-1 theorem 9.7 4 3 0 126 0 0 0 3922 11 124 0 4281 [0.00] SYN334-1 theorem 0.1 4 10 0 39 0 0 0 117 23 14 0 184 [0.00] SYN343-1 theorem 0.0 4 2 1 1 4 2 0 0 3 2 5 2 [0.00] SYN345-1 theorem 0.0 4 4 5 3 28 10 0 0 4 4 17 8 [0.00] SYN347-1 theorem 0.0 4 10 6 12 8 4 0 8 5 6 46 60 [0.00] SYN349-1 theorem 0.0 4 17 0 30 0 0 0 138 4 9 0 372 [0.00] SYN350-1 theorem 0.0 4 5 3 6 0 0 0 12 7 7 17 51 [0.00] SYN352-1 theorem 0.0 4 4 2 6 1 0 0 26 5 7 3 56 [0.00] SYN354-1 theorem 0.0 4 3 2 2 2 0 0 0 5 4 15 6 [0.00] SYN430-1 non_thm 0.0 4 0 36 11 71 15 0 165 2 47 40 176 [0.00] SYN431-1 non_thm 0.0 4 1 45 13 89 19 0 170 2 55 47 196 [0.00] SYN432-1 non_thm 0.0 4 0 54 16 101 21 0 459 2 70 54 491 [0.00] SYN433-1 non_thm 0.6 4 2 58 19 97 26 0 29975 2 62 137 34703 [0.00] SYN445-1 theorem 3.6 4 49 958 54 1513 378 0 95936 2 93 3373 288649 [0.00] SYN446-1 non_thm 0.6 4 13 261 22 459 110 0 14622 2 83 1381 37841 [0.00] SYN463-1 non_thm 0.2 4 3 75 14 169 37 0 5746 2 80 154 8067 [0.00] SYN478-1 theorem 3.7 4 127 1952 142 4032 968 0 46296 2 64 6399 285933 [0.00] SYN484-1 theorem 0.7 4 32 507 32 965 228 0 6375 2 54 1873 63539 [0.00] SYN490-1 non_thm 0.0 4 0 13 4 30 6 0 14 2 17 13 18 [0.00] SYN491-1 non_thm 0.0 4 0 10 3 21 7 0 17 2 13 10 20 [0.00] SYN492-1 non_thm 0.0 4 0 7 2 21 6 0 7 2 9 7 9 [0.00] SYN493-1 non_thm 0.0 4 0 10 3 23 7 0 8 2 13 10 11 [0.00] SYN494-1 non_thm 0.0 4 0 7 2 20 5 0 12 2 9 7 14 [0.00] SYN495-1 non_thm 0.0 4 0 25 8 49 10 0 25 2 33 25 33 [0.00] SYN496-1 non_thm 0.0 4 0 7 2 19 6 0 4 2 9 7 6 [0.00] SYN497-1 non_thm 0.0 4 0 13 4 30 6 0 11 2 17 13 15 [0.00] SYN501-1 theorem 0.7 4 25 390 24 831 184 0 7592 2 63 1473 61962 [0.00] SYN504-1 theorem 1.7 4 33 422 48 845 219 0 40410 2 75 3037 134377 [0.00] SYN505-1 theorem 0.9 4 80 920 86 1979 537 0 17476 2 72 3030 66506 [0.00] SYN510-1 theorem 1.7 4 124 1840 139 3911 867 0 21205 2 77 6315 112841 [0.00] SYN515-1 non_thm 0.0 4 0 8 20 71 26 0 23 2 19 8 37 [0.00] SYN516-1 non_thm 0.0 4 0 0 6 41 12 0 12 2 6 0 18 [0.00] SYN517-1 non_thm 0.0 4 0 16 18 154 50 0 64 2 15 16 52 [0.00] SYN521-1 non_thm 0.0 4 0 16 15 89 16 0 47 3 31 16 62 [0.00] SYN522-1 non_thm 0.0 4 0 25 43 148 53 0 80 2 36 25 98 [0.00] SYN523-1 non_thm 0.0 4 0 4 9 39 14 0 19 2 13 4 28 [0.00] SYN524-1 non_thm 0.0 4 0 8 14 90 41 0 27 2 16 8 31 [0.00] SYN525-1 non_thm 0.0 4 0 8 15 89 27 0 27 2 23 8 42 [0.00] SYN526-1 non_thm 0.0 4 0 9 11 65 27 0 23 3 20 9 34 [0.00] SYN527-1 non_thm 0.0 4 0 24 32 221 63 0 51 2 22 24 58 [0.00] SYN528-1 non_thm 0.0 4 0 2 15 84 21 0 22 2 17 2 37 [0.00] SYN529-1 non_thm 0.0 4 0 24 20 121 33 0 78 3 44 24 98 [0.00] SYN530-1 non_thm 0.0 4 0 7 13 72 22 0 25 2 20 7 38 [0.00] SYN531-1 non_thm 0.0 4 0 24 43 163 60 0 71 2 33 24 92 [0.00] SYN532-1 non_thm 0.0 4 0 27 19 109 44 0 67 2 29 27 72 [0.00] SYN533-1 non_thm 0.0 4 0 11 12 87 18 0 20 3 23 11 32 [0.00] SYN534-1 non_thm 0.0 4 0 12 13 73 26 0 17 3 25 12 30 [0.00] SYN535-1 non_thm 0.0 4 0 5 11 87 26 0 24 2 16 5 36 [0.00] SYN536-1 non_thm 0.0 4 0 15 15 139 49 0 30 2 16 15 34 [0.00] SYN537-1 non_thm 0.0 4 0 22 14 86 36 0 33 3 36 22 47 [0.00] SYN554-1 theorem 0.1 4 1 10 0 4 0 0 0 7 10 43 1 [0.00] SYN560-1 timeout 299.0 20 [0.00] SYN567-1 theorem 0.0 4 1 9 0 7 0 0 0 5 9 24 0 [0.00] SYN568-1 theorem 0.0 4 1 8 0 6 0 0 0 15 8 29 1 [0.00] SYN571-1 theorem 0.0 4 1 17 0 6 0 0 0 6 17 60 1 [0.00] SYN573-1 theorem 0.0 4 1 8 0 5 0 0 0 4 8 23 0 [0.00] SYN574-1 theorem 0.1 4 2 47 1 8 0 0 259 8 46 293 267 [0.00] SYN575-1 theorem 0.0 4 2 47 1 8 0 0 259 8 46 293 267 [0.00] SYN578-1 theorem 0.0 4 2 50 1 9 0 0 190 6 49 223 197 [0.00] SYN579-1 theorem 0.0 4 2 50 1 9 0 0 190 6 49 223 197 [0.00] SYN580-1 theorem 0.0 4 1 20 0 8 0 0 0 5 20 60 0 [0.00] SYN581-1 theorem 0.1 4 1 75 0 9 0 0 0 7 75 450 0 [0.00] SYN582-1 theorem 0.0 4 1 52 0 9 0 0 0 7 52 297 0 [0.00] SYN583-1 theorem 0.1 4 1 82 0 9 0 0 0 7 82 763 0 [0.00] SYN585-1 timeout 299.0 28 [0.00] SYN586-1 theorem 0.1 4 1 42 0 9 0 0 0 7 42 179 1 [0.00] SYN587-1 theorem 0.0 4 1 23 0 9 0 0 0 5 23 78 1 [0.00] SYN591-1 theorem 0.0 4 1 29 0 13 0 0 0 7 29 91 0 [0.00] SYN592-1 theorem 0.0 4 1 29 0 13 0 0 0 7 29 91 0 [0.00] SYN593-1 theorem 0.0 4 1 10 0 10 0 0 0 2 10 14 0 [0.00] SYN594-1 theorem 0.0 4 1 19 0 8 0 0 0 12 19 60 0 [0.00] SYN605-1 theorem 0.2 4 1 133 0 12 1 0 0 9 133 598 0 [0.00] SYN608-1 theorem 0.3 4 1 131 0 12 1 0 0 10 131 734 0 [0.00] SYN613-1 theorem 0.0 4 1 14 0 10 0 0 0 5 14 41 0 [0.00] SYN619-1 theorem 0.1 4 1 92 0 8 0 0 0 8 92 512 0 [0.00] SYN621-1 timeout 299.0 31 [0.00] SYN622-1 theorem 2.9 4 1 29 0 12 0 0 0 9 29 203 0 [0.00] SYN623-1 theorem 5.1 5 1 707 0 15 0 0 0 15 707 14856 0 [0.00] SYN624-1 theorem 0.1 4 1 71 0 14 0 0 0 9 71 270 0 [0.00] SYN626-1 theorem 0.1 4 1 17 0 10 0 0 0 15 17 68 0 [0.00] SYN627-1 timeout 299.0 4 [0.00] SYN656-1 theorem 0.1 4 1 45 0 18 0 0 0 15 45 144 1 [0.00] SYN660-1 theorem 0.4 4 1 48 0 23 0 0 0 9 48 237 0 [0.00] SYN661-1 theorem 0.4 4 1 41 0 23 0 0 0 9 41 215 0 [0.00] SYN662-1 theorem 0.3 4 1 40 0 23 0 0 0 9 40 171 0 [0.00] SYN663-1 theorem 0.3 4 1 33 0 23 0 0 0 9 33 151 0 [0.00] SYN664-1 theorem 0.4 4 1 48 0 23 0 0 0 9 48 237 0 [0.00] SYN665-1 theorem 0.4 4 1 41 0 23 0 0 0 9 41 215 0 [0.00] SYN666-1 theorem 0.0 4 1 39 0 23 0 0 0 9 39 145 0 [0.00] SYN667-1 theorem 0.1 4 1 34 0 23 0 0 0 9 34 131 0 [0.00] SYN668-1 theorem 0.1 4 1 39 0 23 0 0 0 9 39 145 0 [0.00] SYN669-1 theorem 0.0 4 1 34 0 23 0 0 0 9 34 131 0 [0.00] SYN670-1 theorem 0.0 4 1 31 0 23 0 0 0 9 31 83 0 [0.00] SYN671-1 theorem 0.0 4 1 26 0 23 0 0 0 9 26 71 0 [0.00] SYN672-1 theorem 0.1 4 1 30 0 22 0 0 0 17 30 93 0 [0.00] SYN673-1 theorem 23.7 8 1 479 0 19 0 0 0 19 479 6519 0 [0.00] SYN674-1 theorem 0.4 4 1 49 0 24 0 0 0 9 49 239 0 [0.00] SYN675-1 theorem 0.4 4 1 42 0 24 0 0 0 9 42 217 0 [0.00] SYN676-1 theorem 0.3 4 1 41 0 24 0 0 0 9 41 173 0 [0.00] SYN677-1 theorem 0.3 4 1 34 0 24 0 0 0 9 34 153 0 [0.00] SYN678-1 theorem 0.4 4 1 49 0 24 0 0 0 9 49 239 0 [0.00] SYN679-1 theorem 0.4 4 1 42 0 24 0 0 0 9 42 217 0 [0.00] SYN680-1 theorem 0.4 4 1 49 0 24 0 0 0 9 49 239 0 [0.00] SYN681-1 theorem 0.4 4 1 42 0 24 0 0 0 9 42 217 0 [0.00] SYN682-1 theorem 0.4 4 1 49 0 24 0 0 0 9 49 239 0 [0.00] SYN683-1 theorem 0.4 4 1 42 0 24 0 0 0 9 42 217 0 [0.00] SYN684-1 theorem 0.3 4 1 41 0 24 0 0 0 9 41 173 0 [0.00] SYN685-1 theorem 0.3 4 1 34 0 24 0 0 0 9 34 153 0 [0.00] SYN686-1 theorem 0.1 4 1 186 0 22 0 0 0 9 186 1199 0 [0.00] SYN710-1 timeout 299.0 17 [0.00] SYN713-1 theorem 0.1 4 1 73 0 40 0 0 0 11 73 233 0 [0.00] SYN717-1 theorem 0.0 4 1 50 0 46 0 0 0 7 50 136 0 [0.00] SYN718-1 timeout 299.0 36 [0.00] SYN724-1 theorem 0.0 4 2 5 1 8 6 0 0 2 4 9 6 [0.00] SYN726-1 theorem 0.0 4 6 47 22 2 0 0 227 3 30 193 537 [0.00] SYN728-1 theorem 0.0 4 3 3 6 3 3 0 1 8 6 9 11 [0.00] SYN811-1 non_thm 1.7 6 0 376 120 64 489 0 433 3 489 712 548 [0.00] SYN823-1 non_thm 0.9 19 0 160 523 32 249 0 624 3 261 288 1007 [0.00] SYN824-1 non_thm 4.9 19 0 515 315 65 896 0 809 3 676 965 1110 [0.00] SYN827-1 non_thm 0.6 19 0 188 104 36 269 0 238 3 244 340 324 [0.00] SYN867-1 non_thm 0.4 22 0 48 23 48 458 0 15 4 64 48 36 [0.00] SYN868-1 non_thm 0.1 22 0 45 5 45 433 0 0 3 50 45 5 [0.00] SYN870-1 non_thm 0.4 22 6 36 70 36 262 0 178 4 88 42 266 [0.00] SYN872-1 non_thm 0.7 22 0 94 5 94 1717 0 1 3 99 94 6 [0.00] SYN888-1 non_thm 1.8 22 1 102 37 102 1760 0 36 3 123 103 60 [0.00] SYN902-1 non_thm 6.7 22 5 102 89 102 1757 0 86 5 165 107 166 [0.00] TOP001-2 timeout 298.9 22 [0.00] TOP002-2 theorem 0.0 22 1 2 0 2 0 0 0 2 2 2 1 [0.00] TOP004-1 theorem 0.0 22 1 1 0 0 0 0 0 2 1 4 2 [0.00] TOP004-2 theorem 0.0 22 1 1 0 0 0 0 0 2 1 5 1 [0.11] PUZ010-1 theorem 1.3 4 344 6918 359 576 446 0 9902 3 204 20149 27734 [0.11] PUZ017-1 theorem 0.1 4 5 306 4 85 1 6 723 3 231 1167 1632 [0.11] PUZ018-1 theorem 0.1 4 1 53 0 41 6 0 0 3 53 76 2 [0.11] PUZ028-6 theorem 0.1 4 20 376 19 36 0 0 137 3 82 1298 292 [0.11] SYN452-1 theorem 1.3 4 78 906 90 1623 412 0 26268 2 81 3108 81217 [0.11] SYN459-1 theorem 1.9 4 80 1222 85 2211 548 0 32743 2 74 4534 181353 [0.11] SYN461-1 theorem 0.8 4 77 900 81 1716 468 0 12279 2 58 3040 56095 [0.11] SYN462-1 theorem 1.8 4 60 946 66 1637 423 0 44025 2 67 3846 153293 [0.11] SYN471-1 theorem 4.3 5 53 610 55 1208 298 0 175300 2 80 3711 323880 [0.11] SYN475-1 theorem 2.6 4 67 1051 71 1960 506 0 57714 2 65 3827 255975 [0.11] SYN479-1 theorem 1.1 4 40 588 43 1166 324 0 12984 2 79 2213 115338 [0.11] SYN482-1 theorem 1.6 4 90 1200 99 2147 578 0 27509 2 74 6693 71566 [0.11] SYN483-1 theorem 1.1 4 62 1091 62 2169 520 0 8410 2 66 3550 76206 [0.11] SYN486-1 theorem 1.2 4 76 1035 75 2153 525 0 13495 2 58 4195 115142 [0.11] SYN500-1 theorem 1.7 4 73 985 74 1731 468 0 20216 2 62 4348 189946 [0.11] SYN502-1 theorem 4.9 5 111 2466 117 4509 979 0 45224 2 79 10862 407213 [0.11] SYN506-1 theorem 0.4 4 17 406 18 802 173 0 1967 2 69 1289 19104 [0.11] SYN508-1 theorem 5.7 4 120 1447 128 3053 768 0 166563 2 84 10321 353972 [0.11] SYN509-1 theorem 0.6 4 53 665 54 1407 374 0 6400 2 54 2357 42898 [0.11] SYN512-1 theorem 1.4 4 66 1629 69 3116 684 0 9265 2 86 4021 77044 [0.11] SYN836-1 theorem 1.7 20 2 188 157 36 269 0 285 4 278 342 574 [0.11] SYN869-1 theorem 0.1 22 2 36 5 36 266 0 0 3 40 38 28 [0.11] SYN871-1 theorem 0.3 22 4 36 27 36 256 0 31 5 55 40 85 [0.11] SYN873-1 theorem 3.6 22 3 36 14 36 269 0 8 5 44 39 41 [0.11] SYN874-1 theorem 0.7 22 6 36 30 36 269 0 8 5 47 42 161 [0.11] SYN875-1 theorem 0.1 22 12 36 36 36 265 0 27 2 45 48 155 [0.11] SYN876-1 theorem 9.5 22 66 52 421 52 487 0 1667 8 135 118 2928 [0.11] SYN877-1 theorem 0.2 22 3 36 17 36 268 0 18 3 46 39 93 [0.11] SYN878-1 theorem 0.3 22 4 36 15 36 271 0 16 3 44 40 84 [0.11] SYN879-1 theorem 0.2 22 2 36 10 36 271 0 5 3 42 38 66 [0.11] SYN880-1 theorem 0.3 22 2 52 6 52 488 0 0 3 56 54 38 [0.11] SYN881-1 theorem 67.6 22 782 52 5702 52 490 0 92280 5 167 834 103481 [0.11] SYN882-1 theorem 0.5 22 5 52 18 52 485 0 12 4 60 57 66 [0.11] SYN883-1 theorem 5.6 22 21 52 64 52 491 0 104 4 74 73 252 [0.11] SYN884-1 theorem 1.0 22 3 70 8 70 932 0 0 4 75 73 39 [0.11] SYN889-1 theorem 0.1 22 3 36 5 36 271 0 0 2 39 39 46 [0.11] SYN890-1 theorem 0.1 22 2 36 5 36 273 0 2 2 40 38 46 [0.11] SYN891-1 theorem 0.1 22 2 36 6 36 259 0 0 2 40 38 42 [0.11] SYN892-1 theorem 0.1 22 3 36 10 36 273 0 11 2 43 39 71 [0.11] SYN893-1 theorem 0.3 22 2 52 16 52 485 0 2 3 63 54 68 [0.11] SYN894-1 theorem 0.3 22 3 52 11 52 489 0 3 3 60 55 44 [0.11] SYN895-1 theorem 0.3 22 3 52 13 52 479 0 5 3 63 55 75 [0.14] HWV034-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.14] KRS005-1 non_thm 0.0 4 0 8 0 1 0 0 36 5 8 8 36 [0.14] KRS006-1 non_thm 0.0 4 0 20 3 5 0 0 68 7 23 31 71 [0.14] KRS007-1 non_thm 0.0 4 0 27 2 2 0 0 83 7 29 37 85 [0.14] KRS008-1 non_thm 0.1 4 0 44 32 2 0 0 774 7 76 72 810 [0.14] KRS009-1 non_thm 0.0 4 0 31 26 1 0 0 163 5 33 53 165 [0.14] KRS011-1 non_thm 0.0 4 0 36 3 2 0 0 46 5 39 44 49 [0.14] KRS014-1 non_thm 0.0 4 0 14 2 1 0 0 30 5 16 17 32 [0.14] KRS016-1 non_thm 0.0 4 0 4 4 2 0 0 10 2 8 4 14 [0.14] MSC009-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 [0.14] NLP043-1 non_thm 0.0 4 0 17 2 35 3 0 29 4 19 17 31 [0.14] NLP044-1 non_thm 0.0 4 0 17 2 35 3 0 29 4 19 17 31 [0.14] NLP045-1 non_thm 0.0 4 0 17 2 35 3 0 29 4 19 17 31 [0.14] NLP046-1 non_thm 0.0 4 0 17 2 35 3 0 29 4 19 17 31 [0.14] NLP047-1 non_thm 0.0 4 0 17 2 35 3 0 29 4 19 17 31 [0.14] NLP048-1 non_thm 0.0 4 0 17 2 35 3 0 29 4 19 17 31 [0.14] NLP066-1 non_thm 0.0 4 0 9 14 22 4 0 35 3 15 9 25 [0.14] NLP067-1 non_thm 0.1 4 2 12 12 13 3 0 34 5 16 24 42 [0.14] NLP068-1 non_thm 0.0 4 0 5 3 12 3 0 12 3 8 5 15 [0.14] NLP095-1 non_thm 0.0 4 0 2 1 20 3 0 6 2 3 2 7 [0.14] NLP096-1 non_thm 0.0 4 0 2 1 20 3 0 6 2 3 2 7 [0.14] NLP097-1 non_thm 0.0 4 0 2 1 21 2 0 7 2 3 2 8 [0.14] NLP098-1 non_thm 0.0 4 0 2 1 21 2 0 7 2 3 2 8 [0.14] NLP099-1 non_thm 0.0 4 0 3 1 22 3 0 2 3 4 3 3 [0.14] NLP100-1 non_thm 0.0 4 0 2 1 21 3 0 14 2 3 2 15 [0.14] NLP101-1 non_thm 0.0 4 0 2 1 21 3 0 14 2 3 2 15 [0.14] NLP102-1 non_thm 0.0 4 0 3 1 22 4 0 9 3 4 3 10 [0.14] NLP103-1 non_thm 0.0 4 0 4 1 22 4 0 10 3 5 4 11 [0.14] NLP130-1 non_thm 0.0 4 0 21 7 44 4 0 40 5 27 21 45 [0.14] NLP131-1 non_thm 0.0 4 0 21 2 44 4 0 38 4 23 21 40 [0.14] NLP132-1 non_thm 0.0 4 0 21 3 44 4 0 38 4 24 21 41 [0.14] NLP133-1 non_thm 0.0 4 0 21 3 44 4 0 38 4 24 21 41 [0.14] NLP134-1 non_thm 0.0 4 0 21 2 44 4 0 37 4 23 21 39 [0.14] NLP135-1 non_thm 0.0 4 0 21 7 44 4 0 40 5 27 21 45 [0.14] NLP136-1 non_thm 0.0 4 0 40 3 86 5 0 78 4 23 40 60 [0.14] NLP137-1 non_thm 0.0 4 0 42 26 86 5 0 113 4 35 42 106 [0.14] NLP138-1 non_thm 0.0 4 0 40 3 86 5 0 78 4 23 40 60 [0.14] NLP139-1 non_thm 0.0 4 0 42 26 86 5 0 113 4 35 42 106 [0.14] NLP221-1 non_thm 0.0 4 0 20 1 43 4 0 34 5 21 20 35 [0.14] NLP222-1 non_thm 0.0 4 0 20 1 43 4 0 34 5 21 20 35 [0.14] NLP223-1 non_thm 0.0 4 0 19 1 42 4 0 33 5 20 19 34 [0.14] NLP230-1 non_thm 0.1 4 1 80 1 159 5 0 72 5 45 82 112 [0.14] NLP231-1 non_thm 0.0 4 0 37 1 78 4 0 69 5 38 37 70 [0.14] NLP232-1 non_thm 0.1 4 0 38 1 79 4 0 70 5 39 38 71 [0.14] NLP233-1 non_thm 0.1 4 0 39 1 78 4 0 70 5 40 39 71 [0.14] NLP234-1 non_thm 0.0 4 0 38 1 79 4 0 70 5 39 38 71 [0.14] NLP235-1 non_thm 0.1 4 0 37 1 78 4 0 69 5 38 37 70 [0.14] NLP236-1 non_thm 0.0 4 0 37 1 78 4 0 69 5 38 37 70 [0.14] NLP237-1 non_thm 0.0 4 0 38 1 79 4 0 70 5 39 38 71 [0.14] NLP238-1 non_thm 0.1 4 0 37 1 78 4 0 69 5 38 37 70 [0.14] NLP239-1 non_thm 0.0 4 0 37 1 78 4 0 69 5 38 37 70 [0.14] PUZ044-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 [0.14] PUZ045-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 [0.14] SET777-1 non_thm 0.0 4 0 0 2 0 0 0 2 2 2 0 4 [0.14] SET778-1 non_thm 0.0 4 0 0 3 0 0 0 2 2 3 0 5 [0.14] SET779-1 non_thm 0.0 4 0 0 3 0 0 0 3 2 3 0 6 [0.14] SET780-1 non_thm 0.0 4 0 0 3 0 0 0 2 2 3 0 5 [0.14] SYN036-2 non_thm 0.0 4 0 0 1 124 44 0 0 2 1 0 1 [0.14] SYN084-1 non_thm 0.0 4 0 1 1 13 14 1 0 2 2 1 1 [0.14] SYN304-1 non_thm 0.0 4 0 6 1 6 0 0 3 6 7 9 4 [0.14] SYN306-1 timeout 299.0 4 [0.14] SYN308-1 non_thm 0.0 4 0 1 2 2 0 0 0 4 3 1 2 [0.14] SYN309-1 non_thm 0.0 4 0 2 2 5 0 0 0 5 4 2 2 [0.14] SYN320-1 non_thm 0.0 4 0 2 1 2 0 0 0 2 3 2 1 [0.14] SYN344-1 non_thm 0.0 4 1 4 1 9 5 2 4 3 4 6 5 [0.14] SYN348-1 non_thm 0.0 4 0 0 1 0 0 0 0 2 1 0 1 [0.14] SYN735-1 non_thm 0.0 4 0 1 2 1 0 0 4 2 3 1 6 [0.14] SYN738-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.14] SYN740-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.14] SYN743-1 non_thm 0.0 4 0 1 7 1 0 0 12 2 8 1 19 [0.14] SYN744-1 non_thm 0.0 4 0 1 2 1 0 0 1 2 3 1 3 [0.14] SYN756-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.14] SYN772-1 non_thm 0.0 4 0 2 49 2 0 0 407 2 19 2 393 [0.17] FLD001-3 theorem 0.0 4 1 25 0 7 0 0 0 4 25 172 0 [0.17] FLD002-3 theorem 0.0 4 1 26 0 7 0 0 0 4 26 189 0 [0.17] FLD005-3 theorem 0.2 4 1 130 0 6 0 0 0 5 130 1306 0 [0.17] FLD007-3 timeout 299.0 16 [0.17] FLD008-4 theorem 8.4 9 1 66 0 10 0 0 0 5 66 556 0 [0.17] FLD009-3 theorem 0.2 4 1 166 0 7 0 0 0 5 166 1774 0 [0.17] FLD010-5 theorem 0.2 4 1 81 0 5 0 0 0 6 81 1157 0 [0.17] FLD011-3 timeout 298.9 10 [0.17] FLD012-4 theorem 1.4 4 1 268 0 12 0 0 0 5 268 2787 0 [0.17] FLD013-3 theorem 128.1 26 1 85 0 10 0 0 0 6 85 1319 0 [0.17] FLD013-4 theorem 0.0 4 1 22 0 12 0 0 0 4 22 196 0 [0.17] FLD013-5 theorem 0.0 4 1 19 0 14 0 0 0 4 19 182 0 [0.17] FLD014-3 theorem 5.6 5 1 162 0 7 0 0 0 6 162 2981 0 [0.17] FLD015-3 theorem 0.2 4 1 92 0 7 0 0 0 5 92 607 0 [0.17] FLD016-3 theorem 0.6 4 1 72 0 10 0 0 0 5 72 616 0 [0.17] FLD016-5 theorem 2.3 4 1 98 0 12 0 0 0 5 98 1184 0 [0.17] FLD017-3 theorem 0.0 4 1 11 0 10 0 0 0 4 11 109 0 [0.17] FLD021-1 timeout 299.0 4 [0.17] FLD022-3 theorem 0.8 4 1 70 0 10 0 0 0 5 70 594 0 [0.17] FLD023-3 theorem 0.4 4 1 49 0 7 0 0 0 5 49 630 0 [0.17] FLD024-3 theorem 0.2 4 1 20 0 7 0 0 0 5 20 120 0 [0.17] FLD025-3 theorem 126.1 27 1 85 0 10 0 0 0 6 85 1319 0 [0.17] FLD025-4 theorem 0.0 4 1 29 0 12 0 0 0 4 29 217 0 [0.17] FLD025-5 theorem 0.0 4 1 27 0 14 0 0 0 4 27 210 0 [0.17] FLD026-3 theorem 287.8 13 1 2273 0 8 0 0 0 6 2273 274157 0 [0.17] FLD027-3 theorem 0.1 4 1 148 0 9 0 0 0 5 148 1454 0 [0.17] FLD028-3 theorem 2.1 4 1 101 0 11 0 0 0 5 101 977 0 [0.17] FLD029-3 theorem 1.0 4 1 586 0 11 0 0 0 5 586 6496 0 [0.17] FLD030-1 theorem 0.0 4 1 9 0 8 0 0 0 3 9 23 0 [0.17] FLD030-2 timeout 299.0 4 [0.17] FLD030-3 theorem 24.9 9 1 20 0 8 0 0 0 6 20 178 0 [0.17] FLD030-4 theorem 0.0 4 1 11 0 10 0 0 0 4 11 109 0 [0.17] FLD031-3 theorem 0.1 4 1 60 0 7 0 0 0 5 60 2026 0 [0.17] FLD031-5 theorem 1.8 4 1 174 0 7 0 0 0 6 174 7861 0 [0.17] FLD032-3 theorem 0.0 4 1 14 0 7 0 0 0 5 14 82 0 [0.17] FLD034-1 timeout 299.0 4 [0.17] FLD035-3 theorem 2.0 4 1 101 0 11 0 0 0 5 101 977 0 [0.17] FLD036-3 theorem 2.1 4 1 101 0 11 0 0 0 5 101 977 0 [0.17] FLD037-1 timeout 299.0 4 [0.17] FLD037-3 theorem 0.2 4 1 89 0 8 0 0 0 5 89 1744 0 [0.17] FLD038-3 theorem 0.2 4 1 26 0 8 0 0 0 5 26 169 0 [0.17] FLD040-3 theorem 0.1 4 1 44 0 6 0 0 0 5 44 449 0 [0.17] FLD040-5 theorem 0.1 4 1 45 0 6 0 0 0 5 45 504 0 [0.17] FLD041-3 theorem 0.2 4 1 187 0 8 0 0 0 5 187 2312 0 [0.17] FLD041-4 theorem 0.7 4 1 342 0 10 0 0 0 5 342 10064 0 [0.17] FLD043-3 theorem 0.2 4 1 68 0 7 0 0 0 5 68 741 0 [0.17] FLD049-4 theorem 29.4 12 1 156 0 15 0 0 0 5 156 1487 0 [0.17] FLD050-4 theorem 39.3 15 1 159 0 15 0 0 0 5 159 1530 0 [0.17] FLD055-3 theorem 0.0 4 1 16 0 9 0 0 0 4 16 110 0 [0.17] FLD058-3 theorem 0.0 4 1 23 0 9 0 0 0 4 23 153 0 [0.17] FLD059-1 timeout 299.0 4 [0.17] FLD059-3 theorem 0.8 4 1 53 0 6 0 0 0 6 53 578 0 [0.17] FLD059-4 theorem 0.0 4 1 11 0 8 0 0 0 4 11 66 0 [0.17] FLD060-3 timeout 299.0 24 [0.17] FLD060-4 theorem 44.1 9 1 365 0 11 0 0 0 6 365 5462 0 [0.17] FLD061-4 timeout 299.0 13 [0.17] FLD063-3 timeout 299.0 12 [0.17] FLD064-3 theorem 0.9 4 1 83 0 6 0 0 0 6 83 983 0 [0.17] FLD065-3 theorem 0.1 4 1 8 0 6 0 0 0 5 8 42 0 [0.17] FLD066-3 theorem 2.6 4 1 208 0 12 0 0 0 5 208 1664 0 [0.17] FLD067-3 timeout 299.0 19 [0.17] FLD067-4 theorem 0.7 4 1 47 0 9 0 0 0 5 47 350 0 [0.17] FLD068-3 timeout 299.0 19 [0.17] FLD068-4 theorem 0.7 4 1 31 0 9 0 0 0 5 31 210 0 [0.17] FLD069-3 theorem 0.0 4 1 12 0 9 0 0 0 4 12 73 0 [0.17] FLD070-1 timeout 298.9 4 [0.17] FLD070-3 theorem 5.0 4 1 83 0 8 0 0 0 6 83 1058 0 [0.17] FLD070-4 theorem 0.0 4 1 13 0 10 0 0 0 4 13 91 0 [0.17] FLD071-1 theorem 0.0 4 1 8 0 8 0 0 0 2 8 8 0 [0.17] GRP123-3.004 non_thm 0.0 4 1 143 1 32 0 1 219 4 133 950 253 [0.17] GRP123-8.004 non_thm 0.1 4 0 178 2 33 0 1 342 4 180 879 372 [0.17] GRP123-9.004 non_thm 0.0 4 0 138 29 18 0 0 322 4 167 813 379 [0.17] GRP125-1.004 non_thm 0.0 4 0 77 1 17 0 0 165 4 78 469 180 [0.17] GRP125-2.004 non_thm 0.0 4 0 96 0 26 0 0 180 4 96 490 180 [0.17] GRP125-3.004 non_thm 0.1 4 1 143 1 32 0 1 206 4 133 668 243 [0.17] GRP127-2.005 non_thm 0.1 4 1 187 1 40 0 0 447 4 175 1050 542 [0.17] GRP128-1.004 non_thm 0.1 4 7 171 8 16 0 0 215 4 84 925 392 [0.17] GRP128-2.004 non_thm 0.0 4 1 100 3 25 0 0 188 4 102 537 198 [0.17] GRP128-3.004 non_thm 0.0 4 3 212 4 31 0 0 232 4 139 876 345 [0.17] GRP130-3.004 non_thm 0.0 4 2 200 2 31 0 0 232 4 139 850 333 [0.17] GRP133-2.004 non_thm 0.0 4 2 121 5 25 0 0 186 4 102 613 250 [0.17] HWV008-1.001 theorem 0.1 4 1 243 0 11 0 0 0 14 243 572 0 [0.17] HWV008-1.002 theorem 0.2 4 1 366 0 14 0 0 0 14 366 824 0 [0.17] HWV008-2.001 theorem 0.1 4 1 241 0 9 0 0 0 10 241 519 0 [0.17] HWV008-2.002 theorem 0.2 4 1 366 0 12 0 0 0 10 366 758 0 [0.17] NLP079-1 theorem 0.0 4 2 40 1 76 4 0 0 5 22 80 52 [0.17] NLP080-1 theorem 0.0 4 2 40 1 76 4 0 0 5 22 78 52 [0.17] NLP081-1 theorem 0.0 4 2 38 1 72 4 0 0 5 21 74 49 [0.17] NLP094-1 theorem 0.0 4 2 42 1 64 4 0 0 6 23 50 44 [0.17] PUZ035-3 theorem 0.0 4 4 10 3 6 8 0 3 4 7 16 6 [0.17] PUZ035-4 theorem 0.0 4 4 10 3 6 8 0 3 4 7 16 6 [0.17] SET005-1 theorem 0.0 4 2 37 1 4 0 0 0 6 33 94 53 [0.17] SET007-1 theorem 0.0 4 3 157 2 5 0 2 0 6 87 318 205 [0.17] SET014-2 timeout 298.9 17 [0.17] SET055-6 timeout 299.0 24 [0.17] SYN002-1.007.008 theorem 0.1 4 2 0 37 0 0 0 234 23 22 0 309 [0.17] SYN015-2 theorem 0.0 4 1 33 0 7 0 0 0 4 33 149 2 [0.17] SYN036-3 theorem 0.0 4 11 74 10 254 174 14 28 2 17 115 80 [0.17] SYN037-1 theorem 0.0 4 10 70 9 244 178 12 18 2 17 103 73 [0.17] SYN037-2 theorem 0.0 4 12 18 15 171 87 8 14 2 9 66 54 [0.17] SYN313-1.001.002 theorem 66.4 6 952 4509 2060 0 0 4 10030 83 58 5619 26346 [0.17] SYN419-1 non_thm 4.8 8 0 56 90 376 107 0 191 3 146 57 283 [0.17] SYN420-1 non_thm 0.6 4 0 39 136 463 123 0 914 3 175 39 1050 [0.17] SYN425-1 non_thm 0.3 4 0 122 114 402 122 0 1082 3 236 128 1205 [0.17] SYN434-1 non_thm 4.6 9 3 125 30 199 43 0 148785 2 146 889 170063 [0.17] SYN435-1 non_thm 0.1 4 0 91 27 175 32 0 2182 2 118 159 2209 [0.17] SYN437-1 non_thm 0.7 4 18 291 39 418 109 0 22669 2 91 1948 47429 [0.17] SYN438-1 non_thm 0.6 4 20 174 31 348 100 0 26078 2 55 946 41517 [0.17] SYN449-1 non_thm 5.1 4 199 3030 220 5002 1339 0 70244 2 89 12938 322102 [0.17] SYN456-1 non_thm 6.6 6 225 2444 264 4412 1200 0 216245 2 77 12369 450415 [0.17] SYN538-1 non_thm 0.0 4 0 2 15 73 26 0 16 2 17 2 31 [0.17] SYN539-1 non_thm 0.0 4 0 32 32 160 52 0 145 2 48 32 171 [0.17] SYN540-1 non_thm 0.1 4 3 28 21 204 60 0 70 3 44 53 105 [0.17] SYN541-1 non_thm 0.0 4 0 32 43 204 75 0 96 2 36 32 125 [0.17] SYN545-1 non_thm 2.9 4 3 51 166 458 111 0 3721 3 212 105 3941 [0.17] SYN606-1 theorem 1.1 4 1 303 0 12 1 0 0 10 303 1226 0 [0.17] SYN607-1 theorem 2.2 4 1 348 0 12 1 0 0 11 348 3018 0 [0.17] SYN620-1 theorem 0.1 4 1 26 0 13 0 0 0 10 26 128 0 [0.17] SYN625-1 timeout 299.0 5 [0.17] SYN630-1 theorem 0.0 4 1 9 0 9 0 0 0 2 9 13 0 [0.17] SYN633-1 timeout 299.0 7 [0.17] SYN634-1 timeout 299.0 7 [0.17] SYN635-1 timeout 299.0 7 [0.17] SYN636-1 timeout 299.0 7 [0.17] SYN641-1 theorem 4.9 6 1 70 0 15 0 0 0 14 70 500 0 [0.17] SYN642-1 theorem 4.9 5 1 62 0 15 0 0 0 14 62 484 0 [0.17] SYN643-1 theorem 4.9 5 1 66 0 15 0 0 0 14 66 492 0 [0.17] SYN648-1 timeout 299.0 45 [0.17] SYN659-1 theorem 8.0 6 1 242 0 22 0 0 0 11 242 2322 0 [0.17] SYN692-1 timeout 299.0 28 [0.17] SYN693-1 timeout 299.0 27 [0.17] SYN695-1 timeout 299.0 28 [0.17] SYN697-1 timeout 299.0 27 [0.17] SYN699-1 timeout 299.0 28 [0.17] SYN701-1 timeout 299.0 27 [0.17] SYN714-1 theorem 0.0 4 1 42 0 31 0 0 0 8 42 143 0 [0.17] SYN815-1 non_thm 6.4 17 0 674 282 85 939 0 876 3 883 1293 1148 [0.17] SYN816-1 non_thm 18.7 17 0 590 252 79 939 0 790 4 842 1127 1043 [0.17] SYN817-1 non_thm 6.9 17 0 626 278 82 939 0 782 3 839 1198 1041 [0.17] SYN825-1 non_thm 12.8 19 0 945 117 85 1649 0 964 3 1062 1805 1081 [0.17] SYN826-1 non_thm 12.3 19 0 858 25 84 1763 0 798 3 883 1632 823 [0.17] SYN828-1 non_thm 5.5 19 0 646 236 68 899 0 789 3 832 1224 1010 [0.17] SYN835-1 non_thm 6.5 20 1 188 210 36 269 0 494 5 391 341 709 [0.17] TOP005-2 timeout 299.0 34 [0.22] GRP128-2.006 theorem 0.1 4 8 428 7 56 0 0 379 4 251 1751 1545 [0.22] GRP128-3.005 theorem 0.1 4 7 395 6 46 0 0 143 4 207 1467 858 [0.22] SYN442-1 theorem 18.2 6 173 2966 208 4720 1172 0 604960 2 100 11714 1206041 [0.22] SYN443-1 theorem 1.8 4 65 1031 65 1909 487 0 24113 2 78 3166 168269 [0.22] SYN444-1 theorem 0.9 4 74 1039 78 1725 444 0 10143 2 77 4533 57454 [0.22] SYN448-1 theorem 4.7 5 179 2699 201 4693 1248 0 54688 2 88 8162 353093 [0.22] SYN450-1 theorem 0.5 4 54 688 56 1265 328 0 7491 2 72 2246 28302 [0.22] SYN451-1 theorem 0.8 4 58 758 69 1394 363 0 14777 2 61 2519 49292 [0.22] SYN454-1 theorem 1.6 4 65 1044 69 1903 452 0 21906 2 69 3401 113545 [0.22] SYN455-1 theorem 12.5 4 126 1969 194 3353 888 0 459156 2 96 8900 825538 [0.22] SYN458-1 theorem 1.0 4 36 759 37 1271 317 0 4495 2 85 2118 83408 [0.22] SYN460-1 theorem 3.8 4 115 2424 132 3214 917 0 10867 2 84 8861 312766 [0.22] SYN465-1 theorem 1.5 4 67 1108 71 1958 462 0 19112 2 70 4436 100623 [0.22] SYN466-1 theorem 1.6 4 80 1220 87 2187 536 0 25230 2 85 5683 88129 [0.22] SYN467-1 theorem 0.6 4 40 657 41 1128 295 0 6204 2 60 2414 46843 [0.22] SYN469-1 theorem 3.3 4 137 2149 148 3986 950 0 54235 2 64 7564 300711 [0.22] SYN472-1 theorem 4.6 4 136 1770 148 3201 829 0 105259 2 66 9420 414112 [0.22] SYN477-1 theorem 1.0 4 57 624 63 1256 333 0 22276 2 55 2793 92723 [0.22] SYN480-1 theorem 1.7 4 73 999 76 1935 492 0 34929 2 62 3866 141294 [0.22] SYN485-1 theorem 1.3 4 41 717 40 1429 326 0 22086 2 81 2404 116507 [0.22] SYN488-1 theorem 5.6 5 167 2914 185 5455 1290 0 74054 2 82 11914 358354 [0.22] SYN489-1 theorem 0.7 4 42 942 44 1648 406 0 2850 2 76 2937 33727 [0.22] SYN499-1 theorem 5.9 4 83 1209 90 2382 582 0 157129 2 85 9465 434234 [0.22] SYN507-1 theorem 2.7 4 80 1371 80 2673 603 0 53797 2 89 4775 187253 [0.22] SYN813-1 theorem 3.7 17 17 188 1054 44 269 0 1536 5 469 365 2949 [0.22] SYN833-1 theorem 0.8 20 3 188 47 36 269 0 185 4 218 343 313 [0.22] SYN834-1 theorem 9.5 20 61 188 2727 36 269 0 4802 5 572 401 8784 [0.22] SYN843-1 theorem 3.5 22 4 188 119 36 269 0 251 4 267 344 462 [0.22] SYN849-1 timeout 299.0 58 [0.22] SYN856-1 theorem 9.5 22 3 188 129 36 269 0 257 4 270 343 539 [0.22] SYN857-1 theorem 1.5 22 8 188 487 36 269 0 864 3 509 348 1623 [0.22] SYN859-1 timeout 299.0 41 [0.22] SYN886-1 theorem 0.8 22 2 72 9 72 909 0 0 3 79 74 41 [0.22] SYN887-1 theorem 0.6 22 3 72 12 72 938 0 1 3 81 75 45 [0.22] SYN896-1 theorem 70.2 22 1833 52 8244 52 492 0 34170 3 116 1885 66178 [0.22] SYN898-1 theorem 1.1 22 5 72 21 72 941 0 9 4 84 77 84 [0.22] SYN899-1 theorem 1.2 22 3 72 16 72 931 0 5 4 83 75 77 [0.22] SYN900-1 theorem 1.1 22 5 72 32 72 923 0 11 5 94 77 76 [0.22] SYN901-1 theorem 90.8 22 4 101 21 101 1680 0 11 6 117 105 72 [0.29] HWV034-2 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.29] HWV035-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.29] HWV036-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.29] NLP059-1 non_thm 0.0 4 3 15 16 13 3 0 102 5 19 33 111 [0.29] NLP064-1 non_thm 0.1 4 1 8 6 13 3 0 9 5 12 14 14 [0.29] NLP065-1 non_thm 0.1 4 1 8 6 13 3 0 10 5 12 14 15 [0.29] SYN316-1 timeout 299.0 4 [0.29] SYN324-1 timeout 298.9 4 [0.29] SYN330-1 timeout 299.0 19 [0.29] SYN335-1 timeout 298.9 6 [0.29] SYN351-1 timeout 299.0 22 [0.29] SYN734-1 non_thm 0.0 4 0 1 1 1 0 0 0 2 2 1 1 [0.29] SYN742-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.29] SYN748-1 non_thm 0.1 4 0 1 6 1 0 0 83 3 6 1 86 [0.29] SYN749-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.29] SYN754-1 non_thm 0.0 4 0 1 8 1 0 0 26 2 6 1 35 [0.29] SYN757-1 non_thm 0.0 4 0 1 3 1 0 0 26 2 4 1 29 [0.29] SYN760-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 [0.29] SYN774-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.29] SYN785-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.29] SYN797-1 non_thm 0.0 4 0 2 1 2 0 0 20 2 3 2 21 [0.29] SYN798-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.33] ANA002-1 timeout 299.0 14 [0.33] ANA002-2 timeout 299.0 73 [0.33] ANA002-3 timeout 299.0 21 [0.33] ANA002-4 timeout 299.0 11 [0.33] ANA003-4 timeout 299.0 23 [0.33] FLD003-1 timeout 299.0 4 [0.33] FLD005-1 timeout 299.0 4 [0.33] FLD009-1 timeout 299.0 4 [0.33] FLD013-1 timeout 298.9 4 [0.33] FLD013-2 timeout 299.0 4 [0.33] FLD015-1 timeout 299.0 4 [0.33] FLD017-1 timeout 299.0 4 [0.33] FLD018-1 timeout 299.0 4 [0.33] FLD019-1 timeout 299.0 4 [0.33] FLD023-1 timeout 299.0 4 [0.33] FLD024-1 timeout 298.9 4 [0.33] FLD025-1 timeout 299.0 4 [0.33] FLD025-2 timeout 299.0 4 [0.33] FLD031-1 timeout 299.0 4 [0.33] FLD032-1 timeout 299.0 4 [0.33] FLD043-5 timeout 299.0 15 [0.33] FLD047-4 theorem 31.9 12 1 440 0 15 0 0 0 5 440 4258 0 [0.33] FLD049-3 timeout 299.0 10 [0.33] FLD054-4 theorem 6.5 5 1 418 0 14 0 0 0 5 418 4756 0 [0.33] FLD059-2 timeout 299.0 4 [0.33] FLD060-1 timeout 299.0 4 [0.33] FLD060-2 timeout 299.0 4 [0.33] FLD061-1 timeout 299.0 4 [0.33] FLD061-2 timeout 299.0 4 [0.33] FLD061-3 timeout 298.9 22 [0.33] FLD062-3 timeout 298.9 12 [0.33] FLD064-1 timeout 299.0 4 [0.33] FLD065-1 timeout 298.9 4 [0.33] FLD067-1 timeout 299.0 4 [0.33] FLD067-2 timeout 298.9 4 [0.33] FLD068-2 timeout 299.0 4 [0.33] FLD069-1 timeout 299.0 4 [0.33] FLD070-2 timeout 299.0 4 [0.33] FLD071-2 theorem 4.4 4 1 100 0 10 0 0 0 5 100 370 0 [0.33] GRP039-6 theorem 56.0 5 5 828 11 9 0 78 23876 6 740 134421 26425 [0.33] GRP123-4.004 non_thm 0.0 4 0 77 1 17 0 0 406 4 78 802 449 [0.33] GRP125-4.004 non_thm 0.1 4 0 77 1 17 0 0 419 4 78 719 462 [0.33] GRP126-2.005 non_thm 0.1 4 0 173 2 40 0 0 450 4 175 969 484 [0.33] GRP127-3.005 non_thm 0.1 4 2 277 2 47 0 1 550 4 228 1412 776 [0.33] GRP128-4.004 non_thm 0.0 4 5 83 6 16 0 0 474 4 84 884 512 [0.33] GRP130-2.005 non_thm 0.1 4 3 248 4 39 0 0 484 4 183 1296 688 [0.33] GRP130-4.004 non_thm 0.0 4 5 120 6 16 0 0 500 4 84 911 650 [0.33] MSC007-1.008 theorem 4.4 15 5040 55182 5039 282303 78952 0 2779 2 56 105582 27398 [0.33] PUZ018-2 non_thm 0.2 4 2 89 22 40 6 0 2963 3 111 163 3095 [0.33] PUZ035-7 timeout 299.0 6 [0.33] SET010-1 theorem 0.0 4 3 209 2 5 0 2 0 6 115 408 255 [0.33] SET012-1 timeout 299.0 21 [0.33] SET012-2 timeout 298.9 22 [0.33] SET013-1 timeout 299.0 24 [0.33] SET015-1 timeout 299.0 22 [0.33] SYN036-1 theorem 13.2 7 122 165 140 6020 824 72 187156 2 15 117155 952238 [0.33] SYN036-4 theorem 0.0 4 10 10 10 307 138 16 15 2 7 67 149 [0.33] SYN353-1 timeout 299.0 8 [0.33] SYN418-1 non_thm 1.8 5 0 61 116 404 92 0 946 3 177 61 1064 [0.33] SYN421-1 non_thm 19.5 25 0 45 105 455 98 0 228 3 150 47 333 [0.33] SYN422-1 non_thm 183.5 99 0 51 107 381 110 0 549 3 158 52 659 [0.33] SYN423-1 non_thm 0.3 4 0 140 183 471 126 0 432 3 323 142 615 [0.33] SYN424-1 non_thm 0.6 4 0 112 146 656 146 0 753 3 258 115 937 [0.33] SYN426-1 memory 69.6 399 [0.33] SYN427-1 non_thm 1.8 4 0 168 140 567 164 0 5105 3 308 168 5245 [0.33] SYN428-1 timeout 299.0 16 [0.33] SYN429-1 non_thm 0.2 4 1 100 101 660 144 0 489 3 200 130 607 [0.33] SYN436-1 theorem 8.5 5 155 2423 170 3211 966 0 242967 2 82 7677 782479 [0.33] SYN441-1 non_thm 6.7 4 64 1253 92 1459 420 0 126720 2 136 10580 294666 [0.33] SYN453-1 non_thm 5.3 10 58 1502 83 1747 482 0 101075 2 156 7041 184027 [0.33] SYN464-1 non_thm 19.0 8 69 1329 124 1757 501 0 590908 2 133 11574 1250174 [0.33] SYN468-1 theorem 1.6 4 98 1531 109 2911 726 0 11778 2 101 6370 90582 [0.33] SYN470-1 theorem 3.7 4 138 2632 145 4358 1051 0 26585 2 95 8910 242356 [0.33] SYN474-1 theorem 3.5 4 139 2238 143 4011 1050 0 40656 2 72 8227 298411 [0.33] SYN476-1 theorem 1.7 4 123 1982 131 3529 919 0 10959 2 84 7110 83103 [0.33] SYN481-1 theorem 3.3 4 119 1665 127 3325 805 0 60934 2 71 6479 311796 [0.33] SYN487-1 theorem 4.2 4 136 2429 157 4668 1108 0 71747 2 101 9894 196619 [0.33] SYN498-1 theorem 2.8 4 85 1353 92 2751 658 0 41153 2 76 4938 256428 [0.33] SYN503-1 theorem 0.9 4 56 664 60 1348 358 0 14286 2 66 3374 57289 [0.33] SYN511-1 theorem 1.0 4 60 803 63 1585 409 0 11862 2 80 4511 35254 [0.33] SYN513-1 non_thm 1.1 4 3 161 204 378 106 0 15887 3 360 251 16194 [0.33] SYN518-1 non_thm 0.9 4 0 144 201 394 98 0 9818 3 345 148 10041 [0.33] SYN542-1 non_thm 5.6 9 0 133 75 214 41 0 195640 2 208 642 196945 [0.33] SYN543-1 non_thm 6.5 7 0 132 68 210 38 0 203382 2 200 1015 204756 [0.33] SYN544-1 non_thm 0.4 4 1 136 158 234 87 0 2440 3 293 155 2627 [0.33] SYN546-1 non_thm 1.1 4 0 89 123 455 107 0 822 3 212 90 969 [0.33] SYN547-1 non_thm 0.8 4 1 78 114 504 121 0 993 3 189 96 1133 [0.33] SYN576-1 timeout 299.0 40 [0.33] SYN595-1 timeout 298.9 26 [0.33] SYN604-1 timeout 299.0 18 [0.33] SYN610-1 timeout 299.0 10 [0.33] SYN611-1 timeout 299.0 30 [0.33] SYN612-1 timeout 299.0 10 [0.33] SYN645-1 timeout 299.0 4 [0.33] SYN657-1 timeout 299.0 9 [0.33] SYN658-1 timeout 299.0 9 [0.33] SYN687-1 timeout 299.0 6 [0.33] SYN694-1 timeout 299.0 13 [0.33] SYN696-1 timeout 299.0 17 [0.33] SYN698-1 timeout 299.0 13 [0.33] SYN700-1 timeout 298.9 19 [0.33] SYN755-1 theorem 3.6 4 146 1 366 1 0 0 48385 5 21 1 60249 [0.33] SYN759-1 theorem 70.8 4 356 1 1123 1 0 0 344577 8 32 1 419398 [0.33] SYN762-1 theorem 53.0 4 232 1 852 1 0 0 251140 8 30 1 295979 [0.33] SYN784-1 theorem 4.5 4 82 2 339 2 0 0 39521 4 23 2 55079 [0.33] SYN796-1 theorem 1.0 4 42 2 143 2 0 0 13240 3 16 2 19609 [0.33] SYN812-1 non_thm 17.0 19 0 936 214 101 1708 0 1032 3 1150 1801 1246 [0.33] SYN814-1 non_thm 90.1 29 0 376 2648 64 489 0 5422 5 1273 712 8045 [0.33] SYN819-1 theorem 11.8 19 61 188 4270 44 269 0 7504 4 630 409 13343 [0.33] SYN820-1 timeout 299.0 77 [0.33] SYN829-1 non_thm 18.1 24 0 1177 145 95 1704 0 1199 3 1322 2259 1344 [0.33] SYN831-1 non_thm 23.7 26 0 1268 676 96 1763 0 1989 3 1698 2440 2627 [0.33] SYN832-1 non_thm 80.9 30 0 1033 269 93 1704 0 1199 4 1246 1973 1459 [0.33] SYN837-1 timeout 299.0 37 [0.33] SYN838-1 non_thm 84.6 22 5 634 6465 70 939 0 7988 5 1185 1203 13959 [0.33] SYN841-1 non_thm 94.7 38 8 1330 7795 102 1763 0 9744 3 1752 2566 16223 [0.33] SYN844-1 theorem 0.9 22 6 188 181 36 269 0 327 3 275 346 626 [0.33] SYN845-1 theorem 1.4 22 2 188 93 36 269 0 236 4 239 342 425 [0.33] SYN847-1 theorem 11.1 22 5 376 643 52 489 0 938 4 679 705 1871 [0.33] SYN848-1 theorem 57.4 22 7 376 497 52 489 0 812 5 587 707 1567 [0.33] SYN851-1 non_thm 33.6 22 1 696 500 72 939 0 1177 8 1136 1321 1738 [0.33] SYN858-1 theorem 2.5 22 2 376 181 52 489 0 523 3 506 702 873 [0.33] SYN860-1 timeout 299.0 32 [0.33] SYN863-1 timeout 298.9 54 [0.33] SYN864-1 non_thm 25.2 22 0 696 777 72 939 0 1379 6 1473 1320 2158 [0.33] SYN897-1 theorem 10.1 22 2 72 20 72 940 0 0 7 84 74 77 [0.43] HWV035-2 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.43] HWV036-2 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 [0.43] NLP026-1 non_thm 0.0 4 0 4 5 10 3 0 4 3 9 4 9 [0.43] NLP031-1 non_thm 0.0 4 0 8 8 23 5 0 14 3 10 8 16 [0.43] SYN736-1 non_thm 0.0 4 0 1 1 1 0 0 1 2 2 1 2 [0.43] SYN737-1 non_thm 0.0 4 0 1 9 1 0 0 153 2 8 1 158 [0.43] SYN739-1 non_thm 0.0 4 0 1 5 1 0 0 2 2 6 1 7 [0.43] SYN745-1 non_thm 0.0 4 0 1 15 1 0 0 47 2 8 1 59 [0.43] SYN752-1 non_thm 0.0 4 0 1 1 1 0 0 2 2 2 1 3 [0.43] SYN768-1 non_thm 0.0 4 0 2 1 2 0 0 5 2 3 2 6 [0.43] SYN794-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 [0.43] SYN804-1 non_thm 0.4 4 0 2 7 2 0 0 107 3 9 2 114 [0.43] TOP003-2 non_thm 0.0 22 0 12 4 3 0 0 25 9 16 20 29 [0.44] SYN447-1 theorem 68.7 23 354 7741 423 9283 3032 0 867115 2 130 27326 5669521 [0.44] SYN457-1 theorem 188.5 19 999 21446 1481 23793 6817 0 4562905 2 156 203897 6609426 [0.44] SYN473-1 theorem 2.6 4 89 1394 92 2407 634 0 26700 2 76 6183 247403 [0.44] SYN846-1 theorem 100.0 22 208 376 11025 52 489 0 15355 5 1058 908 31570 [0.44] SYN862-1 timeout 299.0 54 [0.44] SYN885-1 theorem 29.3 22 23 72 117 72 908 0 86 8 96 95 402 [0.50] ANA004-4 timeout 299.0 23 [0.50] ANA004-5 timeout 299.0 17 [0.50] COM003-1 timeout 299.0 26 [0.50] FLD004-1 timeout 298.9 4 [0.50] FLD007-1 timeout 298.9 4 [0.50] FLD016-1 timeout 299.0 4 [0.50] FLD020-1 timeout 299.0 4 [0.50] FLD022-1 timeout 299.0 4 [0.50] FLD033-1 timeout 299.0 4 [0.50] FLD050-3 timeout 299.0 9 [0.50] FLD052-4 timeout 299.0 53 [0.50] FLD057-3 timeout 299.0 11 [0.50] FLD063-1 timeout 299.0 4 [0.50] FLD066-1 timeout 299.0 4 [0.50] FLD068-1 timeout 298.9 4 [0.50] GRP123-1.005 non_thm 0.1 4 0 143 4 26 0 0 465 4 147 1556 505 [0.50] GRP123-2.005 non_thm 0.1 4 1 189 2 40 0 0 493 4 175 1815 595 [0.50] GRP123-6.005 non_thm 0.1 4 0 264 4 27 0 0 879 4 268 1624 947 [0.50] GRP123-7.005 non_thm 0.1 4 0 284 4 41 0 0 879 4 288 1644 947 [0.50] GRP124-1.005 non_thm 0.1 4 0 142 5 26 0 0 458 4 147 1556 505 [0.50] GRP124-2.005 non_thm 0.1 4 0 173 2 40 0 0 460 4 175 1590 505 [0.50] GRP124-3.005 non_thm 0.1 4 2 245 4 47 0 1 551 4 224 1899 670 [0.50] GRP124-4.005 non_thm 0.1 4 0 143 4 26 0 0 1190 4 147 1606 1305 [0.50] GRP124-6.005 non_thm 0.1 4 0 263 5 27 0 0 877 4 268 1624 947 [0.50] GRP124-7.005 non_thm 0.1 4 0 283 5 41 0 0 877 4 288 1644 947 [0.50] GRP124-8.005 non_thm 0.1 4 0 323 6 48 0 1 938 4 329 1739 1009 [0.50] GRP124-9.005 non_thm 0.1 4 0 263 50 27 0 0 882 4 313 1624 997 [0.50] GRP126-1.005 non_thm 0.0 4 0 143 4 26 0 0 443 4 147 935 484 [0.50] GRP126-3.005 non_thm 0.1 4 2 245 4 47 0 1 536 4 224 1271 649 [0.50] GRP126-4.005 non_thm 0.1 4 0 144 3 26 0 0 1212 4 147 1427 1326 [0.50] GRP127-1.005 non_thm 0.0 4 0 145 2 26 0 0 456 4 147 935 484 [0.50] GRP127-4.005 non_thm 0.1 4 0 145 2 26 0 0 1244 4 147 1427 1326 [0.50] GRP129-1.005 non_thm 0.2 4 24 686 28 25 0 0 737 4 155 3378 2149 [0.50] GRP129-2.005 non_thm 0.1 4 10 316 15 39 0 0 592 4 183 1745 820 [0.50] GRP129-3.005 non_thm 0.1 4 7 390 9 46 0 0 827 4 232 1914 992 [0.50] GRP129-4.005 non_thm 0.1 4 13 234 16 25 0 0 1454 4 155 2184 1880 [0.50] GRP130-1.005 non_thm 0.1 4 15 393 18 25 0 0 628 4 155 2174 1188 [0.50] GRP131-1.005 non_thm 0.1 4 0 147 8 25 0 0 484 4 155 1575 525 [0.50] GRP131-2.005 non_thm 0.8 4 80 1612 88 39 0 0 2453 4 183 16728 7868 [0.50] GRP132-2.005 non_thm 1.2 4 92 2522 99 39 0 0 1994 4 183 29511 12989 [0.50] GRP133-1.004 non_thm 0.0 4 1 87 3 16 0 0 186 4 84 530 211 [0.50] GRP134-1.005 non_thm 0.1 4 6 217 10 25 0 0 471 4 155 1724 855 [0.50] GRP134-2.005 non_thm 0.1 4 6 456 11 39 0 0 640 4 183 3295 1717 [0.50] GRP135-1.005 non_thm 0.5 4 60 1853 64 25 0 0 2405 4 155 12748 6877 [0.50] GRP135-2.005 non_thm 0.2 4 20 828 21 39 0 0 1088 4 183 5153 2994 [0.50] SET013-2 timeout 299.0 21 [0.50] SET015-2 timeout 299.0 16 [0.50] SYN067-1 theorem 17.6 5 468 4203 557 7854 718 0 113379 5 55 18004 714786 [0.50] SYN307-1 non_thm 0.0 4 0 2 1 2 0 0 5 2 3 4 6 [0.50] SYN514-1 non_thm 7.9 6 1 77 77 286 80 0 10796 3 152 88 10919 [0.50] SYN520-1 timeout 299.0 134 [0.50] SYN609-1 timeout 299.0 30 [0.50] SYN644-1 timeout 299.0 4 [0.50] SYN690-1 timeout 299.0 14 [0.50] SYN758-1 theorem 71.2 4 301 1 942 1 0 0 230632 9 27 1 289978 [0.50] SYN802-1 timeout 299.0 10 [0.50] SYN830-1 non_thm 18.6 22 0 1214 64 98 1763 0 1156 3 1278 2330 1220 [0.50] SYN839-1 timeout 299.0 58 [0.50] SYN840-1 non_thm 36.0 30 2 1150 672 96 1763 0 1724 4 1535 2206 2399 [0.50] SYN842-1 timeout 299.0 56 [0.50] SYN852-1 timeout 298.9 60 [0.50] SYN853-1 timeout 299.0 56 [0.50] SYN854-1 timeout 299.0 56 [0.50] SYN855-1 non_thm 256.1 48 3 1424 7184 104 1763 0 11653 5 2621 2747 18518 [0.56] SYN439-1 theorem 4.4 4 268 5487 299 6404 2033 0 24038 2 92 14706 247325 [0.56] SYN440-1 theorem 254.0 16 1470 19600 1966 24176 7221 0 5971066 2 126 41714112282455 [0.56] SYN850-1 theorem 10.8 22 2 696 183 72 939 0 781 4 795 1322 1105 [0.56] SYN861-1 theorem 25.3 22 7 696 1029 72 939 0 2196 5 1492 1327 3546 [0.56] SYN865-1 theorem 51.8 22 3 696 450 72 939 0 1050 5 1003 1323 1691 [0.56] SYN866-1 timeout 299.0 39 [0.57] NLP032-1 timeout 298.9 19 [0.57] NLP033-1 non_thm 0.0 4 0 6 8 17 4 0 7 3 9 6 10 [0.57] NLP061-1 non_thm 0.7 4 3 17 32 13 3 0 300 5 37 41 325 [0.57] NLP062-1 non_thm 0.2 4 3 16 32 13 3 0 199 5 35 35 222 [0.57] NLP063-1 non_thm 0.1 4 1 8 6 13 3 0 11 5 12 14 16 [0.57] NLP160-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP161-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP162-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP163-1 non_thm 0.0 4 0 50 15 108 5 0 128 4 38 50 115 [0.57] NLP164-1 non_thm 0.0 4 0 50 15 108 5 0 128 4 38 50 115 [0.57] NLP165-1 non_thm 0.0 4 0 50 15 108 5 0 128 4 38 50 115 [0.57] NLP166-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP167-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP168-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP169-1 non_thm 0.0 4 0 26 4 55 4 0 48 4 30 26 52 [0.57] NLP190-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP191-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP192-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP193-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP194-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP195-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP196-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP197-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP198-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] NLP199-1 non_thm 0.0 4 0 33 4 69 4 0 62 5 37 33 66 [0.57] SYN741-1 timeout 299.0 10 [0.57] SYN746-1 non_thm 0.0 4 0 1 1 1 0 0 5 2 2 1 6 [0.57] SYN747-1 timeout 299.0 5 [0.57] SYN750-1 non_thm 0.0 4 0 1 8 1 0 0 35 2 8 1 42 [0.57] SYN751-1 non_thm 0.1 4 0 1 61 1 0 0 1120 3 21 1 1118 [0.57] SYN753-1 non_thm 0.0 4 0 1 12 1 0 0 60 3 9 1 71 [0.57] SYN761-1 timeout 299.0 4 [0.57] SYN763-1 non_thm 0.2 4 31 1 209 1 0 0 3414 2 17 1 3799 [0.57] SYN766-1 non_thm 0.9 4 46 1 477 1 0 0 12536 3 24 1 13512 [0.57] SYN769-1 non_thm 0.0 4 0 2 1 2 0 0 16 3 3 2 17 [0.57] SYN775-1 timeout 299.0 20 [0.57] SYN780-1 non_thm 0.0 4 0 2 1 2 0 0 8 2 3 2 9 [0.57] SYN786-1 non_thm 0.1 4 0 2 4 2 0 0 322 3 6 2 326 [0.57] SYN787-1 non_thm 27.7 4 281 2 823 2 0 0 313546 4 62 2 401672 [0.57] SYN790-1 non_thm 0.1 4 8 2 60 2 0 0 1322 2 25 2 1615 [0.57] SYN791-1 non_thm 0.0 4 0 2 1 2 0 0 7 2 3 2 8 [0.57] SYN800-1 timeout 298.9 7 [0.57] SYN801-1 non_thm 2.8 4 31 2 136 2 0 0 38342 3 30 2 46996 [0.57] SYN903-1 timeout 298.9 22 [0.57] SYN904-1 timeout 299.0 22 [0.57] SYN905-1 timeout 299.0 22 [0.57] SYN907-1 timeout 298.9 22 [0.57] SYN908-1 timeout 299.0 22 [0.57] SYN909-1 timeout 299.0 23 [0.57] SYN910-1 timeout 299.0 27 [0.57] SYN912-1 timeout 298.9 36 [0.57] TOP010-1 timeout 299.0 29 [0.57] TOP011-1 timeout 298.9 22 [0.57] TOP014-1 timeout 299.0 24 [0.57] TOP016-1 timeout 299.0 28 [0.67] COM005-1 timeout 299.0 24 [0.67] FLD008-3 timeout 298.9 18 [0.67] FLD027-1 timeout 299.0 4 [0.67] FLD038-1 timeout 299.0 4 [0.67] FLD040-1 timeout 299.0 4 [0.67] FLD048-4 timeout 299.0 62 [0.67] FLD051-4 timeout 299.0 41 [0.67] FLD086-3 timeout 299.0 11 [0.67] FLD090-3 timeout 298.9 17 [0.67] GRP132-1.005 non_thm 0.1 4 0 147 8 25 0 0 484 4 155 1575 525 [0.67] PUZ034-1.004 timeout 299.0 13 [0.67] SYN067-2 theorem 29.2 6 887 7356 1025 9574 1494 0 297113 5 49 44702 1545998 [0.67] SYN067-3 theorem 8.8 4 412 4459 492 2193 564 0 114289 5 55 15424 508259 [0.67] SYN519-1 timeout 299.0 86 [0.67] SYN650-1 timeout 299.0 4 [0.67] SYN818-1 non_thm 43.2 31 0 1374 1165 125 1763 0 2393 4 1929 2669 3530 [0.67] SYN821-1 non_thm 26.8 19 0 696 215 88 899 0 826 5 911 1336 1041 [0.71] NLP027-1 non_thm 0.0 4 0 4 5 12 4 0 6 3 9 4 11 [0.71] NLP028-1 non_thm 0.0 4 0 5 5 13 4 0 7 4 10 5 12 [0.71] NLP029-1 non_thm 0.0 4 0 4 5 11 4 0 4 3 9 4 9 [0.71] NLP030-1 non_thm 0.0 4 0 7 10 20 5 0 11 3 10 7 14 [0.71] NLP034-1 non_thm 0.0 4 0 7 10 20 4 0 11 3 11 7 15 [0.71] NLP035-1 non_thm 0.0 4 0 7 63 19 4 1 30 3 26 7 70 [0.71] NLP060-1 non_thm 0.3 4 2 12 12 13 3 0 35 5 16 25 44 [0.71] NUM288-1 timeout 299.0 6 [0.71] SET781-1 timeout 299.0 50 [0.71] SYN764-1 non_thm 0.0 4 0 1 39 1 0 0 307 2 14 1 330 [0.71] SYN770-1 non_thm 0.0 4 0 2 1 2 0 0 13 2 3 2 14 [0.71] SYN777-1 non_thm 0.9 4 6 2 51 2 0 0 10028 3 29 2 11241 [0.71] SYN778-1 non_thm 1.9 4 8 2 154 2 0 0 26741 3 29 2 28504 [0.71] SYN781-1 non_thm 0.1 4 0 2 29 2 0 0 861 3 21 2 886 [0.71] SYN783-1 non_thm 0.1 4 1 2 21 2 0 0 641 3 20 2 780 [0.71] SYN793-1 non_thm 0.0 4 0 2 2 2 0 0 27 3 4 2 29 [0.71] SYN799-1 non_thm 211.4 6 895 2 2733 2 0 0 1859061 5 125 2 2296499 [0.71] SYN808-1 timeout 298.9 13 [0.71] SYN810-1 timeout 299.0 22 [0.71] SYN906-1 timeout 299.0 22 [0.71] SYN913-1 timeout 299.0 32 [0.71] TOP001-1 timeout 298.9 22 [0.71] TOP002-1 timeout 299.0 22 [0.71] TOP003-1 timeout 299.0 22 [0.71] TOP006-1 timeout 299.0 22 [0.71] TOP015-1 timeout 299.0 28 [0.71] TOP018-1 timeout 298.9 22 [0.71] TOP019-1 timeout 299.0 26 [0.83] FLD012-3 timeout 298.9 11 [0.83] FLD014-1 timeout 299.0 4 [0.83] FLD028-1 timeout 299.0 4 [0.83] FLD035-1 timeout 298.9 4 [0.83] FLD036-1 timeout 299.0 4 [0.83] FLD041-1 timeout 299.0 4 [0.83] FLD044-4 timeout 298.9 16 [0.83] FLD045-4 timeout 299.0 16 [0.83] FLD062-1 timeout 299.0 4 [0.83] FLD072-3 timeout 298.9 18 [0.83] FLD072-4 timeout 299.0 11 [0.83] FLD074-3 timeout 298.9 18 [0.83] FLD087-3 timeout 299.0 11 [0.83] FLD088-3 timeout 298.9 11 [0.83] FLD089-3 timeout 299.0 11 [0.83] FLD097-4 timeout 299.0 16 [0.83] SYN314-1.002.001 timeout 299.0 74 [0.83] SYN822-1 timeout 299.0 62 [0.86] GRP025-3 timeout 299.0 13 [0.86] GRP026-3 timeout 299.0 27 [0.86] GRP027-2 timeout 298.9 5 [0.86] PUZ034-1.003 timeout 299.0 13 [0.86] SYN765-1 non_thm 4.0 4 163 1 768 1 0 0 37587 4 30 1 44503 [0.86] SYN767-1 non_thm 0.0 4 0 1 6 1 0 0 23 3 7 1 29 [0.86] SYN771-1 non_thm 0.0 4 0 2 1 2 0 0 27 3 3 2 28 [0.86] SYN773-1 non_thm 0.0 4 0 2 1 2 0 0 9 2 3 2 10 [0.86] SYN776-1 non_thm 0.1 4 0 2 2 2 0 0 122 3 4 2 124 [0.86] SYN779-1 non_thm 4.5 4 18 2 98 2 0 0 28816 4 60 2 31630 [0.86] SYN782-1 non_thm 0.9 4 1 2 81 2 0 0 5018 4 46 2 5113 [0.86] SYN788-1 timeout 299.0 11 [0.86] SYN789-1 timeout 299.0 7 [0.86] SYN792-1 timeout 299.0 14 [0.86] SYN795-1 non_thm 3.2 4 47 2 495 2 0 0 44817 3 55 2 49733 [0.86] SYN803-1 non_thm 0.0 4 0 2 1 2 0 0 10 2 3 2 11 [0.86] SYN805-1 non_thm 79.1 17 4545 2 17248 2 0 0 1467963 3 58 2 1791844 [0.86] SYN806-1 non_thm 2.2 4 22 2 277 2 0 0 29840 3 57 2 33112 [0.86] SYN807-1 non_thm 0.1 4 0 2 5 2 0 0 227 3 7 2 232 [0.86] SYN809-1 timeout 299.0 23 [0.86] SYN911-1 timeout 299.0 26 [0.86] TOP005-1 timeout 298.9 22 [0.86] TOP007-1 timeout 299.0 22 [0.86] TOP008-1 timeout 298.9 25 [0.86] TOP009-1 timeout 299.0 22 [0.86] TOP012-1 timeout 299.0 22 [0.86] TOP013-1 timeout 299.0 27 [0.86] TOP017-1 timeout 299.0 23 [1.00] ANA001-1 timeout 299.0 14 [1.00] ANA005-4 timeout 298.9 18 [1.00] ANA005-5 timeout 299.0 12 [1.00] COM006-1 timeout 299.0 27 [1.00] FLD008-1 timeout 299.0 4 [1.00] FLD008-2 timeout 299.0 4 [1.00] FLD011-1 timeout 299.0 4 [1.00] FLD012-1 timeout 298.9 4 [1.00] FLD012-2 timeout 299.0 4 [1.00] FLD026-1 timeout 299.0 4 [1.00] FLD029-1 timeout 299.0 4 [1.00] FLD041-2 timeout 299.0 4 [1.00] FLD043-1 timeout 299.0 4 [1.00] FLD044-1 timeout 299.0 4 [1.00] FLD044-2 timeout 299.0 4 [1.00] FLD044-3 timeout 299.0 19 [1.00] FLD045-1 timeout 299.0 4 [1.00] FLD045-2 timeout 299.0 4 [1.00] FLD045-3 timeout 299.0 18 [1.00] FLD046-1 timeout 299.0 4 [1.00] FLD046-3 timeout 299.0 10 [1.00] FLD047-1 timeout 299.0 4 [1.00] FLD047-2 timeout 299.0 4 [1.00] FLD047-3 timeout 299.0 10 [1.00] FLD048-1 timeout 299.0 4 [1.00] FLD048-2 timeout 299.0 4 [1.00] FLD048-3 timeout 299.0 10 [1.00] FLD049-1 timeout 299.0 4 [1.00] FLD049-2 timeout 299.0 4 [1.00] FLD050-1 timeout 299.0 4 [1.00] FLD050-2 timeout 299.0 4 [1.00] FLD051-1 timeout 299.0 4 [1.00] FLD051-2 timeout 299.0 4 [1.00] FLD051-3 timeout 299.0 11 [1.00] FLD052-1 timeout 299.0 4 [1.00] FLD052-2 timeout 298.9 4 [1.00] FLD052-3 timeout 299.0 9 [1.00] FLD053-1 timeout 298.9 4 [1.00] FLD053-2 timeout 299.0 4 [1.00] FLD053-3 timeout 299.0 10 [1.00] FLD053-4 timeout 299.0 42 [1.00] FLD054-1 timeout 299.0 4 [1.00] FLD054-2 timeout 299.0 4 [1.00] FLD054-3 timeout 299.0 11 [1.00] FLD057-1 timeout 298.9 4 [1.00] FLD072-1 timeout 298.9 4 [1.00] FLD072-2 timeout 299.0 4 [1.00] FLD073-1 timeout 299.0 4 [1.00] FLD073-2 timeout 298.9 4 [1.00] FLD073-3 timeout 299.0 22 [1.00] FLD073-4 timeout 299.0 11 [1.00] FLD074-1 timeout 299.0 4 [1.00] FLD074-2 timeout 299.0 4 [1.00] FLD074-4 timeout 299.0 12 [1.00] FLD075-1 timeout 298.9 4 [1.00] FLD075-2 timeout 299.0 4 [1.00] FLD075-3 timeout 298.9 18 [1.00] FLD075-4 timeout 299.0 12 [1.00] FLD076-1 timeout 298.9 4 [1.00] FLD076-2 timeout 299.0 4 [1.00] FLD076-3 timeout 299.0 11 [1.00] FLD076-4 timeout 298.9 11 [1.00] FLD077-1 timeout 299.0 4 [1.00] FLD077-2 timeout 299.0 4 [1.00] FLD077-3 timeout 299.0 12 [1.00] FLD077-4 timeout 299.0 10 [1.00] FLD078-1 timeout 299.0 4 [1.00] FLD078-2 timeout 298.9 4 [1.00] FLD078-3 timeout 299.0 18 [1.00] FLD078-4 timeout 298.9 10 [1.00] FLD079-1 timeout 299.0 4 [1.00] FLD079-2 timeout 299.0 4 [1.00] FLD079-3 timeout 299.0 11 [1.00] FLD079-4 timeout 299.0 12 [1.00] FLD080-1 timeout 299.0 4 [1.00] FLD080-2 timeout 299.0 4 [1.00] FLD080-3 timeout 299.0 14 [1.00] FLD080-4 timeout 298.9 11 [1.00] FLD081-1 timeout 299.0 4 [1.00] FLD081-2 timeout 299.0 4 [1.00] FLD081-3 timeout 298.9 28 [1.00] FLD081-4 timeout 299.0 11 [1.00] FLD082-1 timeout 299.0 4 [1.00] FLD082-3 timeout 299.0 11 [1.00] FLD083-1 timeout 299.0 4 [1.00] FLD083-3 timeout 298.9 11 [1.00] FLD084-1 timeout 299.0 4 [1.00] FLD084-3 timeout 299.0 11 [1.00] FLD085-1 timeout 299.0 4 [1.00] FLD085-3 timeout 298.9 11 [1.00] FLD086-1 timeout 299.0 4 [1.00] FLD087-1 timeout 298.9 4 [1.00] FLD088-1 timeout 299.0 4 [1.00] FLD089-1 timeout 299.0 4 [1.00] FLD090-1 timeout 299.0 4 [1.00] FLD091-1 timeout 299.0 4 [1.00] FLD091-3 timeout 299.0 10 [1.00] FLD092-1 timeout 298.9 4 [1.00] FLD092-3 timeout 299.0 10 [1.00] FLD093-1 timeout 299.0 4 [1.00] FLD093-3 timeout 298.9 10 [1.00] FLD094-1 timeout 299.0 4 [1.00] FLD094-3 timeout 299.0 10 [1.00] FLD095-1 timeout 299.0 4 [1.00] FLD095-2 timeout 299.0 4 [1.00] FLD095-3 timeout 298.9 10 [1.00] FLD095-4 timeout 299.0 22 [1.00] FLD096-1 timeout 298.9 4 [1.00] FLD096-2 timeout 299.0 4 [1.00] FLD096-3 timeout 298.9 10 [1.00] FLD096-4 timeout 299.0 20 [1.00] FLD097-1 timeout 298.9 4 [1.00] FLD097-2 timeout 299.0 4 [1.00] FLD097-3 timeout 299.0 19 [1.00] FLD098-1 timeout 298.9 4 [1.00] FLD098-2 timeout 299.0 3 [1.00] FLD098-3 timeout 299.0 19 [1.00] FLD098-4 timeout 299.0 23 [1.00] FLD099-1 timeout 299.0 4 [1.00] FLD099-2 timeout 299.0 4 [1.00] FLD099-3 timeout 299.0 15 [1.00] FLD099-4 timeout 298.9 15 [1.00] FLD100-1 timeout 299.0 4 [1.00] FLD100-2 timeout 298.9 4 [1.00] FLD100-3 timeout 299.0 19 [1.00] FLD100-4 timeout 299.0 17 [1.00] MSC008-1.010 timeout 298.9 4