-------------------------------------------------------------------------------- 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 ALG001-1 timeout 500.0 8 ALG001-2 memory 440.0 499 ALG001-3 timeout 500.0 65 ALG002-1 theorem 0.0 2 1 45 0 4 0 0 0 3 45 280 101 0 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 ALG009-1 memory 442.6 499 ALG010-1 timeout 500.0 130 ANA001-1 timeout 500.0 70 ANA002-1 timeout 500.0 50 ANA002-2 timeout 500.0 53 ANA002-3 timeout 500.0 17 ANA002-4 timeout 500.0 15 ANA003-1 timeout 500.0 70 ANA003-2 timeout 500.0 137 ANA003-3 timeout 500.0 90 ANA003-4 timeout 500.0 281 ANA004-1 timeout 500.0 67 ANA004-2 timeout 500.0 126 ANA004-3 timeout 500.0 91 ANA004-4 timeout 500.0 283 ANA004-5 timeout 500.0 26 ANA005-1 timeout 500.0 69 ANA005-2 timeout 500.0 133 ANA005-3 timeout 500.0 93 ANA005-4 timeout 500.0 27 ANA005-5 timeout 500.0 88 ANA006-1 timeout 500.0 249 ANA006-2 timeout 500.0 284 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-3 theorem 452.4 14 1 441 0 8 0 0 0 3 441 6157 5627 0 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-3 theorem 88.2 7 1 119 0 8 0 0 0 3 119 983 755 0 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-3 theorem 332.1 10 1 195 0 8 0 0 0 3 195 1906 1725 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-3 theorem 83.8 7 1 117 0 8 0 0 0 3 117 955 751 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-3 theorem 0.7 3 1 46 0 6 0 0 0 3 46 351 278 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-3 theorem 0.7 3 1 43 0 6 0 0 0 3 43 328 255 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 CAT007-3 theorem 0.0 2 1 5 0 5 0 0 0 2 5 12 6 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-3 timeout 500.0 73 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-3 timeout 500.0 53 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-3 theorem 0.0 2 1 20 0 6 0 0 0 3 20 127 118 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-3 theorem 0.0 2 1 9 0 6 0 0 0 3 9 48 38 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-3 timeout 500.0 53 CAT014-4 theorem 0.6 3 1 302 0 6 0 0 0 4 302 6752 0 0 CAT015-3 non_thm 0.0 2 0 7 0 24 20 4 47 5 0 52 49 0 CAT015-4 non_thm 0.0 2 0 7 0 19 15 4 36 5 0 42 38 0 CAT016-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 61 18 0 CAT016-4 theorem 0.0 2 1 14 0 6 0 0 0 2 14 49 0 0 CAT017-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 61 18 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-3 timeout 500.0 63 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-3 theorem 0.0 2 1 35 0 5 0 0 0 2 35 156 22 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-3 timeout 500.0 151 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 COL074-1 timeout 500.0 58 COL074-2 timeout 500.0 54 COL074-3 timeout 500.0 21 COL075-1 timeout 500.0 58 COL075-2 theorem 6.5 8 1 591 0 4 0 29 0 5 591 26868 0 0 COL076-1 timeout 500.0 56 COL076-2 timeout 500.0 44 COL077-1 timeout 500.0 41 COL078-1 timeout 500.0 41 COL078-2 timeout 500.0 125 COL079-1 timeout 500.0 49 COL079-2 timeout 500.0 30 COL080-1 timeout 500.0 40 COL080-2 timeout 500.0 35 COL081-1 timeout 500.0 40 COL081-2 timeout 500.0 35 COL082-1 timeout 500.0 14 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 COM001-1 theorem 0.0 2 1 9 0 7 0 0 0 2 9 18 0 0 COM002-1 theorem 0.0 2 1 26 0 15 0 0 0 2 26 43 0 0 COM002-2 theorem 0.0 2 1 26 0 15 0 0 0 2 26 47 9 0 COM003-1 theorem 3.8 4 673 6793 5147 372 192 0 35441 2 213 20622 145471 0 COM003-2 theorem 0.0 2 1 12 0 17 13 1 0 2 12 24 22 0 COM004-1 theorem 0.0 2 1 14 0 9 0 0 0 2 14 69 0 0 FLD001-3 theorem 0.0 2 1 62 0 7 0 0 0 2 62 283 2000 0 FLD002-3 theorem 0.0 2 1 63 0 7 0 0 0 2 63 300 2005 0 FLD003-1 timeout 500.0 19 FLD004-1 timeout 500.0 19 FLD005-1 timeout 500.0 19 FLD005-3 theorem 0.0 2 1 91 0 6 0 0 0 2 91 629 2082 0 FLD006-1 theorem 27.5 4 1 154 0 4 0 0 0 3 154 1362 16646 0 FLD006-3 theorem 0.0 2 1 5 0 4 0 0 0 2 5 31 32 0 FLD007-1 timeout 500.0 14 FLD007-3 timeout 500.0 86 FLD008-1 timeout 500.0 19 FLD008-2 timeout 500.0 50 FLD008-3 timeout 500.0 56 FLD008-4 theorem 0.1 2 1 145 0 10 0 0 0 2 145 804 7875 0 FLD009-1 timeout 500.0 19 FLD009-3 theorem 0.1 2 1 112 0 7 0 0 0 2 112 907 2094 0 FLD010-1 theorem 34.7 5 1 168 0 5 0 0 0 3 168 1396 18973 0 FLD010-3 theorem 0.0 2 1 6 0 5 0 0 0 2 6 35 34 0 FLD010-5 theorem 0.0 2 1 54 0 5 0 0 0 2 54 658 341 0 FLD011-1 timeout 500.0 15 FLD011-3 timeout 500.0 62 FLD012-1 timeout 500.0 19 FLD012-2 timeout 500.0 26 FLD012-3 timeout 500.0 76 FLD012-4 theorem 0.2 3 1 270 0 12 0 0 0 2 270 3112 8519 0 FLD013-1 theorem 6.9 3 1 272 0 10 0 0 0 2 272 1327 8600 0 FLD013-2 theorem 16.1 3 1 345 0 12 0 0 0 2 345 1638 14448 0 FLD013-3 theorem 0.5 3 1 324 0 10 0 0 0 2 324 6414 9245 0 FLD013-4 theorem 0.0 2 1 29 0 12 0 0 0 2 29 315 509 0 FLD013-5 theorem 0.0 2 1 27 0 14 0 0 0 2 27 334 599 0 FLD014-1 timeout 500.0 19 FLD014-3 theorem 0.2 2 1 192 0 7 0 0 0 2 192 3602 2729 0 FLD015-1 timeout 500.0 19 FLD015-3 theorem 0.0 2 1 93 0 7 0 0 0 2 93 636 2018 0 FLD016-1 timeout 500.0 23 FLD016-3 theorem 0.1 2 1 151 0 10 0 0 0 2 151 851 7883 0 FLD016-5 theorem 0.2 3 1 204 0 12 0 0 0 2 204 1500 13874 0 FLD017-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 310 460 0 FLD017-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 187 219 0 FLD018-1 timeout 500.0 15 FLD018-3 theorem 0.0 2 1 73 0 6 0 0 0 2 73 1562 1180 0 FLD019-1 timeout 500.0 15 FLD019-3 theorem 0.0 2 1 14 0 6 0 0 0 2 14 96 133 0 FLD020-1 timeout 500.0 19 FLD020-3 theorem 0.0 2 1 83 0 7 0 0 0 2 83 518 2102 0 FLD021-1 theorem 0.8 2 1 55 0 7 0 0 0 2 55 216 1950 0 FLD021-3 theorem 0.0 2 1 14 0 7 0 0 0 2 14 104 171 0 FLD022-1 timeout 500.0 19 FLD022-3 theorem 0.1 2 1 149 0 10 0 0 0 2 149 827 7875 0 FLD023-1 theorem 89.2 12 1 212 0 7 0 0 0 3 212 10330 36163 0 FLD023-3 theorem 0.0 2 1 86 0 7 0 0 0 2 86 738 2163 0 FLD024-1 timeout 500.0 19 FLD024-3 theorem 0.0 2 1 57 0 7 0 0 0 2 57 227 1951 0 FLD025-1 theorem 7.0 3 1 284 0 10 0 0 0 2 284 1371 8644 0 FLD025-2 theorem 34.0 4 1 460 0 14 0 0 0 2 460 2232 23137 0 FLD025-3 theorem 0.5 3 1 324 0 10 0 0 0 2 324 6414 9245 0 FLD025-4 theorem 0.0 2 1 36 0 12 0 0 0 2 36 336 530 0 FLD025-5 theorem 0.0 2 1 35 0 14 0 0 0 2 35 362 623 0 FLD026-1 timeout 500.0 19 FLD026-3 theorem 0.5 3 1 410 0 8 0 0 0 2 410 12031 3013 0 FLD027-1 timeout 500.0 19 FLD027-3 theorem 0.1 2 1 149 0 9 0 0 0 2 149 1648 2240 0 FLD028-1 timeout 500.0 27 FLD028-3 theorem 0.2 3 1 181 0 11 0 0 0 2 181 1229 8064 0 FLD029-1 timeout 500.0 23 FLD029-3 theorem 0.6 3 1 589 0 11 0 0 0 2 589 8391 8884 0 FLD030-1 theorem 0.0 2 1 9 0 8 0 0 0 2 9 149 167 0 FLD030-2 theorem 0.0 2 1 24 0 10 0 0 0 2 24 310 460 0 FLD030-3 theorem 0.0 2 1 25 0 8 0 0 0 2 25 188 291 0 FLD030-4 theorem 0.0 2 1 11 0 10 0 0 0 2 11 187 219 0 FLD031-1 timeout 500.0 15 FLD031-3 theorem 0.1 2 1 83 0 7 0 0 0 2 83 2127 1244 0 FLD031-5 theorem 0.1 2 1 100 0 7 0 0 0 2 100 2896 1342 0 FLD032-1 timeout 500.0 15 FLD032-3 theorem 0.0 2 1 18 0 7 0 0 0 2 18 110 139 0 FLD033-1 timeout 500.0 19 FLD033-3 theorem 0.1 2 1 126 0 8 0 0 0 2 126 1084 2200 0 FLD034-1 theorem 0.8 2 1 60 0 7 0 0 0 2 60 233 2047 0 FLD034-3 theorem 0.0 2 1 18 0 7 0 0 0 2 18 120 183 0 FLD035-1 timeout 500.0 19 FLD035-3 theorem 0.2 3 1 181 0 11 0 0 0 2 181 1229 8064 0 FLD036-1 timeout 500.0 19 FLD036-3 theorem 0.1 3 1 181 0 11 0 0 0 2 181 1229 8064 0 FLD037-1 theorem 135.1 14 1 275 0 8 0 0 0 3 275 11553 51689 0 FLD037-3 theorem 0.1 2 1 128 0 8 0 0 0 2 128 1883 2362 0 FLD038-1 timeout 500.0 19 FLD038-3 theorem 0.0 2 1 64 0 8 0 0 0 2 64 277 2055 0 FLD039-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 65 71 0 FLD039-3 theorem 0.0 2 1 15 0 6 0 0 0 2 15 81 126 0 FLD040-1 timeout 500.0 15 FLD040-3 theorem 0.0 2 1 67 0 6 0 0 0 2 67 537 907 0 FLD040-5 theorem 0.0 2 1 68 0 6 0 0 0 2 68 601 904 0 FLD041-1 timeout 500.0 19 FLD041-2 timeout 500.0 20 FLD041-3 theorem 0.1 2 1 188 0 8 0 0 0 2 188 2588 2269 0 FLD041-4 theorem 0.4 3 1 343 0 10 0 0 0 2 343 10802 5214 0 FLD042-1 timeout 500.0 19 FLD042-3 theorem 0.1 2 1 188 0 8 0 0 0 2 188 2588 2269 0 FLD043-1 timeout 500.0 14 FLD043-3 theorem 0.0 2 1 107 0 7 0 0 0 2 107 851 2223 0 FLD043-5 theorem 9.7 11 1 684 0 5 0 0 0 2 684 101318 13914 0 FLD044-1 timeout 500.0 19 FLD044-2 timeout 500.0 31 FLD044-3 timeout 500.0 56 FLD044-4 timeout 500.0 56 FLD045-1 timeout 500.0 19 FLD045-2 timeout 500.0 21 FLD045-3 timeout 500.0 56 FLD045-4 timeout 500.0 52 FLD046-1 timeout 500.0 15 FLD046-3 timeout 500.0 64 FLD047-1 timeout 500.0 19 FLD047-2 timeout 500.0 30 FLD047-3 timeout 500.0 80 FLD047-4 theorem 0.5 2 1 441 0 15 0 0 0 2 441 5200 22960 0 FLD048-1 timeout 500.0 20 FLD048-2 timeout 500.0 28 FLD048-3 timeout 500.0 66 FLD048-4 theorem 259.8 31 1 2432 0 20 0 0 0 2 2432 157881 113120 0 FLD049-1 timeout 500.0 21 FLD049-2 timeout 500.0 31 FLD049-3 timeout 500.0 67 FLD049-4 theorem 0.3 4 1 295 0 15 0 0 0 2 295 1927 22696 0 FLD050-1 timeout 500.0 28 FLD050-2 timeout 500.0 31 FLD050-3 timeout 500.0 67 FLD050-4 theorem 0.3 4 1 298 0 15 0 0 0 2 298 1974 22714 0 FLD051-1 timeout 500.0 18 FLD051-2 timeout 500.0 26 FLD051-3 timeout 500.0 74 FLD051-4 theorem 407.7 38 1 3114 0 21 0 0 0 2 3114 213946 113454 0 FLD052-1 timeout 500.0 20 FLD052-2 timeout 500.0 14 FLD052-3 timeout 500.0 67 FLD052-4 theorem 3.5 13 1 932 0 25 0 0 0 2 932 9605 182444 0 FLD053-1 timeout 500.0 20 FLD053-2 timeout 500.0 13 FLD053-3 timeout 500.0 66 FLD053-4 timeout 500.0 39 FLD054-1 timeout 500.0 19 FLD054-2 timeout 500.0 21 FLD054-3 timeout 500.0 76 FLD054-4 theorem 0.4 4 1 419 0 14 0 0 0 2 419 5923 14352 0 FLD055-1 theorem 0.0 4 1 27 0 9 0 0 0 2 27 278 396 0 FLD055-3 theorem 0.0 4 1 20 0 9 0 0 0 2 20 154 259 0 FLD056-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 57 64 0 FLD056-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 57 64 0 FLD057-1 timeout 500.0 13 FLD057-3 timeout 500.0 120 FLD058-1 theorem 0.0 4 1 25 0 9 0 0 0 2 25 213 275 0 FLD058-3 theorem 0.0 4 1 21 0 9 0 0 0 2 21 131 199 0 FLD059-1 theorem 0.2 4 1 40 0 6 0 0 0 2 40 141 791 0 FLD059-2 theorem 0.8 4 1 177 0 8 0 0 0 2 177 908 2480 0 FLD059-3 theorem 0.0 4 1 54 0 6 0 0 0 2 54 322 833 0 FLD059-4 theorem 0.0 4 1 14 0 8 0 0 0 2 14 107 173 0 FLD060-1 theorem 0.8 4 1 133 0 7 0 0 0 2 133 517 2165 0 FLD060-2 theorem 6.9 4 1 267 0 11 0 0 0 2 267 1054 8300 0 FLD060-3 theorem 32.5 17 1 996 0 7 0 0 0 2 996 145733 26815 0 FLD060-4 theorem 0.3 4 1 313 0 11 0 0 0 2 313 3407 8487 0 FLD061-1 theorem 6.9 4 1 245 0 10 0 0 0 2 245 889 8166 0 FLD061-2 theorem 33.8 4 1 421 0 14 0 0 0 2 421 1571 22732 0 FLD061-3 theorem 191.3 35 1 1854 0 10 0 0 0 2 1854 290812 57117 0 FLD061-4 theorem 0.8 4 1 471 0 14 0 0 0 2 471 5072 22973 0 FLD062-1 timeout 500.0 19 FLD062-3 theorem 91.1 33 1 1101 0 7 0 0 0 2 1101 276678 85188 0 FLD063-1 timeout 500.0 19 FLD063-3 theorem 24.7 15 1 818 0 7 0 0 0 2 818 111768 25639 0 FLD064-1 timeout 500.0 15 FLD064-3 theorem 0.1 4 1 87 0 6 0 0 0 2 87 1933 1305 0 FLD065-1 timeout 500.0 15 FLD065-3 theorem 0.0 4 1 12 0 6 0 0 0 2 12 67 105 0 FLD066-1 timeout 500.0 19 FLD066-3 theorem 0.2 4 1 207 0 12 0 0 0 2 207 1580 13965 0 FLD067-1 theorem 86.5 12 1 202 0 7 0 0 0 3 202 9543 35389 0 FLD067-2 timeout 500.0 19 FLD067-3 timeout 500.0 56 FLD067-4 theorem 0.1 4 1 107 0 9 0 0 0 2 107 531 4188 0 FLD068-1 timeout 500.0 19 FLD068-2 timeout 500.0 20 FLD068-3 timeout 500.0 56 FLD068-4 theorem 0.1 4 1 87 0 9 0 0 0 2 87 372 4172 0 FLD069-1 theorem 0.8 4 1 98 0 9 0 0 0 2 98 401 2130 0 FLD069-3 theorem 0.0 4 1 16 0 9 0 0 0 2 16 110 194 0 FLD070-1 theorem 0.8 4 1 60 0 8 0 0 0 2 60 220 1955 0 FLD070-2 theorem 2.6 4 1 266 0 10 0 0 0 2 266 1401 5021 0 FLD070-3 theorem 0.0 4 1 80 0 8 0 0 0 2 80 453 2008 0 FLD070-4 theorem 0.0 4 1 17 0 10 0 0 0 2 17 155 255 0 FLD071-1 theorem 0.0 4 1 8 0 8 0 0 0 2 8 103 116 0 FLD071-2 theorem 2.6 4 1 100 0 10 0 0 0 2 100 376 4176 0 FLD071-3 theorem 0.0 4 1 9 0 8 0 0 0 2 9 98 104 0 FLD071-4 theorem 0.0 4 1 9 0 9 0 0 0 2 9 141 157 0 FLD072-1 timeout 500.0 19 FLD072-2 timeout 500.0 20 FLD072-3 timeout 500.0 62 FLD072-4 timeout 500.0 99 FLD073-1 timeout 500.0 19 FLD073-2 timeout 500.0 20 FLD073-3 timeout 500.0 72 FLD073-4 timeout 500.0 99 FLD074-1 timeout 500.0 19 FLD074-2 timeout 500.0 33 FLD074-3 timeout 500.0 53 FLD074-4 timeout 500.0 51 FLD075-1 timeout 500.0 19 FLD075-2 timeout 500.0 27 FLD075-3 timeout 500.0 53 FLD075-4 timeout 500.0 51 FLD076-1 timeout 500.0 20 FLD076-2 timeout 500.0 23 FLD076-3 timeout 500.0 69 FLD076-4 timeout 500.0 56 FLD077-1 timeout 500.0 19 FLD077-2 timeout 500.0 22 FLD077-3 timeout 500.0 69 FLD077-4 timeout 500.0 56 FLD078-1 timeout 500.0 19 FLD078-2 timeout 500.0 19 FLD078-3 timeout 500.0 65 FLD078-4 timeout 500.0 70 FLD079-1 timeout 500.0 19 FLD079-2 timeout 500.0 20 FLD079-3 timeout 500.0 84 FLD079-4 timeout 500.0 94 FLD080-1 timeout 500.0 14 FLD080-2 timeout 500.0 19 FLD080-3 timeout 500.0 88 FLD080-4 timeout 500.0 79 FLD081-1 timeout 500.0 29 FLD081-2 timeout 500.0 34 FLD081-3 timeout 500.0 53 FLD081-4 timeout 500.0 71 FLD082-1 timeout 500.0 19 FLD082-3 timeout 500.0 85 FLD083-1 timeout 500.0 19 FLD083-3 timeout 500.0 85 FLD084-1 timeout 500.0 19 FLD084-3 timeout 500.0 75 FLD085-1 timeout 500.0 19 FLD085-3 timeout 500.0 77 FLD086-1 timeout 500.0 15 FLD086-3 timeout 500.0 65 FLD087-1 timeout 500.0 15 FLD087-3 timeout 500.0 67 FLD088-1 timeout 500.0 15 FLD088-3 timeout 500.0 67 FLD089-1 timeout 500.0 15 FLD089-3 timeout 500.0 67 FLD090-1 timeout 500.0 14 FLD090-3 timeout 500.0 70 FLD091-1 timeout 500.0 15 FLD091-3 timeout 500.0 62 FLD092-1 timeout 500.0 15 FLD092-3 timeout 500.0 62 FLD093-1 timeout 500.0 15 FLD093-3 timeout 500.0 64 FLD094-1 timeout 500.0 15 FLD094-3 timeout 500.0 62 FLD095-1 timeout 500.0 20 FLD095-2 timeout 500.0 31 FLD095-3 timeout 500.0 72 FLD095-4 timeout 500.0 43 FLD096-1 timeout 500.0 28 FLD096-2 timeout 500.0 31 FLD096-3 timeout 500.0 73 FLD096-4 timeout 500.0 43 FLD097-1 timeout 500.0 19 FLD097-2 timeout 500.0 28 FLD097-3 timeout 500.0 56 FLD097-4 theorem 362.3 39 1 1998 0 18 0 0 0 2 1998 249621 145167 0 FLD098-1 timeout 500.0 19 FLD098-2 timeout 500.0 30 FLD098-3 timeout 500.0 56 FLD098-4 timeout 500.0 52 FLD099-1 timeout 500.0 15 FLD099-2 timeout 500.0 19 FLD099-3 timeout 500.0 63 FLD099-4 timeout 500.0 108 FLD100-1 timeout 500.0 19 FLD100-2 timeout 500.0 28 FLD100-3 timeout 500.0 56 FLD100-4 timeout 500.0 53 GEO001-1 timeout 500.0 124 GEO001-2 timeout 500.0 121 GEO001-3 timeout 500.0 114 GEO001-4 timeout 500.0 60 GEO002-1 theorem 9.1 9 1 54 0 8 0 6 0 2 54 1531 68593 0 GEO002-2 theorem 8.4 8 1 48 0 8 0 3 0 2 48 1227 52544 0 GEO002-3 theorem 0.0 2 1 15 0 15 0 0 0 2 15 292 715 0 GEO002-4 theorem 0.0 2 1 13 0 3 0 3 0 2 13 57 0 0 GEO003-1 theorem 0.0 2 1 12 0 8 0 0 0 2 12 150 273 0 GEO003-2 theorem 0.0 2 1 11 0 8 0 0 0 2 11 115 209 0 GEO003-3 theorem 0.0 2 1 14 0 14 0 0 0 2 14 232 443 0 GEO004-1 timeout 500.0 126 GEO004-2 timeout 500.0 120 GEO005-1 timeout 500.0 125 GEO005-2 timeout 500.0 120 GEO006-1 timeout 500.0 121 GEO006-2 timeout 500.0 122 GEO006-3 timeout 500.0 104 GEO007-1 timeout 500.0 126 GEO007-2 timeout 500.0 121 GEO007-3 timeout 500.0 69 GEO008-1 timeout 500.0 123 GEO008-2 timeout 500.0 120 GEO008-3 timeout 500.0 71 GEO009-1 timeout 500.0 124 GEO009-2 timeout 500.0 122 GEO009-3 timeout 500.0 70 GEO010-1 timeout 500.0 127 GEO010-2 timeout 500.0 124 GEO010-3 timeout 500.0 68 GEO011-1 timeout 500.0 126 GEO011-2 theorem 0.0 2 1 8 0 8 0 0 0 2 8 72 61 0 GEO011-3 theorem 0.3 3 1 24 0 25 0 0 0 2 24 2483 4272 0 GEO011-4 theorem 0.0 2 1 7 0 7 0 0 0 2 7 68 50 0 GEO011-5 theorem 0.0 2 1 7 0 7 0 0 0 2 7 52 30 0 GEO012-1 timeout 500.0 123 GEO012-2 timeout 500.0 122 GEO012-3 timeout 500.0 67 GEO013-1 timeout 500.0 122 GEO013-2 timeout 500.0 125 GEO013-3 timeout 500.0 67 GEO014-2 theorem 0.0 2 1 8 0 8 0 0 0 2 8 72 51 0 GEO015-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 92 58 0 GEO015-3 theorem 0.0 2 1 10 0 10 0 0 0 2 10 109 176 0 GEO016-2 theorem 0.0 2 1 9 0 9 0 0 0 2 9 80 55 0 GEO016-3 theorem 0.0 2 1 10 0 10 0 0 0 2 10 111 178 0 GEO017-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 117 185 0 GEO017-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 120 187 0 GEO018-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 89 58 0 GEO018-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 129 187 0 GEO019-2 theorem 0.0 2 1 9 0 9 0 0 0 2 9 82 56 0 GEO019-3 theorem 0.0 2 1 10 0 10 0 0 0 2 10 119 184 0 GEO020-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 114 183 0 GEO020-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 120 187 0 GEO021-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 89 58 0 GEO021-3 theorem 0.0 2 1 11 0 10 0 0 0 2 11 129 187 0 GEO022-2 theorem 0.0 2 1 12 0 10 0 0 0 2 12 130 195 0 GEO022-3 theorem 0.0 2 1 12 0 11 0 0 0 2 12 168 223 0 GEO024-2 theorem 0.0 2 1 11 0 8 0 0 0 2 11 120 188 0 GEO024-3 theorem 0.0 2 1 15 0 14 0 0 0 2 15 250 328 0 GEO025-2 timeout 500.0 123 GEO025-3 timeout 500.0 119 GEO026-2 theorem 0.0 2 1 14 0 12 0 0 0 2 14 157 275 0 GEO026-3 theorem 0.0 2 1 20 0 19 0 0 0 2 20 409 739 0 GEO027-2 theorem 0.1 2 1 20 0 10 0 0 0 2 20 442 1239 0 GEO027-3 theorem 0.0 2 1 18 0 17 0 0 0 2 18 344 632 0 GEO028-2 timeout 500.0 116 GEO028-3 timeout 500.0 113 GEO029-2 timeout 500.0 117 GEO029-3 theorem 7.4 6 1 52 0 16 0 0 0 2 52 4258 41496 0 GEO030-2 timeout 500.0 120 GEO030-3 timeout 500.0 102 GEO031-2 timeout 500.0 118 GEO031-3 timeout 500.0 102 GEO032-2 timeout 500.0 124 GEO032-3 theorem 0.2 2 1 27 0 28 0 0 0 2 27 1652 3159 0 GEO033-2 timeout 500.0 119 GEO033-3 theorem 0.3 3 1 31 0 31 0 0 0 2 31 2362 4694 0 GEO034-2 timeout 500.0 119 GEO034-3 timeout 500.0 93 GEO035-2 theorem 0.0 2 1 8 0 8 0 0 0 2 8 66 51 0 GEO035-3 theorem 0.0 2 1 9 0 9 0 0 0 2 9 118 199 0 GEO036-2 timeout 500.0 121 GEO036-3 timeout 500.0 105 GEO037-2 timeout 500.0 119 GEO037-3 timeout 500.0 103 GEO038-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 86 64 0 GEO038-3 theorem 0.0 2 1 12 0 11 0 0 0 2 12 159 244 0 GEO039-2 timeout 500.0 122 GEO039-3 timeout 500.0 115 GEO040-2 timeout 500.0 121 GEO040-3 timeout 500.0 104 GEO041-2 timeout 500.0 120 GEO041-3 timeout 500.0 104 GEO042-2 timeout 500.0 121 GEO042-3 timeout 500.0 104 GEO043-2 timeout 500.0 120 GEO043-3 timeout 500.0 105 GEO044-2 timeout 500.0 124 GEO044-3 timeout 500.0 103 GEO045-2 timeout 500.0 122 GEO045-3 timeout 500.0 103 GEO046-2 timeout 500.0 120 GEO046-3 timeout 500.0 103 GEO047-2 timeout 500.0 120 GEO047-3 timeout 500.0 104 GEO048-2 timeout 500.0 122 GEO048-3 timeout 500.0 102 GEO049-2 timeout 500.0 123 GEO049-3 timeout 500.0 65 GEO050-2 timeout 500.0 125 GEO050-3 timeout 500.0 69 GEO051-2 timeout 500.0 125 GEO051-3 timeout 500.0 69 GEO052-2 timeout 500.0 122 GEO052-3 timeout 500.0 70 GEO053-2 timeout 500.0 119 GEO053-3 theorem 0.6 3 1 29 0 29 0 0 0 2 29 3658 6484 0 GEO054-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 85 65 0 GEO054-3 theorem 0.0 2 1 11 0 11 0 0 0 2 11 154 239 0 GEO055-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 89 62 0 GEO055-3 theorem 0.0 2 1 12 0 11 0 0 0 2 12 185 235 0 GEO056-2 timeout 500.0 108 GEO056-3 theorem 0.0 2 1 15 0 14 0 0 0 2 15 265 377 0 GEO057-2 theorem 0.0 2 1 14 0 9 0 0 0 2 14 152 233 0 GEO057-3 theorem 0.0 2 1 13 0 13 0 0 0 2 13 191 300 0 GEO058-2 timeout 500.0 113 GEO058-3 theorem 0.1 2 1 23 0 15 0 0 0 2 23 570 1207 0 GEO059-2 timeout 500.0 109 GEO059-3 theorem 0.1 2 1 22 0 15 0 0 0 2 22 505 1128 0 GEO060-2 timeout 500.0 110 GEO061-2 timeout 500.0 108 GEO061-3 timeout 500.0 95 GEO062-2 timeout 500.0 108 GEO062-3 timeout 500.0 68 GEO063-2 timeout 500.0 105 GEO063-3 timeout 500.0 65 GEO064-2 timeout 500.0 124 GEO064-3 theorem 0.5 3 1 28 0 28 0 0 0 2 28 3383 6051 0 GEO065-2 timeout 500.0 124 GEO065-3 theorem 0.5 3 1 28 0 28 0 0 0 2 28 3383 6051 0 GEO066-2 timeout 500.0 124 GEO066-3 theorem 0.5 3 1 28 0 28 0 0 0 2 28 3383 6051 0 GEO067-2 timeout 500.0 124 GEO067-3 timeout 500.0 66 GEO068-2 timeout 500.0 125 GEO068-3 timeout 500.0 65 GEO069-2 timeout 500.0 124 GEO069-3 timeout 500.0 68 GEO070-2 timeout 500.0 120 GEO070-3 timeout 500.0 66 GEO071-2 timeout 500.0 119 GEO071-3 timeout 500.0 67 GEO072-2 timeout 500.0 119 GEO072-3 timeout 500.0 68 GEO073-1 timeout 500.0 119 GEO073-2 timeout 500.0 121 GEO073-3 timeout 500.0 69 GEO074-2 timeout 500.0 120 GEO075-2 timeout 500.0 96 GEO076-4 theorem 0.3 2 1 108 0 3 0 0 0 3 108 898 2793 0 GEO077-4 theorem 0.3 3 1 89 0 13 0 0 0 2 89 491 7913 0 GEO078-4 timeout 500.0 21 GEO078-5 timeout 500.0 40 GEO079-1 theorem 0.0 2 1 3 0 2 0 0 0 2 3 6 0 0 GEO080-1 theorem 0.0 2 1 4 0 3 0 0 0 2 4 18 21 0 GEO081-1 theorem 0.0 2 1 52 0 5 0 0 0 2 52 254 350 0 GEO082-1 theorem 0.1 2 2 117 9 5 0 0 916 2 125 1307 1715 0 GEO083-1 timeout 500.0 34 GEO084-1 timeout 500.0 52 GEO085-1 timeout 500.0 188 GEO086-1 theorem 0.0 2 1 12 0 5 0 0 0 2 12 75 51 0 GEO087-1 theorem 0.0 2 1 7 0 4 0 0 0 2 7 46 33 0 GEO088-1 timeout 500.0 101 GEO089-1 timeout 500.0 101 GEO090-1 timeout 500.0 17 GEO091-1 timeout 500.0 12 GEO092-1 timeout 500.0 122 GEO093-1 timeout 500.0 39 GEO094-1 theorem 0.0 2 1 52 0 6 0 0 0 2 52 254 477 0 GEO095-1 memory 474.4 499 GEO096-1 timeout 500.0 15 GEO097-1 timeout 500.0 123 GEO098-1 timeout 500.0 108 GEO099-1 timeout 500.0 13 GEO100-1 timeout 500.0 181 GEO101-1 timeout 500.0 182 GEO102-1 timeout 500.0 12 GEO103-1 timeout 500.0 14 GEO104-1 timeout 500.0 38 GEO105-1 timeout 500.0 12 GEO106-1 timeout 500.0 13 GEO107-1 timeout 500.0 38 GEO108-1 timeout 500.0 31 GEO109-1 timeout 500.0 146 GEO110-1 timeout 500.0 16 GEO111-1 theorem 0.0 2 1 42 0 4 5 0 0 2 42 212 394 0 GEO112-1 theorem 0.0 2 1 22 0 4 0 0 0 2 22 96 111 0 GEO113-1 timeout 500.0 116 GEO114-1 timeout 500.0 191 GEO115-1 timeout 500.0 29 GEO116-1 timeout 500.0 11 GEO117-1 theorem 0.0 2 1 7 0 5 0 0 0 2 7 37 25 0 GEO118-1 theorem 0.0 2 1 8 0 6 0 0 0 2 8 46 32 0 GEO119-1 timeout 500.0 30 GEO120-1 timeout 500.0 28 GEO121-1 timeout 500.0 37 GEO122-1 timeout 500.0 189 GEO123-1 timeout 500.0 24 GEO124-1 theorem 0.0 2 1 26 0 7 0 0 0 2 26 107 134 0 GEO125-1 theorem 0.0 2 1 26 0 7 0 0 0 2 26 106 134 0 GEO126-1 timeout 500.0 199 GEO127-1 timeout 500.0 27 GEO128-1 timeout 500.0 24 GEO129-1 timeout 500.0 58 GEO130-1 timeout 500.0 20 GEO131-1 timeout 500.0 25 GEO132-1 timeout 500.0 10 GEO133-1 timeout 500.0 13 GEO134-1 timeout 500.0 16 GEO135-1 timeout 500.0 44 GEO136-1 timeout 500.0 16 GEO137-1 timeout 500.0 8 GEO138-1 timeout 500.0 8 GEO139-1 memory 201.5 499 GEO140-1 timeout 500.0 21 GEO141-1 timeout 500.0 24 GEO142-1 timeout 500.0 23 GEO143-1 timeout 500.0 19 GEO144-1 timeout 500.0 12 GEO145-1 timeout 500.0 295 GEO146-1 timeout 500.0 74 GEO147-1 timeout 500.0 83 GEO148-1 timeout 500.0 54 GEO149-1 timeout 500.0 28 GEO150-1 timeout 500.0 143 GEO151-1 timeout 500.0 21 GEO152-1 timeout 500.0 21 GEO153-1 timeout 500.0 128 GEO153-2 timeout 500.0 121 GEO154-1 timeout 500.0 127 GEO154-2 timeout 500.0 123 GEO155-1 timeout 500.0 110 GEO156-1 timeout 500.0 109 GEO157-1 timeout 500.0 63 GEO158-1 timeout 500.0 57 GEO159-1 timeout 500.0 70 GEO160-1 timeout 500.0 214 GEO161-1 timeout 500.0 130 GRA001-1 theorem 0.0 4 4 10 3 16 28 0 1 2 5 22 10 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-3 timeout 500.0 460 GRP001-4 theorem 0.6 4 1 211 0 6 0 2 0 3 211 10655 0 0 GRP001-5 theorem 0.0 4 1 7 0 5 0 0 0 2 7 96 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 GRP003-1 theorem 0.0 4 1 5 0 3 0 0 0 3 5 48 0 0 GRP003-2 theorem 0.0 4 1 24 0 4 0 0 0 2 24 860 0 0 GRP004-1 theorem 0.0 4 1 11 0 3 0 0 0 2 11 160 0 0 GRP004-2 theorem 0.0 4 1 22 0 4 0 0 0 2 22 824 0 0 GRP005-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 72 0 0 GRP006-1 theorem 0.0 4 1 7 0 6 0 0 0 2 7 74 0 0 GRP007-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 229 0 0 GRP008-1 theorem 3.8 6 2 81 1 7 0 0 42222 2 81 42594 42367 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 GRP015-1 memory 462.2 499 GRP016-1 memory 481.5 499 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-4 timeout 500.0 391 GRP024-5 timeout 500.0 340 GRP025-1 timeout 500.0 79 GRP025-2 timeout 500.0 129 GRP025-3 timeout 500.0 79 GRP025-4 timeout 500.0 131 GRP026-1 timeout 500.0 101 GRP026-2 timeout 500.0 164 GRP026-3 timeout 500.0 101 GRP026-4 timeout 500.0 170 GRP027-1 timeout 500.0 27 GRP027-2 timeout 500.0 27 GRP028-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 5 0 0 GRP028-2 theorem 0.0 4 1 5 0 5 0 0 0 2 5 34 0 0 GRP028-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 9 0 0 GRP028-4 theorem 0.0 4 1 3 0 3 0 0 0 2 3 6 0 0 GRP029-1 theorem 0.2 4 1 11 0 5 0 0 0 3 11 284 0 0 GRP029-2 theorem 0.2 4 1 11 0 5 0 0 0 3 11 281 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 GRP031-2 theorem 0.0 4 1 11 0 4 0 0 0 2 11 176 0 0 GRP032-3 theorem 0.0 4 1 7 0 7 0 0 0 2 7 80 0 0 GRP033-3 theorem 0.0 4 1 8 0 7 0 0 0 2 8 155 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 GRP034-4 theorem 0.0 4 1 7 0 6 0 0 0 2 7 78 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 GRP039-1 timeout 500.0 87 GRP039-2 timeout 500.0 29 GRP039-3 timeout 500.0 89 GRP039-4 timeout 500.0 88 GRP039-5 timeout 500.0 29 GRP039-6 theorem 13.9 4 20 1644 23 9 0 1 26271 2 640 199863 28775 0 GRP039-7 timeout 500.0 30 GRP040-3 timeout 500.0 159 GRP040-4 timeout 500.0 155 GRP041-2 theorem 0.0 4 1 3 0 3 0 0 0 2 3 20 0 0 GRP042-2 theorem 0.0 4 1 6 0 5 0 0 0 2 6 34 0 0 GRP043-2 theorem 0.0 4 1 15 0 6 0 0 0 2 15 156 0 0 GRP044-2 theorem 0.0 4 1 7 0 6 0 0 0 2 7 62 0 0 GRP045-2 theorem 0.0 4 1 17 0 6 0 0 0 2 17 428 0 0 GRP046-2 theorem 0.0 4 1 16 0 5 0 0 0 2 16 394 0 0 GRP047-2 theorem 0.0 4 1 16 0 5 0 0 0 2 16 425 0 0 GRP048-2 theorem 2.3 4 1 45 0 5 0 0 0 3 45 9873 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 GRP113-1 timeout 500.0 20 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 GRP123-1.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 87 44 0 GRP123-1.005 non_thm 0.1 4 0 143 4 26 0 0 256 2 0 1556 505 0 GRP123-2.003 theorem 0.0 4 1 37 0 15 0 0 0 2 37 94 44 0 GRP123-2.005 non_thm 0.1 4 1 189 2 40 0 0 259 2 152 1815 595 0 GRP123-3.003 theorem 0.0 4 1 51 0 20 0 0 0 2 51 111 53 0 GRP123-3.004 non_thm 0.0 4 1 143 1 32 0 0 155 2 95 951 257 0 GRP123-4.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 105 116 0 GRP123-4.004 non_thm 0.0 4 0 77 1 17 0 0 244 2 0 802 449 0 GRP123-6.003 theorem 0.0 4 1 50 0 11 0 0 0 2 50 143 82 0 GRP123-6.005 non_thm 0.1 4 0 264 4 27 0 0 453 2 0 1624 947 0 GRP123-7.003 theorem 0.0 4 1 56 0 16 0 0 0 2 56 149 82 0 GRP123-7.005 non_thm 0.1 4 0 284 4 41 0 0 453 2 0 1644 947 0 GRP123-8.003 theorem 0.0 4 1 62 0 21 0 0 0 2 62 156 87 0 GRP123-8.004 non_thm 0.0 4 0 177 2 33 0 0 234 2 0 879 372 0 GRP123-9.003 theorem 0.0 4 1 50 0 11 0 0 0 2 50 143 100 0 GRP123-9.004 non_thm 0.0 4 0 138 29 18 0 0 214 2 0 813 379 0 GRP124-1.004 theorem 0.0 4 2 72 1 17 0 0 20 2 64 392 155 0 GRP124-1.005 non_thm 0.1 4 0 142 5 26 0 0 255 2 0 1556 505 0 GRP124-2.004 theorem 0.0 4 1 75 0 26 0 0 0 2 75 182 111 0 GRP124-2.005 non_thm 0.1 4 0 173 2 40 0 0 258 2 0 1590 505 0 GRP124-3.004 theorem 0.0 4 2 117 1 32 0 0 31 2 106 337 171 0 GRP124-3.005 non_thm 0.1 4 2 244 4 47 0 0 331 2 176 1899 670 0 GRP124-4.004 theorem 0.0 4 2 66 1 17 0 0 50 2 62 293 350 0 GRP124-4.005 non_thm 0.1 4 0 143 4 26 0 0 566 2 0 1606 1305 0 GRP124-6.004 theorem 0.0 4 2 109 1 18 0 0 37 2 101 424 234 0 GRP124-6.005 non_thm 0.1 4 0 263 5 27 0 0 452 2 0 1624 947 0 GRP124-7.004 theorem 0.0 4 2 121 1 27 0 0 37 2 113 436 234 0 GRP124-7.005 non_thm 0.1 4 0 283 5 41 0 0 452 2 0 1644 947 0 GRP124-8.004 theorem 0.0 4 2 148 2 33 0 0 56 2 141 490 259 0 GRP124-8.005 non_thm 0.1 4 0 322 6 48 0 0 513 2 0 1739 1009 0 GRP124-9.004 theorem 0.0 4 2 109 1 18 0 0 37 2 101 424 266 0 GRP124-9.005 non_thm 0.1 4 0 263 50 27 0 0 457 2 0 1624 997 0 GRP125-1.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 94 43 0 GRP125-1.004 non_thm 0.0 4 0 77 1 17 0 0 111 2 0 469 180 0 GRP125-2.004 non_thm 0.0 4 0 96 0 26 0 0 112 2 0 490 180 0 GRP125-2.005 theorem 0.0 4 3 184 2 40 0 0 58 2 157 800 479 0 GRP125-3.004 non_thm 0.0 4 1 143 1 32 0 0 142 2 95 669 247 0 GRP125-3.005 theorem 0.1 4 5 280 4 47 0 0 131 2 219 1294 748 0 GRP125-4.003 theorem 0.0 4 1 31 0 10 0 0 0 2 31 146 117 0 GRP125-4.004 non_thm 0.0 4 0 77 1 17 0 0 257 2 0 719 462 0 GRP126-1.004 theorem 0.0 4 2 69 1 17 0 0 19 2 63 316 141 0 GRP126-1.005 non_thm 0.0 4 0 143 4 26 0 0 235 2 0 935 484 0 GRP126-2.004 theorem 0.0 4 1 75 0 26 0 0 0 2 75 224 111 0 GRP126-2.005 non_thm 0.0 4 0 173 2 40 0 0 237 2 0 969 484 0 GRP126-3.004 theorem 0.0 4 2 117 1 32 0 0 30 2 106 371 171 0 GRP126-3.005 non_thm 0.0 4 2 244 4 47 0 0 310 2 174 1271 649 0 GRP126-4.004 theorem 0.0 4 2 67 1 17 0 0 51 2 63 403 367 0 GRP126-4.005 non_thm 0.1 4 0 144 3 26 0 0 588 2 0 1427 1326 0 GRP127-1.004 theorem 0.0 4 2 72 1 17 0 0 19 2 64 352 151 0 GRP127-1.005 non_thm 0.1 4 0 145 2 26 0 0 237 2 0 935 484 0 GRP127-2.005 non_thm 0.0 4 1 187 1 40 0 0 239 2 130 1050 542 0 GRP127-2.006 theorem 0.1 4 3 313 2 57 0 0 85 2 253 1328 1321 0 GRP127-3.004 theorem 0.0 4 2 117 1 32 0 0 30 2 106 347 170 0 GRP127-3.005 non_thm 0.1 4 2 271 2 47 0 0 296 2 181 1407 744 0 GRP127-4.004 theorem 0.0 4 2 68 1 17 0 0 51 2 63 429 368 0 GRP127-4.005 non_thm 0.1 4 0 145 2 26 0 0 589 2 0 1427 1326 0 GRP128-1.003 theorem 0.0 4 4 59 3 9 0 0 5 2 32 200 90 0 GRP128-1.004 non_thm 0.0 4 7 171 8 16 0 0 143 2 48 925 392 0 GRP128-2.004 non_thm 0.0 4 1 100 3 25 0 0 122 2 40 537 198 0 GRP128-2.006 theorem 0.1 4 8 428 7 56 0 0 173 2 251 1751 1545 0 GRP128-3.004 non_thm 0.0 4 3 212 4 31 0 0 156 2 92 876 345 0 GRP128-3.005 theorem 0.1 4 7 395 6 46 0 0 78 2 207 1467 858 0 GRP128-4.003 theorem 0.0 4 4 28 3 9 0 0 9 2 28 193 108 0 GRP128-4.004 non_thm 0.0 4 5 83 6 16 0 0 275 2 54 884 512 0 GRP129-1.003 theorem 0.0 4 4 59 3 9 0 0 5 2 29 238 92 0 GRP129-1.005 non_thm 0.1 4 24 686 28 25 0 0 429 2 85 3378 2149 0 GRP129-2.004 theorem 0.0 4 7 164 7 25 0 0 47 2 78 599 258 0 GRP129-2.005 non_thm 0.1 4 10 316 15 39 0 0 300 2 122 1745 820 0 GRP129-3.004 theorem 0.0 4 7 236 7 31 0 0 140 2 115 783 344 0 GRP129-3.005 non_thm 0.1 4 7 390 9 46 0 0 519 2 171 1914 992 0 GRP129-4.004 theorem 0.0 4 9 116 8 16 0 0 35 2 51 665 526 0 GRP129-4.005 non_thm 0.1 4 13 234 16 25 0 0 658 2 49 2184 1880 0 GRP130-1.003 theorem 0.0 4 4 71 3 9 0 0 5 2 36 316 123 0 GRP130-1.005 non_thm 0.1 4 15 393 18 25 0 0 321 2 125 2174 1188 0 GRP130-2.003 theorem 0.0 4 3 68 2 14 0 0 6 2 43 282 104 0 GRP130-2.005 non_thm 0.0 4 3 248 4 39 0 0 254 2 136 1296 688 0 GRP130-3.003 theorem 0.0 4 2 94 1 19 0 0 2 2 68 289 108 0 GRP130-3.004 non_thm 0.0 4 2 202 2 31 0 0 154 2 83 826 334 0 GRP130-4.003 theorem 0.0 4 4 43 3 9 0 0 9 2 25 177 143 0 GRP130-4.004 non_thm 0.0 4 5 120 6 16 0 0 291 2 40 911 650 0 GRP131-1.002 theorem 0.0 4 2 20 1 4 0 0 0 2 14 81 32 0 GRP131-1.005 non_thm 0.1 4 0 147 8 25 0 0 272 2 0 1575 525 0 GRP131-2.002 theorem 0.0 4 2 22 1 6 0 0 0 2 16 84 32 0 GRP131-2.005 non_thm 0.6 4 80 1612 88 39 0 0 1489 2 172 16728 7868 0 GRP132-1.002 theorem 0.0 4 2 20 1 4 0 0 0 2 14 81 32 0 GRP132-1.005 non_thm 0.1 4 0 147 8 25 0 0 272 2 0 1575 525 0 GRP132-2.002 theorem 0.0 4 2 22 1 6 0 0 0 2 16 84 32 0 GRP132-2.005 non_thm 1.0 4 92 2522 99 39 0 0 1228 2 174 29511 12989 0 GRP133-1.003 theorem 0.0 4 4 80 3 9 0 0 5 2 33 340 139 0 GRP133-1.004 non_thm 0.0 4 1 87 3 16 0 0 122 2 52 530 211 0 GRP133-2.003 theorem 0.0 4 3 69 2 14 0 0 6 2 43 251 97 0 GRP133-2.004 non_thm 0.0 4 2 121 5 25 0 0 121 2 79 613 250 0 GRP134-1.003 theorem 0.0 4 4 92 3 9 0 0 5 2 34 434 169 0 GRP134-1.005 non_thm 0.1 4 6 219 10 25 0 0 256 2 138 1724 855 0 GRP134-2.003 theorem 0.0 4 3 86 2 14 0 0 6 2 44 352 127 0 GRP134-2.005 non_thm 0.1 4 6 456 11 39 0 0 368 2 171 3295 1717 0 GRP135-1.002 theorem 0.0 4 2 19 1 4 0 0 0 2 14 61 25 0 GRP135-1.005 non_thm 0.4 4 60 1853 64 25 0 0 1360 2 133 12748 6877 0 GRP135-2.002 theorem 0.0 4 2 21 1 6 0 0 0 2 16 63 25 0 GRP135-2.005 non_thm 0.2 4 20 828 21 39 0 0 545 2 168 5153 2994 0 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 GRP208-1 timeout 500.0 66 GRP209-1 timeout 500.0 66 GRP210-1 timeout 500.0 63 GRP211-1 timeout 500.0 79 GRP212-1 timeout 500.0 119 GRP213-1 timeout 500.0 119 GRP214-1 timeout 500.0 45 GRP215-1 timeout 500.0 65 GRP216-1 timeout 500.0 122 GRP217-1 timeout 500.0 63 GRP218-1 timeout 500.0 66 GRP219-1 timeout 500.0 68 GRP220-1 timeout 500.0 120 GRP221-1 timeout 500.0 120 GRP222-1 timeout 500.0 65 GRP223-1 timeout 500.0 76 GRP224-1 timeout 500.0 63 GRP225-1 timeout 500.0 68 GRP226-1 timeout 500.0 77 GRP227-1 timeout 500.0 119 GRP228-1 timeout 500.0 120 GRP229-1 timeout 500.0 122 GRP230-1 timeout 500.0 63 GRP231-1 timeout 500.0 119 GRP232-1 timeout 500.0 119 GRP233-1 timeout 500.0 119 GRP234-1 timeout 500.0 121 GRP235-1 timeout 500.0 119 GRP236-1 timeout 500.0 116 GRP237-1 timeout 500.0 119 GRP238-1 timeout 500.0 121 GRP239-1 timeout 500.0 119 GRP240-1 timeout 500.0 123 GRP241-1 timeout 500.0 122 GRP242-1 timeout 500.0 121 GRP243-1 timeout 500.0 75 GRP244-1 timeout 500.0 65 GRP245-1 timeout 500.0 72 GRP246-1 timeout 500.0 63 GRP247-1 timeout 500.0 77 GRP248-1 timeout 500.0 70 GRP249-1 timeout 500.0 74 GRP250-1 timeout 500.0 76 GRP251-1 timeout 500.0 75 GRP252-1 timeout 500.0 68 GRP253-1 timeout 500.0 71 GRP254-1 timeout 500.0 66 GRP255-1 timeout 500.0 69 GRP256-1 timeout 500.0 74 GRP257-1 timeout 500.0 70 GRP258-1 timeout 500.0 67 GRP259-1 timeout 500.0 69 GRP260-1 timeout 500.0 67 GRP261-1 timeout 500.0 74 GRP262-1 timeout 500.0 69 GRP263-1 timeout 500.0 67 GRP264-1 timeout 500.0 75 GRP265-1 timeout 500.0 67 GRP266-1 timeout 500.0 69 GRP267-1 timeout 500.0 94 GRP268-1 timeout 500.0 90 GRP269-1 timeout 500.0 67 GRP270-1 timeout 500.0 69 GRP271-1 timeout 500.0 67 GRP272-1 timeout 500.0 67 GRP273-1 timeout 500.0 67 GRP274-1 timeout 500.0 61 GRP275-1 timeout 500.0 75 GRP276-1 timeout 500.0 121 GRP277-1 timeout 500.0 73 GRP278-1 timeout 500.0 67 GRP279-1 timeout 500.0 63 GRP280-1 timeout 500.0 77 GRP281-1 timeout 500.0 74 GRP282-1 timeout 500.0 119 GRP283-1 timeout 500.0 122 GRP284-1 timeout 500.0 74 GRP285-1 timeout 500.0 75 GRP286-1 timeout 500.0 70 GRP287-1 timeout 500.0 79 GRP288-1 timeout 500.0 67 GRP289-1 timeout 500.0 69 GRP290-1 timeout 500.0 63 GRP291-1 timeout 500.0 61 GRP292-1 timeout 500.0 38 GRP293-1 timeout 500.0 73 GRP294-1 timeout 500.0 77 GRP295-1 timeout 500.0 74 GRP296-1 timeout 500.0 75 GRP297-1 timeout 500.0 84 GRP298-1 timeout 500.0 80 GRP299-1 timeout 500.0 86 GRP300-1 timeout 500.0 122 GRP301-1 timeout 500.0 121 GRP302-1 timeout 500.0 180 GRP303-1 timeout 500.0 73 GRP304-1 timeout 500.0 175 GRP305-1 timeout 500.0 126 GRP306-1 timeout 500.0 96 GRP307-1 timeout 500.0 68 GRP308-1 timeout 500.0 139 GRP309-1 timeout 500.0 128 GRP310-1 timeout 500.0 90 GRP311-1 timeout 500.0 126 GRP312-1 timeout 500.0 67 GRP313-1 timeout 500.0 75 GRP314-1 timeout 500.0 77 GRP315-1 timeout 500.0 76 GRP316-1 timeout 500.0 62 GRP317-1 timeout 500.0 119 GRP318-1 timeout 500.0 68 GRP319-1 timeout 500.0 77 GRP320-1 timeout 500.0 69 GRP321-1 timeout 500.0 69 GRP322-1 timeout 500.0 80 GRP323-1 timeout 500.0 79 GRP324-1 timeout 500.0 119 GRP325-1 timeout 500.0 96 GRP326-1 timeout 500.0 64 GRP327-1 timeout 500.0 63 GRP328-1 timeout 500.0 119 GRP329-1 timeout 500.0 119 GRP330-1 timeout 500.0 67 GRP331-1 timeout 500.0 75 GRP332-1 timeout 500.0 73 GRP333-1 timeout 500.0 70 GRP334-1 timeout 500.0 121 GRP335-1 timeout 500.0 74 GRP336-1 timeout 500.0 79 GRP337-1 timeout 500.0 119 GRP338-1 timeout 500.0 67 GRP339-1 timeout 500.0 62 GRP340-1 timeout 500.0 67 GRP341-1 timeout 500.0 69 GRP342-1 timeout 500.0 63 GRP343-1 timeout 500.0 53 GRP344-1 timeout 500.0 66 GRP345-1 timeout 500.0 131 GRP346-1 timeout 500.0 127 GRP347-1 timeout 500.0 121 GRP348-1 timeout 500.0 67 GRP349-1 timeout 500.0 127 GRP350-1 timeout 500.0 67 GRP351-1 timeout 500.0 75 GRP352-1 timeout 500.0 68 GRP353-1 timeout 500.0 51 GRP354-1 timeout 500.0 80 GRP355-1 timeout 500.0 74 GRP356-1 timeout 500.0 79 GRP357-1 timeout 500.0 178 GRP358-1 timeout 500.0 140 GRP359-1 timeout 500.0 176 GRP360-1 timeout 500.0 124 GRP361-1 timeout 500.0 182 GRP362-1 timeout 500.0 119 GRP363-1 timeout 500.0 127 GRP364-1 timeout 500.0 66 GRP365-1 timeout 500.0 66 GRP366-1 timeout 500.0 128 GRP367-1 timeout 500.0 63 GRP368-1 timeout 500.0 70 GRP369-1 timeout 500.0 121 GRP370-1 timeout 500.0 62 GRP371-1 timeout 500.0 122 GRP372-1 timeout 500.0 122 GRP373-1 timeout 500.0 119 GRP374-1 timeout 500.0 119 GRP375-1 timeout 500.0 122 GRP376-1 timeout 500.0 122 GRP377-1 timeout 500.0 122 GRP378-1 timeout 500.0 122 GRP379-1 timeout 500.0 120 GRP380-1 timeout 500.0 121 GRP381-1 timeout 500.0 122 GRP382-1 timeout 500.0 121 GRP383-1 timeout 500.0 120 GRP384-1 timeout 500.0 120 GRP385-1 timeout 500.0 118 GRP386-1 timeout 500.0 121 GRP387-1 timeout 500.0 121 GRP388-1 timeout 500.0 118 GRP389-1 timeout 500.0 92 GRP390-1 timeout 500.0 98 GRP391-1 timeout 500.0 136 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-2 timeout 500.0 262 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 HWV005-1 theorem 0.0 2 1 96 0 10 0 0 0 3 96 323 60 0 HWV005-2 unsound 0.0 2 0 160 1 8 0 0 43 3 0 305 46 0 HWV006-1 theorem 0.1 2 1 356 0 15 1 4 0 4 356 1440 162 0 HWV006-2 unsound 0.1 2 0 864 3 13 0 0 118 4 0 1699 124 0 HWV007-1 theorem 0.1 2 1 352 0 13 1 6 0 4 352 941 144 0 HWV007-2 unsound 0.1 2 0 707 2 11 1 0 117 4 0 1387 121 0 HWV008-1.001 theorem 0.1 2 1 215 0 11 0 0 0 5 215 653 133 0 HWV008-1.002 theorem 0.1 2 1 324 0 14 0 0 0 5 324 934 210 0 HWV008-2.001 theorem 0.1 2 1 215 0 9 0 0 0 5 215 601 100 0 HWV008-2.002 theorem 0.1 2 1 326 0 12 0 0 0 5 326 866 162 0 HWV009-1 theorem 89.7 6 1 565 0 8 3 33 0 3 565 19188 4813 0 HWV009-2 timeout 500.0 39 HWV009-3 theorem 0.0 2 1 13 0 13 0 0 0 2 13 179 140 0 HWV009-4 theorem 0.0 2 1 13 0 13 0 0 0 2 13 179 140 0 HWV010-1 theorem 0.1 2 2 103 1 11 4 7 348 2 102 1139 434 0 HWV010-2 theorem 0.0 2 1 29 0 28 0 0 0 2 29 203 147 0 HWV010-3 theorem 0.0 2 1 37 0 28 0 1 0 2 37 264 200 0 HWV011-1 theorem 0.1 2 2 103 1 11 4 7 348 2 102 1123 430 0 HWV011-2 theorem 0.0 2 1 29 0 28 0 0 0 2 29 199 147 0 HWV011-3 theorem 0.1 2 1 37 0 28 0 1 0 2 37 262 200 0 HWV012-1 theorem 0.0 2 1 14 0 10 0 0 0 2 14 98 91 0 HWV012-2 theorem 0.1 2 1 61 0 29 0 1 0 2 61 540 371 0 HWV013-1 timeout 500.0 24 HWV013-2 timeout 500.0 56 HWV014-1 timeout 500.0 22 HWV014-2 timeout 500.0 43 HWV015-1 timeout 500.0 22 HWV015-2 timeout 500.0 43 HWV016-1 timeout 500.0 22 HWV016-2 timeout 500.0 53 HWV017-1 timeout 500.0 21 HWV017-2 timeout 500.0 53 HWV018-1 timeout 500.0 23 HWV018-2 timeout 500.0 41 HWV018-3 theorem 0.1 2 1 107 0 31 0 1 0 2 107 863 505 0 HWV019-1 theorem 0.0 2 1 53 0 10 2 7 0 2 53 470 238 0 HWV019-2 theorem 0.1 2 1 42 0 30 0 1 0 2 42 292 229 0 HWV019-3 theorem 0.0 2 1 15 0 15 0 0 0 2 15 189 170 0 HWV020-1 timeout 500.0 22 HWV020-2 timeout 500.0 43 HWV020-3 theorem 0.1 2 1 107 0 31 0 1 0 2 107 881 512 0 HWV021-1 theorem 0.0 2 1 57 0 11 0 7 0 2 57 521 257 0 HWV021-2 theorem 0.1 2 1 145 0 30 9 7 0 2 145 1568 985 0 HWV022-1 timeout 500.0 22 HWV022-2 timeout 500.0 53 HWV023-1 timeout 500.0 25 HWV023-2 timeout 500.0 43 HWV024-1 theorem 0.1 2 4 109 3 17 8 7 354 2 107 1164 524 0 HWV024-2 timeout 500.0 35 HWV025-1 theorem 0.1 2 4 109 3 17 8 7 354 2 107 1144 516 0 HWV025-2 theorem 0.0 2 1 31 0 30 0 0 0 2 31 204 180 0 HWV025-3 theorem 0.0 2 1 31 0 30 0 0 0 2 31 204 179 0 HWV026-1 theorem 0.0 2 2 106 2 13 4 7 353 2 107 1120 469 0 HWV026-2 theorem 0.0 2 1 15 0 15 0 0 0 2 15 189 166 0 HWV026-3 theorem 0.0 2 1 15 0 15 0 0 0 2 15 187 162 0 HWV027-1 timeout 500.0 79 HWV027-2 timeout 500.0 40 HWV028-1 timeout 500.0 11 HWV028-2 timeout 500.0 50 HWV029-1 timeout 500.0 24 HWV029-2 timeout 500.0 51 HWV030-1 timeout 500.0 11 HWV030-2 timeout 500.0 50 HWV031-1 timeout 500.0 11 HWV031-2 timeout 500.0 50 HWV032-1 timeout 500.0 11 HWV032-2 timeout 500.0 49 HWV033-1 timeout 500.0 25 HWV033-2 timeout 500.0 52 HWV034-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 HWV034-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 HWV035-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 HWV035-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 HWV036-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 0 2 0 0 HWV036-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 HWV037-1 timeout 500.0 40 HWV038-1 timeout 500.0 39 KRS001-1 theorem 0.0 2 1 8 0 1 0 0 0 2 8 16 19 0 KRS002-1 theorem 0.0 2 1 9 0 1 0 0 0 3 9 16 20 0 KRS003-1 theorem 0.0 2 1 9 0 2 0 0 0 2 9 16 18 0 KRS004-1 theorem 0.0 2 1 2 0 1 0 0 0 2 2 5 0 0 KRS005-1 non_thm 0.0 2 0 8 0 1 0 0 36 2 0 8 36 0 KRS006-1 non_thm 0.0 2 0 20 3 5 0 0 64 3 0 31 71 0 KRS007-1 non_thm 0.0 2 0 27 2 2 0 0 74 3 0 37 85 0 KRS008-1 non_thm 0.1 2 0 42 34 2 0 0 528 3 0 72 810 0 KRS009-1 non_thm 0.0 2 0 43 8 1 0 0 229 3 0 65 237 0 KRS010-1 theorem 0.0 2 2 21 1 2 0 0 77 2 18 38 95 0 KRS011-1 non_thm 0.0 2 0 36 3 2 0 0 37 2 0 44 49 0 KRS012-1 theorem 0.0 2 1 5 0 2 0 0 0 2 5 10 5 0 KRS013-1 theorem 0.0 2 1 17 0 2 0 0 0 3 17 27 45 0 KRS014-1 non_thm 0.0 2 0 14 2 1 0 0 30 2 0 17 32 0 KRS015-1 theorem 0.0 2 1 10 0 1 0 0 0 3 10 18 22 0 KRS016-1 non_thm 0.0 2 0 4 4 2 0 0 10 2 0 4 14 0 KRS017-1 theorem 0.0 2 1 3 0 2 0 0 0 2 3 7 3 0 LAT001-1 timeout 500.0 196 LAT002-1 timeout 500.0 86 LAT003-1 timeout 500.0 286 LAT004-1 timeout 500.0 292 LAT005-1 theorem 3.9 6 1 405 0 17 0 14 0 2 405 95285 0 0 LAT005-2 theorem 2.8 5 1 403 0 21 0 14 0 2 403 75398 0 0 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 LAT058-1 timeout 500.0 263 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 LCL001-1 timeout 500.0 10 LCL002-1 timeout 500.0 38 LCL003-1 theorem 461.7 30 1 2838 0 2 0 415 0 8 2838 1951196 0 0 LCL004-1 theorem 2.7 8 1 310 0 2 0 198 0 8 310 29297 0 0 LCL005-1 timeout 500.0 39 LCL006-1 theorem 0.5 2 1 132 0 3 0 0 0 5 132 5234 0 0 LCL007-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 3 0 0 LCL008-1 theorem 0.0 2 1 7 0 2 0 0 0 5 7 38 0 0 LCL009-1 theorem 0.0 2 1 23 0 2 0 2 0 5 23 263 0 0 LCL010-1 theorem 0.0 2 1 11 0 2 0 0 0 5 11 81 0 0 LCL011-1 theorem 0.0 2 1 24 0 2 0 0 0 5 24 292 0 0 LCL012-1 theorem 30.9 11 1 410 0 2 0 0 0 7 410 71592 0 0 LCL013-1 theorem 0.0 2 1 3 0 2 0 0 0 6 3 4 0 0 LCL014-1 theorem 9.6 7 1 245 0 2 0 1 0 7 245 29886 0 0 LCL015-1 theorem 134.3 14 1 402 0 2 0 0 0 8 402 78866 0 0 LCL016-1 theorem 116.0 21 1 635 0 2 0 0 0 8 635 188208 0 0 LCL017-1 timeout 500.0 26 LCL018-1 theorem 95.1 14 1 349 0 2 0 0 0 9 349 66924 0 0 LCL019-1 timeout 500.0 81 LCL020-1 timeout 500.0 58 LCL021-1 timeout 500.0 69 LCL022-1 theorem 0.0 2 1 10 0 2 0 2 0 5 10 82 0 0 LCL023-1 theorem 0.0 2 1 14 0 2 0 2 0 5 14 109 0 0 LCL024-1 timeout 500.0 82 LCL025-1 theorem 5.2 5 1 270 0 4 0 4 0 5 270 18828 0 0 LCL026-1 theorem 22.3 6 1 458 0 4 0 4 0 5 458 45121 0 0 LCL027-1 theorem 0.0 2 1 32 0 4 0 2 0 4 32 230 0 0 LCL028-1 theorem 359.5 12 1 1159 0 4 0 93 0 5 1159 244393 0 0 LCL029-1 theorem 0.7 2 1 138 0 5 0 0 0 5 138 6542 0 0 LCL030-1 theorem 44.2 7 1 496 0 5 0 14 0 5 496 59839 0 0 LCL031-1 theorem 168.8 9 1 838 0 5 0 27 0 5 838 151755 0 0 LCL032-1 timeout 500.0 51 LCL033-1 theorem 0.0 2 1 14 0 2 0 2 0 5 14 108 0 0 LCL034-1 theorem 19.0 8 1 349 0 2 0 15 0 7 349 50552 0 0 LCL035-1 theorem 0.0 2 1 8 0 2 0 0 0 5 8 48 0 0 LCL036-1 theorem 4.3 4 1 153 0 2 0 7 0 7 153 9617 0 0 LCL037-1 timeout 500.0 45 LCL038-1 timeout 500.0 28 LCL039-1 theorem 58.1 9 1 1062 0 6 0 4 0 5 1062 115810 0 0 LCL040-1 theorem 26.7 8 1 946 0 6 0 14 0 5 946 60040 0 0 LCL041-1 theorem 0.0 2 1 47 0 6 0 0 0 4 47 427 0 0 LCL042-1 theorem 180.4 13 1 1298 0 6 0 29 0 5 1298 181161 0 0 LCL043-1 theorem 0.0 2 1 37 0 6 0 0 0 4 37 313 0 0 LCL044-1 theorem 0.2 2 1 11 0 6 0 0 0 5 11 87 0 0 LCL045-1 theorem 158.8 11 1 1197 0 6 0 28 0 5 1197 168394 0 0 LCL046-1 theorem 0.0 2 1 5 0 4 0 0 0 5 5 12 0 0 LCL047-1 theorem 0.1 2 1 86 0 4 0 2 0 5 86 2048 0 0 LCL048-1 theorem 0.2 2 1 98 0 4 0 2 0 5 98 2352 0 0 LCL049-1 theorem 0.4 2 1 139 0 4 0 6 0 5 139 4871 0 0 LCL050-1 theorem 0.5 2 1 141 0 4 0 6 0 5 141 5038 0 0 LCL051-1 theorem 0.5 2 1 131 0 4 0 6 0 5 131 4764 0 0 LCL052-1 theorem 0.5 2 1 134 0 4 0 7 0 5 134 5093 0 0 LCL053-1 theorem 0.7 3 1 156 0 4 0 9 0 5 156 6485 0 0 LCL054-1 theorem 137.6 12 1 1170 0 4 0 27 0 5 1170 155100 0 0 LCL055-1 theorem 1.0 3 1 185 0 4 0 6 0 5 185 6852 0 0 LCL056-1 theorem 0.5 2 1 136 0 4 0 7 0 5 136 5122 0 0 LCL057-1 theorem 0.3 2 1 120 0 4 0 7 0 5 120 4607 0 0 LCL058-1 theorem 48.7 8 1 789 0 4 0 17 0 5 789 89959 0 0 LCL059-1 theorem 0.9 3 1 164 0 4 0 9 0 5 164 6603 0 0 LCL060-1 theorem 265.6 15 1 1466 0 4 0 31 0 5 1466 225874 0 0 LCL061-1 timeout 500.0 18 LCL062-1 timeout 500.0 15 LCL063-1 timeout 500.0 17 LCL064-1 theorem 18.8 8 1 716 0 4 0 17 0 5 716 58528 0 0 LCL064-2 theorem 0.7 2 1 137 0 3 0 2 0 5 137 5086 0 0 LCL065-1 theorem 0.4 2 1 133 0 4 0 1 0 5 133 4748 0 0 LCL066-1 theorem 0.5 2 1 146 0 4 0 1 0 5 146 5169 0 0 LCL067-1 timeout 500.0 20 LCL068-1 theorem 15.0 5 1 612 0 4 0 18 0 5 612 45060 0 0 LCL069-1 theorem 3.4 5 1 451 0 4 0 6 0 5 451 21025 0 0 LCL070-1 theorem 27.3 9 1 966 0 4 0 56 0 5 966 68707 0 0 LCL071-1 theorem 15.2 5 1 621 0 4 0 21 0 5 621 46437 0 0 LCL072-1 theorem 7.8 7 1 574 0 4 0 13 0 5 574 32921 0 0 LCL073-1 timeout 500.0 48 LCL074-1 timeout 500.0 71 LCL075-1 theorem 0.0 2 1 34 0 2 0 2 0 6 34 605 0 0 LCL076-1 theorem 0.2 2 1 94 0 4 0 1 0 5 94 3082 0 0 LCL076-2 theorem 0.0 2 1 4 0 4 0 0 0 2 4 5 0 0 LCL076-3 theorem 0.0 2 1 35 0 4 0 1 0 4 35 609 0 0 LCL077-1 theorem 0.3 2 1 109 0 4 0 1 0 5 109 3206 0 0 LCL077-2 theorem 0.0 2 1 26 0 4 0 1 0 4 26 308 0 0 LCL078-1 timeout 500.0 10 LCL079-1 theorem 0.0 2 1 17 0 6 0 1 0 3 17 76 0 0 LCL080-1 theorem 1.0 2 1 144 0 4 0 1 0 5 144 6520 0 0 LCL080-2 theorem 1.0 3 1 144 0 5 0 1 0 5 144 6521 0 0 LCL081-1 theorem 0.0 2 1 37 0 2 0 4 0 5 37 308 0 0 LCL082-1 theorem 0.0 2 1 36 0 2 0 7 0 5 36 353 0 0 LCL083-1 theorem 1.7 3 1 189 0 2 0 68 0 6 189 7274 0 0 LCL083-2 theorem 0.9 2 1 89 0 3 0 1 0 6 89 2953 0 0 LCL084-2 timeout 500.0 28 LCL084-3 timeout 500.0 27 LCL085-1 timeout 500.0 22 LCL086-1 theorem 0.0 2 1 28 0 2 0 7 0 6 28 443 0 0 LCL087-1 theorem 0.0 2 1 12 0 2 0 2 0 6 12 109 0 0 LCL088-1 theorem 0.2 2 1 64 0 2 0 9 0 6 64 2130 0 0 LCL089-1 theorem 0.3 2 1 86 0 2 0 11 0 6 86 2992 0 0 LCL090-1 theorem 0.0 2 1 42 0 2 0 15 0 6 42 485 0 0 LCL091-1 theorem 0.1 2 1 47 0 2 0 9 0 6 47 791 0 0 LCL092-1 theorem 0.7 2 1 109 0 2 0 12 0 6 109 4568 0 0 LCL093-1 theorem 59.6 8 1 423 0 2 0 19 0 6 423 63419 0 0 LCL094-1 theorem 0.5 2 1 78 0 2 0 8 0 6 78 3632 0 0 LCL095-1 theorem 0.4 2 1 121 0 2 0 14 0 6 121 4145 0 0 LCL096-1 theorem 6.1 3 1 538 0 4 0 1 0 5 538 127303 0 0 LCL097-1 theorem 1.4 3 1 278 0 3 0 1 0 5 278 32082 0 0 LCL098-1 theorem 0.6 2 1 207 0 2 0 0 0 6 207 531 0 0 LCL099-1 theorem 454.0 68 1 2905 0 3 0 1 0 6 2905 2966051 0 0 LCL100-1 theorem 434.4 66 1 2865 0 3 0 0 0 6 2865 2873747 0 0 LCL101-1 theorem 0.0 2 1 14 0 3 0 1 0 5 14 81 0 0 LCL102-1 theorem 0.3 2 1 139 0 4 0 1 0 5 139 9651 0 0 LCL103-1 theorem 3.7 6 1 347 0 3 0 0 0 6 347 52313 0 0 LCL104-1 theorem 0.0 2 1 16 0 3 0 0 0 5 16 94 0 0 LCL105-1 timeout 500.0 84 LCL106-1 theorem 0.0 2 1 22 0 3 0 0 0 6 22 45 0 0 LCL107-1 theorem 0.0 2 1 15 0 2 0 0 0 8 15 114 0 0 LCL108-1 theorem 0.0 2 1 11 0 2 0 0 0 8 11 60 0 0 LCL109-1 timeout 500.0 13 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-1 theorem 0.1 2 1 46 0 5 0 0 0 5 46 1016 0 0 LCL110-2 timeout 500.0 37 LCL111-1 theorem 0.1 2 1 61 0 5 0 0 0 5 61 1452 0 0 LCL111-2 timeout 500.0 149 LCL112-1 theorem 0.3 2 1 155 0 5 0 0 0 5 155 6342 0 0 LCL112-2 timeout 500.0 64 LCL113-1 theorem 33.2 7 1 800 0 5 0 11 0 5 800 67077 0 0 LCL113-2 timeout 500.0 151 LCL114-1 theorem 44.0 8 1 869 0 5 0 24 0 5 869 80481 0 0 LCL114-2 timeout 500.0 152 LCL115-1 theorem 0.7 3 1 202 0 5 0 0 0 5 202 8306 0 0 LCL115-2 timeout 500.0 47 LCL116-1 theorem 78.6 8 1 1037 0 5 0 14 0 5 1037 123260 0 0 LCL116-2 timeout 500.0 155 LCL117-1 theorem 0.0 2 1 4 0 2 0 0 0 5 4 10 0 0 LCL118-1 theorem 0.0 2 1 12 0 2 0 0 0 6 12 81 0 0 LCL119-1 timeout 500.0 70 LCL120-1 theorem 0.1 2 1 40 0 2 0 0 0 6 40 624 0 0 LCL121-1 theorem 4.8 6 1 183 0 2 0 3 0 7 183 20094 0 0 LCL122-1 theorem 50.3 32 1 894 0 2 0 3 0 7 894 370005 0 0 LCL123-1 theorem 45.7 10 1 362 0 2 0 3 0 7 362 69980 0 0 LCL124-1 timeout 500.0 62 LCL125-1 timeout 500.0 85 LCL126-1 theorem 0.0 2 1 6 0 3 0 0 0 5 6 15 0 0 LCL127-1 theorem 2.8 5 1 127 0 2 0 5 0 7 127 10172 0 0 LCL128-1 theorem 0.2 2 1 48 0 2 0 1 0 7 48 1587 0 0 LCL129-1 theorem 65.0 6 1 341 0 2 0 2 0 6 341 50295 0 0 LCL130-1 theorem 235.9 48 1 2303 0 2 0 3 0 6 2303 1919996 0 0 LCL131-1 theorem 0.4 2 1 150 0 2 0 1 0 5 150 10311 0 0 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 LCL144-1 timeout 500.0 221 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 LCL166-1 timeout 500.0 83 LCL167-1 timeout 500.0 58 LCL168-1 timeout 500.0 139 LCL169-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 7 0 0 LCL169-3 theorem 0.0 2 1 12 0 8 0 0 0 4 12 62 0 0 LCL170-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 LCL170-3 theorem 0.0 2 1 131 0 8 0 0 0 3 131 592 0 0 LCL171-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 LCL171-3 theorem 0.0 2 1 89 0 8 0 0 0 4 89 1471 0 0 LCL172-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 LCL172-3 timeout 500.0 283 LCL173-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 LCL173-3 timeout 500.0 296 LCL174-1 theorem 0.2 2 1 807 0 6 0 0 0 5 807 2568 0 0 LCL174-3 timeout 500.0 295 LCL175-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 7 0 0 LCL175-3 theorem 0.0 2 1 6 0 6 0 0 0 2 6 15 0 0 LCL176-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 17 0 0 LCL176-3 theorem 0.0 2 1 83 0 8 0 0 0 4 83 727 0 0 LCL177-1 theorem 0.0 2 1 11 0 6 0 0 0 4 11 31 0 0 LCL178-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 30 0 0 LCL178-3 theorem 0.0 2 1 41 0 8 0 0 0 4 41 331 0 0 LCL179-1 timeout 500.0 77 LCL180-1 timeout 500.0 79 LCL180-3 timeout 500.0 237 LCL181-1 timeout 500.0 66 LCL181-2 theorem 0.0 2 1 2 0 4 2 0 0 2 2 4 2 0 LCL181-3 timeout 500.0 242 LCL182-1 theorem 0.2 2 1 636 0 6 0 0 0 5 636 2295 0 0 LCL182-3 timeout 500.0 267 LCL183-1 timeout 500.0 51 LCL183-3 timeout 500.0 283 LCL184-1 timeout 500.0 81 LCL185-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 18 0 0 LCL185-3 theorem 0.3 3 1 437 0 8 0 0 0 4 437 8496 0 0 LCL186-1 theorem 0.0 2 1 19 0 6 0 0 0 4 19 58 0 0 LCL186-3 theorem 0.2 3 1 329 0 8 0 0 0 4 329 6903 0 0 LCL187-1 theorem 0.0 2 1 20 0 6 0 0 0 4 20 64 0 0 LCL187-3 theorem 0.2 3 1 300 0 8 0 0 0 4 300 6164 0 0 LCL188-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 27 0 0 LCL188-3 theorem 2.5 8 1 1030 0 8 0 0 0 4 1030 47523 0 0 LCL189-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 26 0 0 LCL189-3 theorem 2.5 7 1 918 0 8 0 0 0 4 918 48226 0 0 LCL190-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 14 0 0 LCL190-3 theorem 0.0 2 1 37 0 8 0 0 0 4 37 285 0 0 LCL191-1 theorem 18.3 8 1 4435 0 6 0 0 0 6 4435 22814 0 0 LCL191-3 timeout 500.0 322 LCL192-1 theorem 0.1 2 1 282 0 6 0 0 0 5 282 1119 0 0 LCL192-3 timeout 500.0 319 LCL193-1 theorem 0.1 2 1 247 0 6 0 0 0 5 247 974 0 0 LCL193-3 timeout 500.0 320 LCL194-1 theorem 16.4 7 1 4866 0 6 0 0 0 6 4866 22017 0 0 LCL194-3 timeout 500.0 286 LCL195-1 theorem 14.1 7 1 5032 0 6 0 0 0 6 5032 26402 0 0 LCL195-3 timeout 500.0 291 LCL196-1 theorem 0.4 2 1 787 0 6 0 0 0 5 787 2704 0 0 LCL196-3 theorem 3.6 10 1 1280 0 8 0 0 0 4 1280 62021 0 0 LCL197-1 theorem 0.0 2 1 9 0 6 0 0 0 5 9 37 0 0 LCL197-3 theorem 3.5 9 1 1274 0 8 0 0 0 4 1274 60769 0 0 LCL198-1 theorem 0.3 2 1 764 0 6 0 0 0 5 764 2618 0 0 LCL198-3 theorem 4.1 10 1 1390 0 8 0 0 0 4 1390 68888 0 0 LCL199-1 theorem 0.1 2 1 308 0 6 0 0 0 5 308 1220 0 0 LCL199-3 timeout 500.0 279 LCL200-1 theorem 0.0 2 1 13 0 6 0 0 0 5 13 52 0 0 LCL201-1 theorem 7.9 5 1 1516 0 6 0 0 0 6 1516 9378 0 0 LCL201-3 timeout 500.0 287 LCL202-1 theorem 6.6 4 1 220 0 6 0 0 0 6 220 1851 0 0 LCL202-3 timeout 500.0 285 LCL203-1 theorem 11.1 5 1 210 0 6 0 0 0 6 210 1590 0 0 LCL203-3 timeout 500.0 279 LCL204-1 theorem 2.1 4 1 1478 0 6 0 0 0 6 1478 7687 0 0 LCL205-1 theorem 11.3 5 1 691 0 6 0 0 0 6 691 5382 0 0 LCL205-3 timeout 500.0 293 LCL206-1 theorem 3.7 3 1 665 0 6 0 0 0 6 665 4071 0 0 LCL206-3 timeout 500.0 271 LCL207-1 theorem 7.2 4 1 529 0 6 0 0 0 6 529 3733 0 0 LCL207-3 timeout 500.0 282 LCL208-1 theorem 0.2 2 1 626 0 6 0 0 0 5 626 2144 0 0 LCL208-3 timeout 500.0 247 LCL209-1 timeout 500.0 69 LCL209-3 timeout 500.0 275 LCL210-1 theorem 0.2 2 1 638 0 6 0 0 0 5 638 2205 0 0 LCL210-3 timeout 500.0 240 LCL211-1 theorem 0.2 2 1 589 0 6 0 0 0 5 589 2056 0 0 LCL211-3 timeout 500.0 285 LCL212-1 theorem 2.0 4 1 1688 0 6 0 0 0 6 1688 8314 0 0 LCL212-3 theorem 0.0 2 1 91 0 8 0 0 0 4 91 1464 0 0 LCL213-1 theorem 1.1 3 1 1401 0 6 0 0 0 6 1401 6106 0 0 LCL213-3 timeout 500.0 265 LCL214-1 theorem 4.0 3 1 1398 0 6 0 0 0 6 1398 6762 0 0 LCL214-3 timeout 500.0 245 LCL215-1 theorem 4.1 4 1 1451 0 6 0 0 0 6 1451 7696 0 0 LCL215-3 timeout 500.0 245 LCL216-1 theorem 0.2 2 1 584 0 6 0 0 0 5 584 1999 0 0 LCL216-3 timeout 500.0 283 LCL217-1 theorem 0.2 2 1 587 0 6 0 0 0 5 587 2012 0 0 LCL217-3 timeout 500.0 284 LCL218-1 timeout 500.0 51 LCL218-3 timeout 500.0 298 LCL219-1 timeout 500.0 71 LCL219-3 timeout 500.0 296 LCL220-1 timeout 500.0 78 LCL220-3 timeout 500.0 239 LCL221-1 theorem 28.1 16 1 18689 0 6 0 0 0 6 18689 65074 0 0 LCL221-3 timeout 500.0 284 LCL222-1 theorem 31.1 17 1 19631 0 6 0 0 0 6 19631 67543 0 0 LCL222-3 timeout 500.0 279 LCL223-1 theorem 27.7 18 1 21633 0 6 0 0 0 6 21633 73813 0 0 LCL223-3 timeout 500.0 302 LCL224-1 theorem 14.1 6 1 3424 0 6 0 0 0 6 3424 14060 0 0 LCL224-3 timeout 500.0 303 LCL225-1 theorem 14.3 5 1 3424 0 6 0 0 0 6 3424 13993 0 0 LCL225-3 timeout 500.0 295 LCL226-1 theorem 0.0 2 1 7 0 6 0 0 0 5 7 16 0 0 LCL226-3 timeout 500.0 306 LCL227-1 timeout 500.0 84 LCL227-3 timeout 500.0 308 LCL228-1 timeout 500.0 84 LCL228-3 timeout 500.0 312 LCL229-1 timeout 500.0 83 LCL229-3 timeout 500.0 298 LCL230-1 timeout 500.0 49 LCL230-2 theorem 0.0 2 1 3 0 3 3 0 0 2 3 6 1 0 LCL230-3 timeout 500.0 310 LCL231-1 timeout 500.0 46 LCL231-3 timeout 500.0 298 LCL234-1 theorem 4.2 4 1 2607 0 6 0 0 0 6 2607 10879 0 0 LCL234-3 timeout 500.0 287 LCL235-1 timeout 500.0 43 LCL235-3 timeout 500.0 287 LCL236-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 25 0 0 LCL236-3 timeout 500.0 185 LCL237-1 theorem 4.2 4 1 2608 0 6 0 0 0 6 2608 10884 0 0 LCL237-3 timeout 500.0 277 LCL238-1 theorem 0.1 2 1 298 0 6 0 0 0 5 298 1157 0 0 LCL238-3 timeout 500.0 199 LCL239-1 timeout 500.0 84 LCL239-3 theorem 297.1 117 1 118 0 9 0 0 0 5 118 2856 0 0 LCL240-1 timeout 500.0 81 LCL240-3 timeout 500.0 230 LCL241-1 timeout 500.0 81 LCL241-3 timeout 500.0 232 LCL242-1 timeout 500.0 46 LCL242-3 timeout 500.0 304 LCL243-1 timeout 500.0 81 LCL243-3 timeout 500.0 230 LCL244-1 timeout 500.0 50 LCL245-1 timeout 500.0 50 LCL245-3 timeout 500.0 277 LCL246-1 timeout 500.0 82 LCL246-3 timeout 500.0 228 LCL247-1 timeout 500.0 84 LCL247-3 timeout 500.0 218 LCL248-1 timeout 500.0 51 LCL248-3 timeout 500.0 283 LCL249-1 timeout 500.0 80 LCL249-3 timeout 500.0 260 LCL250-1 theorem 5.0 7 1 6335 0 6 0 0 0 6 6335 24523 0 0 LCL250-3 timeout 500.0 261 LCL251-1 timeout 500.0 58 LCL251-3 timeout 500.0 242 LCL252-1 timeout 500.0 60 LCL252-3 timeout 500.0 232 LCL253-1 timeout 500.0 85 LCL253-3 timeout 500.0 205 LCL254-1 timeout 500.0 84 LCL254-3 timeout 500.0 200 LCL255-1 timeout 500.0 58 LCL255-3 timeout 500.0 288 LCL256-1 theorem 0.2 2 1 110 0 4 0 7 0 5 110 4117 0 0 LCL257-1 theorem 0.0 2 1 28 0 2 0 2 0 5 28 369 0 0 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 LCL355-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 4 0 0 LCL356-1 theorem 0.0 2 1 20 0 4 0 1 0 5 20 104 0 0 LCL357-1 theorem 0.0 2 1 20 0 4 0 1 0 5 20 105 0 0 LCL358-1 theorem 0.0 2 1 25 0 4 0 2 0 5 25 136 0 0 LCL359-1 theorem 0.0 2 1 21 0 4 0 1 0 5 21 109 0 0 LCL360-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 4 0 0 LCL361-1 theorem 0.0 2 1 24 0 4 0 2 0 5 24 123 0 0 LCL362-1 theorem 0.0 2 1 31 0 4 0 2 0 5 31 217 0 0 LCL363-1 theorem 0.0 2 1 31 0 4 0 2 0 5 31 220 0 0 LCL364-1 theorem 0.0 2 1 40 0 4 0 2 0 5 40 455 0 0 LCL365-1 theorem 0.1 2 1 70 0 4 0 2 0 5 70 1547 0 0 LCL366-1 theorem 0.0 2 1 9 0 4 0 0 0 5 9 40 0 0 LCL367-1 theorem 0.1 2 1 78 0 4 0 3 0 5 78 1863 0 0 LCL368-1 theorem 0.7 3 1 157 0 4 0 6 0 5 157 5688 0 0 LCL369-1 theorem 0.7 2 1 155 0 4 0 11 0 5 155 6421 0 0 LCL370-1 theorem 0.9 3 1 169 0 4 0 12 0 5 169 7234 0 0 LCL371-1 theorem 0.9 3 1 169 0 4 0 12 0 5 169 7234 0 0 LCL372-1 theorem 3.3 4 1 298 0 4 0 15 0 5 298 17990 0 0 LCL373-1 theorem 5.1 6 1 352 0 4 0 19 0 5 352 22638 0 0 LCL374-1 theorem 9.1 7 1 452 0 4 0 17 0 5 452 31319 0 0 LCL375-1 timeout 500.0 17 LCL376-1 theorem 430.8 18 1 1679 0 4 0 27 0 5 1679 277887 0 0 LCL377-1 timeout 500.0 18 LCL378-1 theorem 0.8 3 1 165 0 4 0 6 0 5 165 6057 0 0 LCL379-1 theorem 0.4 2 1 124 0 4 0 7 0 5 124 4762 0 0 LCL380-1 theorem 0.7 2 1 156 0 4 0 7 0 5 156 5716 0 0 LCL381-1 theorem 0.9 3 1 172 0 4 0 7 0 5 172 6459 0 0 LCL382-1 theorem 1.1 3 1 196 0 4 0 10 0 5 196 9813 0 0 LCL383-1 theorem 26.2 8 1 661 0 4 0 13 0 5 661 70075 0 0 LCL384-1 theorem 0.3 2 1 125 0 4 0 6 0 5 125 4277 0 0 LCL385-1 theorem 1.1 3 1 182 0 4 0 10 0 5 182 9270 0 0 LCL386-1 theorem 1.3 3 1 194 0 4 0 13 0 5 194 8600 0 0 LCL387-1 theorem 5.0 5 1 368 0 4 0 16 0 5 368 22439 0 0 LCL388-1 theorem 107.3 10 1 1053 0 4 0 21 0 5 1053 143278 0 0 LCL389-1 theorem 28.0 8 1 662 0 4 0 13 0 5 662 74347 0 0 LCL390-1 theorem 4.0 5 1 332 0 4 0 17 0 5 332 19832 0 0 LCL391-1 timeout 500.0 15 LCL392-1 theorem 287.0 15 1 1523 0 4 0 30 0 5 1523 229619 0 0 LCL393-1 timeout 500.0 17 LCL394-1 timeout 500.0 14 LCL395-1 timeout 500.0 18 LCL396-1 theorem 0.7 3 1 151 0 4 0 7 0 5 151 5921 0 0 LCL397-1 theorem 0.0 2 1 39 0 4 0 2 0 5 39 321 0 0 LCL398-1 theorem 0.0 2 1 6 0 4 0 0 0 5 6 16 0 0 LCL399-1 theorem 0.0 2 1 42 0 4 0 2 0 5 42 539 0 0 LCL400-1 theorem 1.3 3 1 181 0 4 0 9 0 5 181 7344 0 0 LCL401-1 theorem 2.1 4 1 225 0 4 0 12 0 5 225 11731 0 0 LCL402-1 theorem 1.6 3 1 206 0 4 0 12 0 5 206 10548 0 0 LCL403-1 theorem 84.7 9 1 955 0 4 0 18 0 5 955 126640 0 0 LCL404-1 theorem 22.4 7 1 606 0 4 0 13 0 5 606 65695 0 0 LCL405-1 theorem 0.5 2 1 160 0 4 0 10 0 5 160 7551 0 0 LCL406-1 timeout 500.0 3 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-1 timeout 500.0 85 LCL411-2 timeout 500.0 54 LCL412-1 timeout 500.0 107 LCL413-1 timeout 500.0 102 LCL414-1 theorem 0.0 2 1 6 0 4 0 0 0 3 6 9 0 0 LCL415-1 timeout 500.0 302 LCL416-1 theorem 0.4 3 1 37 0 2 0 0 0 10 37 659 0 0 LCL417-1 timeout 500.0 71 LCL418-1 timeout 500.0 17 LCL419-1 timeout 500.0 11 LCL420-1 timeout 500.0 10 LCL421-1 timeout 500.0 11 LCL422-1 timeout 500.0 11 LCL423-1 timeout 500.0 34 LCL424-1 timeout 500.0 10 LCL425-1 timeout 500.0 45 LCL426-1 timeout 500.0 28 LCL427-1 timeout 500.0 19 LCL428-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 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 LDA005-1 timeout 500.0 34 LDA005-2 timeout 500.0 35 LDA006-1 timeout 500.0 30 LDA006-2 timeout 500.0 37 LDA007-1 theorem 65.8 13 1 1128 0 16 0 0 0 3 1128 31543 9675 0 LDA007-2 theorem 3.6 8 1 1289 0 16 0 35 0 3 1289 34953 9120 0 LDA007-3 theorem 0.0 2 1 63 0 8 0 0 0 3 63 740 0 0 LDA008-1 timeout 500.0 29 LDA008-2 timeout 500.0 27 LDA009-1 timeout 500.0 30 LDA009-2 timeout 500.0 36 LDA010-1 timeout 500.0 31 LDA010-2 timeout 500.0 36 LDA011-1 timeout 500.0 31 LDA011-2 timeout 500.0 36 LDA012-1 timeout 500.0 30 LDA012-2 timeout 500.0 36 LDA013-1 timeout 500.0 20 LDA014-1 timeout 500.0 19 MGT001-1 theorem 0.0 2 1 19 0 10 0 0 0 2 19 30 0 0 MGT002-1 theorem 0.0 2 1 12 0 7 0 0 0 2 12 26 0 0 MGT003-1 theorem 0.0 2 1 12 0 7 0 0 0 2 12 26 0 0 MGT004-1 theorem 0.0 2 1 15 0 9 0 0 0 2 15 26 12 0 MGT005-1 theorem 0.1 2 1 166 0 20 0 0 0 2 166 849 181 0 MGT005-2 theorem 0.0 2 1 59 0 23 1 0 0 2 59 340 122 0 MGT006-1 theorem 0.0 2 1 13 0 9 1 0 0 2 13 23 0 0 MGT007-1 theorem 0.0 2 1 17 0 9 0 0 0 2 17 28 14 0 MGT008-1 theorem 0.0 2 1 15 0 12 0 0 0 2 15 25 0 0 MGT009-1 theorem 0.0 2 1 15 0 12 0 0 0 2 15 25 0 0 MGT010-1 theorem 0.0 2 1 18 0 14 1 0 0 2 18 28 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 MGT013-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 99 50 0 MGT014-1 theorem 0.0 2 1 24 0 10 0 0 0 2 24 99 50 0 MGT015-1 theorem 0.0 2 1 17 0 13 0 0 0 2 17 27 0 0 MGT016-1 theorem 0.0 2 1 16 0 13 0 0 0 2 16 26 3 0 MGT017-1 theorem 0.0 2 1 17 0 13 0 0 0 2 17 27 0 0 MGT018-1 theorem 0.0 2 1 16 0 13 0 0 0 2 16 26 3 0 MGT019-2 non_thm 0.0 2 0 12 2 6 0 0 33 4 0 47 35 0 MGT020-1 theorem 0.0 2 1 17 0 4 0 0 0 4 17 64 48 0 MGT021-1 theorem 0.0 2 1 10 0 4 0 0 0 3 10 38 30 0 MGT022-1 theorem 0.0 2 2 8 1 7 3 0 0 3 7 19 6 0 MGT022-2 theorem 0.0 2 2 8 1 7 3 0 0 3 7 19 6 0 MGT023-1 theorem 0.0 2 1 11 0 4 0 0 0 4 11 40 25 0 MGT023-2 theorem 0.0 2 10 52 12 4 0 0 42 4 25 322 177 0 MGT024-1 theorem 0.0 2 4 29 3 14 6 0 41 2 23 152 107 0 MGT025-1 theorem 0.1 2 4 88 3 11 7 0 317 3 71 497 431 0 MGT026-1 theorem 0.0 2 3 43 2 5 0 0 39 2 26 213 121 0 MGT027-1 theorem 0.0 2 4 57 3 3 0 0 66 4 35 319 177 0 MGT028-1 theorem 0.0 2 2 13 1 2 0 0 1 4 11 27 15 0 MGT029-1 timeout 500.0 137 MGT030-1 theorem 0.0 2 6 23 8 2 0 0 4 4 14 80 45 0 MGT031-1 non_thm 0.0 2 0 21 0 4 0 0 44 3 0 77 44 0 MGT032-2 theorem 0.0 2 1 7 0 2 0 0 0 4 7 11 0 0 MGT033-1 timeout 500.0 130 MGT033-2 timeout 500.0 59 MGT034-1 non_thm 0.0 2 0 31 4 6 0 0 85 4 0 134 91 0 MGT034-2 theorem 0.1 3 3 195 3 6 0 0 74 4 110 2270 2179 0 MGT035-1 timeout 500.0 139 MGT035-2 timeout 500.0 102 MGT036-1 theorem 0.0 2 1 9 0 4 0 0 0 2 9 15 10 0 MGT036-2 theorem 0.0 2 1 9 0 4 0 0 0 2 9 16 11 0 MGT036-3 theorem 0.0 2 1 6 0 4 0 0 0 2 6 9 0 0 MGT037-1 timeout 500.0 85 MGT037-2 timeout 500.0 160 MGT038-1 timeout 500.0 244 MGT038-2 timeout 500.0 319 MGT039-1 theorem 0.0 2 1 33 0 6 4 0 0 3 33 120 58 0 MGT039-2 theorem 0.9 3 20 1109 19 6 4 0 6953 4 446 11396 8886 0 MGT040-1 non_thm 0.0 2 0 10 5 7 4 0 25 3 0 40 31 0 MGT040-2 non_thm 0.0 2 0 10 5 7 4 0 25 3 0 40 31 0 MGT041-2 theorem 0.0 2 1 7 0 4 0 0 0 2 7 9 3 0 MGT042-1 theorem 0.0 2 5 83 5 16 8 0 85 2 47 432 307 0 MGT043-1 theorem 0.0 2 1 34 0 8 0 0 0 2 34 184 178 0 MGT044-1 theorem 0.0 2 1 9 0 4 0 0 0 2 9 51 44 0 MGT045-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 29 19 0 MGT046-1 theorem 0.0 2 1 30 0 5 0 0 0 2 30 135 113 0 MGT047-1 theorem 0.0 2 1 216 0 8 2 0 0 2 216 1039 585 0 MGT048-1 theorem 0.0 2 1 9 0 4 0 0 0 2 9 51 44 0 MGT049-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 30 19 0 MGT050-1 theorem 0.0 2 1 31 0 5 0 0 0 2 31 156 140 0 MGT051-1 theorem 0.0 2 1 178 0 8 2 0 0 2 178 875 504 0 MGT052-1 theorem 0.0 2 2 5 1 2 0 0 15 2 6 21 22 0 MGT053-1 theorem 0.0 2 4 11 3 5 6 0 21 2 8 63 45 0 MGT054-1 theorem 0.0 2 1 78 0 8 0 0 0 2 78 477 272 0 MGT055-1 theorem 0.0 2 1 238 0 11 2 0 0 2 238 1454 766 0 MGT056-1 theorem 0.0 2 1 63 0 9 1 0 0 2 63 303 178 0 MGT057-1 theorem 0.0 2 1 56 0 8 1 0 0 2 56 289 182 0 MGT058-1 theorem 0.0 2 2 82 1 7 0 0 67 2 65 594 400 0 MGT059-1 theorem 0.0 2 1 12 0 5 0 0 0 2 12 54 43 0 MGT060-1 theorem 0.0 2 2 173 2 10 0 0 441 2 174 995 489 0 MGT061-1 theorem 0.1 2 1 278 0 14 1 0 0 2 278 1865 1023 0 MGT062-1 theorem 0.1 2 1 216 0 12 1 0 0 2 216 1576 1268 0 MGT063-1 theorem 0.2 2 2 660 6 20 4 0 1293 2 574 5094 2451 0 MGT064-1 theorem 0.1 2 1 485 0 19 2 0 0 2 485 3605 1723 0 MGT065-1 theorem 0.1 2 1 292 0 19 1 0 0 2 292 1831 996 0 MGT066-1 non_thm 0.0 2 1 3 6 1 0 0 34 2 6 9 46 0 MSC001-1 theorem 0.0 2 1 65 0 5 1 2 0 5 65 235 99 0 MSC002-1 theorem 0.0 2 1 22 0 3 1 0 0 4 22 42 36 0 MSC002-2 theorem 0.0 2 1 22 0 3 1 0 0 4 22 42 36 0 MSC003-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 9 5 0 MSC004-1 theorem 0.0 2 6 20 11 2 0 0 4 3 14 38 49 0 MSC005-1 theorem 0.0 2 1 15 0 3 0 0 0 4 15 175 0 0 MSC006-1 theorem 0.0 2 6 47 22 2 0 0 196 2 30 193 537 0 MSC007-1.008 theorem 2.6 2 5040 55182 5039 65260 78952 0 3513 2 56 105582 27398 0 MSC007-2.005 theorem 0.1 2 24 800 23 26 0 0 344 2 150 6166 1335 0 MSC008-1.002 theorem 0.2 2 32 155 53 2 0 0 2400 2 23 1364 9005 0 MSC008-1.010 timeout 500.0 171 MSC008-2.002 theorem 0.2 2 32 155 53 2 0 0 2640 2 23 1188 7397 0 MSC009-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 NLP001-1 theorem 0.0 2 2 28 1 28 5 0 0 2 19 32 30 0 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 NLP004-1 theorem 0.0 2 2 59 1 59 5 0 18 2 39 137 136 0 NLP005-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP006-1 non_thm 0.0 2 1 61 1 57 4 0 64 2 36 152 129 0 NLP007-1 theorem 0.0 2 2 59 1 59 5 0 18 2 39 137 136 0 NLP008-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP009-1 theorem 0.0 2 2 53 1 53 5 0 16 2 35 125 124 0 NLP011-1 theorem 0.0 2 2 59 1 59 5 0 18 2 39 137 136 0 NLP012-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 0 NLP013-1 non_thm 0.0 2 0 42 1 38 2 0 81 2 0 105 82 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 NLP026-1 non_thm 0.0 2 0 4 5 5 3 0 4 2 0 4 9 0 NLP027-1 non_thm 0.0 2 0 4 5 5 4 0 6 2 0 4 11 0 NLP028-1 non_thm 0.0 2 0 5 5 6 4 0 7 2 0 5 12 0 NLP029-1 non_thm 0.0 2 0 4 5 5 4 0 4 2 0 4 9 0 NLP030-1 non_thm 0.0 2 0 5 5 6 4 0 6 2 0 5 11 0 NLP031-1 non_thm 0.0 2 6 38 12 12 5 0 14 4 20 77 96 0 NLP032-1 timeout 500.0 8 NLP033-1 non_thm 0.0 2 7 40 12 11 4 0 10 5 21 88 103 0 NLP034-1 timeout 500.0 10 NLP035-1 timeout 500.0 11 NLP036-1 non_thm 0.0 4 0 26 0 4 0 0 11 2 0 79 11 0 NLP037-1 non_thm 0.0 4 0 56 0 5 0 0 49 2 0 182 49 0 NLP038-1 non_thm 0.0 4 0 223 0 7 0 0 338 2 0 854 343 0 NLP039-1 non_thm 0.0 4 0 223 0 7 0 0 339 2 0 854 344 0 NLP040-1 non_thm 0.0 4 0 26 0 4 0 0 11 2 0 79 11 0 NLP041-1 non_thm 0.0 4 0 184 0 6 0 0 300 2 0 665 305 0 NLP042-1 non_thm 0.0 4 0 135 0 13 0 0 0 2 0 504 0 0 NLP043-1 non_thm 0.0 4 0 17 2 18 3 0 29 2 0 17 31 0 NLP044-1 non_thm 0.0 4 0 17 2 18 3 0 29 2 0 17 31 0 NLP045-1 non_thm 0.0 4 0 17 2 18 3 0 29 2 0 17 31 0 NLP046-1 non_thm 0.0 4 0 17 2 18 3 0 29 2 0 17 31 0 NLP047-1 non_thm 0.0 4 0 17 2 18 3 0 29 2 0 17 31 0 NLP048-1 non_thm 0.0 4 0 17 2 18 3 0 29 2 0 17 31 0 NLP049-1 non_thm 264.3 171 0 514 0 22 0 0 1059303 3 0 2140 1059352 0 NLP050-1 non_thm 255.8 169 0 499 0 22 0 0 1059303 3 0 2088 1059352 0 NLP051-1 non_thm 251.3 165 0 499 0 22 0 0 1059303 3 0 2090 1059352 0 NLP052-1 non_thm 263.6 175 0 508 0 22 0 0 1059301 3 0 2119 1059350 0 NLP053-1 non_thm 254.1 165 0 499 0 22 0 0 1059303 3 0 2088 1059352 0 NLP054-1 non_thm 0.1 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP055-1 non_thm 0.0 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP056-1 non_thm 0.0 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP057-1 non_thm 0.0 4 0 168 1 14 0 0 152 2 0 604 153 0 NLP058-1 non_thm 0.0 4 0 168 1 14 0 0 151 2 0 604 152 0 NLP059-1 non_thm 0.0 4 0 10 4 7 3 0 24 2 0 10 28 0 NLP060-1 non_thm 0.0 4 0 9 10 7 3 0 19 2 0 11 29 0 NLP061-1 non_thm 0.0 4 0 10 4 7 3 0 24 2 0 10 28 0 NLP062-1 non_thm 0.0 4 0 10 4 7 3 0 22 2 0 10 26 0 NLP063-1 non_thm 0.0 2 0 8 14 7 3 0 24 2 0 8 38 0 NLP064-1 non_thm 0.0 4 1 20 10 7 3 3 27 3 27 25 57 0 NLP065-1 non_thm 0.0 4 0 8 14 7 3 0 23 2 0 8 37 0 NLP066-1 non_thm 0.0 4 0 12 4 7 3 0 26 2 0 12 30 0 NLP067-1 non_thm 0.0 4 0 10 4 7 3 0 24 2 0 10 28 0 NLP068-1 non_thm 0.0 4 0 5 3 6 3 0 12 2 0 5 15 0 NLP069-1 memory 240.9 499 NLP070-1 memory 234.2 499 NLP071-1 memory 309.6 499 NLP072-1 memory 241.2 499 NLP073-1 memory 236.8 499 NLP074-1 memory 242.8 499 NLP075-1 memory 424.0 499 NLP076-1 memory 174.8 499 NLP077-1 memory 174.1 499 NLP078-1 memory 176.5 499 NLP079-1 theorem 0.0 4 2 40 1 38 4 0 0 2 22 82 54 0 NLP080-1 theorem 0.0 4 2 40 1 38 4 0 0 2 22 80 54 0 NLP081-1 theorem 0.0 4 2 38 1 36 4 0 0 2 21 76 51 0 NLP082-1 timeout 500.0 471 NLP083-1 timeout 500.0 477 NLP084-1 memory 417.6 499 NLP085-1 memory 416.3 499 NLP086-1 memory 424.9 499 NLP087-1 memory 417.4 499 NLP088-1 memory 343.0 499 NLP089-1 memory 344.4 499 NLP090-1 memory 345.5 499 NLP091-1 memory 343.0 499 NLP092-1 memory 345.1 499 NLP093-1 memory 344.2 499 NLP094-1 theorem 0.0 4 2 41 1 30 4 0 0 2 23 50 44 0 NLP095-1 non_thm 0.0 4 0 2 1 3 3 0 6 2 0 2 7 0 NLP096-1 non_thm 0.0 4 0 2 1 3 3 0 6 2 0 2 7 0 NLP097-1 non_thm 0.0 4 0 2 1 3 2 0 7 2 0 2 8 0 NLP098-1 non_thm 0.0 4 0 2 1 3 2 0 7 2 0 2 8 0 NLP099-1 non_thm 0.0 4 0 3 1 4 3 0 2 2 0 3 3 0 NLP100-1 non_thm 0.0 4 0 2 1 3 3 0 14 2 0 2 15 0 NLP101-1 non_thm 0.0 4 0 2 1 3 3 0 14 2 0 2 15 0 NLP102-1 non_thm 0.0 4 0 3 1 4 4 0 9 2 0 3 10 0 NLP103-1 non_thm 0.0 4 0 4 1 5 4 0 10 2 0 4 11 0 NLP104-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 0 1 0 0 NLP105-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 0 1 0 0 NLP106-1 non_thm 0.0 4 0 24 0 2 0 0 0 2 0 25 0 0 NLP107-1 non_thm 0.0 4 0 46 0 3 0 0 0 2 0 48 0 0 NLP108-1 non_thm 0.0 4 0 99 0 10 0 0 0 2 0 105 0 0 NLP109-1 non_thm 0.0 4 0 46 0 3 0 0 0 2 0 48 0 0 NLP110-1 non_thm 0.0 4 0 77 0 9 0 0 0 2 0 82 0 0 NLP111-1 non_thm 0.0 2 0 99 0 10 0 0 0 2 0 105 0 0 NLP112-1 non_thm 0.0 4 0 99 0 10 0 0 0 2 0 105 0 0 NLP113-1 non_thm 0.0 4 0 23 0 2 0 0 0 2 0 24 0 0 NLP114-1 non_thm 0.0 4 0 18 1 19 2 0 31 2 0 18 32 0 NLP115-1 non_thm 0.0 4 0 18 1 19 2 0 31 2 0 18 32 0 NLP116-1 non_thm 0.0 4 0 18 1 19 2 0 31 2 0 18 32 0 NLP117-1 theorem 0.0 4 2 34 1 34 5 0 0 2 19 38 48 0 NLP118-1 non_thm 0.0 4 1 34 1 35 4 0 16 2 19 36 48 0 NLP119-1 non_thm 0.0 4 1 34 1 35 4 0 16 2 19 36 48 0 NLP120-1 non_thm 0.0 4 0 18 1 19 2 0 31 2 0 18 32 0 NLP121-1 non_thm 0.0 4 0 18 1 19 2 0 31 2 0 18 32 0 NLP122-1 theorem 0.0 4 2 34 1 34 5 0 0 2 19 38 48 0 NLP123-1 non_thm 0.0 4 0 18 1 19 2 0 31 2 0 18 32 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 NLP130-1 non_thm 0.0 4 0 24 4 22 4 0 45 2 0 24 49 0 NLP131-1 non_thm 0.0 4 0 21 2 22 4 0 38 2 0 21 40 0 NLP132-1 non_thm 0.0 4 0 21 3 22 4 0 38 2 0 21 41 0 NLP133-1 non_thm 0.0 4 0 21 3 22 4 0 38 2 0 21 41 0 NLP134-1 non_thm 0.0 4 0 21 2 22 4 0 37 2 0 21 39 0 NLP135-1 non_thm 0.0 4 0 24 4 22 4 0 45 2 0 24 49 0 NLP136-1 non_thm 0.0 4 1 43 2 42 5 0 20 2 25 46 62 0 NLP137-1 non_thm 0.0 4 0 30 4 22 4 0 49 3 0 30 57 0 NLP138-1 non_thm 0.0 4 1 43 2 42 5 0 20 2 25 46 62 0 NLP139-1 non_thm 0.0 4 0 30 4 22 4 0 49 3 0 30 57 0 NLP140-1 non_thm 0.0 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP141-1 theorem 0.0 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP142-1 non_thm 0.0 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP143-1 theorem 0.0 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP144-1 non_thm 0.0 4 0 433 0 21 0 0 307 2 0 1764 308 0 NLP145-1 theorem 0.1 4 1 473 0 24 0 0 0 2 473 1935 323 0 NLP146-1 non_thm 0.1 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP147-1 theorem 0.0 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP148-1 non_thm 0.0 4 0 381 0 21 0 0 281 2 0 1538 282 0 NLP149-1 theorem 0.1 4 1 421 0 24 0 0 0 2 421 1714 297 0 NLP150-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP151-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP152-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP153-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP154-1 non_thm 0.0 4 0 224 1 19 0 0 192 2 0 800 193 0 NLP155-1 non_thm 0.0 4 0 224 1 19 0 0 191 2 0 800 192 0 NLP156-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP157-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP158-1 non_thm 0.0 4 0 185 1 19 0 0 166 2 0 657 167 0 NLP159-1 non_thm 0.0 4 0 185 1 19 0 0 165 2 0 657 166 0 NLP160-1 non_thm 0.0 4 0 26 4 27 4 0 48 2 0 26 52 0 NLP161-1 non_thm 0.0 4 0 26 4 27 4 0 48 2 0 26 52 0 NLP162-1 non_thm 0.0 4 0 26 4 27 4 0 48 2 0 26 52 0 NLP163-1 non_thm 0.0 4 1 54 4 52 5 0 25 2 31 57 80 0 NLP164-1 non_thm 0.0 4 1 54 4 52 5 0 25 2 31 57 80 0 NLP165-1 non_thm 0.0 4 1 54 4 52 5 0 25 2 31 57 80 0 NLP166-1 non_thm 0.0 2 0 26 4 27 4 0 48 2 0 26 52 0 NLP167-1 non_thm 0.0 4 0 26 4 27 4 0 48 2 0 26 52 0 NLP168-1 non_thm 0.0 4 0 26 4 27 4 0 48 2 0 26 52 0 NLP169-1 non_thm 0.0 4 0 26 4 27 4 0 48 2 0 26 52 0 NLP170-1 timeout 500.0 16 NLP171-1 timeout 500.0 15 NLP172-1 timeout 500.0 15 NLP173-1 timeout 500.0 15 NLP174-1 timeout 500.0 15 NLP175-1 timeout 500.0 16 NLP176-1 timeout 500.0 15 NLP177-1 timeout 500.0 16 NLP178-1 timeout 500.0 15 NLP179-1 timeout 500.0 15 NLP180-1 timeout 500.0 14 NLP181-1 timeout 500.0 14 NLP182-1 timeout 500.0 14 NLP183-1 timeout 500.0 14 NLP184-1 timeout 500.0 15 NLP185-1 timeout 500.0 14 NLP186-1 timeout 500.0 14 NLP187-1 timeout 500.0 14 NLP188-1 timeout 500.0 14 NLP189-1 timeout 500.0 14 NLP190-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP191-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP192-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP193-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP194-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP195-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP196-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP197-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP198-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP199-1 non_thm 0.0 4 0 33 4 34 4 0 62 2 0 33 66 0 NLP200-1 timeout 500.0 14 NLP201-1 timeout 500.0 15 NLP202-1 timeout 500.0 15 NLP203-1 timeout 500.0 15 NLP204-1 theorem 0.0 4 1 89 0 31 0 0 0 2 89 373 260 0 NLP205-1 timeout 500.0 15 NLP206-1 timeout 500.0 15 NLP207-1 timeout 500.0 15 NLP208-1 theorem 0.0 4 1 89 0 31 0 0 0 2 89 373 260 0 NLP209-1 timeout 500.0 15 NLP210-1 timeout 500.0 15 NLP211-1 timeout 500.0 14 NLP212-1 timeout 500.0 14 NLP213-1 timeout 500.0 14 NLP214-1 timeout 500.0 15 NLP215-1 timeout 500.0 15 NLP216-1 timeout 500.0 15 NLP217-1 timeout 500.0 15 NLP218-1 timeout 500.0 15 NLP219-1 timeout 500.0 15 NLP220-1 non_thm 0.1 4 0 233 0 16 0 0 0 2 0 972 0 0 NLP221-1 non_thm 0.0 4 0 20 1 21 4 0 34 2 0 20 35 0 NLP222-1 non_thm 0.0 4 0 20 1 21 4 0 34 2 0 20 35 0 NLP223-1 non_thm 0.0 4 0 19 1 20 4 0 33 2 0 19 34 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 NLP230-1 non_thm 0.0 4 1 78 1 78 5 0 36 3 43 83 113 0 NLP231-1 non_thm 0.0 4 0 37 1 38 4 0 69 2 0 37 70 0 NLP232-1 non_thm 0.0 4 0 38 1 39 4 0 70 2 0 38 71 0 NLP233-1 non_thm 0.0 4 0 39 1 38 4 0 70 2 0 39 71 0 NLP234-1 non_thm 0.0 4 0 38 1 39 4 0 70 2 0 38 71 0 NLP235-1 non_thm 0.0 4 0 37 1 38 4 0 69 2 0 37 70 0 NLP236-1 non_thm 0.0 4 0 37 1 38 4 0 69 2 0 37 70 0 NLP237-1 non_thm 0.0 4 0 38 1 39 4 0 70 2 0 38 71 0 NLP238-1 non_thm 0.0 0 0 37 1 38 4 0 69 2 0 37 70 0 NLP239-1 non_thm 0.0 4 0 37 1 38 4 0 69 2 0 37 70 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 NUM001-1 theorem 0.0 2 1 26 0 8 0 0 0 3 26 347 0 0 NUM002-1 theorem 0.0 2 1 27 0 8 0 0 0 3 27 356 0 0 NUM003-1 theorem 0.0 2 1 25 0 8 0 0 0 3 25 341 0 0 NUM004-1 theorem 0.0 2 1 27 0 8 0 0 0 3 27 356 0 0 NUM005-1 timeout 500.0 369 NUM006-1 timeout 500.0 283 NUM007-1 timeout 500.0 190 NUM008-1 timeout 500.0 432 NUM009-1 theorem 0.1 2 1 16 0 13 0 0 0 2 16 258 240 0 NUM010-1 timeout 500.0 457 NUM011-1 timeout 500.0 437 NUM012-1 timeout 500.0 433 NUM013-1 timeout 500.0 410 NUM014-1 theorem 0.0 2 1 5 0 4 0 0 0 2 5 11 4 0 NUM015-1 theorem 0.0 2 1 11 0 2 0 0 0 3 11 21 14 0 NUM016-1 theorem 0.0 2 1 14 0 4 0 0 0 3 14 36 12 0 NUM016-2 theorem 0.0 2 1 12 0 2 0 0 0 3 12 18 8 0 NUM017-1 timeout 500.0 104 NUM017-2 timeout 500.0 104 NUM018-1 timeout 500.0 493 NUM019-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 18 0 0 NUM020-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 48 0 0 NUM021-1 theorem 0.0 2 1 80 0 9 0 0 0 3 80 405 210 0 NUM022-1 theorem 0.0 2 1 9 0 3 0 0 0 3 9 14 5 0 NUM023-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 20 0 0 NUM024-1 theorem 0.0 2 1 38 0 8 0 1 0 3 38 314 0 0 NUM025-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 0 0 NUM025-2 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 8 0 NUM026-1 timeout 500.0 33 NUM027-1 theorem 0.0 2 1 49 0 10 0 0 0 2 49 247 142 0 NUM028-1 timeout 500.0 70 NUM029-1 timeout 500.0 84 NUM030-1 timeout 500.0 33 NUM031-1 timeout 500.0 83 NUM032-1 timeout 500.0 71 NUM033-1 timeout 500.0 81 NUM034-1 timeout 500.0 86 NUM035-1 timeout 500.0 70 NUM036-1 timeout 500.0 75 NUM037-1 timeout 500.0 70 NUM038-1 timeout 500.0 74 NUM039-1 timeout 500.0 53 NUM040-1 timeout 500.0 40 NUM041-1 timeout 500.0 69 NUM042-1 timeout 500.0 69 NUM043-1 timeout 500.0 72 NUM044-1 timeout 500.0 73 NUM045-1 timeout 500.0 76 NUM046-1 timeout 500.0 56 NUM047-1 timeout 500.0 60 NUM048-1 timeout 500.0 72 NUM049-1 timeout 500.0 71 NUM050-1 timeout 500.0 51 NUM051-1 timeout 500.0 74 NUM052-1 timeout 500.0 58 NUM053-1 timeout 500.0 45 NUM054-1 timeout 500.0 94 NUM055-1 timeout 500.0 43 NUM056-1 timeout 500.0 74 NUM057-1 timeout 500.0 31 NUM058-1 timeout 500.0 31 NUM059-1 timeout 500.0 51 NUM060-1 timeout 500.0 83 NUM061-1 timeout 500.0 88 NUM062-1 timeout 500.0 50 NUM063-1 timeout 500.0 49 NUM064-1 timeout 500.0 60 NUM065-1 timeout 500.0 58 NUM066-1 timeout 500.0 54 NUM067-1 timeout 500.0 89 NUM068-1 timeout 500.0 73 NUM069-1 timeout 500.0 85 NUM070-1 timeout 500.0 51 NUM071-1 timeout 500.0 53 NUM072-1 timeout 500.0 58 NUM073-1 timeout 500.0 45 NUM074-1 timeout 500.0 50 NUM075-1 timeout 500.0 57 NUM076-1 timeout 500.0 53 NUM077-1 timeout 500.0 53 NUM078-1 timeout 500.0 52 NUM079-1 timeout 500.0 31 NUM080-1 timeout 500.0 69 NUM081-1 timeout 500.0 73 NUM082-1 timeout 500.0 58 NUM083-1 timeout 500.0 26 NUM084-1 timeout 500.0 67 NUM085-1 timeout 500.0 33 NUM086-1 timeout 500.0 71 NUM087-1 timeout 500.0 72 NUM088-1 timeout 500.0 52 NUM089-1 timeout 500.0 62 NUM090-1 timeout 500.0 34 NUM091-1 timeout 500.0 55 NUM092-1 timeout 500.0 53 NUM093-1 timeout 500.0 53 NUM094-1 timeout 500.0 61 NUM095-1 timeout 500.0 60 NUM096-1 timeout 500.0 62 NUM097-1 timeout 500.0 60 NUM098-1 timeout 500.0 38 NUM099-1 timeout 500.0 33 NUM100-1 timeout 500.0 34 NUM101-1 timeout 500.0 30 NUM102-1 timeout 500.0 36 NUM103-1 timeout 500.0 53 NUM104-1 timeout 500.0 29 NUM105-1 timeout 500.0 32 NUM106-1 timeout 500.0 63 NUM107-1 timeout 500.0 54 NUM108-1 timeout 500.0 56 NUM109-1 timeout 500.0 28 NUM110-1 timeout 500.0 35 NUM111-1 timeout 500.0 30 NUM112-1 timeout 500.0 32 NUM113-1 timeout 500.0 74 NUM114-1 timeout 500.0 32 NUM115-1 timeout 500.0 54 NUM116-1 timeout 500.0 31 NUM117-1 timeout 500.0 33 NUM118-1 timeout 500.0 46 NUM119-1 timeout 500.0 54 NUM120-1 timeout 500.0 31 NUM121-1 timeout 500.0 31 NUM122-1 timeout 500.0 31 NUM123-1 timeout 500.0 30 NUM124-1 timeout 500.0 31 NUM125-1 timeout 500.0 53 NUM126-1 timeout 500.0 73 NUM127-1 timeout 500.0 72 NUM128-1 timeout 500.0 73 NUM129-1 timeout 500.0 46 NUM130-1 timeout 500.0 43 NUM131-1 timeout 500.0 48 NUM132-1 timeout 500.0 54 NUM133-1 timeout 500.0 58 NUM134-1 timeout 500.0 55 NUM135-1 timeout 500.0 73 NUM136-1 timeout 500.0 49 NUM137-1 timeout 500.0 55 NUM138-1 timeout 500.0 30 NUM139-1 timeout 500.0 31 NUM140-1 timeout 500.0 51 NUM141-1 timeout 500.0 52 NUM142-1 timeout 500.0 31 NUM143-1 timeout 500.0 69 NUM144-1 timeout 500.0 30 NUM145-1 timeout 500.0 39 NUM146-1 timeout 500.0 30 NUM147-1 timeout 500.0 54 NUM148-1 timeout 500.0 32 NUM149-1 timeout 500.0 28 NUM150-1 timeout 500.0 53 NUM151-1 timeout 500.0 50 NUM152-1 timeout 500.0 32 NUM153-1 timeout 500.0 48 NUM154-1 timeout 500.0 74 NUM155-1 timeout 500.0 81 NUM156-1 timeout 500.0 54 NUM157-1 timeout 500.0 53 NUM158-1 timeout 500.0 32 NUM159-1 timeout 500.0 30 NUM160-1 timeout 500.0 35 NUM161-1 timeout 500.0 72 NUM162-1 timeout 500.0 72 NUM163-1 timeout 500.0 71 NUM164-1 timeout 500.0 72 NUM165-1 timeout 500.0 51 NUM166-1 timeout 500.0 44 NUM167-1 timeout 500.0 70 NUM168-1 timeout 500.0 73 NUM169-1 timeout 500.0 54 NUM170-1 timeout 500.0 56 NUM171-1 timeout 500.0 74 NUM172-1 timeout 500.0 51 NUM173-1 timeout 500.0 59 NUM174-1 timeout 500.0 31 NUM175-1 timeout 500.0 35 NUM176-1 timeout 500.0 49 NUM177-1 timeout 500.0 54 NUM178-1 timeout 500.0 41 NUM179-1 timeout 500.0 45 NUM180-1 theorem 0.1 2 1 235 0 48 0 0 0 2 235 1632 560 0 NUM181-1 timeout 500.0 52 NUM182-1 timeout 500.0 54 NUM183-1 timeout 500.0 31 NUM184-1 timeout 500.0 70 NUM185-1 timeout 500.0 59 NUM186-1 timeout 500.0 72 NUM187-1 timeout 500.0 56 NUM188-1 timeout 500.0 50 NUM189-1 timeout 500.0 56 NUM190-1 timeout 500.0 71 NUM191-1 timeout 500.0 51 NUM192-1 timeout 500.0 55 NUM193-1 timeout 500.0 84 NUM194-1 timeout 500.0 45 NUM195-1 timeout 500.0 62 NUM196-1 timeout 500.0 57 NUM197-1 timeout 500.0 33 NUM198-1 timeout 500.0 55 NUM199-1 timeout 500.0 52 NUM200-1 timeout 500.0 54 NUM201-1 timeout 500.0 55 NUM202-1 timeout 500.0 55 NUM203-1 timeout 500.0 61 NUM204-1 timeout 500.0 50 NUM205-1 timeout 500.0 51 NUM206-1 timeout 500.0 54 NUM207-1 timeout 500.0 54 NUM208-1 timeout 500.0 53 NUM209-1 timeout 500.0 55 NUM210-1 timeout 500.0 53 NUM211-1 timeout 500.0 71 NUM212-1 timeout 500.0 74 NUM213-1 timeout 500.0 65 NUM214-1 timeout 500.0 35 NUM215-1 timeout 500.0 36 NUM216-1 timeout 500.0 50 NUM217-1 timeout 500.0 43 NUM218-1 timeout 500.0 31 NUM219-1 timeout 500.0 31 NUM220-1 timeout 500.0 75 NUM221-1 timeout 500.0 32 NUM222-1 timeout 500.0 44 NUM223-1 timeout 500.0 30 NUM224-1 timeout 500.0 72 NUM225-1 timeout 500.0 33 NUM226-1 timeout 500.0 49 NUM227-1 timeout 500.0 75 NUM228-1 theorem 0.1 2 1 66 0 49 0 0 0 2 66 372 252 0 NUM229-1 timeout 500.0 91 NUM230-1 timeout 500.0 61 NUM231-1 timeout 500.0 60 NUM232-1 timeout 500.0 59 NUM233-1 timeout 500.0 60 NUM234-1 timeout 500.0 59 NUM235-1 timeout 500.0 59 NUM236-1 timeout 500.0 90 NUM237-1 timeout 500.0 97 NUM238-1 timeout 500.0 78 NUM239-1 timeout 500.0 55 NUM240-1 timeout 500.0 49 NUM241-1 timeout 500.0 69 NUM242-1 timeout 500.0 77 NUM243-1 timeout 500.0 34 NUM244-1 timeout 500.0 34 NUM245-1 timeout 500.0 89 NUM245-2 timeout 500.0 92 NUM246-1 timeout 500.0 54 NUM246-2 timeout 500.0 54 NUM247-1 timeout 500.0 25 NUM247-2 timeout 500.0 25 NUM248-1 timeout 500.0 72 NUM248-2 timeout 500.0 74 NUM249-1 timeout 500.0 75 NUM249-2 timeout 500.0 71 NUM250-1 timeout 500.0 32 NUM250-2 timeout 500.0 32 NUM251-1 timeout 500.0 31 NUM251-2 timeout 500.0 32 NUM252-1 timeout 500.0 75 NUM252-2 timeout 500.0 72 NUM253-1 timeout 500.0 50 NUM253-2 timeout 500.0 51 NUM254-1 timeout 500.0 50 NUM254-2 timeout 500.0 50 NUM255-1 timeout 500.0 50 NUM255-2 timeout 500.0 51 NUM256-1 timeout 500.0 51 NUM256-2 timeout 500.0 50 NUM257-1 timeout 500.0 49 NUM257-2 timeout 500.0 50 NUM258-1 timeout 500.0 70 NUM258-2 timeout 500.0 73 NUM259-1 timeout 500.0 72 NUM259-2 timeout 500.0 73 NUM260-1 timeout 500.0 74 NUM260-2 timeout 500.0 74 NUM261-1 timeout 500.0 72 NUM261-2 timeout 500.0 72 NUM262-1 timeout 500.0 70 NUM262-2 timeout 500.0 73 NUM263-1 timeout 500.0 53 NUM263-2 timeout 500.0 54 NUM264-1 timeout 500.0 58 NUM264-2 timeout 500.0 55 NUM265-1 timeout 500.0 71 NUM266-1 timeout 500.0 53 NUM267-1 timeout 500.0 55 NUM268-1 timeout 500.0 55 NUM269-1 timeout 500.0 77 NUM270-1 timeout 500.0 72 NUM271-1 timeout 500.0 44 NUM272-1 timeout 500.0 31 NUM273-1 timeout 500.0 35 NUM274-1 timeout 500.0 64 NUM275-1 timeout 500.0 67 NUM276-1 timeout 500.0 44 NUM277-1 timeout 500.0 31 NUM277-2 timeout 500.0 55 NUM278-1 timeout 500.0 54 NUM279-1 timeout 500.0 73 NUM280-1 timeout 500.0 71 NUM281-1 timeout 500.0 54 NUM282-1 timeout 500.0 57 NUM283-1.005 theorem 0.2 2 1 155 0 4 0 0 0 25 155 158 0 0 NUM284-1.014 theorem 32.0 6 1 249 0 4 0 0 0 234 249 524 0 0 NUM285-1 non_thm 0.0 2 0 16 5 23 44 0 11 2 0 16 16 0 NUM286-1 timeout 500.0 37 NUM286-2 timeout 500.0 176 NUM286-3 memory 482.8 499 NUM287-1 timeout 500.0 54 NUM288-1 timeout 500.0 28 NUM289-1 timeout 500.0 75 PLA001-1 theorem 0.0 2 1 23 0 12 0 0 0 2 23 41 0 0 PLA002-1 theorem 0.0 2 1 7 0 6 8 0 0 2 7 10 3 0 PLA002-2 theorem 4.2 32 1 1994 0 2 0 0 0 5 1994 2625 611529 0 PLA003-1 theorem 0.0 2 1 15 0 5 2 3 0 2 15 33 0 0 PLA004-1 timeout 500.0 59 PLA004-2 timeout 500.0 60 PLA005-1 timeout 500.0 59 PLA005-2 timeout 500.0 59 PLA006-1 theorem 0.0 2 1 21 0 20 0 0 0 2 21 38 0 0 PLA007-1 timeout 500.0 59 PLA008-1 timeout 500.0 59 PLA009-1 timeout 500.0 59 PLA009-2 timeout 500.0 59 PLA010-1 timeout 500.0 59 PLA011-1 timeout 500.0 59 PLA011-2 timeout 500.0 60 PLA012-1 timeout 500.0 59 PLA013-1 timeout 500.0 59 PLA014-1 timeout 500.0 59 PLA014-2 timeout 500.0 59 PLA015-1 timeout 500.0 59 PLA016-1 timeout 500.0 58 PLA017-1 theorem 0.0 2 1 68 0 20 0 0 0 3 68 216 0 0 PLA018-1 timeout 500.0 59 PLA019-1 timeout 500.0 59 PLA020-1 theorem 0.0 2 1 18 0 18 0 0 0 2 18 43 0 0 PLA021-1 timeout 500.0 59 PLA022-1 theorem 2.5 8 1 1066 0 20 0 0 0 4 1066 20905 0 0 PLA022-2 theorem 2.5 8 1 1066 0 20 0 0 0 4 1066 20905 0 0 PLA023-1 timeout 500.0 59 PLA029-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 PLA030-1 timeout 500.0 59 PUZ001-1 theorem 0.0 2 1 17 0 5 2 0 0 2 17 20 8 0 PUZ001-2 theorem 0.0 2 1 42 0 9 0 0 0 2 42 194 92 0 PUZ001-3 non_thm 0.0 2 0 19 0 6 2 0 10 2 0 22 11 0 PUZ002-1 theorem 0.0 2 1 11 0 2 0 0 0 2 11 13 5 0 PUZ003-1 theorem 0.0 2 1 9 0 6 0 0 0 2 9 18 0 0 PUZ004-1 theorem 0.0 2 1 10 0 10 11 0 0 2 10 12 3 0 PUZ005-1 theorem 0.0 2 2 26 1 3 0 0 0 2 21 83 164 0 PUZ006-1 theorem 0.0 2 1 21 0 14 8 0 0 2 21 82 40 0 PUZ007-1 theorem 0.0 2 2 33 1 18 15 0 35 2 22 128 82 0 PUZ008-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 PUZ008-2 theorem 0.0 2 1 15 0 16 14 0 0 3 15 19 0 0 PUZ008-3 theorem 0.0 2 1 37 0 4 0 0 0 6 37 69 0 0 PUZ009-1 theorem 0.0 2 1 5 0 6 11 0 0 2 5 11 11 0 PUZ010-1 theorem 1.1 2 344 6918 359 1227 446 0 4981 2 204 20149 27734 0 PUZ011-1 theorem 0.0 2 1 18 0 18 0 0 0 2 18 55 0 0 PUZ012-1 theorem 0.0 2 1 20 0 13 1 0 0 2 20 36 20 0 PUZ013-1 theorem 0.0 2 1 7 0 10 10 0 0 2 7 12 10 0 PUZ014-1 theorem 0.0 2 2 16 1 21 22 0 10 2 13 22 17 0 PUZ015-1 timeout 500.0 361 PUZ015-2.006 theorem 0.1 2 143 2384 150 2680 5261 0 197 2 59 3255 1759 0 PUZ016-1 timeout 500.0 368 PUZ016-2.004 non_thm 0.0 2 0 22 2 29 39 0 17 2 0 24 30 0 PUZ016-2.005 theorem 0.0 2 26 362 25 417 789 0 25 2 40 472 282 0 PUZ017-1 theorem 0.1 2 5 302 4 85 1 5 403 2 231 1159 1598 0 PUZ018-1 theorem 0.0 2 1 53 0 41 6 0 0 2 53 84 891 0 PUZ018-2 non_thm 0.1 2 2 89 22 40 6 0 1971 2 109 163 3101 0 PUZ019-1 theorem 0.0 2 1 116 0 44 1 3 0 2 116 333 577 0 PUZ020-1 theorem 0.0 2 1 16 0 9 2 0 0 2 16 59 17 0 PUZ021-1 theorem 0.1 2 13 195 66 0 0 6 339 3 55 877 3786 0 PUZ022-1 theorem 0.0 2 1 38 0 31 0 0 0 2 38 64 0 0 PUZ023-1 theorem 0.0 2 2 10 2 8 6 0 4 2 11 30 16 0 PUZ024-1 theorem 0.0 2 1 7 0 9 7 0 0 2 7 19 7 0 PUZ025-1 theorem 0.0 2 8 37 9 7 4 0 40 2 22 223 180 0 PUZ026-1 theorem 0.0 2 3 29 2 12 5 3 10 2 18 99 61 0 PUZ027-1 theorem 0.0 2 3 18 2 13 14 0 1 2 12 73 40 0 PUZ028-1 non_thm 0.0 2 0 31 15 11 0 0 20 2 0 91 35 0 PUZ028-2 non_thm 0.0 2 0 70 18 36 0 0 16 2 0 190 46 0 PUZ028-3 non_thm 0.0 2 0 70 18 88 154 0 12 2 0 114 42 0 PUZ028-4 non_thm 0.0 2 0 28 18 46 106 0 12 2 0 60 42 0 PUZ028-5 theorem 0.1 2 30 742 29 11 0 0 97 2 90 1674 246 0 PUZ028-6 theorem 0.1 2 20 376 19 36 0 0 102 2 82 1298 292 0 PUZ029-1 theorem 0.0 2 1 13 0 4 0 0 0 2 13 17 14 0 PUZ030-1 theorem 0.0 2 24 327 24 363 397 0 115 2 28 875 982 0 PUZ030-2 theorem 0.0 2 9 35 8 51 173 0 7 2 10 94 89 0 PUZ031-1 theorem 0.0 2 1 33 0 6 0 0 0 2 33 56 30 0 PUZ032-1 theorem 0.0 2 2 16 1 4 0 0 6 3 16 54 17 0 PUZ033-1 theorem 0.0 2 1 11 0 11 17 0 0 2 11 15 8 0 PUZ034-1.003 timeout 500.0 65 PUZ034-1.004 timeout 500.0 64 PUZ035-1 theorem 0.0 3 4 16 3 13 17 0 1 2 9 41 14 0 PUZ035-2 theorem 0.0 2 4 25 3 20 30 1 6 2 12 55 28 0 PUZ035-3 theorem 0.0 2 4 12 3 6 8 0 2 2 8 27 6 0 PUZ035-4 theorem 0.0 2 4 12 3 6 8 0 2 2 8 27 6 0 PUZ035-5 theorem 0.0 2 4 7 4 5 0 0 0 2 6 27 20 0 PUZ035-6 theorem 0.0 2 4 5 4 5 0 0 7 2 6 20 31 0 PUZ035-7 theorem 0.1 2 12 217 32 8 0 0 366 3 81 882 2294 0 PUZ036-1.005 theorem 0.0 2 1 61 0 2 0 0 0 2 61 184 0 0 PUZ037-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 28 0 0 PUZ037-2 theorem 0.0 2 1 6 0 2 0 0 0 2 6 102 0 0 PUZ037-3 theorem 0.6 13 1 173 0 2 0 0 0 2 173 3105 0 0 PUZ038-1 theorem 0.0 3 1 2 0 2 0 0 0 2 2 2 0 0 PUZ039-1 timeout 500.0 450 PUZ040-1 timeout 500.0 491 PUZ041-1 timeout 500.0 458 PUZ042-1 timeout 500.0 456 PUZ043-1 non_thm 0.0 3 1 1 5 1 0 0 10 2 5 4 16 0 PUZ044-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 PUZ045-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 0 0 1 0 PUZ046-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 PUZ047-1 theorem 0.0 2 1 10 0 10 11 0 0 2 10 16 0 0 PUZ048-1 timeout 500.0 408 PUZ049-1 timeout 500.0 458 PUZ050-1 memory 331.8 499 PUZ051-1 timeout 500.0 466 RNG001-1 theorem 0.5 3 1 57 0 8 0 0 0 2 57 12264 0 0 RNG001-2 theorem 0.8 3 1 64 0 7 0 0 0 2 64 16590 0 0 RNG001-3 theorem 0.0 2 1 9 0 4 0 0 0 2 9 93 0 0 RNG001-4 theorem 0.5 2 1 53 0 8 0 0 0 2 53 11936 0 0 RNG001-5 theorem 0.5 3 1 57 0 8 0 0 0 2 57 12262 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 RNG004-3 timeout 500.0 289 RNG005-1 theorem 0.3 3 1 50 0 10 0 0 0 2 50 8394 0 0 RNG005-2 theorem 0.0 3 1 11 0 11 0 0 0 2 11 585 0 0 RNG006-1 theorem 0.0 2 1 13 0 12 0 0 0 2 13 277 0 0 RNG006-2 theorem 0.0 2 1 14 0 13 0 0 0 2 14 695 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 RNG037-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 310 0 0 RNG038-1 theorem 0.1 2 1 24 0 10 0 0 0 2 24 1150 0 0 RNG038-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 321 0 0 RNG039-1 theorem 2.2 5 1 84 0 50 0 4 0 2 84 47941 0 0 RNG039-2 theorem 1.2 5 1 64 0 50 0 6 0 2 64 31718 0 0 RNG040-1 theorem 0.0 3 1 14 0 14 0 0 0 2 14 634 565 0 RNG040-2 theorem 2.1 6 1 77 0 14 0 0 0 2 77 23821 22814 0 RNG041-1 theorem 0.4 0 1 45 0 14 0 0 0 2 45 9186 3512 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 ROB025-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 SET001-1 theorem 0.0 2 1 4 0 3 0 0 0 2 4 8 3 0 SET002-1 theorem 0.0 2 3 9 3 2 0 0 0 2 8 21 22 0 SET002-6 timeout 500.0 61 SET003-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 9 6 0 SET004-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 8 5 0 SET005-1 theorem 0.0 2 2 135 1 4 0 0 0 2 131 378 143 0 SET006-1 theorem 0.0 2 1 6 0 2 0 0 0 2 6 10 7 0 SET007-1 theorem 0.1 2 3 578 2 5 0 38 0 2 339 2353 722 0 SET008-1 theorem 0.0 2 1 10 0 3 0 0 0 2 10 34 21 0 SET009-1 theorem 0.0 2 1 22 0 4 0 0 0 2 22 41 17 0 SET010-1 theorem 0.1 2 3 835 2 5 0 61 0 2 486 3402 997 0 SET011-1 theorem 0.0 2 2 73 1 3 0 0 0 2 67 239 94 0 SET012-1 timeout 500.0 76 SET012-2 theorem 0.0 2 3 131 2 6 0 0 510 2 102 1735 1045 0 SET012-3 memory 371.7 499 SET012-4 theorem 0.0 2 2 137 1 5 0 0 69 2 88 663 309 0 SET013-1 timeout 500.0 71 SET013-2 theorem 0.2 3 3 609 2 6 0 0 510 2 336 6941 2910 0 SET013-3 memory 370.7 499 SET013-4 theorem 0.1 2 2 246 1 5 0 0 146 2 150 1880 504 0 SET014-2 theorem 314.0 17 1 294 0 6 0 0 0 3 294 11114 5256 0 SET014-3 memory 356.3 499 SET014-4 timeout 500.0 19 SET014-6 timeout 500.0 60 SET015-1 timeout 500.0 69 SET015-2 theorem 0.1 2 3 381 2 6 0 0 510 2 222 4397 1954 0 SET015-3 memory 366.3 499 SET015-4 timeout 500.0 33 SET016-1 theorem 0.0 2 1 38 0 7 0 0 0 3 38 289 105 0 SET016-3 memory 449.3 499 SET016-6 timeout 500.0 33 SET016-7 theorem 0.0 2 1 41 0 41 0 0 0 2 41 401 351 0 SET017-3 memory 457.2 499 SET017-4 memory 441.2 499 SET017-6 theorem 0.2 2 1 260 0 33 0 1 0 2 260 2119 1260 0 SET017-7 theorem 0.8 3 1 713 0 41 0 1 0 2 713 13708 3291 0 SET018-1 theorem 0.5 3 1 611 0 7 0 43 0 3 611 7030 1171 0 SET018-3 timeout 500.0 106 SET018-4 timeout 500.0 97 SET018-6 timeout 500.0 34 SET018-7 theorem 0.0 2 1 41 0 41 0 0 0 2 41 401 353 0 SET019-3 timeout 500.0 468 SET019-4 memory 357.5 499 SET020-3 timeout 500.0 24 SET020-4 memory 440.0 499 SET020-6 timeout 500.0 137 SET020-7 timeout 500.0 35 SET021-3 timeout 500.0 24 SET021-4 memory 452.6 499 SET021-6 timeout 500.0 136 SET021-7 timeout 500.0 35 SET022-3 timeout 500.0 453 SET022-4 memory 389.9 499 SET023-3 timeout 500.0 435 SET023-4 memory 398.7 499 SET024-3 theorem 0.0 2 1 26 0 14 0 0 0 2 26 277 241 0 SET024-4 theorem 0.0 2 1 26 0 14 0 0 0 2 26 252 216 0 SET024-6 theorem 0.0 2 1 33 0 32 0 0 0 2 33 165 135 0 SET024-7 theorem 0.0 2 1 43 0 42 0 0 0 2 43 341 276 0 SET025-3 theorem 19.9 11 1 957 0 13 0 0 0 2 957 68179 60307 0 SET025-4 theorem 7.5 11 1 957 0 13 0 0 0 2 957 65905 58218 0 SET025-6 theorem 0.0 2 1 24 0 24 0 0 0 2 24 144 112 0 SET025-7 theorem 0.0 2 1 36 0 36 0 0 0 2 36 329 275 0 SET025-8 theorem 0.1 2 1 74 0 15 0 0 0 2 74 1881 861 0 SET025-9 theorem 0.1 2 1 156 0 14 0 0 0 2 156 2501 1050 0 SET027-3 theorem 404.9 17 1 1454 0 16 0 0 0 2 1454 114704 63554 0 SET027-4 theorem 10.4 13 1 1413 0 15 0 0 0 2 1413 73327 58824 0 SET027-6 theorem 0.0 2 1 92 0 33 0 0 0 2 92 585 295 0 SET027-7 theorem 0.0 2 1 92 0 34 0 0 0 2 92 585 295 0 SET028-3 timeout 500.0 236 SET028-4 memory 370.9 499 SET029-3 timeout 500.0 241 SET029-4 memory 357.3 499 SET030-3 timeout 500.0 164 SET030-4 memory 398.8 499 SET030-6 timeout 500.0 62 SET031-3 timeout 500.0 184 SET031-4 memory 447.0 499 SET032-3 timeout 500.0 218 SET032-4 memory 355.6 499 SET032-6 timeout 500.0 61 SET033-3 timeout 500.0 220 SET033-4 memory 356.1 498 SET033-6 timeout 500.0 61 SET034-3 timeout 500.0 23 SET034-4 memory 456.0 499 SET034-6 timeout 500.0 63 SET035-3 timeout 500.0 23 SET035-4 memory 389.6 499 SET035-6 timeout 500.0 62 SET036-3 timeout 500.0 23 SET036-4 memory 437.6 499 SET036-6 timeout 500.0 134 SET037-3 timeout 500.0 23 SET037-4 timeout 500.0 444 SET037-6 timeout 500.0 33 SET038-3 timeout 500.0 18 SET038-4 timeout 500.0 107 SET038-6 timeout 500.0 101 SET039-3 timeout 500.0 23 SET039-4 timeout 500.0 442 SET040-3 timeout 500.0 46 SET040-4 memory 373.0 499 SET040-6 timeout 500.0 62 SET041-3 timeout 500.0 24 SET041-4 timeout 500.0 446 SET041-6 timeout 500.0 50 SET042-3 timeout 500.0 24 SET042-4 memory 479.7 499 SET043-5 theorem 0.0 2 4 0 3 0 0 0 0 2 2 8 9 0 SET044-5 theorem 0.0 2 8 8 13 0 0 0 18 2 6 32 79 0 SET045-5 theorem 0.0 2 6 2 6 1 0 0 8 2 6 15 34 0 SET046-5 theorem 0.0 2 4 4 3 0 0 0 1 2 4 18 19 0 SET047-5 theorem 0.0 2 4 6 3 4 4 0 1 2 4 24 15 0 SET050-6 theorem 0.0 2 1 38 0 32 0 2 0 2 38 209 153 0 SET051-6 theorem 0.0 2 1 38 0 32 0 2 0 2 38 208 153 0 SET052-6 theorem 0.0 2 1 33 0 32 0 1 0 2 33 173 123 0 SET053-6 theorem 0.0 2 1 33 0 32 0 1 0 2 33 172 123 0 SET054-6 theorem 0.0 2 1 5 0 5 0 0 0 2 5 99 67 0 SET054-7 theorem 0.0 2 1 5 0 5 0 0 0 2 5 99 67 0 SET055-6 theorem 118.3 10 51 17443 108 30 0 204 273966 2 5353 370551 283070 0 SET055-7 theorem 0.0 2 1 5 0 5 0 0 0 2 5 47 15 0 SET056-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 189 141 0 SET056-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 208 159 0 SET057-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 199 148 0 SET057-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 221 166 0 SET058-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 199 148 0 SET058-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 221 166 0 SET059-6 theorem 0.0 2 1 38 0 33 0 0 0 2 38 199 153 0 SET059-7 theorem 0.0 2 1 38 0 34 0 0 0 2 38 221 171 0 SET060-6 theorem 0.0 2 1 38 0 31 0 0 0 2 38 206 179 0 SET060-7 theorem 0.0 2 1 38 0 32 0 0 0 2 38 230 203 0 SET061-6 timeout 500.0 42 SET061-7 timeout 500.0 46 SET062-6 theorem 0.1 2 1 176 0 31 0 0 0 2 176 1132 408 0 SET062-7 theorem 0.0 2 1 7 0 7 0 0 0 2 7 119 81 0 SET063-6 theorem 0.1 2 1 202 0 32 0 0 0 2 202 1314 446 0 SET063-7 theorem 0.0 2 1 9 0 9 0 0 0 2 9 145 98 0 SET064-6 theorem 0.1 2 1 258 0 32 0 0 0 2 258 1734 495 0 SET064-7 theorem 0.0 2 1 17 0 17 0 0 0 2 17 191 139 0 SET065-6 theorem 0.0 2 1 32 0 31 0 0 0 2 32 161 122 0 SET065-7 theorem 0.0 2 1 36 0 35 0 0 0 2 36 253 189 0 SET066-6 timeout 500.0 62 SET066-7 timeout 500.0 37 SET067-6 timeout 500.0 62 SET067-7 timeout 500.0 35 SET068-6 timeout 500.0 62 SET068-7 timeout 500.0 35 SET069-6 timeout 500.0 49 SET069-7 timeout 500.0 27 SET070-6 timeout 500.0 49 SET070-7 timeout 500.0 27 SET071-6 timeout 500.0 29 SET071-7 timeout 500.0 21 SET072-6 theorem 0.2 2 1 261 0 33 0 1 0 2 261 2169 1285 0 SET072-7 theorem 0.2 2 1 234 0 41 0 0 0 2 234 3934 1339 0 SET073-6 timeout 500.0 44 SET073-7 theorem 0.0 2 1 41 0 40 0 0 0 2 41 322 269 0 SET074-6 timeout 500.0 44 SET074-7 theorem 0.0 2 1 41 0 40 0 0 0 2 41 322 269 0 SET075-6 timeout 500.0 98 SET075-7 theorem 0.0 2 1 41 0 40 0 0 0 2 41 314 263 0 SET076-6 timeout 500.0 134 SET076-7 timeout 500.0 40 SET077-6 theorem 0.0 2 1 8 0 8 0 0 0 2 8 121 93 0 SET077-7 theorem 0.0 2 1 16 0 16 0 0 0 2 16 235 184 0 SET078-6 theorem 0.0 2 1 32 0 31 0 0 0 2 32 145 122 0 SET078-7 theorem 0.0 2 1 33 0 33 0 0 0 2 33 288 236 0 SET079-6 timeout 500.0 43 SET079-7 theorem 0.0 2 1 43 0 42 0 0 0 2 43 353 291 0 SET080-6 theorem 0.0 2 1 41 0 31 0 0 0 2 41 229 195 0 SET080-7 theorem 0.0 2 1 17 0 17 0 0 0 2 17 248 193 0 SET081-6 theorem 0.0 2 1 35 0 32 0 0 0 2 35 174 143 0 SET081-7 theorem 0.0 2 1 44 0 43 0 0 0 2 44 338 267 0 SET082-6 timeout 500.0 52 SET082-7 theorem 0.0 2 1 48 0 43 0 1 0 2 48 411 291 0 SET083-6 theorem 0.0 2 1 73 0 33 0 0 0 2 73 463 349 0 SET083-7 theorem 0.1 2 1 108 0 44 0 0 0 2 108 1564 834 0 SET084-6 theorem 0.0 2 1 82 0 33 0 0 0 2 82 529 375 0 SET084-7 theorem 0.1 2 1 171 0 44 0 3 0 2 171 2693 999 0 SET085-6 theorem 0.0 2 1 89 0 34 0 0 0 2 89 586 350 0 SET085-7 theorem 0.1 2 1 241 0 45 0 0 0 2 241 3955 1290 0 SET086-6 timeout 500.0 43 SET086-7 timeout 500.0 32 SET087-6 timeout 500.0 43 SET087-7 timeout 500.0 32 SET088-6 timeout 500.0 63 SET088-7 timeout 500.0 31 SET089-6 timeout 500.0 62 SET089-7 timeout 500.0 31 SET090-6 timeout 500.0 43 SET090-7 timeout 500.0 32 SET091-6 timeout 500.0 63 SET091-7 timeout 500.0 41 SET092-6 timeout 500.0 63 SET092-7 timeout 500.0 42 SET093-6 theorem 0.0 2 1 39 0 32 0 1 0 2 39 223 157 0 SET093-7 theorem 0.0 2 1 24 0 24 0 0 0 2 24 300 237 0 SET094-6 timeout 500.0 138 SET094-7 timeout 500.0 19 SET095-6 timeout 500.0 39 SET095-7 theorem 0.0 2 1 44 0 43 0 0 0 2 44 367 293 0 SET096-6 timeout 500.0 35 SET096-7 theorem 0.1 2 1 200 0 44 0 0 0 2 200 3145 1098 0 SET097-6 timeout 500.0 53 SET097-7 timeout 500.0 34 SET098-6 timeout 500.0 54 SET098-7 timeout 500.0 33 SET099-6 timeout 500.0 53 SET099-7 timeout 500.0 34 SET100-6 timeout 500.0 62 SET100-7 timeout 500.0 32 SET101-6 timeout 500.0 62 SET101-7 timeout 500.0 33 SET102-6 timeout 500.0 62 SET102-7 timeout 500.0 32 SET103-6 timeout 500.0 50 SET103-7 timeout 500.0 30 SET104-6 timeout 500.0 50 SET104-7 timeout 500.0 30 SET105-6 timeout 500.0 29 SET105-7 timeout 500.0 21 SET108-6 timeout 500.0 131 SET108-7 timeout 500.0 37 SET109-6 timeout 500.0 64 SET109-7 timeout 500.0 37 SET110-6 timeout 500.0 64 SET110-7 timeout 500.0 38 SET111-6 timeout 500.0 62 SET111-7 timeout 500.0 37 SET112-6 timeout 500.0 64 SET112-7 timeout 500.0 38 SET113-6 timeout 500.0 63 SET113-7 timeout 500.0 44 SET114-6 timeout 500.0 65 SET114-7 timeout 500.0 44 SET115-6 timeout 500.0 63 SET115-7 timeout 500.0 43 SET116-6 timeout 500.0 63 SET116-7 timeout 500.0 43 SET117-6 theorem 0.0 2 1 40 0 32 0 1 0 2 40 229 165 0 SET117-7 theorem 0.0 2 1 40 0 40 0 0 0 2 40 378 327 0 SET118-6 theorem 0.0 2 1 13 0 13 0 0 0 2 13 137 99 0 SET118-7 theorem 0.0 2 1 27 0 27 0 0 0 2 27 346 292 0 SET119-6 timeout 500.0 49 SET119-7 timeout 500.0 34 SET120-6 timeout 500.0 49 SET120-7 timeout 500.0 34 SET121-6 timeout 500.0 49 SET121-7 timeout 500.0 24 SET122-6 timeout 500.0 49 SET122-7 timeout 500.0 24 SET123-6 timeout 500.0 20 SET124-6 timeout 500.0 44 SET125-6 timeout 500.0 99 SET126-6 timeout 500.0 62 SET127-6 timeout 500.0 62 SET128-6 timeout 500.0 62 SET129-6 timeout 500.0 35 SET130-6 timeout 500.0 42 SET131-6 timeout 500.0 44 SET132-6 timeout 500.0 44 SET133-6 timeout 500.0 123 SET134-6 timeout 500.0 42 SET135-6 timeout 500.0 43 SET136-6 timeout 500.0 42 SET137-6 timeout 500.0 131 SET138-6 timeout 500.0 141 SET139-6 timeout 500.0 62 SET140-6 timeout 500.0 62 SET141-6 timeout 500.0 62 SET142-6 timeout 500.0 62 SET143-6 timeout 500.0 61 SET144-6 timeout 500.0 61 SET145-6 timeout 500.0 62 SET146-6 timeout 500.0 63 SET147-6 timeout 500.0 61 SET148-6 timeout 500.0 61 SET149-6 timeout 500.0 61 SET150-6 timeout 500.0 60 SET151-6 timeout 500.0 61 SET152-6 timeout 500.0 61 SET153-6 timeout 500.0 60 SET154-6 timeout 500.0 61 SET155-6 timeout 500.0 61 SET156-6 timeout 500.0 62 SET157-6 timeout 500.0 87 SET158-6 theorem 0.0 2 1 42 0 41 0 0 0 2 42 240 203 0 SET159-6 timeout 500.0 62 SET160-6 timeout 500.0 61 SET161-6 timeout 500.0 61 SET162-6 timeout 500.0 61 SET163-6 timeout 500.0 61 SET165-6 timeout 500.0 61 SET166-6 timeout 500.0 22 SET167-6 timeout 500.0 98 SET168-6 timeout 500.0 100 SET169-6 timeout 500.0 61 SET170-6 timeout 500.0 61 SET171-6 timeout 500.0 61 SET172-6 timeout 500.0 61 SET173-6 timeout 500.0 61 SET174-6 timeout 500.0 61 SET175-6 timeout 500.0 62 SET176-6 timeout 500.0 61 SET177-6 timeout 500.0 62 SET178-6 timeout 500.0 61 SET179-6 timeout 500.0 61 SET180-6 timeout 500.0 61 SET181-6 timeout 500.0 61 SET182-6 timeout 500.0 61 SET183-6 timeout 500.0 71 SET184-6 theorem 0.1 2 1 88 0 40 0 0 0 2 88 514 319 0 SET185-6 timeout 500.0 71 SET186-6 timeout 500.0 49 SET187-6 timeout 500.0 73 SET188-6 timeout 500.0 47 SET189-6 timeout 500.0 49 SET190-6 timeout 500.0 71 SET191-6 timeout 500.0 49 SET192-6 timeout 500.0 50 SET193-6 theorem 0.1 2 1 167 0 40 0 0 0 2 167 989 417 0 SET194-6 timeout 500.0 61 SET195-6 timeout 500.0 62 SET196-6 timeout 500.0 67 SET197-6 timeout 500.0 67 SET199-6 timeout 500.0 59 SET200-6 timeout 500.0 70 SET201-6 timeout 500.0 74 SET202-6 timeout 500.0 66 SET203-6 theorem 0.0 2 1 45 0 41 0 0 0 2 45 248 191 0 SET204-6 theorem 0.0 2 1 46 0 40 0 0 0 2 46 219 175 0 SET205-6 timeout 500.0 62 SET206-6 timeout 500.0 62 SET207-6 timeout 500.0 61 SET208-6 timeout 500.0 49 SET209-6 timeout 500.0 48 SET210-6 timeout 500.0 61 SET211-6 timeout 500.0 61 SET212-6 timeout 500.0 61 SET213-6 timeout 500.0 61 SET214-6 timeout 500.0 62 SET215-6 timeout 500.0 61 SET216-6 timeout 500.0 61 SET217-6 timeout 500.0 61 SET218-6 timeout 500.0 62 SET219-6 timeout 500.0 61 SET220-6 timeout 500.0 61 SET221-6 timeout 500.0 61 SET222-6 timeout 500.0 61 SET223-6 timeout 500.0 61 SET224-6 timeout 500.0 60 SET225-6 timeout 500.0 60 SET226-6 timeout 500.0 48 SET227-6 timeout 500.0 49 SET228-6 timeout 500.0 48 SET229-6 timeout 500.0 46 SET230-6 timeo