-------------------------------------------------------------------------------- Execute format string : ./darwin --restart Eager Problems list file : nne_eager-problems Output file : nne_eager-output Summary file : nne_eager-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.0 4 1 45 0 4 0 0 0 3 45 280 2 [0.00] CAT007-3 theorem 0.0 4 1 5 0 5 0 0 0 2 5 12 2 [0.00] COM002-2 theorem 0.0 4 1 26 0 15 0 0 0 2 26 47 0 [0.00] COM003-2 theorem 0.0 4 1 12 0 22 13 1 0 2 12 24 1 [0.00] FLD006-1 theorem 17.9 4 1 154 0 4 0 0 0 3 154 1362 0 [0.00] FLD006-3 theorem 0.0 4 1 5 0 4 0 0 0 2 5 31 0 [0.00] FLD010-1 theorem 22.2 4 1 168 0 4 0 0 0 3 168 1395 0 [0.00] FLD010-3 theorem 0.0 4 1 6 0 5 0 0 0 2 6 35 0 [0.00] FLD018-3 theorem 0.1 4 1 73 0 6 0 0 0 2 73 1562 0 [0.00] FLD019-3 theorem 0.0 4 1 14 0 6 0 0 0 2 14 96 0 [0.00] FLD020-3 theorem 0.0 4 1 83 0 7 0 0 0 2 83 518 0 [0.00] FLD021-3 theorem 0.0 4 1 14 0 7 0 0 0 2 14 104 0 [0.00] FLD033-3 theorem 0.0 4 1 126 0 8 0 0 0 2 126 1084 0 [0.00] FLD034-3 theorem 0.0 4 1 18 0 7 0 0 0 2 18 120 0 [0.00] FLD039-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 65 0 [0.00] FLD039-3 theorem 0.0 4 1 15 0 6 0 0 0 2 15 81 0 [0.00] FLD055-1 theorem 0.0 4 1 27 0 9 0 0 0 2 27 278 0 [0.00] FLD056-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 57 0 [0.00] FLD056-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 57 0 [0.00] FLD058-1 theorem 0.0 4 1 25 0 9 0 0 0 2 25 213 0 [0.00] FLD071-3 theorem 0.0 4 1 9 0 8 0 0 0 2 9 98 0 [0.00] FLD071-4 theorem 0.0 4 1 9 0 9 0 0 0 2 9 141 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 2 31 87 0 [0.00] GRP123-2.003 theorem 0.0 4 1 37 0 15 0 0 0 2 37 94 0 [0.00] GRP123-3.003 theorem 0.0 4 1 51 0 20 0 0 0 2 51 111 0 [0.00] GRP123-4.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 105 0 [0.00] GRP123-6.003 theorem 0.0 4 1 50 0 11 0 0 0 2 50 143 0 [0.00] GRP123-7.003 theorem 0.0 4 1 56 0 16 0 0 0 2 56 149 0 [0.00] GRP123-8.003 theorem 0.0 4 1 62 0 21 0 0 0 2 62 156 0 [0.00] GRP123-9.003 theorem 0.0 4 1 50 0 11 0 0 0 2 50 143 0 [0.00] GRP124-1.004 theorem 0.0 4 2 72 1 17 0 0 37 2 64 392 155 [0.00] GRP124-2.004 theorem 0.0 4 1 75 0 26 0 0 0 2 75 182 0 [0.00] GRP124-3.004 theorem 0.0 4 2 117 1 32 0 0 48 2 106 337 171 [0.00] GRP124-4.004 theorem 0.0 4 2 66 1 17 0 0 101 2 62 293 350 [0.00] GRP124-6.004 theorem 0.0 4 2 109 1 18 0 0 71 2 101 424 234 [0.00] GRP124-7.004 theorem 0.0 4 2 121 1 27 0 0 71 2 113 436 234 [0.00] GRP124-8.004 theorem 0.0 4 2 148 2 33 0 0 90 2 141 490 259 [0.00] GRP124-9.004 theorem 0.0 4 2 109 1 18 0 0 71 2 101 424 266 [0.00] GRP125-1.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 94 0 [0.00] GRP125-2.005 theorem 0.0 4 3 184 2 40 0 0 137 2 157 800 479 [0.00] GRP125-3.005 theorem 0.1 4 5 280 4 47 0 0 232 2 219 1294 748 [0.00] GRP125-4.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 146 0 [0.00] GRP126-1.004 theorem 0.0 4 2 69 1 17 0 0 36 2 63 316 141 [0.00] GRP126-2.004 theorem 0.0 4 1 75 0 26 0 0 0 2 75 224 0 [0.00] GRP126-3.004 theorem 0.0 4 2 117 1 32 0 0 47 2 106 371 171 [0.00] GRP126-4.004 theorem 0.0 4 2 67 1 17 0 0 102 2 63 403 367 [0.00] GRP127-1.004 theorem 0.0 4 2 72 1 17 0 0 36 2 64 352 151 [0.00] GRP127-2.006 theorem 0.1 4 3 313 2 57 0 0 251 2 253 1328 1321 [0.00] GRP127-3.004 theorem 0.0 4 2 117 1 32 0 0 47 2 106 347 170 [0.00] GRP127-4.004 theorem 0.0 4 2 68 1 17 0 0 102 2 63 429 368 [0.00] GRP128-1.003 theorem 0.0 4 4 59 3 9 0 0 7 2 32 200 90 [0.00] GRP128-4.003 theorem 0.0 4 4 28 3 9 0 0 15 2 28 193 108 [0.00] GRP129-1.003 theorem 0.0 4 4 59 3 9 0 0 7 2 29 238 92 [0.00] GRP129-2.004 theorem 0.0 4 7 164 7 25 0 0 69 2 78 599 258 [0.00] GRP129-3.004 theorem 0.0 4 7 236 7 31 0 0 165 2 115 783 344 [0.00] GRP129-4.004 theorem 0.0 4 9 116 8 16 0 0 94 2 51 665 526 [0.00] GRP130-1.003 theorem 0.0 4 4 71 3 9 0 0 7 2 36 316 123 [0.00] GRP130-2.003 theorem 0.0 4 3 68 2 14 0 0 6 2 43 282 104 [0.00] GRP130-3.003 theorem 0.0 4 2 94 1 19 0 0 2 2 68 289 108 [0.00] GRP130-4.003 theorem 0.0 4 4 43 3 9 0 0 15 2 25 177 143 [0.00] GRP131-1.002 theorem 0.0 4 2 20 1 4 0 0 0 2 14 81 32 [0.00] GRP131-2.002 theorem 0.0 4 2 22 1 6 0 0 0 2 16 84 32 [0.00] GRP132-1.002 theorem 0.0 4 2 20 1 4 0 0 0 2 14 81 32 [0.00] GRP132-2.002 theorem 0.0 4 2 22 1 6 0 0 0 2 16 84 32 [0.00] GRP133-1.003 theorem 0.0 4 4 80 3 9 0 0 7 2 33 340 139 [0.00] GRP133-2.003 theorem 0.0 4 3 69 2 14 0 0 6 2 43 251 97 [0.00] GRP134-1.003 theorem 0.0 4 4 92 3 9 0 0 7 2 34 434 169 [0.00] GRP134-2.003 theorem 0.0 4 3 86 2 14 0 0 6 2 44 352 127 [0.00] GRP135-1.002 theorem 0.0 4 2 19 1 4 0 0 0 2 14 61 25 [0.00] GRP135-2.002 theorem 0.0 4 2 21 1 6 0 0 0 2 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 96 0 10 0 0 0 3 96 323 0 [0.00] HWV005-2 theorem 0.0 4 1 96 0 8 0 0 0 3 96 296 0 [0.00] HWV006-1 theorem 0.1 4 1 356 0 15 1 4 0 4 356 1440 0 [0.00] HWV006-2 theorem 0.1 4 1 360 0 13 1 0 0 4 360 1354 0 [0.00] HWV007-1 theorem 0.1 4 1 352 0 13 1 6 0 4 352 941 0 [0.00] HWV007-2 theorem 0.1 4 1 364 0 11 1 0 0 4 364 898 0 [0.00] KRS001-1 theorem 0.0 4 1 8 0 1 0 0 0 2 8 16 2 [0.00] KRS002-1 theorem 0.0 4 1 9 0 1 0 0 0 3 9 16 2 [0.00] KRS003-1 theorem 0.0 4 1 9 0 2 0 0 0 2 9 16 2 [0.00] KRS010-1 theorem 0.0 4 2 21 1 2 0 0 77 2 18 38 95 [0.00] KRS012-1 theorem 0.0 4 1 5 0 2 0 0 0 2 5 10 3 [0.00] KRS013-1 theorem 0.0 4 1 17 0 2 0 0 0 3 17 27 7 [0.00] KRS015-1 theorem 0.0 4 1 10 0 1 0 0 0 3 10 18 2 [0.00] KRS017-1 theorem 0.0 4 1 3 0 2 0 0 0 2 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 2 15 26 0 [0.00] MGT007-1 theorem 0.0 4 1 17 0 9 0 0 0 2 17 28 0 [0.00] MGT016-1 theorem 0.0 4 1 16 0 13 0 0 0 2 16 26 0 [0.00] MGT018-1 theorem 0.0 4 1 16 0 13 0 0 0 2 16 26 0 [0.00] MGT022-1 theorem 0.0 4 2 8 1 11 3 0 0 3 7 19 6 [0.00] MGT022-2 theorem 0.0 4 2 8 1 11 3 0 0 3 7 19 6 [0.00] MGT028-1 theorem 0.0 4 2 13 1 2 0 0 1 4 11 27 15 [0.00] MGT030-1 theorem 0.0 4 6 23 8 2 0 0 4 4 14 80 45 [0.00] MGT036-1 theorem 0.0 4 1 9 0 4 0 0 0 2 9 15 0 [0.00] MGT036-2 theorem 0.0 4 1 9 0 4 0 0 0 2 9 16 0 [0.00] MGT041-2 theorem 0.0 4 1 7 0 4 0 0 0 2 7 9 0 [0.00] MSC001-1 theorem 0.0 4 1 65 0 5 1 2 0 5 65 235 0 [0.00] MSC002-1 theorem 0.0 4 1 22 0 3 1 0 0 4 22 42 0 [0.00] MSC002-2 theorem 0.0 4 1 22 0 3 1 0 0 4 22 42 0 [0.00] MSC003-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 9 0 [0.00] MSC004-1 theorem 0.0 4 6 20 11 2 0 0 4 3 14 38 49 [0.00] MSC006-1 theorem 0.0 4 6 47 22 2 0 0 228 2 30 193 537 [0.00] MSC008-1.002 theorem 0.2 4 32 155 53 2 0 0 2806 2 23 1364 9005 [0.00] MSC008-2.002 theorem 0.2 4 32 155 53 2 0 0 3238 2 23 1188 7397 [0.00] NLP114-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 [0.00] NLP115-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 [0.00] NLP116-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 [0.00] NLP117-1 theorem 0.0 4 2 34 1 66 5 0 0 2 19 38 48 [0.00] NLP118-1 non_thm 0.0 4 1 34 1 67 4 0 32 2 19 36 48 [0.00] NLP119-1 non_thm 0.0 4 1 34 1 67 4 0 32 2 19 36 48 [0.00] NLP120-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 [0.00] NLP121-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 [0.00] NLP122-1 theorem 0.0 4 2 34 1 66 5 0 0 2 19 38 48 [0.00] NLP123-1 non_thm 0.0 4 0 18 1 35 2 0 31 2 19 18 32 [0.00] NUM014-1 theorem 0.0 4 1 5 0 4 0 0 0 2 5 11 0 [0.00] NUM015-1 theorem 0.0 4 1 11 0 2 0 0 0 3 11 21 3 [0.00] NUM016-1 theorem 0.0 4 1 14 0 4 0 0 0 3 14 36 3 [0.00] NUM016-2 theorem 0.0 4 1 12 0 2 0 0 0 3 12 18 3 [0.00] NUM021-1 theorem 0.0 4 1 80 0 9 0 0 0 3 80 405 0 [0.00] NUM022-1 theorem 0.0 4 1 9 0 3 0 0 0 3 9 14 0 [0.00] NUM025-2 theorem 0.0 4 1 4 0 4 0 0 0 2 4 17 1 [0.00] NUM027-1 theorem 0.0 4 1 49 0 10 0 0 0 2 49 247 1 [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 1 7 0 12 8 0 0 2 7 10 1 [0.00] PLA002-2 theorem 1.3 4 1 1994 0 2 0 0 0 5 1994 2625 0 [0.00] PUZ001-1 theorem 0.0 4 1 17 0 5 2 0 0 2 17 20 1 [0.00] PUZ001-3 non_thm 0.0 4 0 19 0 6 2 0 9 2 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.0 4 2 26 1 3 0 0 0 2 21 83 164 [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 2 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 2 116 333 3 [0.00] PUZ021-1 theorem 0.1 4 13 195 66 0 0 6 344 3 55 877 3786 [0.00] PUZ023-1 theorem 0.0 4 2 10 2 10 6 0 4 2 11 30 16 [0.00] PUZ024-1 theorem 0.0 4 1 7 0 13 7 0 0 2 7 19 1 [0.00] PUZ025-1 theorem 0.0 4 8 37 9 7 4 0 46 2 22 223 180 [0.00] PUZ026-1 theorem 0.0 4 3 29 2 18 5 3 10 2 18 99 61 [0.00] PUZ027-1 theorem 0.0 4 3 18 2 27 14 0 1 2 12 73 40 [0.00] PUZ028-1 non_thm 0.0 4 0 31 15 11 0 0 20 2 46 91 35 [0.00] PUZ028-2 non_thm 0.0 4 0 70 18 36 0 0 28 2 88 190 46 [0.00] PUZ028-3 non_thm 0.0 4 0 70 18 432 154 0 24 2 88 114 42 [0.00] PUZ028-4 non_thm 0.0 4 0 28 18 222 106 0 24 2 46 60 42 [0.00] PUZ028-5 theorem 0.1 4 30 742 29 11 0 0 173 2 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 33 0 6 0 0 0 2 33 56 0 [0.00] PUZ032-1 theorem 0.0 4 2 16 1 4 0 0 8 3 16 54 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 15 3 21 17 0 2 2 8 40 14 [0.00] PUZ035-2 theorem 0.0 4 4 21 3 21 17 0 2 2 10 52 24 [0.00] PUZ035-5 theorem 0.0 4 4 7 4 5 0 0 0 2 6 27 20 [0.00] PUZ035-6 theorem 0.0 4 4 5 4 5 0 0 5 2 6 20 31 [0.00] SET001-1 theorem 0.0 4 1 4 0 3 0 0 0 2 4 8 1 [0.00] SET002-1 theorem 0.0 4 3 9 3 2 0 0 0 2 8 21 22 [0.00] SET003-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 9 2 [0.00] SET004-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 8 2 [0.00] SET006-1 theorem 0.0 4 1 6 0 2 0 0 0 2 6 10 3 [0.00] SET008-1 theorem 0.0 4 1 10 0 3 0 0 0 2 10 34 4 [0.00] SET009-1 theorem 0.0 4 1 22 0 4 0 0 0 2 22 41 2 [0.00] SET011-1 theorem 0.0 4 2 73 1 3 0 0 0 2 67 239 94 [0.00] SET043-5 theorem 0.0 4 4 0 3 0 0 0 0 2 2 8 9 [0.00] SET044-5 theorem 0.0 4 8 8 13 0 0 0 18 2 6 32 79 [0.00] SET045-5 theorem 0.0 4 6 2 6 1 0 0 7 2 6 15 34 [0.00] SET046-5 theorem 0.0 4 4 4 3 0 0 0 0 2 4 18 19 [0.00] SET047-5 theorem 0.0 4 4 6 3 4 4 0 2 2 4 24 15 [0.00] SET055-7 theorem 0.0 4 1 5 0 5 0 0 0 2 5 47 3 [0.00] SET786-1 theorem 0.0 4 4 4 3 0 0 0 0 2 4 16 18 [0.00] SWV001-1 theorem 0.0 4 2 10 1 2 0 0 5 2 9 39 21 [0.00] SWV009-1 theorem 0.0 4 1 9 0 5 0 0 0 2 9 12 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 3 6 7 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 18 0 [0.00] SYN009-2 theorem 0.0 4 1 7 0 4 0 0 0 2 7 9 0 [0.00] SYN009-3 theorem 0.0 4 1 9 0 5 1 0 0 2 9 11 0 [0.00] SYN009-4 theorem 0.0 4 1 8 0 4 0 0 0 2 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.0 4 9 0 37 0 0 0 119 5 16 0 182 [0.00] SYN014-2 theorem 0.0 4 1 8 0 7 0 0 0 2 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 2 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 2 4 16 18 [0.00] SYN038-1 theorem 0.0 4 9 0 37 0 0 0 119 5 16 0 182 [0.00] SYN039-1 theorem 0.0 4 7 4 17 18 0 0 129 4 11 22 236 [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 3 1 6 6 1 0 2 3 7 4 [0.00] SYN052-1 theorem 0.0 4 2 2 1 6 5 0 0 2 2 7 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 6 1 [0.00] SYN069-1 theorem 0.0 4 1 9 0 1 0 0 0 2 9 16 0 [0.00] SYN070-1 theorem 0.0 4 1 15 0 4 0 0 0 2 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 3 3 18 11 [0.00] SYN084-2 theorem 0.0 4 4 17 4 17 19 0 4 3 9 29 39 [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.1 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 5 3 0 0 2 2 7 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 2 2 7 3 [0.00] SYN323-1 theorem 0.0 4 3 2 3 0 0 0 0 2 3 6 7 [0.00] SYN325-1 theorem 0.0 4 1 2 0 1 1 0 0 2 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 2 4 22 25 [0.00] SYN328-1 theorem 0.0 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 4 6 15 1 [0.00] SYN332-1 theorem 0.7 4 3 0 98 0 0 0 2430 5 96 0 2739 [0.00] SYN334-1 theorem 0.0 4 9 0 37 0 0 0 119 5 16 0 182 [0.00] SYN343-1 theorem 0.0 4 2 1 1 4 2 0 0 2 2 5 2 [0.00] SYN345-1 theorem 0.0 4 4 6 3 28 14 0 0 2 4 19 12 [0.00] SYN347-1 theorem 0.0 4 12 10 14 8 4 0 23 2 8 64 82 [0.00] SYN349-1 theorem 0.0 4 17 0 29 0 0 0 135 3 9 0 373 [0.00] SYN350-1 theorem 0.0 4 8 6 9 0 0 0 34 3 8 36 98 [0.00] SYN352-1 theorem 0.0 4 4 5 7 1 0 0 48 3 11 8 85 [0.00] SYN354-1 theorem 0.0 4 3 2 2 2 0 0 0 2 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 7 11 54 22 0 24 2 18 7 35 [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 1 15 7 70 24 0 26 2 18 19 38 [0.00] SYN521-1 non_thm 0.0 4 0 16 11 89 16 0 51 2 27 16 62 [0.00] SYN522-1 non_thm 0.0 4 0 13 17 69 29 0 55 2 30 13 72 [0.00] SYN523-1 non_thm 0.0 4 0 2 10 33 13 0 15 2 12 2 25 [0.00] SYN524-1 non_thm 0.0 4 0 10 10 68 25 0 29 2 20 10 39 [0.00] SYN525-1 non_thm 0.0 4 0 8 14 89 27 0 28 2 22 8 42 [0.00] SYN526-1 non_thm 0.0 4 0 9 10 64 28 0 25 2 19 9 35 [0.00] SYN527-1 non_thm 0.0 4 0 12 9 70 24 0 20 2 21 12 29 [0.00] SYN528-1 non_thm 0.0 4 0 6 14 84 21 0 28 2 20 6 42 [0.00] SYN529-1 non_thm 0.0 4 0 24 16 121 33 0 82 2 40 24 98 [0.00] SYN530-1 non_thm 0.0 4 0 7 12 70 20 0 29 2 19 7 41 [0.00] SYN531-1 non_thm 0.0 4 0 16 18 55 28 0 42 2 34 16 61 [0.00] SYN532-1 non_thm 0.0 4 0 20 11 88 34 0 45 2 31 20 56 [0.00] SYN533-1 non_thm 0.0 4 0 13 12 93 20 0 32 2 25 13 44 [0.00] SYN534-1 non_thm 0.0 4 0 12 10 73 26 0 18 2 22 12 28 [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 9 74 25 0 32 2 24 15 41 [0.00] SYN537-1 non_thm 0.0 4 0 28 11 84 36 0 57 2 39 29 68 [0.00] SYN554-1 theorem 0.0 4 1 10 0 4 0 0 0 2 10 43 1 [0.00] SYN560-1 theorem 0.6 4 1 39 0 6 0 0 0 5 39 1011 1 [0.00] SYN567-1 theorem 0.0 4 1 8 0 7 0 0 0 4 8 25 0 [0.00] SYN568-1 theorem 0.0 4 1 8 0 6 0 0 0 5 8 29 1 [0.00] SYN571-1 theorem 0.0 4 1 23 0 6 0 0 0 3 23 74 1 [0.00] SYN573-1 theorem 0.0 4 1 8 0 5 0 0 0 2 8 23 0 [0.00] SYN574-1 theorem 0.0 4 2 18 1 8 0 0 28 3 17 63 36 [0.00] SYN575-1 theorem 0.0 4 2 18 1 8 0 0 28 3 17 63 36 [0.00] SYN578-1 theorem 0.0 4 2 54 1 9 0 0 258 3 53 298 269 [0.00] SYN579-1 theorem 0.0 4 2 54 1 9 0 0 258 3 53 298 269 [0.00] SYN580-1 theorem 0.0 4 1 21 0 8 0 0 0 2 21 65 0 [0.00] SYN581-1 theorem 0.0 4 1 34 0 9 0 0 0 3 34 205 0 [0.00] SYN582-1 theorem 0.0 4 1 28 0 9 0 0 0 3 28 157 0 [0.00] SYN583-1 theorem 0.0 4 1 27 0 9 0 0 0 3 27 236 0 [0.00] SYN585-1 timeout 299.0 38 [0.00] SYN586-1 theorem 0.0 4 1 42 0 9 0 0 0 3 42 205 1 [0.00] SYN587-1 theorem 0.0 4 1 23 0 9 0 0 0 2 23 78 1 [0.00] SYN591-1 theorem 0.0 4 1 29 0 13 0 0 0 3 29 98 0 [0.00] SYN592-1 theorem 0.0 4 1 25 0 13 0 0 0 3 25 79 0 [0.00] SYN593-1 theorem 0.0 4 1 10 0 10 0 0 0 2 10 31 1 [0.00] SYN594-1 theorem 0.0 4 1 20 0 8 0 0 0 5 20 62 0 [0.00] SYN605-1 theorem 0.4 4 1 131 0 12 1 0 0 4 131 2980 0 [0.00] SYN608-1 theorem 0.5 4 1 153 0 12 1 0 0 4 153 3412 0 [0.00] SYN613-1 theorem 0.0 4 1 14 0 10 0 0 0 3 14 47 0 [0.00] SYN619-1 theorem 0.0 4 1 23 0 8 0 0 0 4 23 115 0 [0.00] SYN621-1 timeout 299.0 108 [0.00] SYN622-1 theorem 0.0 4 1 17 0 12 0 0 0 4 17 107 0 [0.00] SYN623-1 theorem 1.3 4 1 513 0 15 0 0 0 4 513 13804 0 [0.00] SYN624-1 theorem 133.8 14 1 30 0 14 0 0 0 6 30 198 0 [0.00] SYN626-1 theorem 0.0 4 1 24 0 10 0 0 0 5 24 83 0 [0.00] SYN627-1 theorem 0.2 4 1 36 0 10 0 0 0 3 36 215 1 [0.00] SYN656-1 theorem 0.0 4 1 38 0 18 0 0 0 5 38 120 1 [0.00] SYN660-1 theorem 0.1 4 1 91 0 23 0 0 0 3 91 466 0 [0.00] SYN661-1 theorem 0.0 4 1 82 0 23 0 0 0 3 82 434 0 [0.00] SYN662-1 theorem 0.0 4 1 59 0 23 0 0 0 3 59 214 0 [0.00] SYN663-1 theorem 0.0 4 1 50 0 23 0 0 0 3 50 184 0 [0.00] SYN664-1 theorem 0.1 4 1 91 0 23 0 0 0 3 91 466 0 [0.00] SYN665-1 theorem 0.0 4 1 82 0 23 0 0 0 3 82 434 0 [0.00] SYN666-1 theorem 0.0 4 1 61 0 23 0 0 0 3 61 249 0 [0.00] SYN667-1 theorem 0.0 4 1 56 0 23 0 0 0 3 56 235 0 [0.00] SYN668-1 theorem 0.0 4 1 61 0 23 0 0 0 3 61 249 0 [0.00] SYN669-1 theorem 0.0 4 1 56 0 23 0 0 0 3 56 235 0 [0.00] SYN670-1 theorem 0.0 4 1 33 0 23 0 0 0 3 33 85 0 [0.00] SYN671-1 theorem 0.0 4 1 28 0 23 0 0 0 3 28 73 0 [0.00] SYN672-1 theorem 0.0 4 1 30 0 22 0 0 0 4 30 90 0 [0.00] SYN673-1 theorem 9.8 6 1 558 0 19 0 0 0 6 558 14487 0 [0.00] SYN674-1 theorem 0.1 4 1 92 0 24 0 0 0 3 92 467 0 [0.00] SYN675-1 theorem 0.0 4 1 83 0 24 0 0 0 3 83 435 0 [0.00] SYN676-1 theorem 0.0 4 1 60 0 24 0 0 0 3 60 215 0 [0.00] SYN677-1 theorem 0.0 4 1 51 0 24 0 0 0 3 51 185 0 [0.00] SYN678-1 theorem 0.1 4 1 92 0 24 0 0 0 3 92 467 0 [0.00] SYN679-1 theorem 0.0 4 1 83 0 24 0 0 0 3 83 435 0 [0.00] SYN680-1 theorem 0.1 4 1 92 0 24 0 0 0 3 92 467 0 [0.00] SYN681-1 theorem 0.1 4 1 83 0 24 0 0 0 3 83 435 0 [0.00] SYN682-1 theorem 0.0 4 1 92 0 24 0 0 0 3 92 467 0 [0.00] SYN683-1 theorem 0.0 4 1 83 0 24 0 0 0 3 83 435 0 [0.00] SYN684-1 theorem 0.0 4 1 60 0 24 0 0 0 3 60 215 0 [0.00] SYN685-1 theorem 0.0 4 1 51 0 24 0 0 0 3 51 185 0 [0.00] SYN686-1 theorem 0.2 4 1 64 0 22 0 0 0 4 64 521 0 [0.00] SYN710-1 theorem 0.0 4 1 53 0 26 0 0 0 4 53 154 1 [0.00] SYN713-1 theorem 0.0 4 1 60 0 40 0 0 0 4 60 200 0 [0.00] SYN717-1 theorem 0.0 4 1 50 0 46 0 0 0 2 50 131 0 [0.00] SYN718-1 theorem 1.1 4 1 144 0 43 0 0 0 4 144 672 0 [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 228 2 30 193 537 [0.00] SYN728-1 theorem 0.0 4 3 3 6 3 3 0 1 5 6 9 11 [0.00] SYN811-1 non_thm 1.1 4 0 376 84 64 489 0 400 2 460 712 484 [0.00] SYN823-1 non_thm 0.3 19 0 160 86 32 249 0 205 2 246 288 291 [0.00] SYN824-1 non_thm 2.9 19 0 515 126 65 896 0 573 2 641 965 699 [0.00] SYN827-1 non_thm 0.6 19 0 188 138 36 269 0 443 2 326 340 581 [0.00] SYN867-1 non_thm 0.1 22 0 48 11 48 458 0 1 2 59 48 12 [0.00] SYN868-1 non_thm 0.1 22 0 45 6 45 433 0 2 2 51 45 8 [0.00] SYN870-1 non_thm 0.1 22 3 36 14 36 262 0 30 2 47 39 63 [0.00] SYN872-1 non_thm 0.5 22 0 94 4 94 1717 0 0 2 98 94 4 [0.00] SYN888-1 non_thm 0.8 22 0 102 10 102 1760 0 13 2 112 102 23 [0.00] SYN902-1 non_thm 2.0 22 4 102 90 102 1757 0 200 2 189 106 329 [0.00] TOP001-2 theorem 0.0 22 1 34 0 3 0 0 0 6 34 65 1 [0.00] TOP002-2 theorem 0.0 22 1 2 0 2 0 0 0 2 2 4 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 2 204 20149 27734 [0.11] PUZ017-1 theorem 0.1 4 5 302 4 85 1 5 723 2 231 1159 1598 [0.11] PUZ018-1 theorem 0.0 4 1 53 0 41 6 0 0 2 53 84 2 [0.11] PUZ028-6 theorem 0.1 4 20 376 19 36 0 0 137 2 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 4 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.8 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 0.5 20 2 188 133 36 269 0 274 2 272 342 526 [0.11] SYN869-1 theorem 0.0 22 2 36 5 36 266 0 0 2 40 38 34 [0.11] SYN871-1 theorem 0.2 22 15 36 82 36 256 0 254 2 58 51 441 [0.11] SYN873-1 theorem 0.2 22 13 36 65 36 269 0 62 2 52 49 225 [0.11] SYN874-1 theorem 0.1 22 4 36 22 36 269 0 22 2 48 40 84 [0.11] SYN875-1 theorem 0.1 22 4 36 14 36 265 0 4 2 43 40 63 [0.11] SYN876-1 theorem 12.5 22 125 52 1053 52 487 0 16037 2 136 177 18731 [0.11] SYN877-1 theorem 0.1 22 3 36 13 36 268 0 3 2 42 39 87 [0.11] SYN878-1 theorem 0.1 22 3 36 14 36 271 0 18 2 45 39 72 [0.11] SYN879-1 theorem 0.1 22 2 36 12 36 271 0 14 2 45 38 91 [0.11] SYN880-1 theorem 0.1 22 2 52 9 52 488 0 3 2 60 54 46 [0.11] SYN881-1 theorem 170.5 29 2655 52 15389 52 490 0 170019 2 150 2707 226151 [0.11] SYN882-1 theorem 0.2 22 5 52 19 52 485 0 16 2 62 57 72 [0.11] SYN883-1 theorem 0.2 22 6 52 24 52 491 0 48 2 67 58 117 [0.11] SYN884-1 theorem 0.4 22 4 70 14 70 932 0 2 2 77 74 60 [0.11] SYN889-1 theorem 0.1 22 2 36 4 36 271 0 0 2 39 38 53 [0.11] SYN890-1 theorem 0.1 22 2 36 8 36 273 0 2 2 42 38 56 [0.11] SYN891-1 theorem 0.1 22 2 36 7 36 259 0 0 2 40 38 64 [0.11] SYN892-1 theorem 0.1 22 2 36 10 36 273 0 4 2 42 38 94 [0.11] SYN893-1 theorem 0.2 22 2 52 5 52 485 0 1 2 56 54 46 [0.11] SYN894-1 theorem 0.2 22 3 52 9 52 489 0 4 2 58 55 45 [0.11] SYN895-1 theorem 0.2 22 2 52 11 52 479 0 0 2 60 54 68 [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 2 8 8 36 [0.14] KRS006-1 non_thm 0.0 4 0 20 3 5 0 0 68 3 23 31 71 [0.14] KRS007-1 non_thm 0.0 4 0 27 2 2 0 0 83 3 29 37 85 [0.14] KRS008-1 non_thm 0.1 4 0 42 34 2 0 0 772 3 76 72 810 [0.14] KRS009-1 non_thm 0.0 4 0 43 8 1 0 0 229 3 51 65 237 [0.14] KRS011-1 non_thm 0.0 4 0 36 3 2 0 0 46 2 39 44 49 [0.14] KRS014-1 non_thm 0.0 4 0 14 2 1 0 0 30 2 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 2 19 17 31 [0.14] NLP044-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 [0.14] NLP045-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 [0.14] NLP046-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 [0.14] NLP047-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 [0.14] NLP048-1 non_thm 0.0 4 0 17 2 35 3 0 29 2 19 17 31 [0.14] NLP066-1 non_thm 0.0 4 0 12 4 12 3 0 26 2 16 12 30 [0.14] NLP067-1 non_thm 0.0 4 0 10 4 13 3 0 24 2 14 10 28 [0.14] NLP068-1 non_thm 0.0 4 0 5 3 12 3 0 12 2 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 2 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 2 4 3 10 [0.14] NLP103-1 non_thm 0.0 4 0 4 1 22 4 0 10 2 5 4 11 [0.14] NLP130-1 non_thm 0.0 4 0 24 4 44 4 0 45 2 28 24 49 [0.14] NLP131-1 non_thm 0.0 4 0 21 2 44 4 0 38 2 23 21 40 [0.14] NLP132-1 non_thm 0.0 4 0 21 3 44 4 0 38 2 24 21 41 [0.14] NLP133-1 non_thm 0.0 4 0 21 3 44 4 0 38 2 24 21 41 [0.14] NLP134-1 non_thm 0.0 4 0 21 2 44 4 0 37 2 23 21 39 [0.14] NLP135-1 non_thm 0.0 4 0 24 4 44 4 0 45 2 28 24 49 [0.14] NLP136-1 non_thm 0.0 4 1 43 2 86 5 0 39 2 25 46 62 [0.14] NLP137-1 non_thm 0.0 4 0 30 4 44 4 0 53 3 34 30 57 [0.14] NLP138-1 non_thm 0.0 4 1 43 2 86 5 0 39 2 25 46 62 [0.14] NLP139-1 non_thm 0.0 4 0 30 4 44 4 0 53 3 34 30 57 [0.14] NLP221-1 non_thm 0.0 4 0 20 1 43 4 0 34 2 21 20 35 [0.14] NLP222-1 non_thm 0.0 4 0 20 1 43 4 0 34 2 21 20 35 [0.14] NLP223-1 non_thm 0.0 4 0 19 1 42 4 0 33 2 20 19 34 [0.14] NLP230-1 non_thm 0.1 4 1 78 1 159 5 0 72 3 43 83 113 [0.14] NLP231-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 [0.14] NLP232-1 non_thm 0.0 4 0 38 1 79 4 0 70 2 39 38 71 [0.14] NLP233-1 non_thm 0.0 4 0 39 1 78 4 0 70 2 40 39 71 [0.14] NLP234-1 non_thm 0.0 4 0 38 1 79 4 0 70 2 39 38 71 [0.14] NLP235-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 [0.14] NLP236-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 [0.14] NLP237-1 non_thm 0.0 4 0 38 1 79 4 0 70 2 39 38 71 [0.14] NLP238-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 38 37 70 [0.14] NLP239-1 non_thm 0.0 4 0 37 1 78 4 0 69 2 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 2 7 9 4 [0.14] SYN306-1 timeout 298.9 5 [0.14] SYN308-1 non_thm 0.0 4 0 1 2 2 0 0 0 3 3 1 2 [0.14] SYN309-1 non_thm 0.0 4 0 2 2 5 0 0 0 2 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 0 0 2 2 0 0 0 2 2 0 2 [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 7 2 0 0 37 3 9 2 44 [0.17] FLD001-3 theorem 0.0 4 1 62 0 7 0 0 0 2 62 283 0 [0.17] FLD002-3 theorem 0.0 4 1 63 0 7 0 0 0 2 63 300 0 [0.17] FLD005-3 theorem 0.0 4 1 91 0 6 0 0 0 2 91 629 0 [0.17] FLD007-3 timeout 299.0 41 [0.17] FLD008-4 theorem 0.1 4 1 145 0 10 0 0 0 2 145 804 0 [0.17] FLD009-3 theorem 0.1 4 1 112 0 7 0 0 0 2 112 907 0 [0.17] FLD010-5 theorem 0.0 4 1 54 0 5 0 0 0 2 54 658 0 [0.17] FLD011-3 timeout 299.0 44 [0.17] FLD012-4 theorem 0.2 4 1 270 0 12 0 0 0 2 270 3112 0 [0.17] FLD013-3 theorem 0.5 4 1 324 0 10 0 0 0 2 324 6414 0 [0.17] FLD013-4 theorem 0.0 4 1 29 0 12 0 0 0 2 29 315 0 [0.17] FLD013-5 theorem 0.0 4 1 27 0 14 0 0 0 2 27 334 0 [0.17] FLD014-3 theorem 0.2 4 1 192 0 7 0 0 0 2 192 3602 0 [0.17] FLD015-3 theorem 0.0 4 1 93 0 7 0 0 0 2 93 636 0 [0.17] FLD016-3 theorem 0.1 4 1 151 0 10 0 0 0 2 151 851 0 [0.17] FLD016-5 theorem 0.1 4 1 204 0 12 0 0 0 2 204 1500 0 [0.17] FLD017-3 theorem 0.0 4 1 11 0 10 0 0 0 2 11 187 0 [0.17] FLD021-1 theorem 0.5 4 1 55 0 7 0 0 0 2 55 216 0 [0.17] FLD022-3 theorem 0.1 4 1 149 0 10 0 0 0 2 149 827 0 [0.17] FLD023-3 theorem 0.0 4 1 86 0 7 0 0 0 2 86 738 0 [0.17] FLD024-3 theorem 0.0 4 1 57 0 7 0 0 0 2 57 227 0 [0.17] FLD025-3 theorem 0.5 4 1 324 0 10 0 0 0 2 324 6414 0 [0.17] FLD025-4 theorem 0.0 4 1 36 0 12 0 0 0 2 36 336 0 [0.17] FLD025-5 theorem 0.0 4 1 35 0 14 0 0 0 2 35 362 0 [0.17] FLD026-3 theorem 0.6 4 1 410 0 8 0 0 0 2 410 12031 0 [0.17] FLD027-3 theorem 0.1 4 1 149 0 9 0 0 0 2 149 1648 0 [0.17] FLD028-3 theorem 0.1 4 1 181 0 11 0 0 0 2 181 1229 0 [0.17] FLD029-3 theorem 0.5 4 1 589 0 11 0 0 0 2 589 8391 0 [0.17] FLD030-1 theorem 0.0 4 1 9 0 8 0 0 0 2 9 149 0 [0.17] FLD030-2 theorem 0.0 4 1 24 0 10 0 0 0 2 24 310 0 [0.17] FLD030-3 theorem 0.0 4 1 25 0 8 0 0 0 2 25 188 0 [0.17] FLD030-4 theorem 0.0 4 1 11 0 10 0 0 0 2 11 187 0 [0.17] FLD031-3 theorem 0.1 4 1 83 0 7 0 0 0 2 83 2127 0 [0.17] FLD031-5 theorem 0.1 4 1 100 0 7 0 0 0 2 100 2896 0 [0.17] FLD032-3 theorem 0.0 4 1 18 0 7 0 0 0 2 18 110 0 [0.17] FLD034-1 theorem 0.5 4 1 60 0 7 0 0 0 2 60 233 0 [0.17] FLD035-3 theorem 0.1 4 1 181 0 11 0 0 0 2 181 1229 0 [0.17] FLD036-3 theorem 0.1 4 1 181 0 11 0 0 0 2 181 1229 0 [0.17] FLD037-1 theorem 97.3 11 1 275 0 8 0 0 0 3 275 11553 0 [0.17] FLD037-3 theorem 0.1 4 1 128 0 8 0 0 0 2 128 1883 0 [0.17] FLD038-3 theorem 0.0 4 1 64 0 8 0 0 0 2 64 277 0 [0.17] FLD040-3 theorem 0.0 4 1 67 0 6 0 0 0 2 67 537 0 [0.17] FLD040-5 theorem 0.0 4 1 68 0 6 0 0 0 2 68 601 0 [0.17] FLD041-3 theorem 0.1 4 1 188 0 8 0 0 0 2 188 2588 0 [0.17] FLD041-4 theorem 0.4 4 1 343 0 10 0 0 0 2 343 10802 0 [0.17] FLD043-3 theorem 0.0 4 1 107 0 7 0 0 0 2 107 851 0 [0.17] FLD049-4 theorem 0.2 4 1 295 0 15 0 0 0 2 295 1927 0 [0.17] FLD050-4 theorem 0.2 4 1 298 0 15 0 0 0 2 298 1974 0 [0.17] FLD055-3 theorem 0.0 4 1 20 0 9 0 0 0 2 20 154 0 [0.17] FLD058-3 theorem 0.0 4 1 21 0 9 0 0 0 2 21 131 0 [0.17] FLD059-1 theorem 0.1 4 1 40 0 6 0 0 0 2 40 141 0 [0.17] FLD059-3 theorem 0.0 4 1 54 0 6 0 0 0 2 54 322 0 [0.17] FLD059-4 theorem 0.0 4 1 14 0 8 0 0 0 2 14 107 0 [0.17] FLD060-3 theorem 30.3 17 1 996 0 7 0 0 0 2 996 145733 0 [0.17] FLD060-4 theorem 0.3 4 1 313 0 11 0 0 0 2 313 3407 0 [0.17] FLD061-4 theorem 0.7 4 1 471 0 14 0 0 0 2 471 5072 0 [0.17] FLD063-3 theorem 21.8 14 1 818 0 7 0 0 0 2 818 111768 0 [0.17] FLD064-3 theorem 0.1 4 1 87 0 6 0 0 0 2 87 1933 0 [0.17] FLD065-3 theorem 0.0 4 1 12 0 6 0 0 0 2 12 67 0 [0.17] FLD066-3 theorem 0.2 4 1 207 0 12 0 0 0 2 207 1580 0 [0.17] FLD067-3 timeout 299.0 37 [0.17] FLD067-4 theorem 0.1 4 1 107 0 9 0 0 0 2 107 531 0 [0.17] FLD068-3 timeout 299.0 37 [0.17] FLD068-4 theorem 0.0 4 1 87 0 9 0 0 0 2 87 372 0 [0.17] FLD069-3 theorem 0.0 4 1 16 0 9 0 0 0 2 16 110 0 [0.17] FLD070-1 theorem 0.5 4 1 60 0 8 0 0 0 2 60 220 0 [0.17] FLD070-3 theorem 0.0 4 1 80 0 8 0 0 0 2 80 453 0 [0.17] FLD070-4 theorem 0.0 4 1 17 0 10 0 0 0 2 17 155 0 [0.17] FLD071-1 theorem 0.0 4 1 8 0 8 0 0 0 2 8 103 0 [0.17] GRP123-3.004 non_thm 0.0 4 1 143 1 32 0 0 219 2 132 951 257 [0.17] GRP123-8.004 non_thm 0.0 4 0 177 2 33 0 0 342 2 179 879 372 [0.17] GRP123-9.004 non_thm 0.1 4 0 138 29 18 0 0 322 2 167 813 379 [0.17] GRP125-1.004 non_thm 0.0 4 0 77 1 17 0 0 165 2 78 469 180 [0.17] GRP125-2.004 non_thm 0.0 4 0 96 0 26 0 0 180 2 96 490 180 [0.17] GRP125-3.004 non_thm 0.0 4 1 143 1 32 0 0 206 2 132 669 247 [0.17] GRP127-2.005 non_thm 0.1 4 1 187 1 40 0 0 447 2 175 1050 542 [0.17] GRP128-1.004 non_thm 0.0 4 7 171 8 16 0 0 215 2 84 925 392 [0.17] GRP128-2.004 non_thm 0.0 4 1 100 3 25 0 0 188 2 102 537 198 [0.17] GRP128-3.004 non_thm 0.0 4 3 212 4 31 0 0 232 2 139 876 345 [0.17] GRP130-3.004 non_thm 0.0 4 2 202 2 31 0 0 232 2 139 826 334 [0.17] GRP133-2.004 non_thm 0.0 4 2 121 5 25 0 0 186 2 102 613 250 [0.17] HWV008-1.001 theorem 0.1 4 1 215 0 11 0 0 0 5 215 653 0 [0.17] HWV008-1.002 theorem 0.1 4 1 324 0 14 0 0 0 5 324 934 0 [0.17] HWV008-2.001 theorem 0.1 4 1 215 0 9 0 0 0 5 215 601 0 [0.17] HWV008-2.002 theorem 0.1 4 1 326 0 12 0 0 0 5 326 866 0 [0.17] NLP079-1 theorem 0.0 4 2 40 1 76 4 0 0 2 22 82 54 [0.17] NLP080-1 theorem 0.0 4 2 40 1 76 4 0 0 2 22 80 54 [0.17] NLP081-1 theorem 0.0 4 2 38 1 72 4 0 0 2 21 76 51 [0.17] NLP094-1 theorem 0.0 4 2 41 1 64 4 0 0 2 23 50 44 [0.17] PUZ035-3 theorem 0.0 4 4 12 3 6 8 0 3 2 8 27 6 [0.17] PUZ035-4 theorem 0.0 4 4 12 3 6 8 0 3 2 8 27 6 [0.17] SET005-1 theorem 0.0 4 2 135 1 4 0 0 0 2 131 378 143 [0.17] SET007-1 theorem 0.1 4 3 578 2 5 0 38 0 2 339 2353 722 [0.17] SET014-2 theorem 169.2 19 1 294 0 6 0 0 0 3 294 11114 2 [0.17] SET055-6 theorem 132.0 12 51 17443 108 30 0 204 274754 2 5353 370551 283070 [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 2 33 149 2 [0.17] SYN036-3 theorem 0.0 4 10 67 9 220 142 5 29 2 17 111 76 [0.17] SYN037-1 theorem 0.0 4 9 71 8 232 166 11 19 2 17 112 77 [0.17] SYN037-2 theorem 0.0 4 12 22 15 171 87 8 25 2 11 78 66 [0.17] SYN313-1.001.002 theorem 7.8 5 951 4505 2066 0 0 4 10031 29 58 5619 26413 [0.17] SYN419-1 non_thm 0.0 4 0 49 45 369 103 0 163 2 94 50 211 [0.17] SYN420-1 non_thm 0.1 4 1 80 106 531 136 0 1042 2 184 103 1172 [0.17] SYN425-1 non_thm 0.1 4 0 140 97 398 124 0 965 2 237 147 1073 [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.2 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.2 4 199 3030 220 5002 1339 0 70244 2 89 12938 322102 [0.17] SYN456-1 non_thm 6.8 6 225 2444 264 4412 1200 0 216245 2 77 12369 450415 [0.17] SYN538-1 non_thm 0.0 4 0 2 13 74 27 0 19 2 15 2 32 [0.17] SYN539-1 non_thm 0.0 4 0 7 12 77 31 0 30 2 19 7 42 [0.17] SYN540-1 non_thm 0.0 4 3 27 16 204 60 0 57 2 38 51 87 [0.17] SYN541-1 non_thm 0.0 4 0 22 21 118 39 0 58 2 43 22 79 [0.17] SYN545-1 non_thm 0.1 4 3 63 70 447 105 0 497 2 128 118 630 [0.17] SYN606-1 timeout 298.9 17 [0.17] SYN607-1 timeout 298.9 16 [0.17] SYN620-1 theorem 0.0 4 1 67 0 13 0 0 0 4 67 283 0 [0.17] SYN625-1 theorem 0.0 4 1 23 0 8 0 0 0 5 23 73 1 [0.17] SYN630-1 theorem 0.0 4 1 9 0 9 0 0 0 2 9 28 0 [0.17] SYN633-1 theorem 5.7 4 1 186 0 9 0 0 0 6 186 3919 4 [0.17] SYN634-1 theorem 5.7 4 1 186 0 9 0 0 0 6 186 3919 4 [0.17] SYN635-1 theorem 5.7 4 1 186 0 9 0 0 0 6 186 3919 4 [0.17] SYN636-1 theorem 5.7 4 1 186 0 9 0 0 0 6 186 3919 4 [0.17] SYN641-1 theorem 0.1 4 1 178 0 15 0 0 0 4 178 1115 0 [0.17] SYN642-1 theorem 0.1 4 1 170 0 15 0 0 0 4 170 1091 0 [0.17] SYN643-1 theorem 0.1 4 1 174 0 15 0 0 0 4 174 1103 0 [0.17] SYN648-1 timeout 299.0 150 [0.17] SYN659-1 theorem 3.3 5 1 221 0 22 0 0 0 4 221 2111 0 [0.17] SYN692-1 timeout 299.0 251 [0.17] SYN693-1 timeout 299.0 245 [0.17] SYN695-1 timeout 299.0 229 [0.17] SYN697-1 timeout 299.0 251 [0.17] SYN699-1 timeout 299.0 224 [0.17] SYN701-1 timeout 299.0 229 [0.17] SYN714-1 theorem 0.0 4 1 38 0 31 0 0 0 3 38 136 0 [0.17] SYN815-1 non_thm 4.6 17 0 674 193 85 939 0 774 2 867 1293 967 [0.17] SYN816-1 non_thm 4.4 17 0 590 184 79 939 0 720 2 774 1127 904 [0.17] SYN817-1 non_thm 5.0 17 0 626 207 82 939 0 787 2 833 1198 994 [0.17] SYN825-1 non_thm 9.6 19 0 945 117 85 1649 0 964 2 1062 1805 1081 [0.17] SYN826-1 non_thm 9.6 19 0 858 25 84 1763 0 798 2 883 1632 823 [0.17] SYN828-1 non_thm 4.4 19 1 646 246 68 899 0 898 2 892 1225 1153 [0.17] SYN835-1 non_thm 0.6 20 1 188 210 36 269 0 494 2 391 341 709 [0.17] TOP005-2 timeout 299.0 31 [0.22] GRP128-2.006 theorem 0.1 4 8 428 7 56 0 0 379 2 251 1751 1545 [0.22] GRP128-3.005 theorem 0.1 4 7 395 6 46 0 0 143 2 207 1467 858 [0.22] SYN442-1 theorem 18.5 6 173 2966 208 4720 1172 0 604960 2 100 11714 1206041 [0.22] SYN443-1 theorem 1.7 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.6 4 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.4 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.9 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.2 4 137 2149 148 3986 950 0 54235 2 64 7564 300711 [0.22] SYN472-1 theorem 4.5 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.8 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 6.1 5 83 1209 90 2382 582 0 157129 2 85 9465 434234 [0.22] SYN507-1 theorem 2.8 4 80 1371 80 2673 603 0 53797 2 89 4775 187253 [0.22] SYN813-1 theorem 1.7 17 23 188 1068 44 269 0 1340 2 340 371 2847 [0.22] SYN833-1 theorem 0.4 20 3 188 93 36 269 0 230 2 236 343 374 [0.22] SYN834-1 theorem 1.3 20 14 188 793 36 269 0 1217 2 363 354 2305 [0.22] SYN843-1 theorem 0.6 22 4 188 152 36 269 0 314 2 296 344 620 [0.22] SYN849-1 theorem 16.0 22 77 376 5851 52 489 0 10192 2 751 777 20341 [0.22] SYN856-1 theorem 0.6 22 3 188 153 36 269 0 312 2 284 343 620 [0.22] SYN857-1 theorem 0.7 22 3 188 206 36 269 0 337 2 280 343 733 [0.22] SYN859-1 theorem 2.2 22 6 376 462 52 489 0 889 2 538 706 1551 [0.22] SYN886-1 theorem 0.3 22 2 72 6 72 909 0 0 2 77 74 33 [0.22] SYN887-1 theorem 0.4 22 4 72 14 72 938 0 3 2 82 76 58 [0.22] SYN896-1 theorem 0.4 22 13 52 48 52 492 0 36 2 75 65 251 [0.22] SYN898-1 theorem 0.5 22 7 72 29 72 941 0 13 2 85 79 101 [0.22] SYN899-1 theorem 0.4 22 3 72 15 72 931 0 5 2 82 75 83 [0.22] SYN900-1 theorem 0.4 22 4 72 27 72 923 0 8 2 93 76 71 [0.22] SYN901-1 theorem 1.0 22 4 101 23 101 1680 0 25 2 120 105 88 [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 0 10 4 13 3 0 24 2 14 10 28 [0.29] NLP064-1 non_thm 0.0 4 0 10 5 13 3 3 31 2 15 10 36 [0.29] NLP065-1 non_thm 0.0 4 0 10 5 13 3 3 32 2 15 10 37 [0.29] SYN316-1 timeout 298.9 4 [0.29] SYN324-1 timeout 299.0 4 [0.29] SYN330-1 timeout 299.0 39 [0.29] SYN335-1 timeout 298.9 50 [0.29] SYN351-1 non_thm 0.2 4 1 84 34 1 0 0 400 7 118 175 458 [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.0 4 0 1 5 1 0 0 63 4 6 1 68 [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 6 1 0 0 13 5 7 1 19 [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 40 [0.33] ANA002-2 timeout 299.0 52 [0.33] ANA002-3 timeout 299.0 13 [0.33] ANA002-4 timeout 299.0 17 [0.33] ANA003-4 timeout 299.0 177 [0.33] FLD003-1 timeout 298.9 11 [0.33] FLD005-1 timeout 299.0 11 [0.33] FLD009-1 timeout 299.0 11 [0.33] FLD013-1 theorem 4.4 4 1 272 0 10 0 0 0 2 272 1327 0 [0.33] FLD013-2 theorem 10.3 4 1 345 0 12 0 0 0 2 345 1638 0 [0.33] FLD015-1 timeout 299.0 10 [0.33] FLD017-1 theorem 0.0 4 1 24 0 10 0 0 0 2 24 310 0 [0.33] FLD018-1 timeout 299.0 6 [0.33] FLD019-1 timeout 298.9 6 [0.33] FLD023-1 theorem 70.0 11 1 212 0 7 0 0 0 3 212 10330 0 [0.33] FLD024-1 timeout 299.0 10 [0.33] FLD025-1 theorem 4.4 4 1 284 0 10 0 0 0 2 284 1371 0 [0.33] FLD025-2 theorem 22.0 4 1 460 0 14 0 0 0 2 460 2232 0 [0.33] FLD031-1 timeout 299.0 6 [0.33] FLD032-1 timeout 299.0 6 [0.33] FLD043-5 theorem 10.4 12 1 684 0 5 0 0 0 2 684 101318 0 [0.33] FLD047-4 theorem 0.5 4 1 441 0 15 0 0 0 2 441 5200 0 [0.33] FLD049-3 timeout 299.0 47 [0.33] FLD054-4 theorem 0.4 4 1 419 0 14 0 0 0 2 419 5923 0 [0.33] FLD059-2 theorem 0.5 4 1 177 0 8 0 0 0 2 177 908 0 [0.33] FLD060-1 theorem 0.5 4 1 133 0 7 0 0 0 2 133 517 0 [0.33] FLD060-2 theorem 4.4 4 1 267 0 11 0 0 0 2 267 1054 0 [0.33] FLD061-1 theorem 4.4 4 1 245 0 10 0 0 0 2 245 889 0 [0.33] FLD061-2 theorem 21.9 4 1 421 0 14 0 0 0 2 421 1571 0 [0.33] FLD061-3 theorem 174.3 32 1 1854 0 10 0 0 0 2 1854 290812 0 [0.33] FLD062-3 theorem 83.4 27 1 1101 0 7 0 0 0 2 1101 276678 0 [0.33] FLD064-1 timeout 298.9 6 [0.33] FLD065-1 timeout 299.0 6 [0.33] FLD067-1 theorem 70.8 11 1 202 0 7 0 0 0 3 202 9543 0 [0.33] FLD067-2 timeout 298.9 18 [0.33] FLD068-2 timeout 299.0 18 [0.33] FLD069-1 theorem 0.5 4 1 98 0 9 0 0 0 2 98 401 0 [0.33] FLD070-2 theorem 1.7 4 1 266 0 10 0 0 0 2 266 1401 0 [0.33] FLD071-2 theorem 1.6 4 1 100 0 10 0 0 0 2 100 376 0 [0.33] GRP039-6 theorem 32.9 5 26 2492 27 9 0 2 44752 2 822 345674 48053 [0.33] GRP123-4.004 non_thm 0.0 4 0 77 1 17 0 0 406 2 78 802 449 [0.33] GRP125-4.004 non_thm 0.0 4 0 77 1 17 0 0 419 2 78 719 462 [0.33] GRP126-2.005 non_thm 0.1 4 0 173 2 40 0 0 450 2 175 969 484 [0.33] GRP127-3.005 non_thm 0.1 4 2 271 2 47 0 0 550 2 227 1407 744 [0.33] GRP128-4.004 non_thm 0.1 4 5 83 6 16 0 0 474 2 84 884 512 [0.33] GRP130-2.005 non_thm 0.1 4 3 248 4 39 0 0 484 2 183 1296 688 [0.33] GRP130-4.004 non_thm 0.1 4 5 120 6 16 0 0 500 2 84 911 650 [0.33] MSC007-1.008 theorem 4.3 14 5040 55182 5039 282303 78952 0 2779 2 56 105582 27398 [0.33] PUZ018-2 non_thm 0.1 4 0 89 19 40 6 0 1428 2 108 150 1519 [0.33] PUZ035-7 theorem 0.1 4 13 217 23 8 0 0 343 3 73 857 2007 [0.33] SET010-1 theorem 0.1 4 3 835 2 5 0 61 0 2 486 3402 997 [0.33] SET012-1 timeout 299.0 51 [0.33] SET012-2 theorem 0.1 4 3 131 2 6 0 0 517 2 102 1735 1045 [0.33] SET013-1 timeout 299.0 67 [0.33] SET015-1 timeout 299.0 62 [0.33] SYN036-1 theorem 6.9 10 46 118 45 2320 350 3 51805 2 18 184838 350068 [0.33] SYN036-4 theorem 0.0 4 8 9 7 199 98 6 0 2 5 61 56 [0.33] SYN353-1 timeout 299.0 19 [0.33] SYN418-1 non_thm 0.1 4 0 59 57 407 95 0 231 2 116 60 291 [0.33] SYN421-1 non_thm 0.0 4 0 45 61 456 97 0 213 2 106 47 274 [0.33] SYN422-1 non_thm 0.1 4 0 47 63 378 107 0 227 2 110 50 290 [0.33] SYN423-1 non_thm 0.1 4 0 140 83 494 132 0 379 2 223 143 463 [0.33] SYN424-1 non_thm 0.1 4 0 115 114 662 149 0 728 2 229 120 854 [0.33] SYN426-1 non_thm 0.2 4 1 136 157 691 203 0 878 2 292 146 1048 [0.33] SYN427-1 non_thm 0.2 4 0 165 90 530 151 0 1231 2 255 172 1321 [0.33] SYN428-1 non_thm 0.6 4 2 222 252 566 176 0 11692 2 447 290 12210 [0.33] SYN429-1 non_thm 0.1 4 1 107 55 667 147 0 246 2 161 137 318 [0.33] SYN436-1 theorem 8.7 5 155 2423 170 3211 966 0 242967 2 82 7677 782479 [0.33] SYN441-1 non_thm 6.8 4 64 1253 92 1459 420 0 126720 2 136 10580 294666 [0.33] SYN453-1 non_thm 5.5 10 58 1502 83 1747 482 0 101075 2 156 7041 184027 [0.33] SYN464-1 non_thm 19.1 9 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.6 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.5 4 119 1665 127 3325 805 0 60934 2 71 6479 311796 [0.33] SYN487-1 theorem 4.1 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.8 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 0.1 4 3 103 79 375 107 0 1712 2 178 165 1892 [0.33] SYN518-1 non_thm 0.2 4 0 143 67 395 98 0 2505 2 210 150 2604 [0.33] SYN542-1 non_thm 5.7 9 0 133 75 214 41 0 195640 2 208 642 196945 [0.33] SYN543-1 non_thm 6.5 8 0 132 68 210 38 0 203382 2 200 1015 204756 [0.33] SYN544-1 non_thm 0.1 4 2 140 80 225 85 0 1575 2 216 174 1687 [0.33] SYN546-1 non_thm 0.1 4 0 92 78 451 107 0 639 2 170 97 765 [0.33] SYN547-1 non_thm 0.1 4 1 75 60 491 116 0 225 2 132 91 311 [0.33] SYN576-1 theorem 0.4 4 1 118 0 8 0 0 0 4 118 2989 1 [0.33] SYN595-1 theorem 124.4 22 1 52 0 8 0 0 0 5 52 1141 0 [0.33] SYN604-1 theorem 254.8 18 1 441 0 11 0 0 0 6 441 12872 1 [0.33] SYN610-1 timeout 299.0 16 [0.33] SYN611-1 timeout 299.0 16 [0.33] SYN612-1 timeout 298.9 17 [0.33] SYN645-1 timeout 298.9 9 [0.33] SYN657-1 theorem 157.1 27 1 767 0 20 0 0 0 6 767 27287 1 [0.33] SYN658-1 timeout 299.0 28 [0.33] SYN687-1 theorem 3.8 4 1 41 0 20 0 0 0 7 41 128 1 [0.33] SYN694-1 timeout 299.0 194 [0.33] SYN696-1 timeout 299.0 233 [0.33] SYN698-1 timeout 299.0 192 [0.33] SYN700-1 timeout 299.0 209 [0.33] SYN755-1 theorem 2.2 4 146 1 366 1 0 0 48385 5 21 1 60249 [0.33] SYN759-1 theorem 30.1 4 356 1 1123 1 0 0 344577 8 32 1 419398 [0.33] SYN762-1 theorem 19.9 4 232 1 852 1 0 0 251140 8 30 1 295979 [0.33] SYN784-1 theorem 2.9 4 82 2 339 2 0 0 39521 4 23 2 55079 [0.33] SYN796-1 theorem 0.7 4 42 2 143 2 0 0 13240 3 16 2 19609 [0.33] SYN812-1 non_thm 12.0 19 0 936 186 101 1708 0 1005 2 1122 1801 1191 [0.33] SYN814-1 non_thm 3.2 17 0 376 726 64 489 0 1650 2 1102 712 2398 [0.33] SYN819-1 theorem 3.4 19 40 188 1635 44 269 0 2941 2 394 388 5995 [0.33] SYN820-1 theorem 8.7 19 81 188 4034 44 269 0 11277 2 561 429 17724 [0.33] SYN829-1 non_thm 13.8 22 0 1177 145 95 1704 0 1199 2 1322 2259 1344 [0.33] SYN831-1 non_thm 14.7 23 0 1268 295 96 1763 0 1474 2 1563 2440 1772 [0.33] SYN832-1 non_thm 12.9 21 0 1033 218 93 1704 0 1152 2 1251 1973 1370 [0.33] SYN837-1 theorem 6.6 20 22 376 2246 52 489 0 2755 2 729 722 5875 [0.33] SYN838-1 non_thm 5.8 20 0 634 351 70 939 0 929 2 985 1198 1280 [0.33] SYN841-1 non_thm 20.3 29 0 1330 681 102 1763 0 2045 2 2011 2558 2727 [0.33] SYN844-1 theorem 0.5 22 4 188 125 36 269 0 254 2 249 344 478 [0.33] SYN845-1 theorem 0.5 22 2 188 84 36 269 0 232 2 251 342 393 [0.33] SYN847-1 theorem 2.1 22 4 376 454 52 489 0 743 2 626 704 1503 [0.33] SYN848-1 theorem 1.5 22 3 376 191 52 489 0 485 2 488 703 820 [0.33] SYN851-1 non_thm 5.9 22 1 696 478 72 939 0 1145 2 1086 1321 1662 [0.33] SYN858-1 theorem 1.8 22 3 376 258 52 489 0 595 2 492 703 1088 [0.33] SYN860-1 theorem 3.6 22 15 376 637 52 489 0 1270 2 634 715 2720 [0.33] SYN863-1 non_thm 7.0 22 0 696 718 72 939 0 1622 2 1414 1320 2340 [0.33] SYN864-1 non_thm 6.5 22 0 696 522 72 939 0 1225 2 1218 1320 1749 [0.33] SYN897-1 theorem 0.5 22 2 72 23 72 940 0 5 2 88 74 86 [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 2 9 4 9 [0.43] NLP031-1 timeout 299.0 6 [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 11 1 0 0 227 5 12 1 238 [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 3 1 0 0 5 3 4 1 8 [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.0 4 0 2 7 2 0 0 107 3 9 2 114 [0.43] TOP003-2 non_thm 0.0 22 0 12 22 3 0 0 50 4 34 20 72 [0.44] SYN447-1 theorem 68.8 24 354 7741 423 9283 3032 0 867115 2 130 27326 5669521 [0.44] SYN457-1 theorem 189.0 18 999 21446 1481 23793 6817 0 4562905 2 156 203897 6609426 [0.44] SYN473-1 theorem 2.7 4 89 1394 92 2407 634 0 26700 2 76 6183 247403 [0.44] SYN846-1 theorem 14.3 22 57 376 3943 52 489 0 4644 2 755 757 11420 [0.44] SYN862-1 theorem 137.6 35 308 696 24497 72 939 0 40378 2 1314 1628 70638 [0.44] SYN885-1 theorem 3.4 22 40 72 311 72 908 0 600 2 111 112 1426 [0.50] ANA004-4 timeout 299.0 174 [0.50] ANA004-5 timeout 299.0 26 [0.50] COM003-1 theorem 5.2 9 814 8399 5778 1707 210 12 43771 2 209 25588 167657 [0.50] FLD004-1 timeout 299.0 11 [0.50] FLD007-1 timeout 298.9 6 [0.50] FLD016-1 timeout 299.0 20 [0.50] FLD020-1 timeout 298.9 11 [0.50] FLD022-1 timeout 299.0 17 [0.50] FLD033-1 timeout 299.0 11 [0.50] FLD050-3 timeout 299.0 47 [0.50] FLD052-4 theorem 2.2 4 1 932 0 25 0 0 0 2 932 9605 0 [0.50] FLD057-3 timeout 299.0 60 [0.50] FLD063-1 timeout 298.9 10 [0.50] FLD066-1 timeout 299.0 17 [0.50] FLD068-1 timeout 299.0 10 [0.50] GRP123-1.005 non_thm 0.1 4 0 143 4 26 0 0 465 2 147 1556 505 [0.50] GRP123-2.005 non_thm 0.1 4 1 189 2 40 0 0 493 2 175 1815 595 [0.50] GRP123-6.005 non_thm 0.1 4 0 264 4 27 0 0 879 2 268 1624 947 [0.50] GRP123-7.005 non_thm 0.1 4 0 284 4 41 0 0 879 2 288 1644 947 [0.50] GRP124-1.005 non_thm 0.1 4 0 142 5 26 0 0 458 2 147 1556 505 [0.50] GRP124-2.005 non_thm 0.1 4 0 173 2 40 0 0 460 2 175 1590 505 [0.50] GRP124-3.005 non_thm 0.1 4 2 244 4 47 0 0 551 2 223 1899 670 [0.50] GRP124-4.005 non_thm 0.1 4 0 143 4 26 0 0 1190 2 147 1606 1305 [0.50] GRP124-6.005 non_thm 0.1 4 0 263 5 27 0 0 877 2 268 1624 947 [0.50] GRP124-7.005 non_thm 0.1 4 0 283 5 41 0 0 877 2 288 1644 947 [0.50] GRP124-8.005 non_thm 0.1 4 0 322 6 48 0 0 938 2 328 1739 1009 [0.50] GRP124-9.005 non_thm 0.1 4 0 263 50 27 0 0 882 2 313 1624 997 [0.50] GRP126-1.005 non_thm 0.1 4 0 143 4 26 0 0 443 2 147 935 484 [0.50] GRP126-3.005 non_thm 0.1 4 2 244 4 47 0 0 536 2 223 1271 649 [0.50] GRP126-4.005 non_thm 0.1 4 0 144 3 26 0 0 1212 2 147 1427 1326 [0.50] GRP127-1.005 non_thm 0.1 4 0 145 2 26 0 0 456 2 147 935 484 [0.50] GRP127-4.005 non_thm 0.1 4 0 145 2 26 0 0 1244 2 147 1427 1326 [0.50] GRP129-1.005 non_thm 0.2 4 24 686 28 25 0 0 737 2 155 3378 2149 [0.50] GRP129-2.005 non_thm 0.1 4 10 316 15 39 0 0 592 2 183 1745 820 [0.50] GRP129-3.005 non_thm 0.1 4 7 390 9 46 0 0 827 2 232 1914 992 [0.50] GRP129-4.005 non_thm 0.1 4 13 234 16 25 0 0 1454 2 155 2184 1880 [0.50] GRP130-1.005 non_thm 0.1 4 15 393 18 25 0 0 628 2 155 2174 1188 [0.50] GRP131-1.005 non_thm 0.1 4 0 147 8 25 0 0 484 2 155 1575 525 [0.50] GRP131-2.005 non_thm 0.8 4 80 1612 88 39 0 0 2453 2 183 16728 7868 [0.50] GRP132-2.005 non_thm 1.3 4 92 2522 99 39 0 0 1994 2 183 29511 12989 [0.50] GRP133-1.004 non_thm 0.0 4 1 87 3 16 0 0 186 2 84 530 211 [0.50] GRP134-1.005 non_thm 0.1 4 6 219 10 25 0 0 471 2 155 1724 855 [0.50] GRP134-2.005 non_thm 0.1 4 6 456 11 39 0 0 640 2 183 3295 1717 [0.50] GRP135-1.005 non_thm 0.5 4 60 1853 64 25 0 0 2405 2 155 12748 6877 [0.50] GRP135-2.005 non_thm 0.2 4 20 828 21 39 0 0 1088 2 183 5153 2994 [0.50] SET013-2 theorem 0.3 4 3 609 2 6 0 0 517 2 336 6941 2910 [0.50] SET015-2 theorem 0.2 4 3 381 2 6 0 0 517 2 222 4397 1954 [0.50] SYN067-1 theorem 16.6 4 375 3049 399 7438 853 0 78754 2 41 14393 382978 [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 0.1 4 1 73 36 284 79 0 426 2 107 86 468 [0.50] SYN520-1 timeout 299.0 366 [0.50] SYN609-1 timeout 299.0 16 [0.50] SYN644-1 timeout 299.0 45 [0.50] SYN690-1 timeout 299.0 74 [0.50] SYN758-1 theorem 21.7 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 14.5 22 0 1214 64 98 1763 0 1156 2 1278 2330 1220 [0.50] SYN839-1 non_thm 18.1 28 0 1336 423 102 1763 0 1636 2 1759 2570 2059 [0.50] SYN840-1 non_thm 20.3 29 2 1150 549 96 1763 0 1976 2 1660 2206 2573 [0.50] SYN842-1 non_thm 22.1 31 0 1400 672 102 1763 0 2037 2 2072 2698 2709 [0.50] SYN852-1 non_thm 24.1 32 0 1396 846 102 1763 0 2165 2 2242 2690 3015 [0.50] SYN853-1 non_thm 28.6 33 3 1424 1373 104 1763 0 2969 2 2099 2747 4535 [0.50] SYN854-1 non_thm 46.8 38 5 1424 1828 104 1763 0 6541 2 2934 2749 8790 [0.50] SYN855-1 non_thm 21.1 29 0 1424 717 104 1763 0 2199 2 2141 2744 2916 [0.56] SYN439-1 theorem 4.4 5 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 5.0 22 2 696 160 72 939 0 764 2 789 1322 1052 [0.56] SYN861-1 theorem 8.8 22 10 696 933 72 939 0 1844 2 1211 1330 3296 [0.56] SYN865-1 theorem 6.3 22 3 696 559 72 939 0 1223 2 1106 1323 1962 [0.56] SYN866-1 theorem 32.2 22 29 696 5161 72 939 0 8595 2 1201 1349 15603 [0.57] NLP032-1 timeout 299.0 43 [0.57] NLP033-1 non_thm 0.1 4 19 102 36 22 4 0 73 5 29 271 532 [0.57] NLP061-1 non_thm 0.0 4 0 10 4 13 3 0 24 2 14 10 28 [0.57] NLP062-1 non_thm 0.0 4 0 10 4 13 3 0 22 2 14 10 26 [0.57] NLP063-1 non_thm 0.0 4 0 10 5 13 3 3 33 2 15 10 38 [0.57] NLP160-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP161-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP162-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP163-1 non_thm 0.0 4 1 54 4 108 5 0 49 2 31 57 80 [0.57] NLP164-1 non_thm 0.0 4 1 54 4 108 5 0 49 2 31 57 80 [0.57] NLP165-1 non_thm 0.0 4 1 54 4 108 5 0 49 2 31 57 80 [0.57] NLP166-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP167-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP168-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP169-1 non_thm 0.0 4 0 26 4 55 4 0 48 2 30 26 52 [0.57] NLP190-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP191-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP192-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP193-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP194-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP195-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP196-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP197-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP198-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] NLP199-1 non_thm 0.0 4 0 33 4 69 4 0 62 2 37 33 66 [0.57] SYN741-1 timeout 298.9 4 [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 298.9 5 [0.57] SYN750-1 non_thm 67.4 4 16 1 116 1 0 0 108778 18 107 1 118198 [0.57] SYN751-1 non_thm 0.0 4 0 1 12 1 0 0 82 5 13 1 94 [0.57] SYN753-1 non_thm 0.1 4 0 1 21 1 0 0 430 6 22 1 451 [0.57] SYN761-1 timeout 299.0 5 [0.57] SYN763-1 non_thm 0.0 4 0 1 9 1 0 0 56 3 10 1 65 [0.57] SYN766-1 non_thm 19.1 4 13 1 92 1 0 0 48522 13 79 1 51611 [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 11 [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.0 4 0 2 4 2 0 0 322 3 6 2 326 [0.57] SYN787-1 timeout 299.0 9 [0.57] SYN790-1 timeout 299.0 10 [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 299.0 11 [0.57] SYN801-1 timeout 298.9 12 [0.57] SYN903-1 timeout 299.0 22 [0.57] SYN904-1 timeout 298.9 22 [0.57] SYN905-1 timeout 298.9 22 [0.57] SYN907-1 timeout 299.0 25 [0.57] SYN908-1 timeout 299.0 25 [0.57] SYN909-1 timeout 298.9 33 [0.57] SYN910-1 timeout 299.0 35 [0.57] SYN912-1 timeout 298.9 50 [0.57] TOP010-1 timeout 299.0 94 [0.57] TOP011-1 timeout 299.0 22 [0.57] TOP014-1 timeout 299.0 118 [0.57] TOP016-1 timeout 299.0 60 [0.67] COM005-1 timeout 299.0 23 [0.67] FLD008-3 timeout 299.0 37 [0.67] FLD027-1 timeout 299.0 11 [0.67] FLD038-1 timeout 299.0 11 [0.67] FLD040-1 timeout 299.0 6 [0.67] FLD048-4 theorem 199.6 24 1 2388 0 20 0 0 0 2 2388 141561 0 [0.67] FLD051-4 timeout 299.0 30 [0.67] FLD086-3 timeout 299.0 47 [0.67] FLD090-3 timeout 299.0 41 [0.67] GRP132-1.005 non_thm 0.1 4 0 147 8 25 0 0 484 2 155 1575 525 [0.67] PUZ034-1.004 timeout 299.0 59 [0.67] SYN067-2 theorem 46.1 6 997 8803 1028 11294 1841 0 249484 2 52 47434 1077212 [0.67] SYN067-3 theorem 4.1 4 278 3043 317 1563 483 0 50974 2 42 9913 188244 [0.67] SYN519-1 timeout 299.0 160 [0.67] SYN650-1 timeout 299.0 45 [0.67] SYN818-1 non_thm 18.6 26 0 1374 471 125 1763 0 1728 2 1845 2669 2199 [0.67] SYN821-1 non_thm 5.1 19 0 696 177 88 899 0 788 2 873 1336 965 [0.71] NLP027-1 non_thm 0.3 4 0 92 62 12 4 0 1072 6 154 324 1134 [0.71] NLP028-1 non_thm 0.3 4 6 149 66 13 4 5 979 6 177 326 1101 [0.71] NLP029-1 non_thm 0.0 4 0 4 5 11 4 0 4 2 9 4 9 [0.71] NLP030-1 non_thm 0.0 4 0 5 6 12 4 0 5 2 11 5 11 [0.71] NLP034-1 timeout 299.0 11 [0.71] NLP035-1 timeout 299.0 10 [0.71] NLP060-1 non_thm 0.0 4 0 9 5 13 3 1 24 2 14 11 29 [0.71] NUM288-1 timeout 299.0 7 [0.71] SET781-1 timeout 299.0 30 [0.71] SYN764-1 non_thm 0.0 4 0 1 6 1 0 0 18 4 7 1 24 [0.71] SYN770-1 non_thm 0.0 4 0 2 1 2 0 0 13 2 3 2 14 [0.71] SYN777-1 timeout 299.0 5 [0.71] SYN778-1 non_thm 0.1 4 0 2 6 2 0 0 345 4 8 2 351 [0.71] SYN781-1 non_thm 0.0 4 0 2 5 2 0 0 26 5 7 2 31 [0.71] SYN783-1 non_thm 0.0 4 0 2 3 2 0 0 63 4 5 2 66 [0.71] SYN793-1 non_thm 0.0 4 0 2 2 2 0 0 27 3 4 2 29 [0.71] SYN799-1 timeout 298.9 7 [0.71] SYN808-1 timeout 299.0 8 [0.71] SYN810-1 timeout 298.9 9 [0.71] SYN906-1 timeout 299.0 24 [0.71] SYN913-1 timeout 299.0 40 [0.71] TOP001-1 timeout 299.0 22 [0.71] TOP002-1 timeout 299.0 22 [0.71] TOP003-1 timeout 299.0 37 [0.71] TOP006-1 timeout 299.0 94 [0.71] TOP015-1 timeout 299.0 60 [0.71] TOP018-1 timeout 299.0 64 [0.71] TOP019-1 timeout 299.0 32 [0.83] FLD012-3 timeout 299.0 53 [0.83] FLD014-1 timeout 299.0 12 [0.83] FLD028-1 timeout 299.0 15 [0.83] FLD035-1 timeout 299.0 17 [0.83] FLD036-1 timeout 298.9 17 [0.83] FLD041-1 timeout 299.0 11 [0.83] FLD044-4 timeout 299.0 38 [0.83] FLD045-4 timeout 299.0 37 [0.83] FLD062-1 timeout 298.9 11 [0.83] FLD072-3 timeout 299.0 41 [0.83] FLD072-4 timeout 299.0 62 [0.83] FLD074-3 timeout 299.0 39 [0.83] FLD087-3 timeout 299.0 48 [0.83] FLD088-3 timeout 299.0 47 [0.83] FLD089-3 timeout 299.0 47 [0.83] FLD097-4 theorem 275.0 31 1 1988 0 18 0 0 0 2 1988 245353 0 [0.83] SYN314-1.002.001 timeout 299.0 87 [0.83] SYN822-1 non_thm 7.1 19 0 696 678 88 939 0 1449 2 1374 1336 2128 [0.86] GRP025-3 timeout 298.9 33 [0.86] GRP026-3 timeout 299.0 45 [0.86] GRP027-2 timeout 299.0 14 [0.86] PUZ034-1.003 timeout 299.0 61 [0.86] SYN765-1 timeout 298.9 4 [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.0 4 0 2 2 2 0 0 122 3 4 2 124 [0.86] SYN779-1 timeout 299.0 6 [0.86] SYN782-1 timeout 299.0 8 [0.86] SYN788-1 timeout 298.9 6 [0.86] SYN789-1 timeout 299.0 6 [0.86] SYN792-1 timeout 299.0 9 [0.86] SYN795-1 non_thm 0.3 4 0 2 24 2 0 0 1115 7 26 2 1139 [0.86] SYN803-1 non_thm 0.0 4 0 2 1 2 0 0 10 2 3 2 11 [0.86] SYN805-1 timeout 299.0 30 [0.86] SYN806-1 timeout 299.0 11 [0.86] SYN807-1 non_thm 0.0 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 42 [0.86] TOP005-1 timeout 299.0 33 [0.86] TOP007-1 timeout 298.9 87 [0.86] TOP008-1 memory 233.6 399 [0.86] TOP009-1 timeout 299.0 98 [0.86] TOP012-1 timeout 299.0 116 [0.86] TOP013-1 timeout 298.9 62 [0.86] TOP017-1 timeout 299.0 114 [1.00] ANA001-1 timeout 299.0 29 [1.00] ANA005-4 timeout 299.0 27 [1.00] ANA005-5 timeout 299.0 35 [1.00] COM006-1 timeout 299.0 26 [1.00] FLD008-1 timeout 299.0 11 [1.00] FLD008-2 timeout 299.0 20 [1.00] FLD011-1 timeout 298.9 6 [1.00] FLD012-1 timeout 298.9 11 [1.00] FLD012-2 timeout 299.0 20 [1.00] FLD026-1 timeout 298.9 12 [1.00] FLD029-1 timeout 299.0 15 [1.00] FLD041-2 timeout 299.0 17 [1.00] FLD043-1 timeout 299.0 6 [1.00] FLD044-1 timeout 299.0 11 [1.00] FLD044-2 timeout 299.0 32 [1.00] FLD044-3 timeout 299.0 37 [1.00] FLD045-1 timeout 299.0 11 [1.00] FLD045-2 timeout 299.0 19 [1.00] FLD045-3 timeout 299.0 37 [1.00] FLD046-1 timeout 298.9 6 [1.00] FLD046-3 timeout 299.0 44 [1.00] FLD047-1 timeout 299.0 17 [1.00] FLD047-2 timeout 299.0 20 [1.00] FLD047-3 timeout 299.0 48 [1.00] FLD048-1 timeout 299.0 15 [1.00] FLD048-2 timeout 299.0 21 [1.00] FLD048-3 timeout 299.0 48 [1.00] FLD049-1 timeout 298.9 16 [1.00] FLD049-2 timeout 299.0 20 [1.00] FLD050-1 timeout 299.0 15 [1.00] FLD050-2 timeout 298.9 18 [1.00] FLD051-1 timeout 299.0 15 [1.00] FLD051-2 timeout 299.0 22 [1.00] FLD051-3 timeout 299.0 54 [1.00] FLD052-1 timeout 299.0 16 [1.00] FLD052-2 timeout 298.9 4 [1.00] FLD052-3 timeout 299.0 48 [1.00] FLD053-1 timeout 299.0 15 [1.00] FLD053-2 timeout 299.0 4 [1.00] FLD053-3 timeout 299.0 48 [1.00] FLD053-4 timeout 299.0 22 [1.00] FLD054-1 timeout 299.0 11 [1.00] FLD054-2 timeout 299.0 18 [1.00] FLD054-3 timeout 299.0 53 [1.00] FLD057-1 timeout 298.9 5 [1.00] FLD072-1 timeout 299.0 11 [1.00] FLD072-2 timeout 299.0 17 [1.00] FLD073-1 timeout 299.0 11 [1.00] FLD073-2 timeout 299.0 17 [1.00] FLD073-3 timeout 299.0 37 [1.00] FLD073-4 timeout 299.0 67 [1.00] FLD074-1 timeout 298.9 18 [1.00] FLD074-2 timeout 299.0 30 [1.00] FLD074-4 timeout 298.9 36 [1.00] FLD075-1 timeout 299.0 18 [1.00] FLD075-2 timeout 299.0 25 [1.00] FLD075-3 timeout 298.9 39 [1.00] FLD075-4 timeout 299.0 36 [1.00] FLD076-1 timeout 299.0 17 [1.00] FLD076-2 timeout 299.0 23 [1.00] FLD076-3 timeout 299.0 51 [1.00] FLD076-4 timeout 298.9 40 [1.00] FLD077-1 timeout 298.9 17 [1.00] FLD077-2 timeout 299.0 20 [1.00] FLD077-3 timeout 299.0 49 [1.00] FLD077-4 timeout 299.0 40 [1.00] FLD078-1 timeout 299.0 11 [1.00] FLD078-2 timeout 299.0 18 [1.00] FLD078-3 timeout 299.0 48 [1.00] FLD078-4 timeout 298.9 48 [1.00] FLD079-1 timeout 299.0 12 [1.00] FLD079-2 timeout 299.0 18 [1.00] FLD079-3 timeout 299.0 60 [1.00] FLD079-4 timeout 299.0 65 [1.00] FLD080-1 timeout 299.0 6 [1.00] FLD080-2 timeout 299.0 11 [1.00] FLD080-3 timeout 299.0 41 [1.00] FLD080-4 timeout 299.0 54 [1.00] FLD081-1 timeout 299.0 30 [1.00] FLD081-2 timeout 299.0 33 [1.00] FLD081-3 timeout 299.0 41 [1.00] FLD081-4 timeout 299.0 47 [1.00] FLD082-1 timeout 299.0 11 [1.00] FLD082-3 timeout 298.9 59 [1.00] FLD083-1 timeout 299.0 12 [1.00] FLD083-3 timeout 299.0 60 [1.00] FLD084-1 timeout 299.0 11 [1.00] FLD084-3 timeout 299.0 53 [1.00] FLD085-1 timeout 299.0 11 [1.00] FLD085-3 timeout 298.9 54 [1.00] FLD086-1 timeout 299.0 6 [1.00] FLD087-1 timeout 299.0 6 [1.00] FLD088-1 timeout 299.0 6 [1.00] FLD089-1 timeout 299.0 6 [1.00] FLD090-1 timeout 298.9 6 [1.00] FLD091-1 timeout 299.0 6 [1.00] FLD091-3 timeout 299.0 44 [1.00] FLD092-1 timeout 299.0 6 [1.00] FLD092-3 timeout 298.9 44 [1.00] FLD093-1 timeout 298.9 6 [1.00] FLD093-3 timeout 299.0 44 [1.00] FLD094-1 timeout 299.0 6 [1.00] FLD094-3 timeout 299.0 44 [1.00] FLD095-1 timeout 299.0 15 [1.00] FLD095-2 timeout 298.9 21 [1.00] FLD095-3 timeout 299.0 51 [1.00] FLD095-4 timeout 299.0 33 [1.00] FLD096-1 timeout 298.9 20 [1.00] FLD096-2 timeout 299.0 22 [1.00] FLD096-3 timeout 299.0 51 [1.00] FLD096-4 timeout 298.9 33 [1.00] FLD097-1 timeout 299.0 11 [1.00] FLD097-2 timeout 298.9 24 [1.00] FLD097-3 timeout 299.0 37 [1.00] FLD098-1 timeout 298.9 11 [1.00] FLD098-2 timeout 299.0 26 [1.00] FLD098-3 timeout 299.0 37 [1.00] FLD098-4 timeout 299.0 35 [1.00] FLD099-1 timeout 298.9 6 [1.00] FLD099-2 timeout 298.9 20 [1.00] FLD099-3 timeout 299.0 44 [1.00] FLD099-4 timeout 299.0 71 [1.00] FLD100-1 timeout 299.0 11 [1.00] FLD100-2 timeout 299.0 23 [1.00] FLD100-3 timeout 299.0 37 [1.00] FLD100-4 timeout 299.0 34 [1.00] MSC008-1.010 timeout 299.0 142