-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true Problems list file : all-problems Output file : all-output Summary file : all-summary Time limit : 500 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] ALG005-1 timeout 500.0 228 [0.00] ALG006-1 timeout 500.0 51 [0.00] ALG007-1 theorem 450.9 56 1 3928 0 5 0 1468 0 4 3928 1742578 0 0 [0.00] ANA006-1 timeout 500.0 249 [0.00] BOO001-1 theorem 21.1 12 1 853 0 7 0 175 0 3 853 213852 0 0 [0.00] BOO003-1 theorem 0.0 2 1 13 0 12 0 0 0 2 13 852 0 0 [0.00] BOO003-2 theorem 257.1 48 1 3296 0 16 0 8 0 3 3296 641083 0 0 [0.00] BOO003-4 theorem 261.6 46 1 3296 0 10 0 8 0 3 3296 641025 0 0 [0.00] BOO004-1 theorem 0.0 2 1 13 0 12 0 0 0 2 13 888 0 0 [0.00] BOO004-2 theorem 257.9 48 1 3296 0 16 0 8 0 3 3296 641453 0 0 [0.00] BOO004-4 theorem 262.6 46 1 3296 0 10 0 8 0 3 3296 641395 0 0 [0.00] BOO005-1 theorem 0.0 2 1 13 0 12 0 0 0 2 13 897 0 0 [0.00] BOO005-2 timeout 500.0 57 [0.00] BOO005-4 timeout 500.0 56 [0.00] BOO006-1 theorem 0.0 2 1 13 0 12 0 0 0 2 13 863 0 0 [0.00] BOO006-2 timeout 500.0 56 [0.00] BOO006-4 timeout 500.0 58 [0.00] BOO007-1 timeout 500.0 150 [0.00] BOO008-3 non_thm 32.4 20 0 56 0 18 24 51 0 5 0 192550 0 0 [0.00] BOO008-4 timeout 500.0 197 [0.00] BOO009-1 theorem 149.9 67 1 160 0 12 0 4 0 2 160 1051886 0 0 [0.00] BOO009-2 timeout 500.0 191 [0.00] BOO009-4 timeout 500.0 194 [0.00] BOO010-1 theorem 83.1 38 1 136 0 12 0 4 0 2 136 649869 0 0 [0.00] BOO010-2 timeout 500.0 191 [0.00] BOO011-1 theorem 0.0 2 1 12 0 12 0 0 0 2 12 786 0 0 [0.00] BOO011-2 theorem 0.0 2 1 17 0 16 0 0 0 2 17 64 0 0 [0.00] BOO011-4 theorem 0.0 2 1 16 0 10 0 0 0 2 16 89 0 0 [0.00] BOO012-1 timeout 500.0 151 [0.00] BOO012-2 timeout 500.0 193 [0.00] BOO012-3 timeout 500.0 207 [0.00] BOO012-4 timeout 500.0 193 [0.00] BOO013-1 theorem 194.0 83 1 181 0 16 0 4 0 2 181 1201178 0 0 [0.00] BOO013-2 theorem 19.9 18 1 1236 0 20 0 15 0 3 1236 162167 0 0 [0.00] BOO013-3 theorem 193.6 83 1 182 0 17 0 4 0 2 182 1201183 0 0 [0.00] BOO013-4 timeout 500.0 200 [0.00] BOO014-2 timeout 500.0 184 [0.00] BOO014-4 timeout 500.0 198 [0.00] BOO015-2 timeout 500.0 184 [0.00] BOO015-4 timeout 500.0 198 [0.00] BOO016-1 theorem 147.9 94 1 175 0 13 0 4 0 2 175 1261849 0 0 [0.00] BOO016-2 timeout 500.0 68 [0.00] BOO017-1 theorem 256.4 145 1 199 0 13 0 4 0 2 199 1969556 0 0 [0.00] BOO017-2 timeout 500.0 66 [0.00] BOO018-4 theorem 0.0 2 1 15 0 10 0 0 0 2 15 78 0 0 [0.00] BOO021-1 theorem 0.0 2 1 33 0 8 0 0 0 4 33 621 0 0 [0.00] BOO022-1 timeout 500.0 285 [0.00] BOO024-1 timeout 500.0 89 [0.00] BOO025-1 timeout 500.0 91 [0.00] BOO026-1 timeout 500.0 335 [0.00] BOO027-1 timeout 500.0 101 [0.00] BOO029-1 timeout 500.0 213 [0.00] BOO036-1 timeout 500.0 91 [0.00] BOO037-1 timeout 500.0 155 [0.00] BOO037-2 timeout 500.0 211 [0.00] BOO037-3 timeout 500.0 204 [0.00] BOO068-1 timeout 500.0 20 [0.00] BOO069-1 timeout 500.0 18 [0.00] BOO070-1 timeout 500.0 20 [0.00] BOO071-1 timeout 500.0 18 [0.00] BOO075-1 timeout 500.0 10 [0.00] CAT001-1 theorem 0.1 2 1 169 0 11 0 0 0 2 169 3146 0 0 [0.00] CAT001-2 timeout 500.0 106 [0.00] CAT001-4 theorem 0.2 2 1 419 0 8 0 0 0 3 419 5411 0 0 [0.00] CAT002-1 theorem 0.1 2 1 177 0 11 0 0 0 2 177 3234 0 0 [0.00] CAT002-2 timeout 500.0 89 [0.00] CAT003-1 theorem 0.1 2 1 168 0 11 0 0 0 2 168 3095 0 0 [0.00] CAT003-4 theorem 0.1 2 1 183 0 8 0 0 0 3 183 1649 0 0 [0.00] CAT004-1 theorem 0.1 2 1 177 0 11 0 0 0 2 177 3234 0 0 [0.00] CAT005-1 theorem 0.0 2 1 30 0 10 0 0 0 2 30 352 0 0 [0.00] CAT006-1 theorem 0.0 2 1 31 0 10 0 0 0 2 31 374 0 0 [0.00] CAT007-1 theorem 0.0 2 1 10 0 9 0 0 0 2 10 68 0 0 [0.00] CAT008-1 theorem 0.0 2 1 25 0 9 0 0 0 2 25 262 0 0 [0.00] CAT009-1 theorem 41.1 14 1 901 0 9 0 17 0 3 901 244413 0 0 [0.00] CAT010-1 theorem 162.3 29 1 1501 0 9 0 19 0 3 1501 709575 0 0 [0.00] CAT011-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 71 0 0 [0.00] CAT011-2 theorem 0.0 2 1 14 0 6 0 0 0 4 14 129 0 0 [0.00] CAT012-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 70 0 0 [0.00] CAT013-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 70 0 0 [0.00] CAT013-4 theorem 0.0 2 1 9 0 6 0 0 0 3 9 42 0 0 [0.00] CAT014-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 71 0 0 [0.00] CAT014-2 theorem 0.0 2 1 15 0 6 0 0 0 4 15 136 0 0 [0.00] CAT016-4 theorem 0.0 2 1 14 0 6 0 0 0 2 14 49 0 0 [0.00] CAT017-4 theorem 0.0 2 1 12 0 6 0 0 0 3 12 71 0 0 [0.00] CAT018-1 theorem 0.0 2 1 32 0 10 0 0 0 2 32 406 0 0 [0.00] CAT019-1 theorem 0.0 2 1 8 0 8 0 0 0 2 8 45 0 0 [0.00] CAT019-2 theorem 0.0 2 1 2 0 2 0 0 0 2 2 15 0 0 [0.00] CAT020-1 timeout 500.0 39 [0.00] CAT020-2 timeout 500.0 194 [0.00] CAT020-4 timeout 500.0 200 [0.00] COL001-1 theorem 6.9 6 1 54 0 4 0 0 0 5 54 931 0 0 [0.00] COL001-2 theorem 0.7 3 1 16 0 7 0 0 0 4 16 161 0 0 [0.00] COL002-1 theorem 0.1 2 1 14 0 6 0 0 0 4 14 134 0 0 [0.00] COL002-2 timeout 500.0 111 [0.00] COL005-1 timeout 500.0 35 [0.00] COL007-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 7 0 0 [0.00] COL008-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 0 0 [0.00] COL009-1 theorem 0.1 2 1 41 0 4 0 0 0 4 41 497 0 0 [0.00] COL010-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 12 0 0 [0.00] COL012-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 7 0 0 [0.00] COL013-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 8 0 0 [0.00] COL014-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 8 0 0 [0.00] COL015-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 0 0 [0.00] COL016-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 9 0 0 [0.00] COL017-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 18 0 0 [0.00] COL018-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 9 0 0 [0.00] COL019-1 theorem 0.0 2 1 6 0 5 0 0 0 4 6 34 0 0 [0.00] COL020-1 theorem 0.0 2 1 9 0 5 0 0 0 4 9 49 0 0 [0.00] COL021-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 18 0 0 [0.00] COL022-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 18 0 0 [0.00] COL023-1 theorem 0.0 2 1 8 0 4 0 0 0 5 8 53 0 0 [0.00] COL024-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 18 0 0 [0.00] COL025-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 12 0 0 [0.00] COL026-1 theorem 0.1 2 1 52 0 4 0 0 0 4 52 673 0 0 [0.00] COL027-1 theorem 0.1 2 1 8 0 4 0 0 0 5 8 54 0 0 [0.00] COL029-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 8 0 0 [0.00] COL031-1 theorem 0.0 2 1 7 0 4 0 0 0 3 7 29 0 0 [0.00] COL032-1 theorem 38.4 8 1 210 0 4 0 0 0 5 210 12180 0 0 [0.00] COL045-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 18 0 0 [0.00] COL048-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 18 0 0 [0.00] COL050-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 21 0 0 [0.00] COL051-1 theorem 0.0 2 1 6 0 4 0 0 0 2 6 25 0 0 [0.00] COL052-1 theorem 0.0 2 1 22 0 5 0 0 0 3 22 137 0 0 [0.00] COL052-2 theorem 0.0 2 1 39 0 5 0 0 0 3 39 229 0 0 [0.00] COL053-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 10 0 0 [0.00] COL054-1 theorem 0.0 2 1 10 0 3 0 0 0 3 10 65 0 0 [0.00] COL055-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 8 0 0 [0.00] COL058-1 theorem 0.0 2 1 7 0 3 0 0 0 4 7 43 0 0 [0.00] COL058-2 theorem 0.8 4 1 193 0 3 0 2 0 5 193 6744 0 0 [0.00] COL058-3 theorem 1.8 6 1 315 0 3 0 2 0 5 315 12310 0 0 [0.00] COL059-1 theorem 200.6 12 1 207 0 9 0 1 0 4 207 5420 0 0 [0.00] COL060-2 timeout 500.0 208 [0.00] COL060-3 timeout 500.0 202 [0.00] COL061-2 timeout 500.0 209 [0.00] COL061-3 timeout 500.0 210 [0.00] COL062-2 timeout 500.0 206 [0.00] COL062-3 timeout 500.0 207 [0.00] COL063-2 timeout 500.0 199 [0.00] COL063-3 timeout 500.0 206 [0.00] COL063-4 timeout 500.0 207 [0.00] COL063-5 timeout 500.0 203 [0.00] COL063-6 timeout 500.0 209 [0.00] COL064-10 timeout 500.0 205 [0.00] COL064-11 timeout 500.0 210 [0.00] COL064-2 timeout 500.0 207 [0.00] COL064-3 timeout 500.0 207 [0.00] COL064-4 timeout 500.0 211 [0.00] COL064-5 timeout 500.0 208 [0.00] COL064-6 timeout 500.0 210 [0.00] COL064-7 timeout 500.0 206 [0.00] COL064-8 timeout 500.0 206 [0.00] COL064-9 timeout 500.0 210 [0.00] COL066-3 timeout 500.0 152 [0.00] COL070-1 theorem 0.0 2 1 8 0 4 0 0 0 5 8 53 0 0 [0.00] COL075-2 theorem 6.5 8 1 591 0 4 0 29 0 5 591 26868 0 0 [0.00] COL083-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] COL084-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] COL085-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] COL086-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] COM004-1 theorem 0.0 2 1 14 0 9 0 0 0 2 14 69 0 0 [0.00] GRP001-1 theorem 0.0 4 1 12 0 9 0 0 0 2 12 515 0 0 [0.00] GRP001-2 theorem 2.3 5 1 504 0 9 0 4 0 3 504 37873 0 0 [0.00] GRP001-4 theorem 0.6 4 1 211 0 6 0 2 0 3 211 10655 0 0 [0.00] GRP002-2 timeout 500.0 90 [0.00] GRP002-3 timeout 500.0 327 [0.00] GRP002-4 timeout 500.0 299 [0.00] GRP007-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 229 0 0 [0.00] GRP009-1 theorem 0.0 4 1 22 0 9 0 0 0 2 22 831 0 0 [0.00] GRP010-1 theorem 0.0 4 1 9 0 8 0 0 0 2 9 217 0 0 [0.00] GRP010-4 theorem 9.5 6 1 257 0 6 0 6 0 4 257 18242 0 0 [0.00] GRP011-4 theorem 3.9 8 1 324 0 6 0 6 0 4 324 26088 0 0 [0.00] GRP012-1 theorem 0.0 4 1 10 0 9 0 0 0 2 10 236 0 0 [0.00] GRP012-2 theorem 0.1 4 1 39 0 9 0 0 0 2 39 4626 0 0 [0.00] GRP012-3 theorem 1.8 4 1 31 0 7 0 0 0 3 31 3133 0 0 [0.00] GRP012-4 theorem 18.0 22 1 1081 0 7 0 6 0 4 1081 204624 0 0 [0.00] GRP013-1 theorem 0.2 4 1 34 0 10 0 0 0 2 34 5404 0 0 [0.00] GRP017-1 theorem 0.0 4 1 12 0 11 0 0 0 2 12 341 0 0 [0.00] GRP018-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 151 0 0 [0.00] GRP019-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 151 0 0 [0.00] GRP020-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 147 0 0 [0.00] GRP021-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 147 0 0 [0.00] GRP022-1 theorem 1.7 4 1 8 0 7 0 0 0 3 8 251 0 0 [0.00] GRP022-2 theorem 2.1 4 1 77 0 7 0 2 0 4 77 2649 0 0 [0.00] GRP023-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 151 0 0 [0.00] GRP023-2 theorem 0.0 4 1 8 0 7 0 0 0 2 8 30 0 0 [0.00] GRP028-2 theorem 0.0 4 1 5 0 5 0 0 0 2 5 34 0 0 [0.00] GRP029-1 theorem 0.2 4 1 11 0 5 0 0 0 3 11 284 0 0 [0.00] GRP030-1 theorem 0.0 4 1 25 0 5 0 0 0 2 25 996 0 0 [0.00] GRP031-1 theorem 0.0 4 1 17 0 5 0 0 0 2 17 409 0 0 [0.00] GRP032-3 theorem 0.0 4 1 7 0 7 0 0 0 2 7 80 0 0 [0.00] GRP033-4 theorem 0.0 4 1 8 0 7 0 0 0 2 8 156 0 0 [0.00] GRP034-3 theorem 0.0 4 1 9 0 8 0 0 0 2 9 158 0 0 [0.00] GRP035-3 timeout 500.0 73 [0.00] GRP036-3 theorem 0.0 4 1 10 0 8 0 0 0 2 10 231 0 0 [0.00] GRP037-3 theorem 0.2 4 1 45 0 11 0 1 0 2 45 5949 0 0 [0.00] GRP038-3 theorem 0.0 4 1 11 0 11 0 0 0 2 11 178 0 0 [0.00] GRP050-1 timeout 500.0 73 [0.00] GRP052-1 timeout 500.0 74 [0.00] GRP053-1 timeout 500.0 112 [0.00] GRP057-1 timeout 500.0 64 [0.00] GRP058-1 timeout 500.0 83 [0.00] GRP059-1 timeout 500.0 116 [0.00] GRP060-1 timeout 500.0 72 [0.00] GRP063-1 timeout 500.0 352 [0.00] GRP066-1 timeout 500.0 346 [0.00] GRP067-1 timeout 500.0 346 [0.00] GRP075-1 timeout 500.0 90 [0.00] GRP076-1 timeout 500.0 88 [0.00] GRP077-1 timeout 500.0 88 [0.00] GRP078-1 timeout 500.0 88 [0.00] GRP079-1 timeout 500.0 88 [0.00] GRP080-1 timeout 500.0 287 [0.00] GRP115-1 theorem 5.7 13 1 212 0 3 0 44 0 8 212 22655 0 0 [0.00] GRP116-1 theorem 40.2 21 1 382 0 3 0 52 0 8 382 62112 0 0 [0.00] GRP117-1 theorem 3.2 6 1 91 0 3 0 0 0 8 91 3488 0 0 [0.00] GRP118-1 theorem 12.6 21 1 390 0 3 0 69 0 8 390 77966 0 0 [0.00] GRP119-1 timeout 500.0 218 [0.00] GRP120-1 timeout 500.0 254 [0.00] GRP121-1 timeout 500.0 250 [0.00] GRP122-1 timeout 500.0 257 [0.00] GRP136-1 theorem 0.0 4 1 20 0 19 0 0 0 2 20 72 0 0 [0.00] GRP137-1 theorem 0.0 4 1 20 0 19 0 0 0 2 20 66 0 0 [0.00] GRP138-1 timeout 500.0 110 [0.00] GRP139-1 theorem 47.1 20 1 2935 0 19 0 66 0 3 2935 418269 0 0 [0.00] GRP140-1 timeout 500.0 111 [0.00] GRP141-1 theorem 185.2 51 1 6385 0 19 0 148 0 3 6385 1540332 0 0 [0.00] GRP142-1 theorem 0.0 4 1 17 0 17 0 0 0 2 17 45 0 0 [0.00] GRP143-1 theorem 0.0 4 1 43 0 17 0 0 0 3 43 508 0 0 [0.00] GRP144-1 theorem 0.0 4 1 24 0 17 0 0 0 3 24 252 0 0 [0.00] GRP145-1 theorem 0.0 4 1 49 0 17 0 0 0 3 49 619 0 0 [0.00] GRP146-1 theorem 47.1 20 1 2947 0 19 0 66 0 3 2947 422273 0 0 [0.00] GRP147-1 timeout 500.0 113 [0.00] GRP148-1 timeout 500.0 111 [0.00] GRP149-1 theorem 187.7 50 1 6389 0 19 0 148 0 3 6389 1545064 0 0 [0.00] GRP150-1 theorem 0.0 4 1 18 0 17 0 0 0 3 18 154 0 0 [0.00] GRP151-1 theorem 0.0 4 1 4 0 3 0 0 0 2 4 32 0 0 [0.00] GRP152-1 theorem 0.1 4 1 137 0 17 0 6 0 3 137 3182 0 0 [0.00] GRP153-1 theorem 0.0 4 1 18 0 17 0 0 0 3 18 157 0 0 [0.00] GRP154-1 theorem 4.8 7 1 912 0 18 0 16 0 3 912 63994 0 0 [0.00] GRP155-1 theorem 4.8 7 1 911 0 18 0 16 0 3 911 63971 0 0 [0.00] GRP156-1 theorem 147.9 45 1 6009 0 18 0 148 0 3 6009 1390656 0 0 [0.00] GRP157-1 theorem 4.9 7 1 914 0 18 0 16 0 3 914 64052 0 0 [0.00] GRP158-1 theorem 4.9 7 1 913 0 18 0 16 0 3 913 64023 0 0 [0.00] GRP159-1 theorem 161.2 45 1 6155 0 18 0 148 0 3 6155 1461814 0 0 [0.00] GRP160-1 theorem 0.0 4 1 3 0 2 0 0 0 2 3 29 0 0 [0.00] GRP161-1 theorem 0.0 4 1 2 0 1 0 0 0 2 2 26 0 0 [0.00] GRP162-1 theorem 86.5 23 1 3082 0 19 0 66 0 3 3082 452445 0 0 [0.00] GRP163-1 theorem 85.4 22 1 3077 0 19 0 66 0 3 3077 448839 0 0 [0.00] GRP165-1 theorem 6.0 7 1 1066 0 18 0 16 0 3 1066 75082 0 0 [0.00] GRP165-2 theorem 45.9 20 1 2929 0 18 0 66 0 3 2929 416779 0 0 [0.00] GRP166-1 timeout 500.0 130 [0.00] GRP166-2 timeout 500.0 138 [0.00] GRP166-3 theorem 6.1 8 1 1070 0 19 0 16 0 3 1070 75611 0 0 [0.00] GRP166-4 theorem 46.0 21 1 2939 0 19 0 66 0 3 2939 417885 0 0 [0.00] GRP168-1 timeout 500.0 108 [0.00] GRP168-2 timeout 500.0 108 [0.00] GRP169-1 timeout 500.0 42 [0.00] GRP169-2 timeout 500.0 42 [0.00] GRP170-1 timeout 500.0 121 [0.00] GRP170-2 timeout 500.0 122 [0.00] GRP170-3 timeout 500.0 122 [0.00] GRP170-4 timeout 500.0 122 [0.00] GRP171-1 timeout 500.0 129 [0.00] GRP171-2 timeout 500.0 131 [0.00] GRP172-1 timeout 500.0 139 [0.00] GRP172-2 timeout 500.0 140 [0.00] GRP173-1 timeout 500.0 55 [0.00] GRP174-1 timeout 500.0 51 [0.00] GRP175-1 timeout 500.0 105 [0.00] GRP175-2 timeout 500.0 109 [0.00] GRP175-3 timeout 500.0 107 [0.00] GRP175-4 timeout 500.0 109 [0.00] GRP176-1 theorem 401.0 49 1 18 0 17 0 0 0 4 18 268 0 0 [0.00] GRP176-2 theorem 407.9 49 1 19 0 18 0 0 0 4 19 283 0 0 [0.00] GRP182-1 theorem 0.0 4 1 18 0 17 0 0 0 3 18 158 0 0 [0.00] GRP182-2 theorem 0.0 4 1 21 0 20 0 0 0 3 21 182 0 0 [0.00] GRP182-3 theorem 0.0 4 1 18 0 17 0 0 0 3 18 158 0 0 [0.00] GRP182-4 theorem 0.0 4 1 21 0 20 0 0 0 3 21 182 0 0 [0.00] GRP186-3 timeout 500.0 81 [0.00] GRP186-4 timeout 500.0 93 [0.00] GRP188-1 theorem 0.1 4 1 137 0 17 0 6 0 3 137 3182 0 0 [0.00] GRP188-2 theorem 0.2 4 1 146 0 20 0 6 0 3 146 3439 0 0 [0.00] GRP189-1 theorem 0.0 4 1 18 0 17 0 0 0 3 18 157 0 0 [0.00] GRP189-2 theorem 0.0 4 1 21 0 20 0 0 0 3 21 180 0 0 [0.00] GRP190-1 timeout 500.0 109 [0.00] GRP190-2 timeout 500.0 111 [0.00] GRP191-1 timeout 500.0 107 [0.00] GRP191-2 timeout 500.0 106 [0.00] GRP192-1 timeout 500.0 165 [0.00] GRP193-1 timeout 500.0 78 [0.00] GRP193-2 timeout 500.0 99 [0.00] GRP206-1 timeout 500.0 191 [0.00] GRP392-1 timeout 500.0 245 [0.00] GRP393-1 timeout 500.0 98 [0.00] GRP393-2 timeout 500.0 45 [0.00] GRP394-1 timeout 500.0 282 [0.00] GRP394-3 timeout 500.0 247 [0.00] GRP395-1 timeout 500.0 135 [0.00] GRP397-1 timeout 500.0 45 [0.00] GRP398-1 timeout 500.0 282 [0.00] GRP398-2 timeout 500.0 282 [0.00] GRP398-3 timeout 500.0 242 [0.00] GRP402-1 timeout 500.0 193 [0.00] GRP406-1 timeout 500.0 29 [0.00] GRP407-1 timeout 500.0 27 [0.00] GRP408-1 timeout 500.0 28 [0.00] GRP409-1 timeout 500.0 60 [0.00] GRP412-1 timeout 500.0 31 [0.00] GRP413-1 timeout 500.0 29 [0.00] GRP414-1 timeout 500.0 31 [0.00] GRP415-1 timeout 500.0 42 [0.00] GRP416-1 timeout 500.0 63 [0.00] GRP418-1 timeout 500.0 22 [0.00] GRP424-1 timeout 500.0 58 [0.00] GRP425-1 timeout 500.0 61 [0.00] GRP427-1 timeout 500.0 27 [0.00] GRP428-1 timeout 500.0 25 [0.00] GRP430-1 timeout 500.0 32 [0.00] GRP431-1 timeout 500.0 41 [0.00] GRP432-1 timeout 500.0 33 [0.00] GRP433-1 timeout 500.0 20 [0.00] GRP434-1 timeout 500.0 14 [0.00] GRP435-1 timeout 500.0 20 [0.00] GRP436-1 timeout 500.0 33 [0.00] GRP437-1 timeout 500.0 34 [0.00] GRP438-1 timeout 500.0 33 [0.00] GRP445-1 theorem 24.8 26 1 933 0 5 0 11 0 5 933 161152 0 0 [0.00] GRP446-1 theorem 36.3 29 1 1001 0 5 0 12 0 5 1001 182715 0 0 [0.00] GRP448-1 timeout 500.0 299 [0.00] GRP449-1 timeout 500.0 162 [0.00] GRP451-1 timeout 500.0 305 [0.00] GRP454-1 theorem 0.0 2 1 35 0 6 0 0 0 3 35 372 0 0 [0.00] GRP455-1 timeout 500.0 326 [0.00] GRP456-1 timeout 500.0 335 [0.00] GRP457-1 theorem 0.0 2 1 35 0 6 0 0 0 3 35 372 0 0 [0.00] GRP458-1 timeout 500.0 325 [0.00] GRP459-1 timeout 500.0 341 [0.00] GRP460-1 theorem 0.0 2 1 35 0 6 0 0 0 3 35 372 0 0 [0.00] GRP461-1 timeout 500.0 324 [0.00] GRP462-1 timeout 500.0 339 [0.00] GRP463-1 theorem 0.0 2 1 35 0 6 0 0 0 3 35 372 0 0 [0.00] GRP464-1 timeout 500.0 323 [0.00] GRP465-1 timeout 500.0 338 [0.00] GRP466-1 timeout 500.0 232 [0.00] GRP467-1 timeout 500.0 243 [0.00] GRP468-1 timeout 500.0 240 [0.00] GRP481-1 timeout 500.0 47 [0.00] GRP482-1 timeout 500.0 91 [0.00] GRP483-1 timeout 500.0 88 [0.00] GRP484-1 timeout 500.0 47 [0.00] GRP485-1 timeout 500.0 88 [0.00] GRP486-1 timeout 500.0 88 [0.00] GRP487-1 timeout 500.0 47 [0.00] GRP488-1 timeout 500.0 91 [0.00] GRP489-1 timeout 500.0 90 [0.00] GRP490-1 timeout 500.0 46 [0.00] GRP491-1 timeout 500.0 87 [0.00] GRP492-1 timeout 500.0 89 [0.00] GRP493-1 timeout 500.0 44 [0.00] GRP494-1 timeout 500.0 90 [0.00] GRP495-1 timeout 500.0 92 [0.00] GRP496-1 theorem 5.6 5 1 45 0 6 0 2 0 4 45 461 0 0 [0.00] GRP497-1 timeout 500.0 269 [0.00] GRP498-1 timeout 500.0 289 [0.00] GRP499-1 timeout 500.0 240 [0.00] GRP500-1 timeout 500.0 239 [0.00] GRP508-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] GRP509-1 theorem 0.2 3 1 92 0 3 0 2 0 6 92 2531 0 0 [0.00] GRP510-1 theorem 0.1 3 1 81 0 3 0 0 0 6 81 1767 0 0 [0.00] GRP511-1 theorem 0.6 5 1 140 0 3 0 2 0 6 140 6976 0 0 [0.00] GRP512-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] GRP514-1 timeout 500.0 24 [0.00] GRP515-1 timeout 500.0 23 [0.00] GRP516-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] GRP517-1 theorem 1.3 5 1 94 0 3 0 2 0 8 94 3835 0 0 [0.00] GRP518-1 theorem 0.8 4 1 94 0 3 0 2 0 8 94 3835 0 0 [0.00] GRP519-1 theorem 1.4 3 1 57 0 3 0 0 0 8 57 1326 0 0 [0.00] GRP520-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 3 0 0 [0.00] GRP521-1 theorem 10.6 7 1 34 0 5 0 0 0 5 34 528 0 0 [0.00] GRP522-1 theorem 17.4 15 1 720 0 5 0 1 0 5 720 99966 0 0 [0.00] GRP523-1 timeout 500.0 350 [0.00] GRP524-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 5 0 0 [0.00] GRP525-1 theorem 0.0 2 1 42 0 5 0 0 0 4 42 548 0 0 [0.00] GRP526-1 theorem 0.1 2 1 100 0 5 0 0 0 4 100 3043 0 0 [0.00] GRP527-1 timeout 500.0 266 [0.00] GRP528-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 5 0 0 [0.00] GRP530-1 theorem 0.1 2 1 72 0 5 0 0 0 4 72 1522 0 0 [0.00] GRP531-1 timeout 500.0 73 [0.00] GRP532-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 5 0 0 [0.00] GRP533-1 theorem 10.0 7 1 83 0 6 0 0 0 4 83 1914 0 0 [0.00] GRP534-1 timeout 500.0 330 [0.00] GRP535-1 timeout 500.0 333 [0.00] GRP536-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP537-1 theorem 0.1 2 1 135 0 6 0 0 0 3 135 3385 0 0 [0.00] GRP538-1 theorem 24.7 10 1 263 0 6 0 0 0 4 263 17250 0 0 [0.00] GRP539-1 timeout 500.0 344 [0.00] GRP540-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP541-1 theorem 0.0 2 1 83 0 6 0 0 0 3 83 1618 0 0 [0.00] GRP542-1 timeout 500.0 328 [0.00] GRP543-1 timeout 500.0 330 [0.00] GRP544-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP545-1 theorem 0.1 2 1 83 0 6 0 0 0 3 83 1618 0 0 [0.00] GRP546-1 theorem 12.8 8 1 174 0 6 0 3 0 4 174 6101 0 0 [0.00] GRP547-1 timeout 500.0 339 [0.00] GRP548-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP549-1 theorem 0.1 2 1 83 0 6 0 0 0 3 83 1618 0 0 [0.00] GRP550-1 theorem 60.8 58 1 2434 0 6 0 5 0 4 2434 655566 0 0 [0.00] GRP551-1 timeout 500.0 358 [0.00] GRP552-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP553-1 timeout 500.0 165 [0.00] GRP554-1 timeout 500.0 165 [0.00] GRP555-1 timeout 500.0 210 [0.00] GRP556-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP557-1 theorem 123.5 21 1 496 0 4 0 0 0 6 496 78426 0 0 [0.00] GRP558-1 timeout 500.0 22 [0.00] GRP559-1 theorem 394.7 183 1 1885 0 4 0 0 0 6 1885 1393778 0 0 [0.00] GRP560-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP562-1 timeout 500.0 44 [0.00] GRP563-1 timeout 500.0 64 [0.00] GRP564-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP565-1 timeout 500.0 46 [0.00] GRP566-1 timeout 500.0 88 [0.00] GRP568-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP569-1 timeout 500.0 46 [0.00] GRP570-1 timeout 500.0 88 [0.00] GRP572-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP573-1 timeout 500.0 46 [0.00] GRP574-1 timeout 500.0 88 [0.00] GRP576-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP577-1 timeout 500.0 46 [0.00] GRP578-1 timeout 500.0 87 [0.00] GRP579-1 timeout 500.0 87 [0.00] GRP580-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP581-1 timeout 500.0 45 [0.00] GRP582-1 timeout 500.0 87 [0.00] GRP583-1 timeout 500.0 88 [0.00] GRP584-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 6 0 0 [0.00] GRP585-1 timeout 500.0 173 [0.00] GRP586-1 timeout 500.0 200 [0.00] GRP587-1 timeout 500.0 223 [0.00] GRP588-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP589-1 timeout 500.0 170 [0.00] GRP590-1 timeout 500.0 197 [0.00] GRP591-1 timeout 500.0 199 [0.00] GRP592-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP593-1 theorem 68.5 26 1 709 0 4 0 2 0 6 709 112515 0 0 [0.00] GRP594-1 theorem 268.2 24 1 679 0 4 0 2 0 6 679 94176 0 0 [0.00] GRP595-1 theorem 93.1 16 1 514 0 4 0 0 0 6 514 44159 0 0 [0.00] GRP596-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP597-1 timeout 500.0 185 [0.00] GRP598-1 timeout 500.0 200 [0.00] GRP599-1 timeout 500.0 192 [0.00] GRP600-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP601-1 timeout 500.0 187 [0.00] GRP602-1 timeout 500.0 146 [0.00] GRP603-1 timeout 500.0 218 [0.00] GRP604-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP605-1 timeout 500.0 188 [0.00] GRP606-1 timeout 500.0 208 [0.00] GRP607-1 timeout 500.0 219 [0.00] GRP608-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP609-1 theorem 60.3 17 1 563 0 4 0 0 0 6 563 54195 0 0 [0.00] GRP610-1 theorem 226.5 17 1 564 0 4 0 0 0 6 564 53278 0 0 [0.00] GRP611-1 theorem 92.5 19 1 585 0 4 0 0 0 6 585 63316 0 0 [0.00] GRP612-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] GRP613-1 timeout 500.0 199 [0.00] GRP614-1 timeout 500.0 191 [0.00] GRP615-1 timeout 500.0 194 [0.00] GRP616-1 theorem 0.0 2 1 1 0 0 0 0 0 2 1 4 0 0 [0.00] HEN001-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 27 0 0 [0.00] HEN001-3 theorem 0.0 2 1 5 0 5 0 0 0 2 5 23 0 0 [0.00] HEN001-5 theorem 0.0 2 1 2 0 1 0 0 0 2 2 10 0 0 [0.00] HEN002-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 27 0 0 [0.00] HEN002-2 theorem 0.0 2 1 6 0 6 0 0 0 2 6 40 0 0 [0.00] HEN002-3 theorem 0.0 2 1 5 0 5 0 0 0 2 5 23 0 0 [0.00] HEN002-4 theorem 0.0 2 1 6 0 6 0 0 0 2 6 31 0 0 [0.00] HEN002-5 theorem 0.0 2 1 3 0 2 0 0 0 2 3 14 0 0 [0.00] HEN003-1 theorem 43.5 24 1 131 0 5 0 4 0 3 131 834339 0 0 [0.00] HEN003-2 theorem 72.6 43 1 147 0 7 0 6 0 3 147 1891880 0 0 [0.00] HEN003-3 theorem 0.0 2 1 73 0 6 0 3 0 3 73 1290 0 0 [0.00] HEN003-4 theorem 0.0 2 1 75 0 8 0 3 0 3 75 1325 0 0 [0.00] HEN003-5 theorem 0.5 2 1 85 0 6 0 6 0 4 85 2552 0 0 [0.00] HEN004-1 timeout 500.0 202 [0.00] HEN004-3 theorem 17.3 7 1 817 0 6 0 106 0 4 817 127993 0 0 [0.00] HEN004-4 theorem 7.5 5 1 487 0 9 0 26 0 4 487 50299 0 0 [0.00] HEN004-5 theorem 102.3 16 1 1266 0 7 0 101 0 4 1266 307024 0 0 [0.00] HEN004-6 theorem 17.5 7 1 829 0 8 0 103 0 4 829 129933 0 0 [0.00] HEN005-1 timeout 500.0 210 [0.00] HEN005-2 theorem 436.0 212 1 253 0 11 0 3 0 2 25313462119 0 0 [0.00] HEN005-3 theorem 5.0 5 1 760 0 8 0 48 0 3 760 70369 0 0 [0.00] HEN005-4 theorem 13.1 8 1 974 0 12 0 22 0 3 974 103392 0 0 [0.00] HEN005-5 theorem 431.8 42 1 2889 0 8 0 209 0 4 2889 904107 0 0 [0.00] HEN005-6 theorem 4.8 5 1 760 0 10 0 45 0 3 760 69290 0 0 [0.00] HEN006-1 timeout 500.0 228 [0.00] HEN006-2 timeout 500.0 259 [0.00] HEN006-3 timeout 500.0 52 [0.00] HEN006-4 theorem 11.7 7 1 1480 0 11 0 45 0 3 1480 145765 0 0 [0.00] HEN006-5 timeout 500.0 37 [0.00] HEN006-6 timeout 500.0 54 [0.00] HEN006-7 timeout 500.0 244 [0.00] HEN007-1 timeout 500.0 201 [0.00] HEN007-2 theorem 3.0 4 1 106 0 12 0 0 0 2 106 100761 0 0 [0.00] HEN007-3 timeout 500.0 54 [0.00] HEN007-4 theorem 0.1 2 1 21 0 11 0 0 0 3 21 362 0 0 [0.00] HEN007-5 timeout 500.0 42 [0.00] HEN007-6 theorem 2.4 5 1 89 0 12 0 1 0 2 89 87221 0 0 [0.00] HEN008-1 theorem 2.0 4 1 154 0 8 0 0 0 2 154 82928 0 0 [0.00] HEN008-2 theorem 3.9 6 1 129 0 12 0 0 0 2 129 125421 0 0 [0.00] HEN008-3 theorem 2.4 4 1 518 0 7 0 45 0 3 518 42710 0 0 [0.00] HEN008-4 theorem 5.1 6 1 504 0 11 0 19 0 3 504 54298 0 0 [0.00] HEN008-5 theorem 3.2 5 1 343 0 7 0 85 0 4 343 51528 0 0 [0.00] HEN008-6 theorem 2.9 5 1 566 0 10 0 23 0 3 566 46739 0 0 [0.00] HEN009-1 timeout 500.0 50 [0.00] HEN009-2 theorem 0.5 3 1 33 0 12 0 0 0 2 33 24143 0 0 [0.00] HEN009-3 theorem 65.8 23 1 3431 0 10 0 360 0 3 3431 461657 0 0 [0.00] HEN009-4 theorem 167.5 11 1 20 0 10 0 0 0 4 20 434 0 0 [0.00] HEN009-5 theorem 321.3 104 1 2705 0 6 0 217 0 4 2705 2494499 0 0 [0.00] HEN009-6 theorem 7.4 6 1 728 0 13 0 33 0 3 728 73361 0 0 [0.00] HEN010-1 timeout 500.0 150 [0.00] HEN010-2 timeout 500.0 315 [0.00] HEN010-3 theorem 102.4 45 1 2289 0 6 0 571 0 4 2289 1417051 0 0 [0.00] HEN010-4 theorem 6.2 4 1 175 0 11 0 16 0 4 175 19752 0 0 [0.00] HEN010-5 theorem 171.4 69 1 2161 0 6 0 161 0 4 2161 1762878 0 0 [0.00] HEN010-6 theorem 3.3 4 1 125 0 11 0 15 0 4 125 8325 0 0 [0.00] HEN010-7 timeout 500.0 321 [0.00] HEN011-2 timeout 500.0 107 [0.00] HEN011-4 theorem 53.4 28 1 1315 0 12 0 123 0 4 1315 800142 0 0 [0.00] HEN011-5 timeout 500.0 139 [0.00] HEN012-1 theorem 42.9 21 1 134 0 5 0 4 0 3 134 838917 0 0 [0.00] HEN012-3 theorem 0.0 2 1 75 0 6 0 3 0 3 75 1312 0 0 [0.00] HEN013-1 timeout 500.0 227 [0.00] HEN013-2 timeout 500.0 137 [0.00] HEN013-3 timeout 500.0 167 [0.00] HWC001-1 timeout 500.0 158 [0.00] HWC004-1 timeout 500.0 93 [0.00] HWC004-2 timeout 500.0 88 [0.00] LAT005-6 timeout 500.0 232 [0.00] LAT006-1 timeout 500.0 218 [0.00] LAT008-1 theorem 1.2 6 1 284 0 4 0 17 0 4 284 16702 0 0 [0.00] LAT009-1 timeout 500.0 184 [0.00] LAT010-1 timeout 500.0 206 [0.00] LAT012-1 timeout 500.0 256 [0.00] LAT014-1 theorem 0.0 2 1 28 0 6 0 0 0 4 28 215 0 0 [0.00] LAT019-1 timeout 500.0 197 [0.00] LAT021-1 timeout 500.0 202 [0.00] LAT028-1 timeout 500.0 64 [0.00] LAT029-1 timeout 500.0 86 [0.00] LAT031-1 timeout 500.0 180 [0.00] LAT032-1 timeout 500.0 175 [0.00] LAT033-1 theorem 0.1 2 1 150 0 8 0 0 0 3 150 3047 0 0 [0.00] LAT034-1 theorem 0.1 2 1 151 0 8 0 0 0 3 151 3072 0 0 [0.00] LAT035-1 timeout 500.0 204 [0.00] LAT037-1 theorem 429.5 124 1 5532 0 20 0 282 0 3 5532 2320204 0 0 [0.00] LAT039-1 theorem 0.0 2 1 14 0 13 0 0 0 3 14 109 0 0 [0.00] LAT039-2 theorem 0.0 2 1 12 0 11 0 0 0 2 12 39 0 0 [0.00] LAT040-1 theorem 336.1 37 1 5154 0 14 0 204 0 3 5154 1254064 0 0 [0.00] LAT042-1 theorem 365.8 198 1 3503 0 14 0 208 0 4 3503 1867371 0 0 [0.00] LAT043-1 timeout 500.0 267 [0.00] LAT045-1 timeout 500.0 15 [0.00] LAT055-1 timeout 500.0 198 [0.00] LAT055-2 timeout 500.0 210 [0.00] LAT056-1 timeout 500.0 186 [0.00] LAT057-1 timeout 500.0 217 [0.00] LAT059-1 timeout 500.0 333 [0.00] LAT060-1 timeout 500.0 215 [0.00] LAT061-1 timeout 500.0 223 [0.00] LAT088-1 theorem 13.2 13 1 1008 0 7 0 2 0 5 1008 68567 0 0 [0.00] LAT089-1 timeout 500.0 77 [0.00] LAT090-1 theorem 0.0 2 1 67 0 7 0 9 0 4 67 905 0 0 [0.00] LAT091-1 timeout 500.0 78 [0.00] LCL109-5 theorem 0.1 2 1 160 0 17 7 110 0 3 160 4101 0 0 [0.00] LCL110-2 timeout 500.0 37 [0.00] LCL111-2 timeout 500.0 149 [0.00] LCL112-2 timeout 500.0 64 [0.00] LCL113-2 timeout 500.0 151 [0.00] LCL114-2 timeout 500.0 152 [0.00] LCL115-2 timeout 500.0 47 [0.00] LCL116-2 timeout 500.0 155 [0.00] LCL132-1 theorem 0.0 2 1 36 0 6 0 0 0 3 36 365 0 0 [0.00] LCL133-1 theorem 0.1 2 1 59 0 7 0 3 0 3 59 1269 0 0 [0.00] LCL134-1 theorem 3.2 3 1 148 0 6 0 9 0 4 148 6519 0 0 [0.00] LCL135-1 theorem 2.0 4 1 177 0 6 0 55 0 4 177 11029 0 0 [0.00] LCL139-1 timeout 500.0 135 [0.00] LCL140-1 timeout 500.0 115 [0.00] LCL141-1 timeout 500.0 147 [0.00] LCL143-1 theorem 108.4 20 1 2655 0 9 0 389 0 3 2655 558191 0 0 [0.00] LCL145-1 timeout 500.0 167 [0.00] LCL146-1 timeout 500.0 169 [0.00] LCL153-1 timeout 500.0 66 [0.00] LCL154-1 timeout 500.0 65 [0.00] LCL155-1 timeout 500.0 66 [0.00] LCL156-1 timeout 500.0 65 [0.00] LCL157-1 timeout 500.0 63 [0.00] LCL158-1 timeout 500.0 66 [0.00] LCL159-1 timeout 500.0 65 [0.00] LCL161-1 theorem 0.9 5 1 327 0 15 0 2 0 3 327 19692 0 0 [0.00] LCL164-1 timeout 500.0 236 [0.00] LCL169-3 theorem 0.0 2 1 12 0 8 0 0 0 4 12 62 0 0 [0.00] LCL170-3 theorem 0.0 2 1 131 0 8 0 0 0 3 131 592 0 0 [0.00] LCL171-3 theorem 0.0 2 1 89 0 8 0 0 0 4 89 1471 0 0 [0.00] LCL172-3 timeout 500.0 283 [0.00] LCL173-3 timeout 500.0 296 [0.00] LCL175-3 theorem 0.0 2 1 6 0 6 0 0 0 2 6 15 0 0 [0.00] LCL176-3 theorem 0.0 2 1 83 0 8 0 0 0 4 83 727 0 0 [0.00] LCL178-3 theorem 0.0 2 1 41 0 8 0 0 0 4 41 331 0 0 [0.00] LCL185-3 theorem 0.3 3 1 437 0 8 0 0 0 4 437 8496 0 0 [0.00] LCL186-3 theorem 0.2 3 1 329 0 8 0 0 0 4 329 6903 0 0 [0.00] LCL187-3 theorem 0.2 3 1 300 0 8 0 0 0 4 300 6164 0 0 [0.00] LCL188-3 theorem 2.5 8 1 1030 0 8 0 0 0 4 1030 47523 0 0 [0.00] LCL189-3 theorem 2.5 7 1 918 0 8 0 0 0 4 918 48226 0 0 [0.00] LCL190-3 theorem 0.0 2 1 37 0 8 0 0 0 4 37 285 0 0 [0.00] LCL196-3 theorem 3.6 10 1 1280 0 8 0 0 0 4 1280 62021 0 0 [0.00] LCL197-3 theorem 3.5 9 1 1274 0 8 0 0 0 4 1274 60769 0 0 [0.00] LCL207-3 timeout 500.0 282 [0.00] LCL209-3 timeout 500.0 275 [0.00] LCL210-3 timeout 500.0 240 [0.00] LCL211-3 timeout 500.0 285 [0.00] LCL212-3 theorem 0.0 2 1 91 0 8 0 0 0 4 91 1464 0 0 [0.00] LCL235-3 timeout 500.0 287 [0.00] LCL236-3 timeout 500.0 185 [0.00] LCL239-3 theorem 297.1 117 1 118 0 9 0 0 0 5 118 2856 0 0 [0.00] LCL240-3 timeout 500.0 230 [0.00] LCL258-3 theorem 2.7 8 1 1011 0 8 0 0 0 4 1011 51491 0 0 [0.00] LCL259-3 theorem 4.3 10 1 1419 0 8 0 0 0 4 1419 70651 0 0 [0.00] LCL268-3 timeout 500.0 149 [0.00] LCL287-3 timeout 500.0 128 [0.00] LCL294-3 timeout 500.0 133 [0.00] LCL296-3 timeout 500.0 129 [0.00] LCL297-3 timeout 500.0 130 [0.00] LCL301-3 timeout 500.0 128 [0.00] LCL321-3 theorem 0.1 2 1 108 0 8 0 0 0 4 108 2132 0 0 [0.00] LCL322-3 theorem 0.3 3 1 328 0 8 0 0 0 4 328 6841 0 0 [0.00] LCL323-3 theorem 0.3 3 1 328 0 8 0 0 0 4 328 6841 0 0 [0.00] LCL407-1 timeout 500.0 150 [0.00] LCL407-2 timeout 500.0 281 [0.00] LCL408-1 timeout 500.0 168 [0.00] LCL409-1 timeout 500.0 285 [0.00] LCL410-1 timeout 500.0 179 [0.00] LCL411-2 timeout 500.0 54 [0.00] LCL412-1 timeout 500.0 107 [0.00] LCL413-1 timeout 500.0 102 [0.00] LDA001-1 theorem 1.8 5 1 797 0 6 0 0 0 3 797 22713 0 0 [0.00] LDA002-1 timeout 500.0 100 [0.00] LDA003-1 theorem 0.0 2 1 83 0 7 0 0 0 3 83 609 0 0 [0.00] LDA007-3 theorem 0.0 2 1 63 0 8 0 0 0 3 63 740 0 0 [0.00] MGT011-1 theorem 0.0 2 1 27 0 8 0 0 0 2 27 133 0 0 [0.00] MGT012-1 theorem 0.0 2 1 27 0 8 0 0 0 2 27 133 0 0 [0.00] MGT038-1 timeout 500.0 244 [0.00] NLP002-1 non_thm 0.0 2 0 109 0 16 0 0 0 2 0 313 0 0 [0.00] NLP003-1 non_thm 0.0 2 0 109 0 16 0 0 0 2 0 313 0 0 [0.00] NLP014-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP015-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP016-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP017-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP018-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP019-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP020-1 non_thm 0.0 2 0 234 0 23 0 0 0 2 0 694 0 0 [0.00] NLP021-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP022-1 non_thm 0.0 2 0 277 0 28 0 0 0 2 0 857 0 0 [0.00] NLP023-1 non_thm 0.0 2 0 239 0 16 0 0 0 2 0 1000 0 0 [0.00] NLP024-1 non_thm 0.0 2 0 391 0 20 0 0 0 2 0 1743 0 0 [0.00] NLP025-1 non_thm 0.0 2 0 265 0 16 0 0 0 2 0 1098 0 0 [0.00] NLP042-1 non_thm 0.0 4 0 135 0 13 0 0 0 2 0 504 0 0 [0.00] NLP124-1 non_thm 0.0 4 0 146 0 18 0 0 0 2 0 524 0 0 [0.00] NLP125-1 non_thm 0.0 4 0 123 0 18 0 0 0 2 0 440 0 0 [0.00] NLP126-1 non_thm 0.0 4 0 123 0 18 0 0 0 2 0 440 0 0 [0.00] NLP127-1 non_thm 0.0 4 0 146 0 18 0 0 0 2 0 524 0 0 [0.00] NLP128-1 non_thm 0.0 4 0 123 0 18 0 0 0 2 0 440 0 0 [0.00] NLP129-1 non_thm 0.0 4 0 123 0 18 0 0 0 2 0 440 0 0 [0.00] NLP220-1 non_thm 0.1 4 0 233 0 16 0 0 0 2 0 972 0 0 [0.00] NLP224-1 non_thm 0.0 4 0 553 0 23 0 0 0 2 0 3194 0 0 [0.00] NLP225-1 non_thm 0.1 4 0 482 0 22 0 0 0 2 0 3063 0 0 [0.00] NLP226-1 non_thm 0.0 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.00] NLP227-1 non_thm 0.0 4 0 261 0 16 0 0 0 2 0 1116 0 0 [0.00] NLP228-1 non_thm 0.0 4 0 261 0 16 0 0 0 2 0 1116 0 0 [0.00] NLP229-1 non_thm 0.0 4 0 261 0 16 0 0 0 2 0 1116 0 0 [0.00] NLP240-1 non_thm 0.1 4 0 1191 0 40 0 0 0 2 0 7414 0 0 [0.00] NLP241-1 non_thm 0.1 4 0 1312 0 41 0 0 0 2 0 7558 0 0 [0.00] NLP242-1 non_thm 0.1 4 0 1185 0 40 0 0 0 2 0 7342 0 0 [0.00] NLP243-1 non_thm 0.1 4 0 1191 0 40 0 0 0 2 0 7414 0 0 [0.00] NLP244-1 non_thm 0.1 4 0 1191 0 40 0 0 0 2 0 7414 0 0 [0.00] NLP245-1 non_thm 0.1 4 0 1069 0 39 0 0 0 2 0 7666 0 0 [0.00] NLP246-1 non_thm 0.1 4 0 1070 0 39 0 0 0 2 0 7066 0 0 [0.00] NLP247-1 non_thm 0.2 4 0 1243 0 40 0 0 0 2 0 9134 0 0 [0.00] NLP248-1 non_thm 0.1 4 0 1115 0 39 0 0 0 2 0 8547 0 0 [0.00] NLP249-1 non_thm 0.2 4 0 1126 0 39 0 0 0 2 0 9291 0 0 [0.00] NLP251-1 theorem 0.1 4 1 528 0 22 0 0 0 2 528 2567 0 0 [0.00] NLP252-1 theorem 0.0 4 1 528 0 22 0 0 0 2 528 2567 0 0 [0.00] NLP255-1 non_thm 0.1 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.00] NLP257-1 theorem 0.1 4 1 528 0 22 0 0 0 2 528 2567 0 0 [0.00] NLP258-1 theorem 0.1 4 1 528 0 22 0 0 0 2 528 2567 0 0 [0.00] NLP259-1 non_thm 0.1 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.00] NUM017-2 timeout 500.0 104 [0.00] PUZ016-1 timeout 500.0 368 [0.00] RNG001-1 theorem 0.5 3 1 57 0 8 0 0 0 2 57 12264 0 0 [0.00] RNG001-4 theorem 0.5 2 1 53 0 8 0 0 0 2 53 11936 0 0 [0.00] RNG002-1 theorem 0.1 2 1 39 0 10 0 0 0 2 39 4616 0 0 [0.00] RNG003-1 theorem 0.1 2 1 39 0 10 0 0 0 2 39 4642 0 0 [0.00] RNG004-1 timeout 500.0 260 [0.00] RNG004-2 timeout 500.0 261 [0.00] RNG005-1 theorem 0.3 3 1 50 0 10 0 0 0 2 50 8394 0 0 [0.00] RNG006-1 theorem 0.0 2 1 13 0 12 0 0 0 2 13 277 0 0 [0.00] RNG006-3 theorem 107.9 124 1 279 0 12 0 14 0 2 279 2297593 0 0 [0.00] RNG007-1 theorem 5.1 6 1 99 0 9 0 6 0 2 99 82036 0 0 [0.00] RNG007-4 timeout 500.0 47 [0.00] RNG008-1 timeout 500.0 268 [0.00] RNG008-2 timeout 500.0 258 [0.00] RNG008-3 timeout 500.0 80 [0.00] RNG008-4 timeout 500.0 81 [0.00] RNG008-6 timeout 500.0 273 [0.00] RNG008-7 timeout 500.0 82 [0.00] RNG010-2 theorem 0.0 3 1 11 0 11 0 0 0 2 11 55 0 0 [0.00] RNG011-5 theorem 0.0 3 1 17 0 16 0 0 0 2 17 56 0 0 [0.00] RNG012-6 timeout 500.0 207 [0.00] RNG013-6 timeout 500.0 201 [0.00] RNG014-6 timeout 500.0 207 [0.00] RNG015-6 timeout 500.0 203 [0.00] RNG016-6 timeout 500.0 218 [0.00] RNG017-6 timeout 500.0 207 [0.00] RNG018-6 timeout 500.0 202 [0.00] RNG023-6 timeout 500.0 129 [0.00] RNG023-7 timeout 500.0 130 [0.00] RNG024-6 timeout 500.0 129 [0.00] RNG024-7 timeout 500.0 130 [0.00] RNG037-1 theorem 0.3 3 1 50 0 10 0 0 0 2 50 8394 0 0 [0.00] RNG038-1 theorem 0.1 2 1 24 0 10 0 0 0 2 24 1150 0 0 [0.00] RNG039-1 theorem 2.2 5 1 84 0 50 0 4 0 2 84 47941 0 0 [0.00] RNG042-1 timeout 500.0 224 [0.00] RNG042-2 timeout 500.0 290 [0.00] RNG042-3 timeout 500.0 307 [0.00] RNG043-1 timeout 500.0 203 [0.00] RNG043-2 timeout 500.0 285 [0.00] ROB002-1 timeout 500.0 104 [0.00] ROB003-1 timeout 500.0 102 [0.00] ROB004-1 timeout 500.0 206 [0.00] ROB008-1 timeout 500.0 96 [0.00] ROB009-1 timeout 500.0 94 [0.00] ROB010-1 timeout 500.0 96 [0.00] ROB011-1 timeout 500.0 193 [0.00] ROB013-1 timeout 500.0 96 [0.00] ROB016-1 timeout 500.0 194 [0.00] ROB021-1 timeout 500.0 95 [0.00] ROB022-1 timeout 500.0 95 [0.00] ROB023-1 timeout 500.0 109 [0.00] ROB028-1 timeout 500.0 94 [0.00] ROB029-1 timeout 500.0 193 [0.00] SYN080-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 11 0 0 [0.00] SYN083-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 7 0 0 [0.00] SYN552-1 timeout 500.0 85 [0.09] BOO002-1 timeout 500.0 74 [0.09] BOO002-2 timeout 500.0 81 [0.09] BOO007-4 timeout 500.0 203 [0.09] BOO008-2 timeout 500.0 206 [0.09] BOO010-4 timeout 500.0 195 [0.09] BOO028-1 timeout 500.0 218 [0.09] BOO031-1 timeout 500.0 322 [0.09] BOO072-1 timeout 500.0 103 [0.09] COL002-4 timeout 500.0 53 [0.09] COL003-13 timeout 500.0 95 [0.09] COL003-14 timeout 500.0 93 [0.09] COL003-15 timeout 500.0 92 [0.09] COL003-16 timeout 500.0 93 [0.09] COL030-1 theorem 0.1 2 1 24 0 4 0 0 0 5 24 308 0 0 [0.09] COL033-1 timeout 500.0 42 [0.09] COL035-1 theorem 0.0 2 1 50 0 5 0 0 0 4 50 552 0 0 [0.09] COL039-1 theorem 0.0 2 1 15 0 5 0 0 0 3 15 106 0 0 [0.09] COL056-1 theorem 0.0 2 1 10 0 5 0 0 0 3 10 59 0 0 [0.09] COL066-2 timeout 500.0 152 [0.09] GRP167-2 timeout 500.0 156 [0.09] GRP167-5 timeout 500.0 139 [0.09] GRP184-4 timeout 500.0 90 [0.09] GRP195-1 timeout 500.0 49 [0.09] GRP403-1 timeout 500.0 28 [0.09] GRP417-1 timeout 500.0 45 [0.09] GRP421-1 timeout 500.0 22 [0.09] GRP439-1 timeout 500.0 41 [0.09] GRP440-1 timeout 500.0 35 [0.09] GRP443-1 timeout 500.0 34 [0.09] GRP447-1 timeout 500.0 356 [0.09] GRP450-1 timeout 500.0 302 [0.09] GRP478-1 timeout 500.0 260 [0.09] GRP479-1 timeout 500.0 244 [0.09] GRP501-1 timeout 500.0 232 [0.09] GRP502-1 timeout 500.0 226 [0.09] GRP503-1 timeout 500.0 233 [0.09] GRP504-1 timeout 500.0 228 [0.09] GRP513-1 timeout 500.0 26 [0.09] GRP529-1 timeout 500.0 66 [0.09] GRP561-1 timeout 500.0 70 [0.09] GRP567-1 timeout 500.0 88 [0.09] GRP571-1 timeout 500.0 87 [0.09] GRP575-1 timeout 500.0 87 [0.09] LAT011-1 timeout 500.0 90 [0.09] LAT022-1 timeout 500.0 215 [0.09] LAT023-1 timeout 500.0 213 [0.09] LAT026-1 timeout 500.0 204 [0.09] LAT027-1 timeout 500.0 206 [0.09] LCL109-6 timeout 500.0 237 [0.09] LCL162-1 timeout 500.0 236 [0.09] LCL163-1 timeout 500.0 236 [0.09] ROB005-1 timeout 500.0 132 [0.12] COL081-2 timeout 500.0 35 [0.12] GRP055-1 timeout 500.0 114 [0.12] GRP061-1 timeout 500.0 115 [0.12] GRP064-1 timeout 500.0 302 [0.12] GRP065-1 timeout 500.0 314 [0.12] GRP068-1 timeout 500.0 346 [0.12] GRP069-1 timeout 500.0 350 [0.12] GRP070-1 timeout 500.0 231 [0.12] GRP074-1 timeout 500.0 242 [0.12] GRP082-1 timeout 500.0 236 [0.12] GRP088-1 timeout 500.0 374 [0.12] GRP089-1 timeout 500.0 282 [0.12] GRP090-1 timeout 500.0 74 [0.12] GRP091-1 timeout 500.0 327 [0.12] GRP092-1 timeout 500.0 347 [0.12] GRP093-1 timeout 500.0 337 [0.12] GRP094-1 timeout 500.0 353 [0.12] GRP099-1 timeout 500.0 88 [0.12] GRP102-1 timeout 500.0 89 [0.12] GRP103-1 timeout 500.0 88 [0.17] BOO008-1 timeout 500.0 155 [0.17] BOO014-3 timeout 500.0 150 [0.17] BOO015-1 timeout 500.0 150 [0.17] CAT002-4 theorem 0.0 2 1 114 0 8 0 0 0 3 114 849 0 0 [0.17] CAT004-4 theorem 0.0 2 1 112 0 8 0 0 0 3 112 823 0 0 [0.17] CAT005-4 theorem 0.0 2 1 40 0 6 0 0 0 3 40 277 0 0 [0.17] CAT006-4 theorem 0.0 2 1 38 0 6 0 0 0 3 38 262 0 0 [0.17] CAT009-4 theorem 0.7 4 1 355 0 6 0 0 0 4 355 7993 0 0 [0.17] CAT010-4 theorem 0.7 4 1 357 0 6 0 0 0 4 357 8027 0 0 [0.17] CAT011-4 theorem 0.6 3 1 299 0 6 0 0 0 4 299 6726 0 0 [0.17] CAT012-4 theorem 0.0 2 1 19 0 6 0 0 0 3 19 105 0 0 [0.17] CAT014-4 theorem 0.6 3 1 302 0 6 0 0 0 4 302 6752 0 0 [0.17] CAT018-4 theorem 1.8 6 1 488 0 7 0 0 0 4 488 16056 0 0 [0.17] COL002-3 timeout 500.0 112 [0.17] COL003-2 timeout 500.0 91 [0.17] COL003-3 timeout 500.0 93 [0.17] COL003-4 timeout 500.0 92 [0.17] COL003-5 timeout 500.0 95 [0.17] COL003-6 timeout 500.0 92 [0.17] COL042-2 timeout 500.0 133 [0.17] COL042-3 timeout 500.0 131 [0.17] COL042-4 timeout 500.0 131 [0.17] COL042-5 timeout 500.0 132 [0.17] GRP002-1 timeout 500.0 84 [0.17] HEN004-2 timeout 500.0 118 [0.17] HEN011-1 timeout 500.0 67 [0.17] HEN011-3 timeout 500.0 96 [0.17] HWC002-1 timeout 500.0 313 [0.17] HWV001-1 timeout 500.0 263 [0.17] LAT005-5 timeout 500.0 243 [0.17] LCL174-3 timeout 500.0 295 [0.17] LCL180-3 timeout 500.0 237 [0.17] LCL181-3 timeout 500.0 242 [0.17] LCL182-3 timeout 500.0 267 [0.17] LCL183-3 timeout 500.0 283 [0.17] LCL198-3 theorem 4.1 10 1 1390 0 8 0 0 0 4 1390 68888 0 0 [0.17] LCL199-3 timeout 500.0 279 [0.17] LCL201-3 timeout 500.0 287 [0.17] LCL202-3 timeout 500.0 285 [0.17] LCL203-3 timeout 500.0 279 [0.17] LCL205-3 timeout 500.0 293 [0.17] LCL206-3 timeout 500.0 271 [0.17] LCL208-3 timeout 500.0 247 [0.17] LCL226-3 timeout 500.0 306 [0.17] LCL238-3 timeout 500.0 199 [0.17] LCL241-3 timeout 500.0 232 [0.17] LCL248-3 timeout 500.0 283 [0.17] LCL249-3 timeout 500.0 260 [0.17] LCL271-3 timeout 500.0 139 [0.17] LCL311-3 timeout 500.0 134 [0.17] LCL320-3 theorem 0.3 3 1 356 0 8 0 0 0 4 356 9460 0 0 [0.17] RNG008-5 timeout 500.0 283 [0.17] ROB014-2 timeout 500.0 193 [0.18] BOO007-2 timeout 500.0 204 [0.18] BOO074-1 timeout 500.0 103 [0.18] COL003-12 timeout 500.0 91 [0.18] COL042-6 timeout 500.0 134 [0.18] COL042-7 timeout 500.0 130 [0.18] COL042-8 timeout 500.0 135 [0.18] COL042-9 timeout 500.0 129 [0.18] COL044-1 theorem 0.0 2 1 24 0 4 0 0 0 5 24 207 0 0 [0.18] GRP014-1 timeout 500.0 27 [0.18] GRP167-1 timeout 500.0 139 [0.18] GRP184-2 timeout 500.0 92 [0.18] GRP203-1 timeout 500.0 137 [0.18] GRP410-1 timeout 500.0 59 [0.18] GRP419-1 timeout 500.0 20 [0.18] GRP426-1 timeout 500.0 58 [0.18] GRP429-1 timeout 500.0 27 [0.18] GRP441-1 timeout 500.0 40 [0.18] GRP442-1 timeout 500.0 40 [0.18] GRP452-1 timeout 500.0 282 [0.18] GRP469-1 timeout 500.0 257 [0.18] GRP470-1 timeout 500.0 242 [0.18] GRP471-1 timeout 500.0 242 [0.18] GRP472-1 timeout 500.0 250 [0.18] GRP473-1 timeout 500.0 237 [0.18] GRP474-1 timeout 500.0 244 [0.18] LAT013-1 timeout 500.0 264 [0.18] RNG019-6 timeout 500.0 207 [0.25] BOO035-1 timeout 500.0 127 [0.25] CAT003-2 theorem 0.2 2 1 334 0 10 0 0 0 3 334 3950 0 0 [0.25] COL078-2 timeout 500.0 125 [0.25] COL080-2 timeout 500.0 35 [0.25] GRP051-1 timeout 500.0 110 [0.25] GRP056-1 timeout 500.0 107 [0.25] GRP062-1 timeout 500.0 116 [0.25] GRP071-1 timeout 500.0 255 [0.25] GRP072-1 timeout 500.0 249 [0.25] GRP073-1 timeout 500.0 250 [0.25] GRP083-1 timeout 500.0 237 [0.25] GRP095-1 timeout 500.0 364 [0.25] GRP096-1 timeout 500.0 214 [0.25] GRP097-1 theorem 369.8 260 1 2139 0 3 4 0 0 6 2139 1835618 0 0 [0.25] GRP098-1 timeout 500.0 75 [0.25] GRP100-1 timeout 500.0 88 [0.25] GRP101-1 timeout 500.0 87 [0.25] LAT005-4 timeout 500.0 158 [0.25] LCL109-3 timeout 500.0 197 [0.27] BOO034-1 timeout 500.0 91 [0.27] BOO067-1 timeout 500.0 17 [0.27] COL003-17 timeout 500.0 92 [0.27] COL003-18 timeout 500.0 93 [0.27] COL003-19 timeout 500.0 94 [0.27] COL004-3 timeout 500.0 136 [0.27] COL041-1 theorem 114.1 35 1 1207 0 5 0 0 0 5 1207 230707 0 0 [0.27] COL049-1 timeout 500.0 41 [0.27] COL057-1 theorem 1.4 5 1 245 0 6 0 0 0 4 245 13187 0 0 [0.27] GRP185-1 timeout 500.0 82 [0.27] GRP185-2 timeout 500.0 92 [0.27] GRP200-1 timeout 500.0 192 [0.27] GRP405-1 timeout 500.0 28 [0.27] GRP422-1 timeout 500.0 19 [0.27] GRP444-1 timeout 500.0 41 [0.27] GRP453-1 timeout 500.0 298 [0.27] GRP475-1 timeout 500.0 267 [0.27] GRP476-1 timeout 500.0 242 [0.27] GRP477-1 timeout 500.0 242 [0.27] GRP480-1 timeout 500.0 242 [0.27] LAT007-1 timeout 500.0 216 [0.27] LAT044-1 timeout 500.0 271 [0.27] LCL109-2 timeout 500.0 147 [0.27] LCL138-1 timeout 500.0 147 [0.27] LCL160-1 timeout 500.0 64 [0.27] RNG019-7 timeout 500.0 202 [0.27] RNG021-6 timeout 500.0 207 [0.33] ALG008-1 timeout 500.0 69 [0.33] BOO014-1 timeout 500.0 150 [0.33] BOO019-1 timeout 500.0 31 [0.33] BOO030-1 timeout 500.0 267 [0.33] BOO032-1 timeout 500.0 216 [0.33] BOO033-1 timeout 500.0 225 [0.33] BOO056-1 timeout 500.0 94 [0.33] BOO057-1 timeout 500.0 92 [0.33] BOO058-1 timeout 500.0 114 [0.33] BOO059-1 timeout 500.0 88 [0.33] BOO061-1 timeout 500.0 152 [0.33] CAT019-4 timeout 500.0 31 [0.33] CAT019-5 timeout 500.0 34 [0.33] COL003-10 timeout 500.0 93 [0.33] COL003-7 timeout 500.0 92 [0.33] COL003-8 timeout 500.0 93 [0.33] COL003-9 timeout 500.0 93 [0.33] COL006-2 timeout 500.0 136 [0.33] COL043-2 timeout 500.0 97 [0.33] COL044-2 timeout 500.0 163 [0.33] COL044-3 timeout 500.0 163 [0.33] COL044-4 timeout 500.0 167 [0.33] COL047-1 timeout 500.0 38 [0.33] COL071-1 timeout 500.0 33 [0.33] COL073-1 timeout 500.0 110 [0.33] GRP081-1 timeout 500.0 235 [0.33] GRP112-1 timeout 500.0 188 [0.33] GRP204-1 timeout 500.0 146 [0.33] GRP207-1 timeout 500.0 102 [0.33] GRP399-1 timeout 500.0 85 [0.33] HWC003-2 timeout 500.0 348 [0.33] LAT016-1 timeout 500.0 328 [0.33] LAT024-1 timeout 500.0 41 [0.33] LAT025-1 timeout 500.0 61 [0.33] LAT046-1 timeout 500.0 224 [0.33] LAT047-1 timeout 500.0 209 [0.33] LAT048-1 timeout 500.0 15 [0.33] LAT049-1 timeout 500.0 275 [0.33] LAT050-1 timeout 500.0 271 [0.33] LAT051-1 timeout 500.0 275 [0.33] LAT052-1 timeout 500.0 272 [0.33] LAT053-1 timeout 500.0 272 [0.33] LAT054-1 timeout 500.0 267 [0.33] LAT062-1 timeout 500.0 272 [0.33] LAT063-1 timeout 500.0 269 [0.33] LCL136-1 timeout 500.0 36 [0.33] LCL137-1 timeout 500.0 148 [0.33] LCL142-1 timeout 500.0 44 [0.33] LCL165-1 timeout 500.0 284 [0.33] LCL192-3 timeout 500.0 319 [0.33] LCL193-3 timeout 500.0 320 [0.33] LCL194-3 timeout 500.0 286 [0.33] LCL218-3 timeout 500.0 298 [0.33] LCL219-3 timeout 500.0 296 [0.33] LCL234-3 timeout 500.0 287 [0.33] LCL237-3 timeout 500.0 277 [0.33] LCL246-3 timeout 500.0 228 [0.33] LCL250-3 timeout 500.0 261 [0.33] LCL261-3 timeout 500.0 292 [0.33] LCL267-3 timeout 500.0 128 [0.33] LCL272-3 timeout 500.0 137 [0.33] LCL274-3 timeout 500.0 133 [0.33] LCL280-3 timeout 500.0 135 [0.33] LCL288-3 timeout 500.0 129 [0.33] LCL290-3 timeout 500.0 127 [0.33] LCL291-3 timeout 500.0 129 [0.33] LCL292-3 timeout 500.0 127 [0.33] LCL298-3 timeout 500.0 128 [0.33] LCL338-3 timeout 500.0 130 [0.33] NLP250-1 non_thm 0.0 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.33] NLP253-1 non_thm 0.0 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.33] NLP254-1 non_thm 0.0 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.33] NLP256-1 non_thm 0.0 4 0 460 0 22 0 0 0 2 0 2203 0 0 [0.33] PUZ015-1 timeout 500.0 361 [0.33] RNG007-5 timeout 500.0 277 [0.33] RNG025-8 timeout 500.0 237 [0.33] RNG025-9 timeout 500.0 239 [0.33] RNG031-6 timeout 500.0 221 [0.33] RNG031-7 timeout 500.0 218 [0.33] ROB012-1 timeout 500.0 193 [0.33] ROB012-2 timeout 500.0 189 [0.33] ROB015-1 timeout 500.0 193 [0.36] BOO023-1 timeout 500.0 89 [0.36] BOO073-1 timeout 500.0 97 [0.36] COL003-20 timeout 500.0 93 [0.36] COL011-1 theorem 2.9 5 1 176 0 4 0 0 0 5 176 4827 0 0 [0.36] COL034-1 timeout 500.0 107 [0.36] COL037-1 theorem 12.4 14 1 576 0 5 0 0 0 5 576 22855 0 0 [0.36] COL060-1 timeout 500.0 155 [0.36] COL061-1 timeout 500.0 188 [0.36] COL062-1 timeout 500.0 195 [0.36] COL063-1 timeout 500.0 186 [0.36] GRP114-1 timeout 500.0 156 [0.36] GRP177-2 timeout 500.0 162 [0.36] GRP181-4 timeout 500.0 55 [0.36] GRP183-1 timeout 500.0 88 [0.36] GRP183-3 timeout 500.0 89 [0.36] GRP184-1 timeout 500.0 84 [0.36] GRP185-3 timeout 500.0 87 [0.36] GRP185-4 timeout 500.0 91 [0.36] GRP201-1 timeout 500.0 192 [0.36] GRP202-1 timeout 500.0 191 [0.36] GRP205-1 timeout 500.0 191 [0.36] GRP404-1 timeout 500.0 26 [0.36] GRP420-1 timeout 500.0 23 [0.36] GRP423-1 timeout 500.0 22 [0.36] LAT038-1 timeout 500.0 67 [0.36] RNG009-5 timeout 500.0 249 [0.36] RNG009-7 timeout 500.0 20 [0.36] RNG020-6 timeout 500.0 202 [0.36] RNG020-7 timeout 500.0 203 [0.36] RNG025-6 timeout 500.0 129 [0.38] BOO038-1 timeout 500.0 105 [0.38] CAT004-2 theorem 0.1 2 1 293 0 10 0 0 0 3 293 3275 0 0 [0.38] GRP049-1 timeout 500.0 73 [0.38] GRP085-1 theorem 0.6 6 1 155 0 2 4 4 0 6 155 9338 0 0 [0.38] GRP087-1 theorem 0.9 8 1 150 0 2 4 6 0 8 150 11884 0 0 [0.38] GRP104-1 timeout 500.0 229 [0.38] GRP105-1 timeout 500.0 217 [0.38] GRP106-1 theorem 160.5 134 1 1678 0 3 4 2 0 6 1678 932289 0 0 [0.38] GRP107-1 timeout 500.0 212 [0.38] GRP108-1 timeout 500.0 231 [0.38] GRP109-1 timeout 500.0 233 [0.38] GRP110-1 theorem 68.4 40 1 901 0 3 4 0 0 6 901 212795 0 0 [0.38] GRP111-1 timeout 500.0 213 [0.45] COL002-5 timeout 500.0 53 [0.45] COL064-1 timeout 500.0 193 [0.45] COL065-1 timeout 500.0 210 [0.45] GRP167-3 timeout 500.0 49 [0.45] GRP167-4 timeout 500.0 87 [0.45] GRP178-1 timeout 500.0 78 [0.45] GRP178-2 timeout 500.0 99 [0.45] GRP179-1 timeout 500.0 78 [0.45] GRP179-2 timeout 500.0 56 [0.45] GRP179-3 timeout 500.0 91 [0.45] GRP181-3 timeout 500.0 43 [0.45] GRP183-2 timeout 500.0 91 [0.45] GRP183-4 timeout 500.0 91 [0.45] GRP184-3 timeout 500.0 87 [0.45] GRP411-1 timeout 500.0 62 [0.45] LAT092-1 timeout 500.0 69 [0.45] LAT093-1 timeout 500.0 70 [0.45] LAT094-1 timeout 500.0 69 [0.45] LAT095-1 timeout 500.0 70 [0.45] LAT096-1 timeout 500.0 69 [0.45] LAT097-1 timeout 500.0 69 [0.45] RNG021-7 timeout 500.0 200 [0.45] RNG025-4 timeout 500.0 202 [0.50] ALG003-1 theorem 98.4 20 1 580 0 4 0 0 0 5 580 162261 0 0 [0.50] ALG004-1 theorem 143.1 21 1 552 0 6 0 0 0 4 552 119107 0 0 [0.50] BOO020-1 timeout 500.0 126 [0.50] COL079-2 timeout 500.0 30 [0.50] GRP054-1 timeout 500.0 112 [0.50] GRP086-1 theorem 240.1 18 1 235 0 3 3 0 0 8 235 30869 0 0 [0.50] GRP401-1 timeout 500.0 200 [0.50] HWC003-1 timeout 500.0 40 [0.50] HWV003-1 timeout 500.0 289 [0.50] LAT005-3 timeout 500.0 200 [0.50] LAT030-1 timeout 500.0 69 [0.50] LCL109-4 timeout 500.0 33 [0.50] LCL191-3 timeout 500.0 322 [0.50] LCL195-3 timeout 500.0 291 [0.50] LCL213-3 timeout 500.0 265 [0.50] LCL215-3 timeout 500.0 245 [0.50] LCL216-3 timeout 500.0 283 [0.50] LCL217-3 timeout 500.0 284 [0.50] LCL220-3 timeout 500.0 239 [0.50] LCL230-3 timeout 500.0 310 [0.50] LCL231-3 timeout 500.0 298 [0.50] LCL265-3 timeout 500.0 134 [0.50] LCL273-3 timeout 500.0 132 [0.50] LCL285-3 timeout 500.0 129 [0.50] LCL286-3 timeout 500.0 128 [0.50] LCL300-3 timeout 500.0 130 [0.50] LCL306-3 timeout 500.0 196 [0.50] LCL312-3 timeout 500.0 132 [0.50] LCL326-3 timeout 500.0 132 [0.50] LDA004-1 timeout 500.0 58 [0.50] RNG025-1 timeout 500.0 276 [0.50] RNG034-1 timeout 500.0 163 [0.50] ROB015-2 timeout 500.0 193 [0.55] COL004-1 timeout 500.0 62 [0.55] COL046-1 timeout 500.0 156 [0.55] GRP180-1 timeout 500.0 85 [0.55] GRP180-2 timeout 500.0 91 [0.55] GRP181-1 timeout 500.0 43 [0.55] GRP181-2 timeout 500.0 55 [0.55] GRP186-1 timeout 500.0 88 [0.55] GRP186-2 timeout 500.0 93 [0.55] GRP187-1 timeout 500.0 49 [0.55] LAT020-1 timeout 500.0 201 [0.55] LAT080-1 timeout 500.0 71 [0.55] LAT081-1 timeout 500.0 71 [0.55] LAT083-1 timeout 500.0 71 [0.55] LAT086-1 timeout 500.0 71 [0.55] LAT087-1 timeout 500.0 71 [0.55] RNG025-5 timeout 500.0 202 [0.55] RNG025-7 timeout 500.0 129 [0.62] GRP084-1 timeout 500.0 26 [0.62] GRP197-1 timeout 500.0 66 [0.62] RNG029-3 timeout 500.0 228 [0.64] COL006-1 timeout 500.0 52 [0.64] COL036-1 theorem 498.9 53 1 1613 0 5 0 0 0 5 1613 352619 0 0 [0.64] COL038-1 timeout 500.0 99 [0.64] GRP024-5 timeout 500.0 340 [0.64] GRP505-1 timeout 500.0 34 [0.64] GRP507-1 timeout 500.0 35 [0.64] LAT082-1 timeout 500.0 73 [0.64] LAT084-1 timeout 500.0 71 [0.64] LAT085-1 timeout 500.0 73 [0.64] RNG026-6 timeout 500.0 209 [0.64] RNG026-7 timeout 500.0 203 [0.67] ANA003-1 timeout 500.0 70 [0.67] ANA004-1 timeout 500.0 67 [0.67] BOO060-1 timeout 500.0 20 [0.67] COL006-3 timeout 500.0 135 [0.67] COL044-5 timeout 500.0 162 [0.67] HWV002-1 timeout 500.0 300 [0.67] LCL152-1 timeout 500.0 171 [0.67] LCL214-3 timeout 500.0 245 [0.67] LCL222-3 timeout 500.0 279 [0.67] LCL225-3 timeout 500.0 295 [0.67] LCL227-3 timeout 500.0 308 [0.67] LCL229-3 timeout 500.0 298 [0.67] LCL260-3 timeout 500.0 240 [0.67] LCL262-3 timeout 500.0 129 [0.67] LCL269-3 timeout 500.0 135 [0.67] LCL289-3 timeout 500.0 125 [0.67] LCL319-3 timeout 500.0 156 [0.67] LCL337-3 timeout 500.0 129 [0.67] LCL341-3 timeout 500.0 174 [0.67] ROB014-1 timeout 500.0 193 [0.67] ROB018-1 timeout 500.0 193 [0.67] ROB019-1 timeout 500.0 192 [0.67] SYN305-1 timeout 500.0 15 [0.73] COL003-1 timeout 500.0 79 [0.73] COL006-6 timeout 500.0 53 [0.73] GRP506-1 timeout 500.0 32 [0.73] LAT017-1 timeout 500.0 331 [0.73] RNG035-7 timeout 500.0 17 [0.75] COL076-2 timeout 500.0 44 [0.75] GRP198-1 timeout 500.0 46 [0.75] GRP199-1 timeout 500.0 35 [0.75] LAT036-1 timeout 500.0 196 [0.82] COL044-6 timeout 500.0 168 [0.82] COL044-7 timeout 500.0 171 [0.82] COL066-1 timeout 500.0 152 [0.83] ANA005-1 timeout 500.0 69 [0.83] COL006-4 timeout 500.0 135 [0.83] HWV004-1 timeout 500.0 271 [0.83] LAT001-1 timeout 500.0 196 [0.83] LAT002-1 timeout 500.0 86 [0.83] LCL221-3 timeout 500.0 284 [0.83] LCL223-3 timeout 500.0 302 [0.83] LCL228-3 timeout 500.0 312 [0.83] LCL242-3 timeout 500.0 304 [0.83] LCL243-3 timeout 500.0 230 [0.83] LCL245-3 timeout 500.0 277 [0.83] LCL247-3 timeout 500.0 218 [0.83] LCL251-3 timeout 500.0 242 [0.83] LCL252-3 timeout 500.0 232 [0.83] LCL253-3 timeout 500.0 205 [0.83] LCL254-3 timeout 500.0 200 [0.83] LCL255-3 timeout 500.0 288 [0.83] LCL266-3 timeout 500.0 129 [0.83] LCL276-3 timeout 500.0 128 [0.83] LCL278-3 timeout 500.0 139 [0.83] LCL283-3 timeout 500.0 129 [0.83] LCL293-3 timeout 500.0 129 [0.83] LCL295-3 timeout 500.0 129 [0.83] LCL299-3 timeout 500.0 128 [0.83] LCL302-3 timeout 500.0 128 [0.83] LCL303-3 timeout 500.0 129 [0.83] LCL304-3 timeout 500.0 129 [0.83] LCL305-3 timeout 500.0 178 [0.83] LCL313-3 timeout 500.0 128 [0.83] LCL314-3 timeout 500.0 129 [0.83] LCL315-3 timeout 500.0 138 [0.83] LCL316-3 timeout 500.0 138 [0.83] LCL324-3 timeout 500.0 128 [0.83] LCL327-3 timeout 500.0 150 [0.83] LCL330-3 timeout 500.0 128 [0.83] LCL331-3 timeout 500.0 129 [0.83] LCL332-3 timeout 500.0 247 [0.83] LCL335-3 timeout 500.0 193 [0.83] LCL339-3 timeout 500.0 129 [0.83] LCL340-3 timeout 500.0 138 [0.83] LCL344-3 timeout 500.0 140 [0.83] LCL345-3 timeout 500.0 142 [0.83] LCL346-3 timeout 500.0 127 [0.83] LCL347-3 timeout 500.0 130 [0.83] LCL348-3 timeout 500.0 129 [0.83] LCL349-3 timeout 500.0 128 [0.88] LAT015-1 timeout 500.0 70 [0.88] RNG027-1 timeout 500.0 276 [0.88] RNG028-1 timeout 500.0 279 [0.88] RNG029-1 timeout 500.0 282 [0.91] BOO076-1 timeout 500.0 121 [0.91] COL006-5 timeout 500.0 53 [0.91] COL006-7 timeout 500.0 52 [0.91] COL042-1 timeout 500.0 97 [0.91] COL043-1 timeout 500.0 39 [0.91] GRP164-1 timeout 500.0 49 [0.91] GRP164-2 timeout 500.0 49 [0.91] LAT070-1 timeout 500.0 168 [0.91] RNG027-5 timeout 500.0 210 [0.91] RNG027-7 timeout 500.0 203 [0.91] RNG027-8 timeout 500.0 204 [0.91] RNG027-9 timeout 500.0 202 [0.91] RNG028-5 timeout 500.0 209 [0.91] RNG028-7 timeout 500.0 203 [0.91] RNG028-8 timeout 500.0 202 [0.91] RNG028-9 timeout 500.0 202 [0.91] RNG029-5 timeout 500.0 217 [0.91] RNG029-6 timeout 500.0 210 [0.91] RNG029-7 timeout 500.0 202 [0.91] ROB006-1 timeout 500.0 156 [0.91] ROB006-2 timeout 500.0 12 [0.91] ROB026-1 timeout 500.0 158 [1.00] ALG010-1 timeout 500.0 130 [1.00] BOO039-1 timeout 500.0 133 [1.00] BOO040-1 timeout 500.0 88 [1.00] BOO041-1 timeout 500.0 110 [1.00] BOO042-1 timeout 500.0 93 [1.00] BOO043-1 timeout 500.0 90 [1.00] BOO044-1 timeout 500.0 88 [1.00] BOO045-1 timeout 500.0 81 [1.00] BOO046-1 timeout 500.0 97 [1.00] BOO047-1 timeout 500.0 97 [1.00] BOO048-1 timeout 500.0 94 [1.00] BOO049-1 timeout 500.0 119 [1.00] BOO050-1 timeout 500.0 87 [1.00] BOO051-1 timeout 500.0 90 [1.00] BOO052-1 timeout 500.0 94 [1.00] BOO053-1 timeout 500.0 85 [1.00] BOO054-1 timeout 500.0 91 [1.00] BOO055-1 timeout 500.0 89 [1.00] BOO066-1 timeout 500.0 120 [1.00] BOO077-1 timeout 500.0 50 [1.00] BOO078-1 timeout 500.0 75 [1.00] BOO079-1 timeout 500.0 10 [1.00] BOO080-1 timeout 500.0 95 [1.00] BOO081-1 timeout 500.0 19 [1.00] BOO082-1 timeout 500.0 74 [1.00] BOO083-1 timeout 500.0 57 [1.00] BOO084-1 timeout 500.0 77 [1.00] BOO085-1 timeout 500.0 34 [1.00] BOO086-1 timeout 500.0 71 [1.00] BOO087-1 timeout 500.0 33 [1.00] BOO088-1 timeout 500.0 72 [1.00] BOO089-1 timeout 500.0 14 [1.00] BOO090-1 timeout 500.0 78 [1.00] BOO091-1 timeout 500.0 31 [1.00] BOO092-1 timeout 500.0 78 [1.00] BOO093-1 timeout 500.0 77 [1.00] BOO094-1 timeout 500.0 90 [1.00] BOO095-1 timeout 500.0 15 [1.00] BOO096-1 timeout 500.0 96 [1.00] BOO097-1 timeout 500.0 14 [1.00] BOO098-1 timeout 500.0 71 [1.00] BOO099-1 timeout 500.0 56 [1.00] BOO100-1 timeout 500.0 76 [1.00] BOO101-1 timeout 500.0 14 [1.00] BOO102-1 timeout 500.0 74 [1.00] BOO103-1 timeout 500.0 48 [1.00] BOO104-1 timeout 500.0 73 [1.00] BOO105-1 timeout 500.0 11 [1.00] BOO106-1 timeout 500.0 75 [1.00] BOO107-1 timeout 500.0 13 [1.00] BOO108-1 timeout 500.0 72 [1.00] COL043-3 timeout 500.0 97 [1.00] COL044-8 timeout 500.0 164 [1.00] COL044-9 timeout 500.0 171 [1.00] COL067-1 timeout 500.0 69 [1.00] COL068-1 timeout 500.0 52 [1.00] COL069-1 timeout 500.0 41 [1.00] GRP177-1 timeout 500.0 156 [1.00] GRP196-1 timeout 500.0 86 [1.00] GRP400-1 timeout 500.0 195 [1.00] LAT018-1 timeout 500.0 339 [1.00] LAT041-1 timeout 500.0 302 [1.00] LAT064-1 timeout 500.0 212 [1.00] LAT065-1 timeout 500.0 222 [1.00] LAT066-1 timeout 500.0 223 [1.00] LAT067-1 timeout 500.0 223 [1.00] LAT068-1 timeout 500.0 207 [1.00] LAT069-1 timeout 500.0 208 [1.00] LAT071-1 timeout 500.0 122 [1.00] LAT072-1 timeout 500.0 24 [1.00] LAT073-1 timeout 500.0 112 [1.00] LAT074-1 timeout 500.0 73 [1.00] LAT075-1 timeout 500.0 71 [1.00] LAT076-1 timeout 500.0 147 [1.00] LAT077-1 timeout 500.0 131 [1.00] LAT078-1 timeout 500.0 66 [1.00] LAT079-1 timeout 500.0 64 [1.00] LCL147-1 timeout 500.0 167 [1.00] LCL148-1 timeout 500.0 171 [1.00] LCL149-1 timeout 500.0 170 [1.00] LCL150-1 timeout 500.0 165 [1.00] LCL151-1 timeout 500.0 167 [1.00] LCL224-3 timeout 500.0 303 [1.00] LCL263-3 timeout 500.0 127 [1.00] LCL264-3 timeout 500.0 127 [1.00] LCL270-3 timeout 500.0 153 [1.00] LCL275-3 timeout 500.0 129 [1.00] LCL277-3 timeout 500.0 140 [1.00] LCL279-3 timeout 500.0 132 [1.00] LCL281-3 timeout 500.0 128 [1.00] LCL282-3 timeout 500.0 130 [1.00] LCL284-3 timeout 500.0 126 [1.00] LCL307-3 timeout 500.0 133 [1.00] LCL308-3 timeout 500.0 130 [1.00] LCL309-3 timeout 500.0 133 [1.00] LCL310-3 timeout 500.0 130 [1.00] LCL317-3 timeout 500.0 137 [1.00] LCL318-3 timeout 500.0 131 [1.00] LCL325-3 timeout 500.0 128 [1.00] LCL328-3 timeout 500.0 129 [1.00] LCL329-3 timeout 500.0 131 [1.00] LCL333-3 timeout 500.0 130 [1.00] LCL334-3 timeout 500.0 128 [1.00] LCL336-3 timeout 500.0 129 [1.00] LCL342-3 timeout 500.0 179 [1.00] LCL343-3 timeout 500.0 126 [1.00] LCL350-3 timeout 500.0 131 [1.00] LCL351-3 timeout 500.0 148 [1.00] LCL352-3 timeout 500.0 129 [1.00] LCL353-3 timeout 500.0 130 [1.00] RNG010-1 timeout 500.0 164 [1.00] RNG010-5 timeout 500.0 253 [1.00] RNG010-6 timeout 500.0 253 [1.00] RNG010-7 timeout 500.0 258 [1.00] RNG027-2 timeout 500.0 227 [1.00] RNG028-2 timeout 500.0 228 [1.00] RNG029-2 timeout 500.0 228 [1.00] RNG030-6 timeout 500.0 222 [1.00] RNG030-7 timeout 500.0 202 [1.00] RNG032-6 timeout 500.0 223 [1.00] RNG032-7 timeout 500.0 215 [1.00] RNG033-6 timeout 500.0 207 [1.00] RNG033-7 timeout 500.0 202 [1.00] RNG033-8 timeout 500.0 203 [1.00] RNG033-9 timeout 500.0 202 [1.00] RNG036-7 timeout 500.0 17 [1.00] ROB001-1 timeout 500.0 95 [1.00] ROB006-3 timeout 500.0 17 [1.00] ROB007-1 timeout 500.0 96 [1.00] ROB007-2 timeout 500.0 8 [1.00] ROB007-3 timeout 500.0 30 [1.00] ROB007-4 timeout 500.0 30 [1.00] ROB017-1 timeout 500.0 94 [1.00] ROB020-1 timeout 500.0 96 [1.00] ROB020-2 timeout 500.0 9 [1.00] ROB024-1 timeout 500.0 96 [1.00] ROB027-1 timeout 500.0 97