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