-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true -uv true Problems list file : nne-problems Output file : nne-output Summary file : nne-summary Time limit : 300 s Memory limit : 500 MB -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug [0.00] ALG002-1 theorem 0.1 2 1 45 0 4 0 0 0 3 45 280 254 0 [0.00] CAT007-3 theorem 0.0 2 1 5 0 5 0 0 0 2 5 12 2 0 [0.00] COM002-2 theorem 0.0 2 1 26 0 15 0 0 0 2 26 47 31 0 [0.00] COM003-2 theorem 0.0 2 1 12 0 17 13 1 0 2 12 24 4 0 [0.00] FLD001-3 theorem 0.0 2 1 62 0 7 0 0 0 2 62 283 229 0 [0.00] FLD005-3 theorem 0.0 2 1 91 0 6 0 0 0 2 91 629 1807 0 [0.00] FLD006-1 theorem 15.7 3 1 154 0 4 0 0 0 3 154 1362 112 0 [0.00] FLD006-3 theorem 0.0 2 1 5 0 4 0 0 0 2 5 31 12 0 [0.00] FLD009-3 theorem 0.1 2 1 112 0 7 0 0 0 2 112 907 3082 0 [0.00] FLD010-1 theorem 19.5 3 1 168 0 5 0 0 0 3 168 1396 139 0 [0.00] FLD010-3 theorem 0.0 2 1 6 0 5 0 0 0 2 6 35 16 0 [0.00] FLD013-1 theorem 3.7 2 1 272 0 10 0 0 0 2 272 1327 142 0 [0.00] FLD013-2 theorem 8.7 2 1 345 0 12 0 0 0 2 345 1638 215 0 [0.00] FLD013-3 theorem 0.7 4 1 324 0 10 0 0 0 2 324 6414 26099 0 [0.00] FLD013-4 theorem 0.0 2 1 29 0 12 0 0 0 2 29 315 91 0 [0.00] FLD013-5 theorem 0.0 2 1 27 0 14 0 0 0 2 27 334 78 0 [0.00] FLD015-3 theorem 0.0 2 1 93 0 7 0 0 0 2 93 636 1963 0 [0.00] FLD016-3 theorem 0.1 2 1 151 0 10 0 0 0 2 151 852 2207 0 [0.00] FLD016-5 theorem 0.1 2 1 204 0 12 0 0 0 2 204 1500 3867 0 [0.00] FLD017-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 310 10 0 [0.00] FLD017-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 187 21 0 [0.00] FLD018-3 theorem 0.0 2 1 73 0 6 0 0 0 2 73 1562 3247 0 [0.00] FLD019-3 theorem 0.0 2 1 14 0 6 0 0 0 2 14 96 58 0 [0.00] FLD020-3 theorem 0.0 2 1 83 0 7 0 0 0 2 83 518 1220 0 [0.00] FLD021-1 theorem 0.4 2 1 55 0 7 0 0 0 2 55 216 30 0 [0.00] FLD021-3 theorem 0.0 2 1 14 0 7 0 0 0 2 14 104 32 0 [0.00] FLD022-3 theorem 0.1 2 1 149 0 10 0 0 0 2 149 827 2064 0 [0.00] FLD023-3 theorem 0.0 2 1 86 0 7 0 0 0 2 86 738 1521 0 [0.00] FLD024-3 theorem 0.0 2 1 57 0 7 0 0 0 2 57 227 163 0 [0.00] FLD025-1 theorem 3.7 2 1 284 0 10 0 0 0 2 284 1371 142 0 [0.00] FLD025-3 theorem 0.7 4 1 324 0 10 0 0 0 2 324 6414 25873 0 [0.00] FLD025-4 theorem 0.0 2 1 36 0 12 0 0 0 2 36 336 78 0 [0.00] FLD025-5 theorem 0.0 2 1 35 0 14 0 0 0 2 35 362 102 0 [0.00] FLD027-3 theorem 0.1 2 1 149 0 9 0 0 0 2 149 1648 6548 0 [0.00] FLD028-3 theorem 0.1 2 1 181 0 11 0 0 0 2 181 1229 4214 0 [0.00] FLD030-1 theorem 0.0 2 1 9 0 8 0 0 0 2 9 149 8 0 [0.00] FLD030-2 theorem 0.0 2 1 24 0 10 0 0 0 2 24 310 10 0 [0.00] FLD030-3 theorem 0.0 2 1 25 0 8 0 0 0 2 25 188 44 0 [0.00] FLD030-4 theorem 0.0 2 1 11 0 10 0 0 0 2 11 187 17 0 [0.00] FLD031-3 theorem 0.1 2 1 83 0 7 0 0 0 2 83 2127 4850 0 [0.00] FLD031-5 theorem 0.1 2 1 100 0 7 0 0 0 2 100 2896 7441 0 [0.00] FLD032-3 theorem 0.0 2 1 18 0 7 0 0 0 2 18 110 94 0 [0.00] FLD033-3 theorem 0.1 2 1 126 0 8 0 0 0 2 126 1084 3934 0 [0.00] FLD034-1 theorem 0.4 2 1 60 0 7 0 0 0 2 60 233 35 0 [0.00] FLD034-3 theorem 0.0 2 1 18 0 7 0 0 0 2 18 120 47 0 [0.00] FLD035-3 theorem 0.1 2 1 181 0 11 0 0 0 2 181 1229 4214 0 [0.00] FLD036-3 theorem 0.1 2 1 181 0 11 0 0 0 2 181 1229 4214 0 [0.00] FLD037-3 theorem 0.1 2 1 128 0 8 0 0 0 2 128 1883 5673 0 [0.00] FLD038-3 theorem 0.0 2 1 64 0 8 0 0 0 2 64 277 302 0 [0.00] FLD039-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 65 5 0 [0.00] FLD039-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 81 64 0 [0.00] FLD043-3 theorem 0.0 2 1 107 0 7 0 0 0 2 107 851 2763 0 [0.00] FLD055-1 theorem 0.0 2 1 27 0 9 0 0 0 2 27 278 22 0 [0.00] FLD055-3 theorem 0.0 2 1 20 0 9 0 0 0 2 20 154 33 0 [0.00] FLD056-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 57 1 0 [0.00] FLD056-3 theorem 0.0 2 1 4 0 4 0 0 0 2 4 57 1 0 [0.00] FLD058-1 theorem 0.0 2 1 25 0 9 0 0 0 2 25 213 37 0 [0.00] FLD058-3 theorem 0.0 2 1 21 0 9 0 0 0 2 21 131 81 0 [0.00] FLD059-1 theorem 0.1 2 1 40 0 6 0 0 0 2 40 141 25 0 [0.00] FLD059-2 theorem 0.5 2 1 177 0 8 0 0 0 2 177 908 235 0 [0.00] FLD059-3 theorem 0.0 2 1 54 0 6 0 0 0 2 54 322 653 0 [0.00] FLD059-4 theorem 0.0 2 1 14 0 8 0 0 0 2 14 107 22 0 [0.00] FLD060-1 theorem 0.4 2 1 133 0 7 0 0 0 2 133 517 136 0 [0.00] FLD060-2 theorem 3.8 2 1 267 0 11 0 0 0 2 267 1054 182 0 [0.00] FLD060-4 theorem 0.5 3 1 313 0 11 0 0 0 2 313 3407 17592 0 [0.00] FLD061-1 theorem 3.8 2 1 245 0 10 0 0 0 2 245 889 136 0 [0.00] FLD061-4 theorem 1.1 5 1 471 0 14 0 0 0 2 471 5072 30637 0 [0.00] FLD064-3 theorem 0.1 2 1 87 0 6 0 0 0 2 87 1933 3958 0 [0.00] FLD065-3 theorem 0.0 2 1 12 0 6 0 0 0 2 12 67 15 0 [0.00] FLD067-4 theorem 0.0 2 1 107 0 9 0 0 0 2 107 531 942 0 [0.00] FLD068-4 theorem 0.0 2 1 87 0 9 0 0 0 2 87 372 179 0 [0.00] FLD069-1 theorem 0.5 2 1 98 0 9 0 0 0 2 98 401 148 0 [0.00] FLD069-3 theorem 0.0 2 1 16 0 9 0 0 0 2 16 110 27 0 [0.00] FLD070-1 theorem 0.4 2 1 60 0 8 0 0 0 2 60 220 26 0 [0.00] FLD070-2 theorem 1.4 2 1 266 0 10 0 0 0 2 266 1401 283 0 [0.00] FLD070-3 theorem 0.0 2 1 80 0 8 0 0 0 2 80 453 913 0 [0.00] FLD070-4 theorem 0.0 2 1 17 0 10 0 0 0 2 17 155 30 0 [0.00] FLD071-1 theorem 0.0 2 1 8 0 8 0 0 0 2 8 103 3 0 [0.00] FLD071-2 theorem 1.3 2 1 100 0 10 0 0 0 2 100 376 47 0 [0.00] FLD071-3 theorem 0.0 2 1 9 0 8 0 0 0 2 9 98 20 0 [0.00] FLD071-4 theorem 0.0 2 1 9 0 9 0 0 0 2 9 141 15 0 [0.00] GRA001-1 theorem 0.0 2 4 10 3 16 28 0 3 2 5 22 12 0 [0.00] GRP123-1.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 87 224 0 [0.00] GRP123-2.003 theorem 0.0 2 1 37 0 15 0 0 0 2 37 94 233 0 [0.00] GRP123-3.003 theorem 0.0 2 1 51 0 20 0 0 0 2 51 111 788 0 [0.00] GRP123-4.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 105 224 0 [0.00] GRP123-6.003 theorem 0.0 2 1 50 0 11 0 0 0 2 50 143 154 0 [0.00] GRP123-7.003 theorem 0.0 2 1 56 0 16 0 0 0 2 56 149 161 0 [0.00] GRP123-8.003 theorem 0.0 2 1 62 0 21 0 0 0 2 62 156 533 0 [0.00] GRP123-9.003 theorem 0.0 2 1 50 0 11 0 0 0 2 50 143 154 0 [0.00] GRP124-1.004 theorem 0.1 2 6 104 5 17 0 0 927 2 66 824 6101 0 [0.00] GRP124-2.004 theorem 0.0 2 1 75 0 26 0 0 0 2 75 182 525 0 [0.00] GRP124-3.004 theorem 0.1 2 4 148 4 32 0 0 694 2 115 525 4706 0 [0.00] GRP124-4.004 theorem 0.1 2 4 78 3 17 0 0 515 2 63 462 2964 0 [0.00] GRP124-6.004 theorem 0.0 2 6 141 5 18 0 0 301 2 103 769 1207 0 [0.00] GRP124-7.004 theorem 0.0 2 6 153 11 27 0 0 307 2 121 781 1220 0 [0.00] GRP124-8.004 theorem 0.1 2 6 173 67 33 0 0 1877 2 197 838 3474 0 [0.00] GRP124-9.004 theorem 0.0 2 6 141 5 18 0 0 301 2 103 769 1207 0 [0.00] GRP125-1.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 94 101 0 [0.00] GRP125-2.005 theorem 0.1 2 7 328 21 40 0 0 469 2 170 2049 3495 0 [0.00] GRP125-3.005 theorem 0.7 3 32 762 133 47 0 0 7812 2 259 6947 28766 0 [0.00] GRP125-4.003 theorem 0.0 2 1 31 0 10 0 0 0 2 31 146 168 0 [0.00] GRP126-1.004 theorem 0.0 2 6 102 8 17 0 0 169 2 66 795 1272 0 [0.00] GRP126-2.004 theorem 0.0 2 1 75 0 26 0 0 0 2 75 224 259 0 [0.00] GRP126-3.004 theorem 0.1 2 4 148 4 32 0 0 670 2 115 552 4174 0 [0.00] GRP127-1.004 theorem 0.0 2 6 104 6 17 0 0 235 2 67 711 1266 0 [0.00] GRP127-3.004 theorem 0.1 2 4 148 4 32 0 0 670 2 115 529 4156 0 [0.00] GRP128-1.003 theorem 0.1 2 25 266 28 9 0 0 353 2 38 1192 3715 0 [0.00] GRP128-4.003 theorem 0.0 2 8 49 8 9 0 0 105 2 30 354 786 0 [0.00] GRP129-1.003 theorem 0.1 2 26 312 29 9 0 0 406 2 36 1431 4116 0 [0.00] GRP129-2.004 theorem 0.6 2 105 1928 125 25 0 0 3752 2 97 9307 32872 0 [0.00] GRP129-3.004 theorem 0.3 2 22 368 134 31 0 0 4798 2 150 1619 10179 0 [0.00] GRP130-1.003 theorem 0.1 2 16 233 20 9 0 0 132 2 40 1062 2558 0 [0.00] GRP130-2.003 theorem 0.0 2 18 210 26 14 0 0 146 2 42 856 2071 0 [0.00] GRP130-3.003 theorem 0.0 2 3 100 5 19 0 0 55 2 57 298 1760 0 [0.00] GRP130-4.003 theorem 0.0 2 7 66 7 9 0 0 50 2 26 301 829 0 [0.00] GRP131-1.002 theorem 0.0 2 6 50 6 4 0 0 20 2 17 238 1126 0 [0.00] GRP131-2.002 theorem 0.0 2 6 56 8 6 0 0 22 2 23 245 1145 0 [0.00] GRP132-1.002 theorem 0.0 2 6 50 6 4 0 0 21 2 17 237 1108 0 [0.00] GRP132-2.002 theorem 0.0 2 6 56 8 6 0 0 23 2 23 245 1127 0 [0.00] GRP133-1.003 theorem 0.1 2 16 290 19 9 0 0 167 2 38 1325 2833 0 [0.00] GRP133-2.003 theorem 0.0 2 16 223 23 14 0 0 187 2 50 1005 2034 0 [0.00] GRP134-1.003 theorem 0.1 2 16 317 19 9 0 0 167 2 38 1584 3126 0 [0.00] GRP134-2.003 theorem 0.1 2 16 252 23 14 0 0 187 2 50 1223 2374 0 [0.00] GRP135-1.002 theorem 0.0 2 8 58 9 4 0 0 15 2 17 223 534 0 [0.00] GRP135-2.002 theorem 0.0 2 8 61 11 6 0 0 17 2 21 226 546 0 [0.00] HWV005-1 theorem 0.0 2 1 96 0 10 0 0 0 3 96 323 353 0 [0.00] HWV005-2 unsound 0.0 2 0 159 34 8 0 0 404 3 0 307 481 0 [0.00] HWV007-1 theorem 0.1 2 1 352 0 13 1 6 0 4 352 941 994 0 [0.00] HWV007-2 unsound 0.1 2 0 470 41 11 1 0 1026 4 0 927 1165 0 [0.00] HWV034-1 non_thm 0.0 2 0 2 2 2 0 0 10 2 0 2 12 0 [0.00] HWV034-2 non_thm 0.0 2 0 0 4 0 0 0 10 2 0 0 14 0 [0.00] KRS001-1 theorem 0.0 2 1 8 0 1 0 0 0 2 8 16 2 0 [0.00] KRS002-1 theorem 0.0 2 1 9 0 1 0 0 0 3 9 16 2 0 [0.00] KRS003-1 theorem 0.0 2 1 9 0 2 0 0 0 2 9 16 2 0 [0.00] KRS005-1 non_thm 0.0 2 0 8 2 1 0 0 38 2 0 8 40 0 [0.00] KRS006-1 non_thm 0.0 2 0 20 13 5 0 0 81 3 0 31 95 0 [0.00] KRS007-1 non_thm 0.0 2 0 27 14 2 0 0 178 3 0 37 193 0 [0.00] KRS008-1 timeout 300.0 65 [0.00] KRS009-1 non_thm 0.0 2 0 13 17 1 0 0 42 2 0 14 60 0 [0.00] KRS010-1 theorem 0.0 2 2 21 1 2 0 0 3 2 18 38 91 0 [0.00] KRS011-1 non_thm 0.0 2 0 36 11 2 0 0 76 2 0 44 95 0 [0.00] KRS012-1 theorem 0.0 2 1 5 0 2 0 0 0 2 5 10 7 0 [0.00] KRS013-1 theorem 0.0 2 1 17 0 2 0 0 0 3 17 27 14 0 [0.00] KRS014-1 non_thm 0.0 2 0 14 3 1 0 0 17 2 0 17 22 0 [0.00] KRS015-1 theorem 0.0 2 1 10 0 1 0 0 0 3 10 18 2 0 [0.00] KRS016-1 non_thm 0.0 2 0 4 3 2 0 0 5 2 0 4 10 0 [0.00] KRS017-1 theorem 0.0 2 1 3 0 2 0 0 0 2 3 7 4 0 [0.00] LCL181-2 theorem 0.0 2 1 2 0 4 2 0 0 2 2 4 1 0 [0.00] LCL230-2 theorem 0.0 2 1 3 0 3 3 0 0 2 3 6 0 0 [0.00] MGT004-1 theorem 0.0 2 1 15 0 9 0 0 0 2 15 26 3091 0 [0.00] MGT007-1 theorem 0.1 2 1 17 0 9 0 0 0 2 17 28 6853 0 [0.00] MGT016-1 theorem 0.0 2 1 16 0 13 0 0 0 2 16 26 2218 0 [0.00] MGT018-1 theorem 0.0 2 1 16 0 13 0 0 0 2 16 26 2218 0 [0.00] MGT022-1 theorem 0.0 2 4 13 4 9 8 0 6 3 9 30 32 0 [0.00] MGT022-2 theorem 0.0 2 4 13 4 9 8 0 6 3 9 30 32 0 [0.00] MGT028-1 theorem 0.0 2 5 26 5 2 0 0 1 4 12 46 286 0 [0.00] MGT030-1 theorem 0.0 2 3 17 2 2 0 0 1 4 13 34 63 0 [0.00] MGT036-1 theorem 0.0 2 1 9 0 4 0 0 0 2 9 15 3 0 [0.00] MGT036-2 theorem 0.0 2 1 9 0 4 0 0 0 2 9 16 3 0 [0.00] MGT041-2 theorem 0.0 2 1 7 0 4 0 0 0 2 7 9 6 0 [0.00] MSC001-1 theorem 0.1 2 1 65 0 5 1 2 0 5 65 235 164 0 [0.00] MSC002-1 theorem 0.0 2 1 22 0 3 1 0 0 4 22 42 12 0 [0.00] MSC002-2 theorem 0.0 2 1 22 0 3 1 0 0 4 22 42 12 0 [0.00] MSC003-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 9 2 0 [0.00] MSC004-1 theorem 0.0 2 4 15 6 2 0 0 0 3 11 27 20 0 [0.00] MSC006-1 theorem 0.0 2 8 59 12 2 0 0 60 2 24 204 347 0 [0.00] MSC009-1 non_thm 0.0 2 1 0 10 0 0 0 14 2 8 0 27 0 [0.00] NLP001-1 theorem 0.2 4 2 28 1 28 5 0 0 2 19 32 25151 0 [0.00] NLP043-1 non_thm 1.7 5 0 18 7 18 1 0 1583 2 0 18 34309 0 [0.00] NLP044-1 non_thm 1.7 5 0 18 7 18 1 0 1583 2 0 18 34309 0 [0.00] NLP045-1 non_thm 2.7 6 0 18 7 18 1 0 187 2 0 18 57349 0 [0.00] NLP046-1 non_thm 1.7 5 0 18 7 18 1 0 1583 2 0 18 34309 0 [0.00] NLP047-1 non_thm 2.7 6 0 18 7 18 1 0 187 2 0 18 57349 0 [0.00] NLP048-1 non_thm 2.4 6 0 18 7 18 1 0 6689 2 0 18 45061 0 [0.00] NLP066-1 non_thm 0.0 2 0 11 14 6 1 0 57 2 0 14 109 0 [0.00] NLP067-1 non_thm 0.0 2 0 22 14 7 1 0 86 3 0 28 345 0 [0.00] NLP068-1 non_thm 0.0 2 0 15 17 7 1 0 116 2 0 22 152 0 [0.00] NLP095-1 non_thm 8.4 8 1 38 16 30 4 0 8483 4 23 43 67306 0 [0.00] NLP096-1 non_thm 8.4 8 1 38 16 30 4 0 8483 4 23 43 67306 0 [0.00] NLP097-1 non_thm 0.0 2 0 11 11 8 1 0 41 2 0 12 88 0 [0.00] NLP098-1 non_thm 0.0 2 0 11 11 8 1 0 41 2 0 12 88 0 [0.00] NLP099-1 non_thm 0.0 2 0 8 12 9 1 0 62 2 0 8 138 0 [0.00] NLP100-1 non_thm 0.3 3 0 18 8 13 1 0 352 2 0 18 5746 0 [0.00] NLP101-1 non_thm 0.3 3 0 18 8 13 1 0 352 2 0 18 5746 0 [0.00] NLP102-1 non_thm 0.3 3 0 15 8 13 1 0 2322 2 0 15 5644 0 [0.00] NLP103-1 non_thm 1.0 8 1 22 12 23 5 0 94 3 20 27 49804 0 [0.00] NLP114-1 non_thm 2.6 7 1 34 6 35 4 0 11269 2 19 36 96261 0 [0.00] NLP115-1 non_thm 1.3 10 1 34 6 35 4 0 145 2 19 36 85509 0 [0.00] NLP116-1 non_thm 2.1 6 0 18 6 19 1 0 11271 2 0 18 30724 0 [0.00] NLP117-1 theorem 1.0 9 2 34 1 34 5 0 0 2 19 38 131077 0 [0.00] NLP118-1 non_thm 2.0 6 0 18 6 19 1 0 11271 2 0 18 30724 0 [0.00] NLP119-1 non_thm 0.9 5 0 18 6 19 1 0 147 2 0 18 19972 0 [0.00] NLP120-1 non_thm 1.9 10 1 34 6 35 4 0 8965 2 19 36 85509 0 [0.00] NLP121-1 non_thm 2.0 6 0 18 6 19 1 0 11271 2 0 18 30724 0 [0.00] NLP122-1 theorem 1.0 9 2 34 1 34 5 0 0 2 19 38 131077 0 [0.00] NLP123-1 non_thm 1.9 10 1 34 6 35 4 0 8965 2 19 36 85509 0 [0.00] NLP130-1 non_thm 69.6 98 0 30 6 22 1 0 85 3 0 32 524816 0 [0.00] NLP131-1 non_thm 16.4 48 0 21 6 22 1 0 1135 2 0 21 245764 0 [0.00] NLP132-1 non_thm 8.5 26 0 24 13 22 1 0 593 2 0 25 122908 0 [0.00] NLP133-1 non_thm 17.0 26 0 30 8 22 1 0 593 3 0 32 123408 0 [0.00] NLP134-1 non_thm 16.3 48 0 21 6 22 1 0 1135 2 0 21 245764 0 [0.00] NLP135-1 non_thm 69.7 103 0 30 6 22 1 0 85 3 0 32 524432 0 [0.00] NLP136-1 non_thm 16.0 48 0 21 6 22 1 0 1135 2 0 21 245764 0 [0.00] NLP137-1 non_thm 8.3 26 0 24 13 22 1 0 593 2 0 25 122908 0 [0.00] NLP138-1 non_thm 17.3 34 0 21 6 22 1 0 71695 2 0 21 159748 0 [0.00] NLP139-1 non_thm 8.8 19 0 24 13 22 1 0 35873 2 0 25 79900 0 [0.00] NLP221-1 memory 47.0 499 [0.00] NLP222-1 memory 46.6 499 [0.00] NLP223-1 non_thm 82.1 94 0 19 29 22 1 0 106726 2 0 19 1128970 0 [0.00] NLP230-1 memory 71.8 499 [0.00] NLP231-1 memory 71.5 499 [0.00] NLP232-1 memory 73.2 499 [0.00] NLP233-1 memory 71.4 499 [0.00] NLP235-1 memory 71.5 499 [0.00] NLP236-1 memory 73.5 499 [0.00] NLP238-1 memory 67.0 499 [0.00] NLP239-1 memory 72.7 499 [0.00] NUM014-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 11 12 0 [0.00] NUM015-1 theorem 0.0 2 1 11 0 2 0 0 0 3 11 21 8 0 [0.00] NUM016-1 theorem 0.0 2 1 14 0 4 0 0 0 3 14 36 30 0 [0.00] NUM016-2 theorem 0.0 2 1 12 0 2 0 0 0 3 12 18 12 0 [0.00] NUM021-1 theorem 0.4 2 1 80 0 9 0 0 0 3 80 405 233 0 [0.00] NUM022-1 theorem 0.0 2 1 9 0 3 0 0 0 3 9 14 12 0 [0.00] NUM025-2 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 1 0 [0.00] NUM027-1 theorem 0.0 2 1 49 0 10 0 0 0 2 49 247 178 0 [0.00] NUM285-1 non_thm 0.0 2 0 9 3 14 25 0 3 2 0 9 7 0 [0.00] PLA002-1 theorem 0.0 2 1 7 0 6 8 0 0 2 7 10 7 0 [0.00] PLA002-2 theorem 0.9 4 1 1994 0 2 0 0 0 5 1994 2625 1460 0 [0.00] PUZ001-1 theorem 0.0 2 1 17 0 5 2 0 0 2 17 20 17 0 [0.00] PUZ001-3 non_thm 0.0 2 0 19 3 6 2 0 20 2 0 22 26 0 [0.00] PUZ002-1 theorem 0.0 2 1 11 0 2 0 0 0 2 11 13 7 0 [0.00] PUZ004-1 theorem 0.0 2 1 10 0 10 11 0 0 2 10 12 9 0 [0.00] PUZ005-1 theorem 0.0 2 2 26 1 3 0 0 2 2 21 83 85 0 [0.00] PUZ009-1 theorem 0.0 2 1 5 0 6 11 0 0 2 5 11 10 0 [0.00] PUZ012-1 theorem 0.0 2 1 20 0 13 1 0 0 2 20 36 22 0 [0.00] PUZ013-1 theorem 0.0 2 1 7 0 10 10 0 0 2 7 12 6 0 [0.00] PUZ014-1 theorem 0.0 2 2 16 1 21 22 0 0 2 13 23 10 0 [0.00] PUZ015-2.006 theorem 0.1 2 137 2691 136 2967 5778 0 1410 2 59 3410 2240 0 [0.00] PUZ016-2.004 non_thm 0.0 2 0 23 1 29 40 0 51 2 0 26 58 0 [0.00] PUZ016-2.005 theorem 0.0 2 20 332 19 375 685 0 149 2 40 390 317 0 [0.00] PUZ021-1 theorem 0.0 2 6 75 9 0 0 8 25 3 27 359 671 0 [0.00] PUZ023-1 theorem 0.0 2 2 12 3 10 8 0 4 2 13 44 69 0 [0.00] PUZ024-1 theorem 0.0 2 1 7 0 9 7 0 0 2 7 19 16 0 [0.00] PUZ025-1 theorem 0.0 2 2 19 2 7 4 0 8 2 20 67 74 0 [0.00] PUZ026-1 theorem 0.0 2 5 34 4 9 1 2 0 2 18 126 182 0 [0.00] PUZ027-1 theorem 0.0 2 4 18 3 13 15 0 5 2 12 82 119 0 [0.00] PUZ028-1 non_thm 0.0 2 12 55 46 11 0 0 372 2 93 343 752 0 [0.00] PUZ028-2 non_thm 0.0 2 6 76 27 36 0 0 296 2 101 274 665 0 [0.00] PUZ028-3 non_thm 0.0 2 0 81 27 108 162 0 446 2 0 108 666 0 [0.00] PUZ028-4 non_thm 0.0 2 0 35 19 54 108 0 234 2 0 54 387 0 [0.00] PUZ028-5 theorem 0.1 2 44 786 43 11 0 0 1540 2 94 1896 5291 0 [0.00] PUZ029-1 theorem 0.0 2 1 13 0 4 0 0 0 2 13 17 10 0 [0.00] PUZ030-1 theorem 0.0 2 9 144 9 158 165 0 29 2 27 354 366 0 [0.00] PUZ030-2 theorem 0.0 2 6 30 5 40 125 0 6 2 10 74 82 0 [0.00] PUZ031-1 theorem 0.0 2 1 33 0 6 0 0 0 2 33 56 406 0 [0.00] PUZ032-1 theorem 0.0 2 2 16 1 4 0 0 17 3 16 54 56 0 [0.00] PUZ033-1 theorem 0.0 2 1 11 0 11 17 0 0 2 11 15 5 0 [0.00] PUZ035-1 theorem 0.0 2 3 3 2 7 7 0 0 2 5 11 8 0 [0.00] PUZ035-2 theorem 0.0 2 3 3 2 7 7 0 0 2 5 11 8 0 [0.00] PUZ035-3 theorem 0.0 2 3 3 2 5 2 0 0 2 5 12 17 0 [0.00] PUZ035-5 theorem 0.0 2 2 2 1 3 0 0 0 2 3 7 8 0 [0.00] PUZ035-6 theorem 0.0 2 2 2 1 3 0 0 0 2 3 7 9 0 [0.00] PUZ035-7 theorem 0.0 2 3 7 2 3 0 0 1 3 9 35 20 0 [0.00] PUZ044-1 non_thm 0.0 2 0 0 3 0 0 0 10 3 0 0 16 0 [0.00] PUZ045-1 non_thm 0.0 2 0 0 2 0 0 0 4 2 0 0 6 0 [0.00] SET001-1 theorem 0.0 2 1 4 0 3 0 0 0 2 4 8 3 0 [0.00] SET002-1 theorem 0.0 2 2 9 1 2 0 0 0 2 7 21 15 0 [0.00] SET003-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 9 5 0 [0.00] SET004-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 8 5 0 [0.00] SET005-1 theorem 0.0 2 2 135 1 4 0 0 0 2 131 378 595 0 [0.00] SET006-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 10 5 0 [0.00] SET007-1 theorem 0.1 2 3 578 2 5 0 38 0 2 339 2353 3560 0 [0.00] SET008-1 theorem 0.0 2 1 10 0 3 0 0 0 2 10 34 38 0 [0.00] SET009-1 theorem 0.0 2 1 22 0 4 0 0 0 2 22 42 50 0 [0.00] SET011-1 theorem 0.0 2 2 73 1 3 0 0 0 2 67 239 372 0 [0.00] SET014-2 theorem 248.2 17 1 294 0 6 0 0 0 3 294 11114 6223 0 [0.00] SET043-5 theorem 0.0 2 4 0 3 0 0 0 0 2 2 8 9 0 [0.00] SET044-5 theorem 0.0 2 8 8 13 0 0 0 18 2 6 32 79 0 [0.00] SET045-5 theorem 0.0 2 5 2 5 1 0 0 7 2 6 15 35 0 [0.00] SET046-5 theorem 0.0 2 4 4 3 0 0 0 0 2 4 18 45 0 [0.00] SET047-5 theorem 0.0 2 4 6 3 4 4 0 1 2 4 24 18 0 [0.00] SET055-6 theorem 2.4 5 2 1449 1 30 0 2 15015 2 1450 18448 17058 0 [0.00] SET055-7 theorem 0.0 2 1 5 0 5 0 0 0 2 5 47 5 0 [0.00] SET777-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] SET778-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] SET779-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.00] SET780-1 non_thm 0.0 2 0 0 1 0 0 0 3 2 0 0 4 0 [0.00] SET786-1 theorem 0.0 2 6 6 6 0 0 0 9 2 5 24 81 0 [0.00] SWV001-1 theorem 0.0 2 2 15 1 2 0 0 0 2 11 61 53 0 [0.00] SWV009-1 theorem 0.0 2 1 9 0 5 0 0 0 2 9 12 16 0 [0.00] SYN001-1.005 theorem 0.0 2 16 16 15 46 118 0 0 2 5 96 31 0 [0.00] SYN006-1 theorem 0.0 2 1 6 0 4 1 0 0 3 6 7 0 0 [0.00] SYN008-1 theorem 0.0 2 1 3 0 3 4 0 0 2 3 6 0 0 [0.00] SYN009-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 18 0 0 [0.00] SYN009-2 theorem 0.0 2 1 7 0 4 0 0 0 2 7 9 6 0 [0.00] SYN009-3 theorem 0.0 2 1 9 0 5 1 0 0 2 9 11 6 0 [0.00] SYN009-4 theorem 0.0 2 1 8 0 4 0 0 0 2 8 10 6 0 [0.00] SYN011-1 theorem 0.0 2 2 6 1 8 9 0 2 2 5 10 8 0 [0.00] SYN012-1 theorem 0.1 2 9 0 41 0 0 0 169 5 17 0 269 0 [0.00] SYN014-2 theorem 0.0 2 1 8 0 7 0 0 0 2 8 37 19 0 [0.00] SYN015-2 theorem 0.0 2 1 33 0 7 0 0 0 2 33 149 152 0 [0.00] SYN028-1 theorem 0.0 2 1 5 0 5 7 0 0 2 5 7 3 0 [0.00] SYN029-1 theorem 0.0 2 2 3 1 5 8 0 0 2 3 8 3 0 [0.00] SYN030-1 theorem 0.0 2 5 6 4 14 21 0 0 2 4 21 12 0 [0.00] SYN031-1 theorem 0.0 2 5 7 5 0 0 0 7 2 5 28 45 0 [0.00] SYN032-1 theorem 0.0 2 3 4 2 8 11 0 0 2 4 11 6 0 [0.00] SYN034-1 theorem 0.0 2 6 6 6 0 0 0 9 2 5 24 81 0 [0.00] SYN036-2 non_thm 0.0 2 0 0 1 22 35 0 0 2 0 0 1 0 [0.00] SYN038-1 theorem 0.1 2 9 0 41 0 0 0 169 5 17 0 269 0 [0.00] SYN044-1 theorem 0.0 2 2 4 1 6 9 0 0 2 3 8 5 0 [0.00] SYN045-1 theorem 0.0 2 1 3 0 3 3 0 0 2 3 5 2 0 [0.00] SYN047-1 theorem 0.0 2 1 4 0 4 6 0 0 2 4 7 2 0 [0.00] SYN051-1 theorem 0.0 2 2 3 1 6 6 1 0 2 3 7 4 0 [0.00] SYN052-1 theorem 0.0 2 2 2 1 4 7 0 0 2 2 6 3 0 [0.00] SYN053-1 theorem 0.0 2 2 2 1 5 4 1 0 2 3 8 2 0 [0.00] SYN054-1 theorem 0.0 2 5 10 9 4 2 0 1 2 8 18 26 0 [0.00] SYN055-1 theorem 0.0 2 1 9 0 3 0 0 0 2 9 12 10 0 [0.00] SYN056-1 non_thm 0.0 1 1 10 4 9 1 0 11 2 6 21 34 0 [0.00] SYN059-1 non_thm 0.0 2 7 26 7 19 35 0 12 2 11 113 81 0 [0.00] SYN060-1 theorem 0.0 2 1 3 0 1 0 0 0 2 3 5 3 0 [0.00] SYN061-1 theorem 0.0 2 1 5 0 2 0 0 0 2 5 7 6 0 [0.00] SYN063-1 theorem 0.0 2 1 2 0 2 5 0 0 2 2 6 2 0 [0.00] SYN066-1 theorem 0.0 1 1 4 0 5 3 1 0 2 4 6 2 0 [0.00] SYN069-1 theorem 0.0 2 1 9 0 1 0 0 0 2 9 16 10 0 [0.00] SYN070-1 theorem 0.0 2 1 15 0 4 0 0 0 2 15 37 49 0 [0.00] SYN081-1 theorem 0.0 2 2 0 4 0 0 0 4 3 3 0 10 0 [0.00] SYN082-1 theorem 0.0 2 2 2 1 3 2 0 0 3 2 10 8 0 [0.00] SYN084-1 non_thm 0.0 2 0 1 0 1 4 0 0 2 0 1 0 0 [0.00] SYN084-2 theorem 0.0 2 2 9 1 6 10 0 0 3 7 15 6 0 [0.00] SYN091-1.003 non_thm 0.0 2 0 2 4 6 6 0 2 2 0 2 6 0 [0.00] SYN092-1.003 non_thm 0.0 2 0 0 9 9 7 0 6 2 0 0 15 0 [0.00] SYN093-1.002 theorem 0.0 2 2 7 1 9 12 0 3 2 7 13 10 0 [0.00] SYN094-1.005 theorem 0.2 2 593 3402 815 4809 6997 0 3413 2 50 5219 6012 0 [0.00] SYN097-1.002 theorem 0.0 2 2 14 1 16 20 0 3 2 12 20 13 0 [0.00] SYN098-1.002 theorem 0.0 2 35 270 131 435 485 0 201 2 32 406 459 0 [0.00] SYN099-1.003 theorem 0.0 2 1 16 0 14 2 0 0 2 16 35 11 0 [0.00] SYN100-1.005 theorem 0.0 2 1 42 0 8 0 0 0 2 42 83 38 0 [0.00] SYN304-1 non_thm 0.0 2 0 6 0 6 0 0 0 2 0 9 0 0 [0.00] SYN306-1 timeout 300.0 5 [0.00] SYN308-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 [0.00] SYN309-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.00] SYN315-1 theorem 0.0 2 2 2 1 3 3 0 0 2 2 7 3 0 [0.00] SYN316-1 timeout 300.0 2 [0.00] SYN317-1 non_thm 0.0 2 0 2 0 3 3 0 0 2 0 2 0 0 [0.00] SYN319-1 theorem 0.0 2 1 3 0 3 1 0 0 2 3 5 3 0 [0.00] SYN320-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.00] SYN321-1 theorem 0.0 2 2 2 1 4 3 0 0 2 2 6 3 0 [0.00] SYN323-1 theorem 0.0 2 3 2 3 0 0 0 0 2 3 6 5 0 [0.00] SYN324-1 timeout 300.0 2 [0.00] SYN325-1 theorem 0.0 2 1 2 0 1 1 0 0 2 2 3 0 0 [0.00] SYN326-1 theorem 0.0 2 1 4 0 3 3 0 0 2 4 6 2 0 [0.00] SYN327-1 theorem 0.0 2 4 4 3 0 0 0 2 2 4 22 35 0 [0.00] SYN328-1 theorem 0.0 2 7 0 32 0 0 0 28 6 11 0 81 0 [0.00] SYN330-1 timeout 300.0 26 [0.00] SYN331-1 theorem 0.0 2 1 6 0 4 0 0 0 4 6 15 4 0 [0.00] SYN332-1 theorem 0.8 2 3 0 98 0 0 0 2356 5 96 0 3503 0 [0.00] SYN334-1 theorem 0.1 2 9 0 41 0 0 0 169 5 17 0 267 0 [0.00] SYN335-1 timeout 300.0 16 [0.00] SYN343-1 theorem 0.0 2 2 1 1 4 5 0 0 2 2 6 3 0 [0.00] SYN344-1 non_thm 0.0 2 0 3 1 4 2 1 1 2 0 3 2 0 [0.00] SYN345-1 theorem 0.0 2 4 5 3 10 16 0 0 2 4 20 13 0 [0.00] SYN347-1 theorem 0.0 2 10 6 12 2 2 0 8 2 6 46 54 0 [0.00] SYN348-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 [0.00] SYN349-1 theorem 0.0 2 17 0 29 0 0 0 96 3 9 0 346 0 [0.00] SYN350-1 theorem 0.0 2 11 8 13 0 0 0 142 3 9 52 271 0 [0.00] SYN351-1 timeout 300.0 21 [0.00] SYN352-1 theorem 0.0 2 4 5 7 1 0 0 24 3 11 8 64 0 [0.00] SYN354-1 theorem 0.0 2 4 3 5 3 2 0 3 2 7 23 16 0 [0.00] SYN419-1 non_thm 0.0 2 0 97 40 89 87 0 110 2 0 97 160 0 [0.00] SYN422-1 non_thm 0.1 2 0 74 17 60 80 0 80 2 0 76 105 0 [0.00] SYN425-1 non_thm 0.1 2 0 152 77 106 97 0 200 2 0 166 352 0 [0.00] SYN430-1 non_thm 0.0 2 1 25 23 43 32 0 146 2 22 45 350 0 [0.00] SYN431-1 non_thm 0.0 2 5 71 26 89 47 0 256 2 52 165 600 0 [0.00] SYN432-1 non_thm 0.0 2 3 40 25 61 43 0 48 2 32 67 188 0 [0.00] SYN433-1 non_thm 0.0 2 0 14 18 31 27 0 16 2 0 17 37 0 [0.00] SYN445-1 theorem 6.3 3 431 7424 482 6651 3380 0 37208 2 89 24721 278861 0 [0.00] SYN462-1 theorem 20.5 5 956 17468 1191 16360 7389 0 104602 2 91 56536 1572442 0 [0.00] SYN490-1 non_thm 0.0 2 0 9 10 19 15 0 8 2 0 9 18 0 [0.00] SYN491-1 non_thm 0.0 2 0 9 6 15 12 0 4 2 0 9 10 0 [0.00] SYN492-1 non_thm 0.0 2 0 5 12 17 17 0 10 2 0 5 22 0 [0.00] SYN493-1 non_thm 0.0 2 0 5 8 13 13 0 6 2 0 5 14 0 [0.00] SYN494-1 non_thm 0.0 2 0 9 9 18 14 0 5 2 0 9 17 0 [0.00] SYN495-1 non_thm 0.0 2 0 24 12 33 20 0 14 2 0 28 35 0 [0.00] SYN496-1 non_thm 0.0 2 0 9 8 17 14 0 13 2 0 9 23 0 [0.00] SYN497-1 non_thm 0.0 2 0 9 10 19 14 0 6 2 0 11 17 0 [0.00] SYN515-1 non_thm 0.0 2 0 10 6 16 16 0 13 2 0 10 22 0 [0.00] SYN516-1 non_thm 0.0 2 0 3 3 6 8 0 6 2 0 3 9 0 [0.00] SYN517-1 non_thm 0.0 2 0 11 4 14 17 0 7 2 0 11 12 0 [0.00] SYN521-1 non_thm 0.0 2 0 13 8 19 16 0 21 2 0 13 34 0 [0.00] SYN522-1 non_thm 0.0 2 0 21 7 20 22 0 36 2 0 23 43 0 [0.00] SYN523-1 non_thm 0.0 2 0 5 11 12 15 0 7 2 0 5 18 0 [0.00] SYN524-1 non_thm 0.0 2 0 6 4 10 21 0 5 2 0 6 11 0 [0.00] SYN525-1 non_thm 0.0 2 0 13 5 18 20 0 10 2 0 13 15 0 [0.00] SYN526-1 non_thm 0.0 2 0 19 10 19 27 0 19 2 0 21 37 0 [0.00] SYN527-1 non_thm 0.0 2 0 0 2 2 7 0 7 2 0 0 9 0 [0.00] SYN528-1 non_thm 0.0 2 4 20 29 19 29 0 45 2 41 41 126 0 [0.00] SYN529-1 non_thm 0.0 2 0 11 6 17 19 0 5 2 0 11 11 0 [0.00] SYN530-1 non_thm 0.0 2 0 13 3 16 16 0 10 2 0 13 15 0 [0.00] SYN531-1 non_thm 0.0 2 0 6 3 9 14 0 11 2 0 6 14 0 [0.00] SYN532-1 non_thm 0.0 2 0 30 7 34 30 0 16 2 0 30 23 0 [0.00] SYN533-1 non_thm 0.0 2 0 13 3 16 12 0 9 2 0 13 12 0 [0.00] SYN534-1 non_thm 0.0 2 0 8 3 11 22 0 7 2 0 8 11 0 [0.00] SYN535-1 non_thm 0.0 2 0 14 7 20 22 0 34 2 0 14 43 0 [0.00] SYN536-1 non_thm 0.0 2 0 7 3 10 18 0 9 2 0 7 12 0 [0.00] SYN537-1 non_thm 0.0 2 0 15 8 13 31 0 26 2 0 15 37 0 [0.00] SYN538-1 non_thm 0.0 2 0 23 9 24 38 0 23 2 0 23 43 0 [0.00] SYN539-1 non_thm 0.0 2 0 17 5 20 22 0 23 2 0 17 29 0 [0.00] SYN540-1 non_thm 0.0 2 4 38 15 32 43 0 36 2 37 64 63 0 [0.00] SYN541-1 non_thm 0.0 2 0 11 10 18 36 0 21 2 0 11 36 0 [0.00] SYN554-1 theorem 0.0 2 1 10 0 4 0 0 0 2 10 43 41 0 [0.00] SYN567-1 theorem 0.0 2 1 8 0 7 0 0 0 4 8 25 9 0 [0.00] SYN568-1 timeout 300.0 96 [0.00] SYN571-1 theorem 0.2 2 1 23 0 6 0 0 0 3 23 74 72 0 [0.00] SYN573-1 theorem 0.0 2 1 8 0 5 0 0 0 2 8 23 14 0 [0.00] SYN574-1 theorem 0.0 2 2 18 1 8 0 0 0 3 17 63 50 0 [0.00] SYN575-1 theorem 0.0 2 2 18 1 8 0 0 0 3 17 63 50 0 [0.00] SYN576-1 theorem 0.4 3 1 118 0 8 0 0 0 4 118 2989 23 0 [0.00] SYN578-1 theorem 0.0 2 2 54 1 9 0 0 0 3 53 298 51 0 [0.00] SYN579-1 theorem 0.0 2 2 54 1 9 0 0 0 3 53 298 51 0 [0.00] SYN580-1 theorem 0.0 2 1 21 0 8 0 0 0 2 21 65 81 0 [0.00] SYN581-1 theorem 0.2 2 1 34 0 9 0 0 0 3 34 205 93 0 [0.00] SYN582-1 theorem 0.1 2 1 28 0 9 0 0 0 3 28 157 90 0 [0.00] SYN583-1 theorem 0.7 2 1 27 0 9 0 0 0 3 27 236 22 0 [0.00] SYN585-1 timeout 300.0 60 [0.00] SYN586-1 theorem 0.0 2 1 42 0 9 0 0 0 3 42 205 19 0 [0.00] SYN587-1 theorem 0.0 2 1 23 0 9 0 0 0 2 23 78 22 0 [0.00] SYN591-1 theorem 0.0 2 1 29 0 13 0 0 0 3 29 98 37 0 [0.00] SYN592-1 theorem 0.0 2 1 25 0 13 0 0 0 3 25 79 35 0 [0.00] SYN593-1 theorem 0.0 2 1 10 0 10 0 0 0 2 10 31 12 0 [0.00] SYN594-1 timeout 300.0 219 [0.00] SYN595-1 timeout 300.0 79 [0.00] SYN604-1 timeout 300.0 32 [0.00] SYN605-1 theorem 0.3 4 1 131 0 12 1 0 0 4 131 2980 18 0 [0.00] SYN606-1 timeout 300.0 18 [0.00] SYN608-1 theorem 0.4 4 1 153 0 12 1 0 0 4 153 3412 18 0 [0.00] SYN613-1 theorem 0.0 2 1 14 0 10 0 0 0 3 14 47 19 0 [0.00] SYN619-1 theorem 0.0 2 1 23 0 8 0 0 0 4 23 115 40 0 [0.00] SYN620-1 theorem 0.0 2 1 67 0 13 0 0 0 4 67 283 11 0 [0.00] SYN621-1 timeout 300.0 187 [0.00] SYN622-1 theorem 0.2 2 1 17 0 12 0 0 0 4 17 107 10 0 [0.00] SYN623-1 theorem 6.0 4 1 513 0 15 0 0 0 4 513 13804 332 0 [0.00] SYN624-1 timeout 300.0 22 [0.00] SYN625-1 timeout 300.0 16 [0.00] SYN626-1 theorem 0.1 2 1 24 0 10 0 0 0 5 24 83 35 0 [0.00] SYN627-1 theorem 22.4 6 1 36 0 10 0 0 0 3 36 215 64 0 [0.00] SYN633-1 theorem 3.8 3 1 186 0 9 0 0 0 6 186 3919 1286 0 [0.00] SYN641-1 theorem 6.4 3 1 178 0 15 0 0 0 4 178 1115 36 0 [0.00] SYN642-1 theorem 6.3 3 1 170 0 15 0 0 0 4 170 1091 36 0 [0.00] SYN643-1 theorem 0.2 2 1 174 0 15 0 0 0 4 174 1103 36 0 [0.00] SYN644-1 timeout 300.0 10 [0.00] SYN656-1 theorem 1.9 2 1 38 0 18 0 0 0 5 38 119 127 0 [0.00] SYN657-1 timeout 300.0 113 [0.00] SYN658-1 timeout 300.0 114 [0.00] SYN659-1 timeout 300.0 35 [0.00] SYN660-1 theorem 0.1 2 1 91 0 23 0 0 0 3 91 466 54 0 [0.00] SYN661-1 theorem 0.0 2 1 82 0 23 0 0 0 3 82 434 13 0 [0.00] SYN662-1 theorem 0.0 2 1 59 0 23 0 0 0 3 59 214 50 0 [0.00] SYN663-1 theorem 0.0 2 1 50 0 23 0 0 0 3 50 184 11 0 [0.00] SYN664-1 theorem 0.1 2 1 91 0 23 0 0 0 3 91 466 54 0 [0.00] SYN665-1 theorem 0.1 2 1 82 0 23 0 0 0 3 82 434 13 0 [0.00] SYN666-1 theorem 0.0 2 1 61 0 23 0 0 0 3 61 249 34 0 [0.00] SYN667-1 theorem 0.0 2 1 56 0 23 0 0 0 3 56 235 15 0 [0.00] SYN668-1 theorem 0.0 2 1 61 0 23 0 0 0 3 61 249 34 0 [0.00] SYN669-1 theorem 0.0 2 1 56 0 23 0 0 0 3 56 235 15 0 [0.00] SYN670-1 theorem 0.0 2 1 33 0 23 0 0 0 3 33 85 30 0 [0.00] SYN671-1 theorem 0.0 2 1 28 0 23 0 0 0 3 28 73 13 0 [0.00] SYN672-1 theorem 5.6 3 1 30 0 22 0 0 0 4 30 91 20 0 [0.00] SYN674-1 theorem 0.1 2 1 92 0 24 0 0 0 3 92 467 56 0 [0.00] SYN675-1 theorem 0.0 2 1 83 0 24 0 0 0 3 83 435 15 0 [0.00] SYN676-1 theorem 0.0 2 1 60 0 24 0 0 0 3 60 215 52 0 [0.00] SYN677-1 theorem 0.0 2 1 51 0 24 0 0 0 3 51 185 13 0 [0.00] SYN678-1 theorem 0.1 2 1 92 0 24 0 0 0 3 92 467 56 0 [0.00] SYN679-1 theorem 0.1 2 1 83 0 24 0 0 0 3 83 435 15 0 [0.00] SYN680-1 theorem 0.0 2 1 92 0 24 0 0 0 3 92 467 56 0 [0.00] SYN681-1 theorem 0.0 2 1 83 0 24 0 0 0 3 83 435 15 0 [0.00] SYN682-1 theorem 0.1 2 1 92 0 24 0 0 0 3 92 467 56 0 [0.00] SYN683-1 theorem 0.1 2 1 83 0 24 0 0 0 3 83 435 15 0 [0.00] SYN684-1 theorem 0.0 2 1 60 0 24 0 0 0 3 60 215 52 0 [0.00] SYN685-1 theorem 0.0 2 1 51 0 24 0 0 0 3 51 185 13 0 [0.00] SYN686-1 theorem 0.4 2 1 64 0 22 0 0 0 4 64 521 6 0 [0.00] SYN692-1 timeout 300.0 19 [0.00] SYN693-1 timeout 300.0 19 [0.00] SYN694-1 timeout 300.0 20 [0.00] SYN695-1 timeout 300.0 21 [0.00] SYN696-1 timeout 300.0 20 [0.00] SYN697-1 timeout 300.0 20 [0.00] SYN698-1 timeout 300.0 21 [0.00] SYN699-1 timeout 300.0 21 [0.00] SYN700-1 timeout 300.0 20 [0.00] SYN701-1 timeout 300.0 19 [0.00] SYN710-1 theorem 0.0 2 1 53 0 26 0 0 0 4 53 154 98 0 [0.00] SYN713-1 theorem 0.1 2 1 60 0 40 0 0 0 4 60 200 18 0 [0.00] SYN714-1 theorem 0.0 2 1 38 0 31 0 0 0 3 38 136 30 0 [0.00] SYN717-1 theorem 0.0 2 1 50 0 46 0 0 0 2 50 131 5 0 [0.00] SYN718-1 theorem 2.7 5 1 144 0 43 0 0 0 4 144 672 93 0 [0.00] SYN724-1 theorem 0.0 2 2 5 1 4 7 0 0 2 4 10 4 0 [0.00] SYN726-1 theorem 0.0 2 8 59 12 2 0 0 60 2 24 204 347 0 [0.00] SYN728-1 theorem 0.0 2 2 4 1 6 5 1 0 2 4 8 5 0 [0.00] SYN734-1 non_thm 0.0 2 0 1 1 1 0 0 5 2 0 1 6 0 [0.00] SYN735-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 [0.00] SYN738-1 non_thm 0.0 2 0 1 2 1 0 0 6 2 0 1 8 0 [0.00] SYN740-1 non_thm 0.0 2 0 1 3 1 0 0 93 2 0 1 96 0 [0.00] SYN743-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 [0.00] SYN744-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 [0.00] SYN756-1 non_thm 0.0 2 0 1 3 1 0 0 117 2 0 1 120 0 [0.00] SYN772-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.00] SYN811-1 non_thm 1.3 5 0 376 85 52 489 5 407 2 0 712 706 0 [0.00] SYN819-1 theorem 1.5 5 14 188 678 36 269 130 1008 2 361 362 2248 0 [0.00] SYN823-1 non_thm 0.4 3 0 160 76 32 249 0 253 2 0 288 381 0 [0.00] SYN824-1 non_thm 3.4 9 0 515 44 65 896 0 510 2 0 965 831 0 [0.00] SYN827-1 non_thm 1.0 4 4 188 202 36 269 1 609 2 286 344 1004 0 [0.00] SYN833-1 theorem 5.2 5 181 188 3294 36 269 0 4737 2 449 521 9607 0 [0.00] SYN834-1 theorem 2.6 5 72 188 1270 36 269 14 2287 2 399 412 4193 0 [0.00] SYN835-1 non_thm 1.0 4 19 188 321 36 269 8 555 2 331 359 1097 0 [0.00] SYN836-1 theorem 0.7 4 9 188 179 36 269 4 387 2 286 349 743 0 [0.00] SYN837-1 theorem 14.4 9 109 376 4297 52 489 82 6551 2 828 809 12458 0 [0.00] SYN844-1 theorem 7.0 6 122 188 3414 36 269 64 5890 2 427 462 13395 0 [0.00] SYN845-1 theorem 90.5 11 1492 188 42397 36 269 564 93713 2 538 1832 170381 0 [0.00] SYN847-1 theorem 8.4 9 74 376 2213 52 489 30 3970 2 889 774 7171 0 [0.00] SYN848-1 theorem 3.5 8 21 376 809 52 489 8 1262 2 652 721 2762 0 [0.00] SYN849-1 theorem 6.6 8 76 376 2180 52 489 26 2786 2 651 776 6471 0 [0.00] SYN856-1 theorem 4.7 6 130 188 2154 36 269 7 3850 2 408 470 8040 0 [0.00] SYN857-1 theorem 104.5 11 1423 188 41965 36 269 1239 100251 2 582 1763 173192 0 [0.00] SYN858-1 theorem 11.4 9 110 376 3505 52 489 53 5068 2 737 810 10690 0 [0.00] SYN859-1 theorem 4.6 8 46 376 1092 52 489 5 1825 2 607 746 3927 0 [0.00] SYN860-1 theorem 32.8 10 265 376 7278 52 489 188 14703 2 893 965 25274 0 [0.00] SYN867-1 non_thm 0.1 2 0 48 0 48 458 0 10 2 0 48 129 0 [0.00] SYN868-1 non_thm 0.2 2 0 45 4 45 433 0 55 2 0 45 181 0 [0.00] SYN869-1 theorem 0.1 2 4 36 8 36 266 0 10 2 41 40 144 0 [0.00] SYN870-1 non_thm 0.1 2 3 36 16 36 262 0 35 2 44 39 152 0 [0.00] SYN871-1 theorem 0.2 2 5 36 35 36 256 0 66 2 62 41 289 0 [0.00] SYN872-1 non_thm 3.4 5 0 94 14 94 1717 0 120 2 0 94 696 0 [0.00] SYN873-1 theorem 0.1 2 6 36 28 36 269 0 22 2 49 42 217 0 [0.00] SYN874-1 theorem 0.1 2 2 36 6 36 269 0 9 2 40 38 159 0 [0.00] SYN876-1 theorem 1.4 3 21 52 166 52 487 0 378 2 113 73 1120 0 [0.00] SYN877-1 theorem 0.1 0 4 36 17 36 268 0 21 2 44 40 256 0 [0.00] SYN878-1 theorem 0.1 2 4 36 15 36 271 0 18 2 44 40 205 0 [0.00] SYN879-1 theorem 0.2 2 3 36 20 36 271 0 43 2 47 39 238 0 [0.00] SYN881-1 theorem 0.3 2 2 52 10 52 490 0 13 2 59 54 294 0 [0.00] SYN882-1 theorem 0.5 3 5 52 41 52 485 0 83 2 80 57 459 0 [0.00] SYN884-1 theorem 0.9 3 7 70 26 70 932 0 52 2 85 77 516 0 [0.00] SYN885-1 theorem 9.3 4 93 72 670 72 908 0 1409 2 125 165 3987 0 [0.00] SYN886-1 theorem 0.9 3 4 72 26 72 909 0 47 2 86 76 500 0 [0.00] SYN887-1 theorem 1.3 4 5 72 23 72 938 0 28 2 84 77 626 0 [0.00] SYN888-1 non_thm 4.8 6 6 102 103 102 1760 0 246 2 195 108 1187 0 [0.00] SYN889-1 theorem 0.1 2 3 36 12 36 271 0 23 2 44 39 200 0 [0.00] SYN890-1 theorem 0.1 2 2 36 10 36 273 0 22 2 44 38 242 0 [0.00] SYN892-1 theorem 0.1 2 2 36 5 36 273 0 9 2 40 38 222 0 [0.00] SYN893-1 theorem 0.5 3 4 52 13 52 485 0 33 2 59 56 426 0 [0.00] SYN894-1 theorem 0.5 3 5 52 29 52 489 0 58 2 77 57 457 0 [0.00] SYN895-1 theorem 0.3 3 5 52 19 52 479 0 20 2 64 57 293 0 [0.00] SYN896-1 theorem 3.4 4 71 52 445 52 492 11 1148 2 108 123 3389 0 [0.00] SYN897-1 theorem 1.4 4 9 72 82 72 940 0 184 2 123 81 661 0 [0.00] SYN898-1 theorem 6.9 4 79 72 655 72 941 14 1222 2 139 151 3362 0 [0.00] SYN899-1 theorem 0.8 4 3 72 9 72 931 0 17 2 78 75 457 0 [0.00] SYN900-1 theorem 1.2 4 7 72 48 72 923 0 119 2 96 79 670 0 [0.00] SYN902-1 non_thm 4.7 6 0 102 31 102 1757 0 250 2 0 102 963 0 [0.00] TOP002-2 theorem 0.0 2 1 2 0 2 0 0 0 2 2 4 0 0 [0.00] TOP004-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 4 0 [0.00] TOP004-2 theorem 0.0 2 1 1 0 0 0 0 0 2 1 5 0 0 [0.12] ANA002-4 timeout 300.0 13 [0.12] ANA003-4 timeout 300.0 218 [0.12] FLD002-3 theorem 0.0 2 1 63 0 7 0 0 0 2 63 300 279 0 [0.12] FLD007-3 timeout 300.0 159 [0.12] FLD008-4 theorem 0.1 2 1 145 0 10 0 0 0 2 145 804 1878 0 [0.12] FLD010-5 theorem 0.0 2 1 54 0 5 0 0 0 2 54 658 2028 0 [0.12] FLD014-3 theorem 0.2 3 1 192 0 7 0 0 0 2 192 3602 13553 0 [0.12] FLD018-1 timeout 300.0 6 [0.12] FLD019-1 timeout 300.0 6 [0.12] FLD023-1 theorem 135.5 9 1 212 0 7 0 0 0 3 212 10330 102 0 [0.12] FLD025-2 theorem 18.6 3 1 460 0 14 0 0 0 2 460 2232 474 0 [0.12] FLD026-3 theorem 0.9 6 1 410 0 8 0 0 0 2 410 12031 54348 0 [0.12] FLD029-3 theorem 0.9 6 1 589 0 11 0 0 0 2 589 8391 51738 0 [0.12] FLD031-1 timeout 300.0 6 [0.12] FLD032-1 timeout 300.0 6 [0.12] FLD037-1 theorem 120.9 10 1 275 0 8 0 0 0 3 275 11553 318 0 [0.12] FLD040-3 theorem 0.0 2 1 67 0 6 0 0 0 2 67 537 1463 0 [0.12] FLD040-5 theorem 0.0 2 1 68 0 6 0 0 0 2 68 601 1680 0 [0.12] FLD041-3 theorem 0.1 3 1 188 0 8 0 0 0 2 188 2588 11499 0 [0.12] FLD042-3 theorem 0.1 3 1 188 0 8 0 0 0 2 188 2588 11499 0 [0.12] FLD060-3 theorem 50.5 58 1 996 0 7 0 0 0 2 996 145733 799837 0 [0.12] FLD061-2 theorem 18.8 2 1 421 0 14 0 0 0 2 421 1571 186 0 [0.12] FLD061-3 timeout 300.0 152 [0.12] FLD063-3 theorem 34.3 42 1 818 0 7 0 0 0 2 818 111768 540501 0 [0.12] FLD064-1 timeout 300.0 6 [0.12] FLD065-1 timeout 300.0 6 [0.12] FLD066-3 theorem 0.1 2 1 207 0 12 0 0 0 2 207 1580 3475 0 [0.12] FLD067-1 theorem 112.3 10 1 202 0 7 0 0 0 3 202 9543 87 0 [0.12] FLD067-2 timeout 300.0 13 [0.12] FLD067-3 timeout 300.0 157 [0.12] FLD068-3 timeout 300.0 157 [0.12] HWV006-1 theorem 0.1 2 1 356 0 15 1 4 0 4 356 1440 1522 0 [0.12] HWV006-2 unsound 0.2 2 0 685 83 12 1 0 1561 4 0 1357 1746 0 [0.12] HWV008-1.001 theorem 0.1 2 1 215 0 11 0 0 0 5 215 653 664 0 [0.12] HWV008-1.002 theorem 0.1 2 1 324 0 14 0 0 0 5 324 934 919 0 [0.12] HWV008-2.001 theorem 0.1 2 1 215 0 9 0 0 0 5 215 601 610 0 [0.12] HWV008-2.002 theorem 0.1 2 1 326 0 12 0 0 0 5 326 866 857 0 [0.12] NLP079-1 theorem 6.9 60 2 40 1 38 4 0 0 2 22 82 720167 0 [0.12] NLP080-1 theorem 5.0 38 2 40 1 38 4 0 0 2 22 80 595295 0 [0.12] NLP081-1 theorem 2.3 16 2 38 1 36 4 0 0 2 21 76 267303 0 [0.12] NLP094-1 theorem 0.4 4 2 41 1 30 4 0 0 2 23 50 49557 0 [0.12] PUZ035-4 theorem 0.0 2 3 3 2 5 2 0 0 2 5 11 14 0 [0.12] SET010-1 theorem 0.2 2 3 835 2 5 0 61 0 2 486 3403 5393 0 [0.12] SYN002-1.007.008 theorem 0.0 2 2 0 37 0 0 0 237 23 22 0 311 0 [0.12] SYN036-4 theorem 0.0 2 8 8 7 45 81 5 2 2 4 64 92 0 [0.12] SYN039-1 theorem 0.0 2 6 4 13 13 1 0 57 4 6 19 103 0 [0.12] SYN560-1 timeout 300.0 66 [0.12] SYN607-1 timeout 300.0 16 [0.12] SYN609-1 timeout 300.0 15 [0.12] SYN610-1 timeout 300.0 18 [0.12] SYN611-1 timeout 300.0 16 [0.12] SYN612-1 timeout 300.0 18 [0.12] SYN630-1 theorem 0.0 2 1 9 0 9 0 0 0 2 9 28 5 0 [0.12] SYN634-1 theorem 3.9 3 1 186 0 9 0 0 0 6 186 3919 1286 0 [0.12] SYN635-1 theorem 3.8 3 1 186 0 9 0 0 0 6 186 3919 1286 0 [0.12] SYN636-1 theorem 3.9 3 1 186 0 9 0 0 0 6 186 3919 1286 0 [0.12] SYN645-1 timeout 300.0 18 [0.12] SYN648-1 timeout 300.0 112 [0.12] SYN687-1 timeout 300.0 6 [0.12] TOP001-2 timeout 300.0 12 [0.12] TOP005-2 theorem 0.1 2 1 11 0 2 0 0 0 5 11 16 11 0 [0.17] GRP126-4.004 theorem 0.0 2 4 80 3 17 0 0 271 2 64 623 1315 0 [0.17] GRP127-4.004 theorem 0.0 2 4 82 3 17 0 0 308 2 64 687 1405 0 [0.17] GRP128-3.005 theorem 0.3 3 14 604 21 46 0 0 2289 2 207 2446 21444 0 [0.17] GRP129-4.004 theorem 0.1 2 19 281 19 16 0 0 446 2 52 1594 4492 0 [0.17] MSC008-1.002 theorem 0.2 2 48 203 67 2 0 0 1534 2 23 1828 7720 0 [0.17] MSC008-2.002 theorem 0.1 2 36 153 52 2 0 0 738 2 22 1171 2860 0 [0.17] PUZ010-1 theorem 2.2 3 161 3162 226 552 227 0 6026 2 204 6900 125692 0 [0.17] PUZ017-1 timeout 300.0 358 [0.17] PUZ018-1 theorem 0.0 2 1 53 0 41 6 0 0 2 53 84 780 0 [0.17] PUZ019-1 theorem 0.0 2 1 116 0 44 1 3 0 2 116 333 1601 0 [0.17] PUZ028-6 theorem 0.1 2 22 376 21 36 0 0 696 2 84 1298 3071 0 [0.17] SYN444-1 theorem 31.4 5 2530 34167 3103 33325 15222 0 180393 2 86 108472 1756995 0 [0.17] SYN461-1 theorem 2.7 3 230 3943 263 3701 1839 0 10517 2 75 10629 252270 0 [0.17] SYN471-1 theorem 38.8 5 1347 16524 1803 15672 8587 0 387704 2 87 82418 2904317 0 [0.17] SYN480-1 theorem 18.1 5 610 8529 740 8063 4221 0 142778 2 74 35126 1785255 0 [0.17] SYN484-1 theorem 3.1 3 282 4268 355 4061 2106 0 9874 2 61 17292 212602 0 [0.17] SYN501-1 theorem 5.9 3 404 4644 462 4599 2775 0 50399 2 66 17331 465329 0 [0.17] SYN510-1 theorem 7.5 3 474 6602 556 6251 3228 0 28379 2 83 22788 623514 0 [0.17] SYN813-1 theorem 168.7 11 2223 188 79953 36 269 17543 123432 2 486 2571 253061 0 [0.17] SYN820-1 theorem 0.8 4 10 188 338 36 269 55 496 2 275 358 1135 0 [0.17] SYN843-1 theorem 1.1 4 23 188 406 36 269 0 569 2 334 363 1510 0 [0.17] SYN846-1 timeout 300.0 16 [0.17] SYN862-1 theorem 29.7 17 121 696 3867 72 939 34 6009 2 1187 1441 11663 0 [0.17] SYN875-1 theorem 0.1 2 3 36 13 36 265 0 17 2 46 39 170 0 [0.17] SYN880-1 theorem 0.3 3 3 52 7 52 488 0 16 2 56 55 303 0 [0.17] SYN883-1 theorem 0.6 3 9 52 48 52 491 0 53 2 76 61 514 0 [0.17] SYN891-1 theorem 0.1 2 2 36 7 36 259 0 10 2 41 38 206 0 [0.17] SYN901-1 theorem 4.4 5 5 101 26 101 1680 0 34 2 116 106 1107 0 [0.20] HWV035-1 non_thm 0.0 2 0 2 2 2 0 0 10 2 0 2 12 0 [0.20] HWV035-2 non_thm 0.0 2 0 0 4 0 0 0 10 2 0 0 14 0 [0.20] HWV036-1 non_thm 0.0 2 0 2 2 2 0 0 10 2 0 2 12 0 [0.20] NLP059-1 non_thm 0.1 2 2 23 24 7 1 1 193 3 46 50 996 0 [0.20] NLP064-1 non_thm 0.2 2 0 22 19 7 1 1 615 3 0 37 1274 0 [0.20] NLP234-1 memory 73.4 499 [0.20] NLP237-1 memory 72.0 499 [0.20] SYN737-1 non_thm 0.0 2 0 1 1 1 0 0 15 2 0 1 16 0 [0.20] SYN739-1 non_thm 0.0 2 0 1 1 1 0 0 19 2 0 1 20 0 [0.20] SYN741-1 timeout 300.0 10 [0.20] SYN742-1 non_thm 0.5 2 0 1 8 1 0 0 2425 5 0 1 2480 0 [0.20] SYN748-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 [0.20] SYN749-1 non_thm 0.0 2 0 1 1 1 0 0 7 2 0 1 8 0 [0.20] SYN754-1 non_thm 0.0 2 0 1 4 1 0 0 252 2 0 1 256 0 [0.20] SYN757-1 non_thm 0.0 2 0 1 1 1 0 0 11 2 0 1 12 0 [0.20] SYN760-1 non_thm 11.8 3 5 1 30 1 0 0 42551 7 18 1 59570 0 [0.20] SYN774-1 non_thm 0.0 2 0 2 2 2 0 0 156 2 0 2 158 0 [0.20] SYN785-1 non_thm 0.0 2 0 2 3 2 0 0 287 2 0 2 290 0 [0.20] SYN798-1 non_thm 1.4 2 0 2 5 2 0 0 8043 4 0 2 8107 0 [0.25] ANA002-2 timeout 300.0 41 [0.25] ANA004-4 timeout 300.0 221 [0.25] FLD003-1 timeout 300.0 10 [0.25] FLD004-1 timeout 300.0 10 [0.25] FLD005-1 timeout 300.0 11 [0.25] FLD009-1 timeout 300.0 10 [0.25] FLD049-4 theorem 0.3 3 1 295 0 15 0 0 0 2 295 1927 7308 0 [0.25] FLD050-4 theorem 0.3 3 1 298 0 15 0 0 0 2 298 1974 7621 0 [0.25] GRP123-3.004 non_thm 0.3 2 2 161 39 32 0 0 4843 2 108 1074 13082 0 [0.25] GRP123-4.004 non_thm 0.5 2 0 77 11 17 0 0 3902 2 0 802 18972 0 [0.25] GRP123-8.004 non_thm 0.4 2 0 170 84 33 0 0 4737 2 0 882 15824 0 [0.25] GRP123-9.004 non_thm 0.3 2 0 138 20 18 0 0 2109 2 0 813 12099 0 [0.25] GRP125-1.004 non_thm 0.2 2 0 77 11 17 0 0 1184 2 0 469 6207 0 [0.25] GRP125-2.004 non_thm 0.2 2 0 96 21 26 0 0 1200 2 0 490 6233 0 [0.25] GRP125-3.004 non_thm 0.3 2 2 164 39 32 0 0 3361 2 108 778 11299 0 [0.25] GRP125-4.004 non_thm 0.7 2 0 77 17 17 0 0 3690 2 0 719 29145 0 [0.25] GRP127-2.005 non_thm 1.5 3 0 174 32 40 0 0 4997 2 0 969 50232 0 [0.25] GRP127-3.005 non_thm 1.9 3 5 343 58 47 0 0 10720 2 181 1778 67637 0 [0.25] GRP128-1.004 non_thm 0.2 2 7 163 18 16 0 0 1488 2 46 928 8149 0 [0.25] GRP128-2.004 non_thm 0.2 2 8 207 31 25 0 0 1565 2 78 1069 8625 0 [0.25] GRP128-3.004 non_thm 0.3 2 3 223 47 31 0 0 3840 2 92 940 12451 0 [0.25] GRP128-4.004 non_thm 0.5 2 4 82 16 16 0 0 2927 2 30 851 18142 0 [0.25] GRP130-2.005 non_thm 1.6 3 32 985 61 39 0 0 6346 2 144 4710 61913 0 [0.25] GRP130-3.004 non_thm 0.3 2 2 212 45 31 0 0 3352 2 84 883 11587 0 [0.25] GRP130-4.004 non_thm 0.5 2 8 159 19 16 0 0 3164 2 61 1258 19454 0 [0.25] SET012-1 timeout 300.0 99 [0.25] SET012-2 theorem 0.0 2 2 131 1 6 0 0 246 2 101 1735 1439 0 [0.25] SET013-1 timeout 300.0 23 [0.25] SET015-1 timeout 300.0 23 [0.25] SYN036-3 theorem 0.0 2 17 90 18 133 173 15 46 2 22 176 151 0 [0.25] SYN037-1 theorem 0.0 2 13 107 12 159 242 19 27 2 19 164 110 0 [0.25] SYN037-2 theorem 0.0 2 12 30 15 72 82 8 28 2 11 88 79 0 [0.25] SYN313-1.001.002 timeout 300.0 16 [0.25] SYN418-1 non_thm 0.1 2 1 82 29 94 89 0 112 2 84 93 160 0 [0.25] SYN420-1 non_thm 0.1 2 2 110 61 118 88 0 168 2 156 125 271 0 [0.25] SYN421-1 non_thm 0.1 3 0 65 44 76 82 0 231 2 0 68 301 0 [0.25] SYN423-1 non_thm 0.1 3 3 213 131 141 94 0 583 2 318 254 1242 0 [0.25] SYN424-1 non_thm 0.8 4 2 313 185 135 129 0 5613 2 399 377 11997 0 [0.25] SYN426-1 non_thm 0.1 2 0 153 113 127 152 10 454 2 0 174 644 0 [0.25] SYN427-1 non_thm 0.1 3 3 106 87 97 99 0 209 2 187 157 498 0 [0.25] SYN428-1 non_thm 0.1 2 2 199 68 101 118 0 510 2 199 241 654 0 [0.25] SYN429-1 non_thm 0.1 2 0 121 41 101 106 0 236 2 0 129 322 0 [0.25] SYN434-1 non_thm 204.5 8 7262 69203 10789 68386 32157 0 1930798 2 111 46306713439097 0 [0.25] SYN435-1 non_thm 2.8 6 29 361 87 350 193 0 45385 2 120 1526 100926 0 [0.25] SYN437-1 non_thm 0.2 2 1 30 48 72 64 0 2587 2 69 174 7381 0 [0.25] SYN438-1 non_thm 0.1 2 3 51 25 68 62 0 415 2 32 168 1419 0 [0.25] SYN446-1 non_thm 1.5 4 72 974 109 959 493 0 23751 2 64 3195 66506 0 [0.25] SYN449-1 non_thm 34.6 4 738 7032 920 6926 4318 0 549777 2 98 40637 2357033 0 [0.25] SYN456-1 non_thm 26.9 5 1301 15818 1486 14438 7209 0 220401 2 82 65505 1968790 0 [0.25] SYN463-1 non_thm 0.2 2 39 410 67 428 311 0 3340 2 87 1515 10476 0 [0.25] SYN513-1 non_thm 0.1 2 3 62 30 46 60 0 309 2 67 110 399 0 [0.25] SYN518-1 non_thm 0.2 2 0 215 88 122 82 0 910 2 0 250 1629 0 [0.25] SYN520-1 non_thm 1.8 3 11 245 218 107 83 0 13192 2 353 468 22412 0 [0.25] SYN542-1 non_thm 0.2 2 3 125 40 124 71 0 3277 2 122 518 5306 0 [0.25] SYN543-1 non_thm 0.9 3 20 383 84 351 169 0 12191 2 148 1704 24188 0 [0.25] SYN544-1 non_thm 0.1 2 0 96 41 61 59 0 1482 2 0 110 2649 0 [0.25] SYN546-1 non_thm 0.1 2 1 92 40 79 89 0 196 2 107 110 302 0 [0.25] SYN547-1 non_thm 0.1 2 1 40 12 53 83 0 74 2 9 68 123 0 [0.25] SYN650-1 timeout 300.0 39 [0.25] SYN690-1 timeout 300.0 114 [0.25] SYN815-1 non_thm 5.7 12 0 674 174 70 939 9 766 2 0 1293 1365 0 [0.25] SYN817-1 non_thm 7.3 14 0 626 260 68 939 25 896 2 0 1198 1757 0 [0.25] SYN828-1 non_thm 5.6 12 4 646 207 68 899 0 808 2 822 1228 1465 0 [0.25] SYN838-1 non_thm 15.4 17 8 634 901 70 939 6 2911 2 1247 1206 4483 0 [0.25] SYN851-1 non_thm 7.9 14 17 696 391 72 939 2 1084 2 1074 1337 1990 0 [0.25] SYN863-1 non_thm 114.8 23 141 696 4978 72 939 24 22187 2 2484 1461 34913 0 [0.25] SYN864-1 non_thm 7.5 15 2 696 279 72 939 1 972 2 857 1322 1778 0 [0.33] GRP127-2.006 theorem 1.0 2 90 2634 192 57 0 0 2815 2 270 18546 27240 0 [0.33] SYN448-1 theorem 5.8 3 729 9385 870 8766 4914 0 23016 2 88 32068 258190 0 [0.33] SYN451-1 theorem 62.7 5 3142 43793 3884 40713 20121 0 428351 2 85 198407 3615312 0 [0.33] SYN454-1 theorem 59.8 6 1471 22631 1589 20790 10823 0 541954 2 91 82779 4733148 0 [0.33] SYN458-1 theorem 20.2 4 1386 19524 1848 18042 9841 0 85820 2 103 68930 1062808 0 [0.33] SYN459-1 theorem 14.7 4 1186 13571 1446 12638 7413 0 90920 2 70 57577 1168814 0 [0.33] SYN469-1 theorem 12.2 3 865 10621 1001 9934 5527 0 86338 2 86 46758 692912 0 [0.33] SYN475-1 theorem 15.2 5 881 10166 1126 9840 5672 0 123831 2 72 41218 1270901 0 [0.33] SYN478-1 theorem 5.3 3 481 9163 504 8486 4400 0 12689 2 82 29473 322961 0 [0.33] SYN482-1 timeout 300.0 27 [0.33] SYN483-1 theorem 4.3 3 424 5973 447 5656 3082 0 23342 2 71 17771 338742 0 [0.33] SYN485-1 theorem 5.0 3 381 6534 447 6141 2884 0 30574 2 85 20218 438271 0 [0.33] SYN504-1 theorem 2.6 3 209 3160 235 3031 1590 0 11387 2 76 10650 255108 0 [0.33] SYN505-1 theorem 13.1 4 401 5816 446 5444 2837 0 152218 2 80 18083 1252711 0 [0.33] SYN506-1 theorem 1.4 3 46 998 45 935 418 0 4832 2 73 3068 101803 0 [0.33] SYN512-1 theorem 13.9 4 1032 19927 1135 18335 9456 0 78493 2 112 53367 929320 0 [0.33] SYN850-1 timeout 300.0 22 [0.33] SYN861-1 theorem 161.3 21 818 696 24801 72 939 243 30401 2 1380 2138 66570 0 [0.33] SYN865-1 theorem 121.8 19 242 696 10980 72 939 104 33709 2 1393 1562 49605 0 [0.33] SYN866-1 timeout 300.0 23 [0.38] ANA002-1 timeout 300.0 44 [0.38] ANA002-3 timeout 300.0 12 [0.38] COM003-1 timeout 300.0 5 [0.38] FLD041-4 theorem 0.6 5 1 343 0 10 0 0 0 2 343 10802 42789 0 [0.38] FLD062-3 theorem 127.7 92 1 1101 0 7 0 0 0 2 1101 276678 1092060 0 [0.38] GRP039-6 theorem 4.3 7 2 511 1 9 0 1 28470 2 510 50864 71182 0 [0.38] SET013-2 theorem 0.2 3 2 609 1 6 0 0 270 2 335 6941 7305 0 [0.38] SYN036-1 theorem 0.0 2 14 22 13 83 116 0 23 2 8 580 2491 0 [0.38] SYN673-1 theorem 72.9 10 1 558 0 19 0 0 0 6 558 14487 4721 0 [0.38] SYN755-1 theorem 12.5 2 156 1 371 1 0 0 177711 5 21 1 309859 0 [0.38] SYN759-1 timeout 300.0 6 [0.38] SYN784-1 theorem 13.2 3 75 2 332 2 0 0 151420 4 25 2 279508 0 [0.38] SYN796-1 theorem 4.3 3 44 2 181 2 0 0 71761 3 22 2 123714 0 [0.40] HWV036-2 non_thm 0.0 2 0 0 4 0 0 0 10 2 0 0 14 0 [0.40] NLP026-1 timeout 300.0 11 [0.40] NLP031-1 non_thm 0.0 2 0 9 6 7 1 2 45 2 0 13 65 0 [0.40] NLP033-1 non_thm 0.0 2 0 8 7 6 1 2 23 2 0 10 38 0 [0.40] NLP063-1 non_thm 0.0 2 0 23 15 7 1 0 64 3 0 30 209 0 [0.40] NLP065-1 non_thm 0.1 2 0 23 14 7 1 0 113 3 0 27 355 0 [0.40] SYN736-1 non_thm 0.1 2 0 1 3 1 0 0 423 3 0 1 432 0 [0.40] SYN745-1 non_thm 0.0 2 0 1 2 1 0 0 54 2 0 1 56 0 [0.40] SYN746-1 non_thm 299.6 4 44 1 164 1 0 0 837189 10 25 1 1190828 0 [0.40] SYN747-1 timeout 300.0 10 [0.40] SYN750-1 non_thm 0.3 2 0 1 13 1 0 0 1456 4 0 1 1496 0 [0.40] SYN751-1 non_thm 0.2 2 0 1 7 1 0 0 617 6 0 1 624 0 [0.40] SYN752-1 non_thm 0.0 2 0 1 2 1 0 0 110 2 0 1 112 0 [0.40] SYN753-1 non_thm 0.0 2 0 1 2 1 0 0 158 3 0 1 160 0 [0.40] SYN761-1 timeout 300.0 13 [0.40] SYN763-1 non_thm 0.9 2 2 1 32 1 0 0 6561 6 21 1 7468 0 [0.40] SYN766-1 non_thm 0.2 2 0 1 8 1 0 0 892 4 0 1 900 0 [0.40] SYN768-1 non_thm 0.0 2 0 2 3 2 0 0 173 2 0 2 176 0 [0.40] SYN775-1 timeout 300.0 6 [0.40] SYN790-1 non_thm 0.1 2 1 2 14 2 0 0 879 3 15 2 1016 0 [0.40] SYN797-1 non_thm 0.0 2 0 2 2 2 0 0 152 2 0 2 154 0 [0.40] TOP003-2 non_thm 0.0 2 0 12 0 3 0 0 0 3 0 20 0 0 [0.40] TOP010-1 timeout 300.0 50 [0.40] TOP011-1 timeout 300.0 15 [0.40] TOP014-1 timeout 300.0 31 [0.40] TOP016-1 timeout 300.0 29 [0.50] FLD011-3 timeout 300.0 186 [0.50] FLD020-1 timeout 300.0 10 [0.50] FLD047-4 theorem 0.7 4 1 441 0 15 0 0 0 2 441 5200 28673 0 [0.50] FLD049-3 timeout 300.0 157 [0.50] GRP123-1.005 non_thm 1.3 3 0 144 16 26 0 0 7789 2 0 1556 43372 0 [0.50] GRP123-2.005 non_thm 1.4 3 0 174 28 40 0 0 7813 2 0 1590 43412 0 [0.50] GRP123-6.005 non_thm 2.3 3 0 265 28 27 0 0 7986 2 0 1624 78484 0 [0.50] GRP123-7.005 non_thm 2.4 3 0 285 37 41 0 0 7998 2 0 1644 78505 0 [0.50] GRP124-1.005 non_thm 1.3 3 1 151 18 26 0 0 7825 2 122 1637 43692 0 [0.50] GRP124-2.005 non_thm 1.4 3 0 173 29 40 0 0 7820 2 0 1590 43412 0 [0.50] GRP124-3.005 non_thm 1.8 3 1 225 61 47 0 0 14559 2 145 1835 56717 0 [0.50] GRP124-4.005 non_thm 3.6 4 0 144 16 26 0 0 14038 2 0 1606 119916 0 [0.50] GRP124-6.005 non_thm 2.3 3 1 272 30 27 0 0 7994 2 190 1699 78585 0 [0.50] GRP124-7.005 non_thm 2.4 3 1 292 39 41 0 0 8006 2 218 1719 78606 0 [0.50] GRP124-8.005 non_thm 2.9 3 1 317 124 48 0 0 16243 2 327 1817 91204 0 [0.50] GRP124-9.005 non_thm 2.4 3 1 272 30 27 0 0 7994 2 190 1699 78585 0 [0.50] GRP126-1.005 non_thm 1.2 3 0 144 16 26 0 0 4246 2 0 935 39552 0 [0.50] GRP126-2.005 non_thm 1.2 3 0 173 29 40 0 0 4273 2 0 969 39592 0 [0.50] GRP126-3.005 non_thm 1.6 3 1 229 61 47 0 0 11007 2 145 1214 52834 0 [0.50] GRP126-4.005 non_thm 5.7 6 0 144 24 26 0 0 15425 2 0 1427 197016 0 [0.50] GRP127-1.005 non_thm 1.5 3 0 145 19 26 0 0 4958 2 0 935 50192 0 [0.50] GRP127-4.005 non_thm 5.8 5 0 145 23 26 0 0 15416 2 0 1427 197032 0 [0.50] GRP129-1.005 non_thm 1.6 3 24 686 41 25 0 0 6902 2 90 3378 62411 0 [0.50] GRP129-2.005 non_thm 1.6 3 28 811 58 39 0 0 7033 2 156 4025 63886 0 [0.50] GRP129-3.005 non_thm 1.7 3 13 315 149 46 0 0 14396 2 212 1968 56334 0 [0.50] GRP129-4.005 non_thm 3.5 4 13 234 29 25 0 0 11793 2 50 2184 119340 0 [0.50] GRP130-1.005 non_thm 1.5 3 27 760 44 25 0 0 6113 2 103 3587 57317 0 [0.50] GRP131-1.005 non_thm 1.3 3 0 149 19 25 0 0 7802 2 0 1575 43372 0 [0.50] GRP131-2.005 non_thm 1.4 3 0 177 33 39 0 0 7835 2 0 1609 43412 0 [0.50] GRP132-2.005 non_thm 1.3 3 0 177 33 39 0 0 7831 2 0 1609 43412 0 [0.50] GRP133-1.004 non_thm 0.2 2 1 87 17 16 0 0 1359 2 56 535 7180 0 [0.50] GRP133-2.004 non_thm 0.2 2 6 201 32 25 0 0 1583 2 94 1053 8773 0 [0.50] GRP134-1.005 non_thm 1.3 3 6 219 27 25 0 0 4412 2 143 1729 44940 0 [0.50] GRP134-2.005 non_thm 1.3 3 8 384 38 39 0 0 4945 2 176 2459 43178 0 [0.50] GRP135-1.005 non_thm 2.6 3 52 2123 68 25 0 0 12293 2 142 14695 94546 0 [0.50] GRP135-2.005 non_thm 1.8 3 27 1369 56 39 0 0 7702 2 171 7618 69341 0 [0.50] MSC007-1.008 theorem 7.4 2 13440 148551 29687 191677 219136 0 177530 2 56 311639 194107 0 [0.50] PUZ018-2 non_thm 0.1 2 0 83 34 40 6 0 1488 2 0 134 2550 0 [0.50] SET015-2 theorem 0.1 2 2 381 1 6 0 0 270 2 221 4397 4477 0 [0.50] SYN067-1 timeout 300.0 46 [0.50] SYN307-1 non_thm 0.0 2 0 2 1 2 0 0 5 2 0 4 6 0 [0.50] SYN353-1 timeout 300.0 8 [0.50] SYN436-1 timeout 300.0 13 [0.50] SYN441-1 timeout 300.0 6 [0.50] SYN442-1 theorem 41.4 5 1831 29718 2215 26683 13383 0 506876 2 83 126926 1965293 0 [0.50] SYN443-1 theorem 215.5 16 2325 40453 2848 35669 17445 0 1588320 2 108 15346023347636 0 [0.50] SYN447-1 timeout 300.0 9 [0.50] SYN450-1 theorem 162.3 9 2543 37792 3057 34114 16328 0 1529282 2 97 17776410536147 0 [0.50] SYN452-1 theorem 5.0 3 548 7789 637 7279 3561 0 24026 2 78 27111 279591 0 [0.50] SYN453-1 non_thm 89.0 6 988 17325 1642 16517 7918 0 1053532 2 165 100763 4448918 0 [0.50] SYN455-1 theorem 34.0 4 3887 48385 4311 45000 25351 0 200906 2 94 188725 1700435 0 [0.50] SYN460-1 theorem 18.4 4 1591 21368 2360 20737 10008 0 183047 2 81 90436 1092092 0 [0.50] SYN464-1 timeout 300.0 12 [0.50] SYN465-1 theorem 56.3 7 1710 27518 1934 25964 12515 0 371633 2 90 92089 5633697 0 [0.50] SYN466-1 timeout 300.0 10 [0.50] SYN467-1 theorem 3.1 3 225 3192 288 3063 1564 0 25135 2 87 10831 249492 0 [0.50] SYN468-1 theorem 31.4 4 854 12296 986 11538 5733 0 328208 2 108 52994 1132250 0 [0.50] SYN470-1 theorem 28.9 4 1173 16418 1418 15521 8134 0 404842 2 105 66994 1239606 0 [0.50] SYN472-1 theorem 7.1 3 729 10499 891 9909 4840 0 53469 2 79 39507 338266 0 [0.50] SYN473-1 theorem 67.1 6 3252 39079 3880 36055 21656 0 455248 2 80 184790 6128306 0 [0.50] SYN474-1 theorem 19.5 4 1107 15021 1245 13593 7231 0 103606 2 105 67884 1026737 0 [0.50] SYN476-1 theorem 88.8 7 1860 38654 2031 35062 17000 0 480939 2 112 126993 6969758 0 [0.50] SYN477-1 theorem 43.7 10 586 8648 696 7731 4003 0 723310 2 93 44582 2239480 0 [0.50] SYN479-1 theorem 7.5 3 421 4772 476 4579 2559 0 106008 2 80 27984 419162 0 [0.50] SYN481-1 theorem 23.3 4 568 9419 606 8606 4005 0 149111 2 88 38732 1839199 0 [0.50] SYN486-1 theorem 11.4 4 884 10393 988 9765 6142 0 54244 2 69 40886 809106 0 [0.50] SYN487-1 theorem 51.5 5 1625 23073 2015 21888 11081 0 557622 2 99 88936 3647026 0 [0.50] SYN488-1 theorem 15.5 4 886 17566 978 15872 7567 0 24197 2 92 68754 950743 0 [0.50] SYN489-1 theorem 5.8 4 157 2918 172 2678 1340 0 17841 2 90 10164 539260 0 [0.50] SYN498-1 theorem 31.3 6 557 10094 611 9070 4478 0 231478 2 85 44757 3090752 0 [0.50] SYN499-1 theorem 47.0 5 952 18866 995 17073 8178 0 187934 2 95 117431 3484304 0 [0.50] SYN500-1 theorem 6.6 3 263 3093 313 2927 1636 0 113982 2 77 16961 470212 0 [0.50] SYN502-1 theorem 3.2 3 377 6631 417 6196 3362 0 8038 2 94 19674 178633 0 [0.50] SYN503-1 theorem 21.6 4 331 4939 394 4522 2173 0 209766 2 81 23862 2013755 0 [0.50] SYN507-1 theorem 46.8 6 1929 35197 2025 32083 16084 0 272380 2 92 121388 3118768 0 [0.50] SYN508-1 theorem 13.5 4 641 8283 879 8003 4553 0 131619 2 97 40728 998245 0 [0.50] SYN509-1 theorem 6.5 3 634 8520 753 7997 4342 0 26801 2 63 31898 576109 0 [0.50] SYN511-1 theorem 30.4 4 475 8486 559 7777 3564 0 364927 2 96 41042 1811118 0 [0.50] SYN514-1 non_thm 0.1 2 0 66 29 41 53 0 382 2 0 73 510 0 [0.50] SYN519-1 timeout 300.0 72 [0.50] SYN545-1 non_thm 0.1 2 0 39 17 48 58 0 124 2 0 39 154 0 [0.50] SYN814-1 non_thm 2.4 7 0 376 297 52 489 44 751 2 0 712 1309 0 [0.50] SYN816-1 non_thm 5.9 12 4 590 289 66 939 29 815 2 796 1131 1459 0 [0.50] SYN825-1 non_thm 14.0 20 1 945 224 85 1649 1 1115 2 1132 1806 1902 0 [0.50] SYN826-1 non_thm 13.4 20 0 858 23 84 1763 0 800 2 0 1632 1343 0 [0.50] SYN830-1 non_thm 25.6 28 9 1214 499 98 1763 0 1611 2 1688 2339 3086 0 [0.50] SYN832-1 non_thm 77.5 30 16 1033 1519 93 1704 13 7601 2 2458 1989 11335 0 [0.50] SYN839-1 non_thm 22.2 29 2 1336 157 102 1763 1 1417 2 1490 2572 2359 0 [0.50] SYN840-1 non_thm 31.4 31 15 1150 756 96 1763 4 2118 2 1846 2219 3755 0 [0.50] SYN841-1 non_thm 26.5 30 1 1330 432 102 1763 2 1694 2 1598 2559 3058 0 [0.50] SYN852-1 non_thm 59.5 37 30 1396 1384 102 1763 5 4197 2 2758 2720 6963 0 [0.50] SYN853-1 non_thm 69.7 38 11 1424 1704 104 1763 70 6651 2 2439 2755 10008 0 [0.50] SYN854-1 timeout 300.0 51 [0.50] SYN855-1 non_thm 27.9 31 11 1424 349 104 1763 3 1690 2 1760 2755 3071 0 [0.60] NLP032-1 timeout 300.0 10 [0.60] NLP035-1 non_thm 0.0 2 0 8 22 6 1 1 44 2 0 13 87 0 [0.60] NLP060-1 non_thm 0.0 2 0 23 18 7 1 0 39 3 0 28 249 0 [0.60] NLP061-1 non_thm 0.1 2 0 26 23 7 1 0 183 3 0 40 609 0 [0.60] NLP062-1 non_thm 0.0 2 0 17 16 7 1 2 67 2 0 27 145 0 [0.60] NLP160-1 memory 54.3 499 [0.60] NLP161-1 memory 56.2 499 [0.60] NLP162-1 memory 54.3 497 [0.60] NLP163-1 memory 53.8 499 [0.60] NLP164-1 memory 54.9 499 [0.60] NLP165-1 memory 54.8 499 [0.60] NLP166-1 memory 53.7 499 [0.60] NLP167-1 memory 53.8 499 [0.60] NLP168-1 memory 54.8 499 [0.60] NLP169-1 memory 55.9 498 [0.60] NLP190-1 memory 62.5 499 [0.60] NLP191-1 memory 63.9 495 [0.60] NLP192-1 memory 64.6 499 [0.60] NLP193-1 memory 62.9 499 [0.60] NLP194-1 memory 64.7 499 [0.60] NLP195-1 memory 64.7 499 [0.60] NLP196-1 memory 64.6 499 [0.60] NLP197-1 memory 63.8 499 [0.60] NLP198-1 memory 63.7 499 [0.60] NLP199-1 memory 66.5 499 [0.60] NUM288-1 timeout 300.0 21 [0.60] SET781-1 timeout 300.0 19 [0.60] SYN769-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.60] SYN780-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.60] SYN786-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 [0.60] SYN787-1 timeout 300.0 23 [0.60] SYN794-1 timeout 300.0 16 [0.60] SYN799-1 non_thm 0.0 2 0 2 1 2 0 0 78 2 0 2 79 0 [0.60] SYN800-1 timeout 300.0 18 [0.60] SYN801-1 timeout 300.0 42 [0.60] SYN903-1 timeout 300.0 113 [0.60] SYN904-1 timeout 300.0 140 [0.60] SYN905-1 timeout 300.0 143 [0.60] SYN907-1 timeout 300.0 140 [0.60] SYN908-1 timeout 300.0 172 [0.60] SYN909-1 timeout 300.0 148 [0.60] TOP015-1 timeout 300.0 30 [0.60] TOP018-1 timeout 300.0 54 [0.60] TOP019-1 timeout 300.0 54 [0.62] FLD012-4 theorem 0.3 3 1 270 0 12 0 0 0 2 270 3112 14859 0 [0.62] FLD033-1 timeout 300.0 10 [0.62] FLD038-1 timeout 300.0 10 [0.62] FLD043-5 theorem 17.2 31 1 684 0 5 0 0 0 2 684 101318 413930 0 [0.62] FLD054-4 theorem 0.6 4 1 419 0 14 0 0 0 2 419 5923 32668 0 [0.62] SYN067-2 timeout 300.0 54 [0.62] SYN067-3 timeout 300.0 5 [0.62] SYN758-1 timeout 300.0 5 [0.62] SYN762-1 timeout 300.0 6 [0.67] GRP128-2.006 theorem 24.8 3 788 26355 840 56 0 0 117477 2 272 141378 1184035 0 [0.67] SYN439-1 timeout 300.0 9 [0.67] SYN440-1 timeout 300.0 8 [0.67] SYN457-1 timeout 300.0 7 [0.75] ANA004-5 timeout 300.0 20 [0.75] FLD015-1 timeout 300.0 10 [0.75] FLD024-1 timeout 300.0 10 [0.75] FLD027-1 timeout 300.0 10 [0.75] FLD028-1 timeout 300.0 30 [0.75] FLD063-1 timeout 300.0 11 [0.75] FLD068-1 timeout 300.0 11 [0.75] FLD068-2 timeout 300.0 12 [0.75] GRP132-1.005 non_thm 1.7 3 9 347 30 25 0 0 9535 2 148 4112 63101 0 [0.75] PUZ034-1.004 timeout 300.0 233 [0.75] SYN802-1 timeout 300.0 22 [0.75] SYN812-1 non_thm 15.2 20 0 936 105 86 1708 1 952 2 0 1801 1573 0 [0.75] SYN818-1 non_thm 21.0 27 0 1374 107 102 1763 2 1381 2 0 2669 2117 0 [0.75] SYN821-1 non_thm 12.1 16 7 696 1017 72 899 151 2185 2 1475 1343 3728 0 [0.75] SYN822-1 non_thm 9.1 15 0 696 394 72 939 31 1177 2 0 1336 2336 0 [0.75] SYN829-1 non_thm 21.0 26 3 1177 443 95 1704 1 1538 2 1536 2262 2652 0 [0.75] SYN831-1 non_thm 22.4 27 1 1268 358 96 1763 0 1513 2 1324 2441 2834 0 [0.75] SYN842-1 non_thm 26.8 32 4 1400 440 102 1763 1 1742 2 1654 2702 3032 0 [0.80] GRP025-3 timeout 300.0 37 [0.80] GRP026-3 timeout 300.0 54 [0.80] GRP027-2 timeout 300.0 34 [0.80] NLP027-1 timeout 300.0 11 [0.80] NLP028-1 timeout 300.0 11 [0.80] NLP029-1 timeout 300.0 18 [0.80] NLP030-1 non_thm 0.0 2 0 10 13 7 1 1 33 2 0 14 57 0 [0.80] NLP034-1 non_thm 0.0 2 0 8 14 6 1 1 38 2 0 10 59 0 [0.80] PUZ034-1.003 timeout 300.0 239 [0.80] SYN764-1 non_thm 0.0 2 0 1 3 1 0 0 89 2 0 1 92 0 [0.80] SYN765-1 timeout 300.0 8 [0.80] SYN767-1 non_thm 0.1 2 0 1 7 1 0 0 795 3 0 1 812 0 [0.80] SYN770-1 non_thm 0.1 2 0 2 1 2 0 0 544 3 0 2 545 0 [0.80] SYN771-1 non_thm 0.5 2 0 2 5 2 0 0 1510 5 0 2 1518 0 [0.80] SYN773-1 non_thm 0.2 2 0 2 4 2 0 0 819 4 0 2 831 0 [0.80] SYN776-1 timeout 300.0 27 [0.80] SYN777-1 timeout 300.0 35 [0.80] SYN778-1 non_thm 0.1 2 0 2 1 2 0 0 602 3 0 2 603 0 [0.80] SYN779-1 timeout 300.0 32 [0.80] SYN781-1 non_thm 0.1 2 0 2 2 2 0 0 662 3 0 2 664 0 [0.80] SYN782-1 timeout 300.0 19 [0.80] SYN783-1 non_thm 0.0 2 0 2 1 2 0 0 113 2 0 2 114 0 [0.80] SYN788-1 timeout 300.0 35 [0.80] SYN789-1 timeout 300.0 29 [0.80] SYN791-1 non_thm 0.0 2 0 2 7 2 0 0 387 2 0 2 394 0 [0.80] SYN792-1 timeout 300.0 28 [0.80] SYN793-1 non_thm 0.1 2 0 2 6 2 0 0 597 4 0 2 609 0 [0.80] SYN795-1 non_thm 0.4 2 0 2 5 2 0 0 1940 4 0 2 1945 0 [0.80] SYN803-1 non_thm 0.0 2 0 2 2 2 0 0 58 2 0 2 60 0 [0.80] SYN804-1 timeout 300.0 4 [0.80] SYN805-1 timeout 300.0 7 [0.80] SYN806-1 timeout 300.0 19 [0.80] SYN807-1 non_thm 0.1 2 0 2 4 2 0 0 388 3 0 2 393 0 [0.80] SYN808-1 timeout 300.0 25 [0.80] SYN809-1 non_thm 0.1 2 0 2 1 2 0 0 262 3 0 2 263 0 [0.80] SYN810-1 timeout 300.0 18 [0.80] SYN906-1 timeout 300.0 90 [0.80] SYN910-1 timeout 300.0 227 [0.80] SYN911-1 timeout 300.0 189 [0.80] SYN912-1 timeout 300.0 188 [0.80] SYN913-1 timeout 300.0 199 [0.80] TOP001-1 timeout 300.0 324 [0.80] TOP002-1 timeout 300.0 53 [0.80] TOP003-1 timeout 300.0 72 [0.80] TOP005-1 timeout 300.0 96 [0.80] TOP006-1 timeout 300.0 15 [0.80] TOP007-1 timeout 300.0 33 [0.80] TOP008-1 timeout 300.0 62 [0.80] TOP009-1 timeout 300.0 257 [0.80] TOP012-1 timeout 300.0 201 [0.80] TOP013-1 timeout 300.0 30 [0.80] TOP017-1 timeout 300.0 32 [0.88] FLD007-1 timeout 300.0 6 [0.88] FLD008-3 timeout 300.0 156 [0.88] FLD016-1 timeout 300.0 18 [0.88] FLD022-1 timeout 300.0 12 [0.88] FLD035-1 timeout 300.0 16 [0.88] FLD036-1 timeout 300.0 16 [0.88] FLD048-4 timeout 300.0 66 [0.88] FLD050-3 timeout 300.0 156 [0.88] FLD052-4 theorem 2.9 7 1 932 0 25 0 0 0 2 932 9605 65901 0 [0.88] FLD057-3 timeout 300.0 180 [0.88] FLD066-1 timeout 300.0 12 [0.88] FLD072-4 timeout 300.0 191 [0.88] FLD086-3 timeout 300.0 190 [0.88] FLD090-3 timeout 300.0 180 [0.88] FLD097-4 timeout 300.0 91 [1.00] ANA001-1 timeout 300.0 52 [1.00] ANA005-4 timeout 300.0 30 [1.00] ANA005-5 timeout 300.0 40 [1.00] FLD008-1 timeout 300.0 10 [1.00] FLD008-2 timeout 300.0 14 [1.00] FLD011-1 timeout 300.0 6 [1.00] FLD012-1 timeout 300.0 10 [1.00] FLD012-2 timeout 300.0 17 [1.00] FLD012-3 timeout 300.0 203 [1.00] FLD014-1 timeout 300.0 13 [1.00] FLD026-1 timeout 300.0 10 [1.00] FLD029-1 timeout 300.0 21 [1.00] FLD040-1 timeout 300.0 6 [1.00] FLD041-1 timeout 300.0 10 [1.00] FLD041-2 timeout 300.0 16 [1.00] FLD042-1 timeout 300.0 10 [1.00] FLD043-1 timeout 300.0 6 [1.00] FLD044-1 timeout 300.0 10 [1.00] FLD044-2 timeout 300.0 33 [1.00] FLD044-3 timeout 300.0 156 [1.00] FLD044-4 timeout 300.0 168 [1.00] FLD045-1 timeout 300.0 10 [1.00] FLD045-2 timeout 300.0 32 [1.00] FLD045-3 timeout 300.0 157 [1.00] FLD045-4 timeout 300.0 168 [1.00] FLD046-1 timeout 300.0 6 [1.00] FLD046-3 timeout 300.0 187 [1.00] FLD047-1 timeout 300.0 12 [1.00] FLD047-2 timeout 300.0 11 [1.00] FLD047-3 timeout 300.0 189 [1.00] FLD048-1 timeout 300.0 19 [1.00] FLD048-2 timeout 300.0 11 [1.00] FLD048-3 timeout 300.0 159 [1.00] FLD049-1 timeout 300.0 19 [1.00] FLD049-2 timeout 300.0 23 [1.00] FLD050-1 timeout 300.0 21 [1.00] FLD050-2 timeout 300.0 17 [1.00] FLD051-1 timeout 300.0 23 [1.00] FLD051-2 timeout 300.0 18 [1.00] FLD051-3 timeout 300.0 133 [1.00] FLD051-4 timeout 300.0 71 [1.00] FLD052-1 timeout 300.0 19 [1.00] FLD052-2 timeout 300.0 3 [1.00] FLD052-3 timeout 300.0 154 [1.00] FLD053-1 timeout 300.0 19 [1.00] FLD053-2 timeout 300.0 3 [1.00] FLD053-3 timeout 300.0 156 [1.00] FLD053-4 timeout 300.0 66 [1.00] FLD054-1 timeout 300.0 10 [1.00] FLD054-2 timeout 300.0 19 [1.00] FLD054-3 timeout 300.0 202 [1.00] FLD057-1 timeout 300.0 5 [1.00] FLD062-1 timeout 300.0 10 [1.00] FLD072-1 timeout 300.0 10 [1.00] FLD072-2 timeout 300.0 13 [1.00] FLD072-3 timeout 300.0 173 [1.00] FLD073-1 timeout 300.0 10 [1.00] FLD073-2 timeout 300.0 13 [1.00] FLD073-3 timeout 300.0 155 [1.00] FLD073-4 timeout 300.0 188 [1.00] FLD074-1 timeout 300.0 14 [1.00] FLD074-2 timeout 300.0 15 [1.00] FLD074-3 timeout 300.0 167 [1.00] FLD074-4 timeout 300.0 105 [1.00] FLD075-1 timeout 300.0 16 [1.00] FLD075-2 timeout 300.0 14 [1.00] FLD075-3 timeout 300.0 166 [1.00] FLD075-4 timeout 300.0 104 [1.00] FLD076-1 timeout 300.0 12 [1.00] FLD076-2 timeout 300.0 15 [1.00] FLD076-3 timeout 300.0 183 [1.00] FLD076-4 timeout 300.0 89 [1.00] FLD077-1 timeout 300.0 12 [1.00] FLD077-2 timeout 300.0 17 [1.00] FLD077-3 timeout 300.0 183 [1.00] FLD077-4 timeout 300.0 89 [1.00] FLD078-1 timeout 300.0 10 [1.00] FLD078-2 timeout 300.0 13 [1.00] FLD078-3 timeout 300.0 207 [1.00] FLD078-4 timeout 300.0 160 [1.00] FLD079-1 timeout 300.0 10 [1.00] FLD079-2 timeout 300.0 12 [1.00] FLD079-3 timeout 300.0 213 [1.00] FLD079-4 timeout 300.0 181 [1.00] FLD080-1 timeout 300.0 6 [1.00] FLD080-2 timeout 300.0 10 [1.00] FLD080-3 timeout 300.0 161 [1.00] FLD080-4 timeout 300.0 214 [1.00] FLD081-1 timeout 300.0 23 [1.00] FLD081-2 timeout 300.0 16 [1.00] FLD081-3 timeout 300.0 176 [1.00] FLD081-4 timeout 300.0 99 [1.00] FLD082-1 timeout 300.0 11 [1.00] FLD082-3 timeout 300.0 214 [1.00] FLD083-1 timeout 300.0 10 [1.00] FLD083-3 timeout 300.0 212 [1.00] FLD084-1 timeout 300.0 10 [1.00] FLD084-3 timeout 300.0 205 [1.00] FLD085-1 timeout 300.0 10 [1.00] FLD085-3 timeout 300.0 203 [1.00] FLD086-1 timeout 300.0 6 [1.00] FLD087-1 timeout 300.0 6 [1.00] FLD087-3 timeout 300.0 190 [1.00] FLD088-1 timeout 300.0 6 [1.00] FLD088-3 timeout 300.0 189 [1.00] FLD089-1 timeout 300.0 6 [1.00] FLD089-3 timeout 300.0 194 [1.00] FLD090-1 timeout 300.0 6 [1.00] FLD091-1 timeout 300.0 6 [1.00] FLD091-3 timeout 300.0 188 [1.00] FLD092-1 timeout 300.0 6 [1.00] FLD092-3 timeout 300.0 187 [1.00] FLD093-1 timeout 300.0 6 [1.00] FLD093-3 timeout 300.0 187 [1.00] FLD094-1 timeout 300.0 6 [1.00] FLD094-3 timeout 300.0 184 [1.00] FLD095-1 timeout 300.0 14 [1.00] FLD095-2 timeout 300.0 13 [1.00] FLD095-3 timeout 300.0 147 [1.00] FLD095-4 timeout 300.0 73 [1.00] FLD096-1 timeout 300.0 19 [1.00] FLD096-2 timeout 300.0 15 [1.00] FLD096-3 timeout 300.0 152 [1.00] FLD096-4 timeout 300.0 74 [1.00] FLD097-1 timeout 300.0 10 [1.00] FLD097-2 timeout 300.0 15 [1.00] FLD097-3 timeout 300.0 155 [1.00] FLD098-1 timeout 300.0 10 [1.00] FLD098-2 timeout 300.0 16 [1.00] FLD098-3 timeout 300.0 153 [1.00] FLD098-4 timeout 300.0 91 [1.00] FLD099-1 timeout 300.0 6 [1.00] FLD099-2 timeout 300.0 14 [1.00] FLD099-3 timeout 300.0 182 [1.00] FLD099-4 timeout 300.0 189 [1.00] FLD100-1 timeout 300.0 10 [1.00] FLD100-2 timeout 300.0 15 [1.00] FLD100-3 timeout 300.0 154 [1.00] FLD100-4 timeout 300.0 89 [1.00] MSC008-1.010 timeout 300.0 107 [1.00] SYN314-1.002.001 timeout 300.0 13