-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj false -uv false -uh false Problems list file : hne-problems Output file : hne-output Summary file : hne-summary Time limit : 300 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 ANA003-2 timeout 300.0 15 ANA004-2 timeout 300.0 15 ANA005-2 timeout 300.0 15 COM001-1 theorem 0.0 2 1 9 0 7 0 0 0 2 9 18 4 1 COM002-1 theorem 0.0 2 1 26 0 15 0 0 0 2 26 43 19 1 GEO001-4 timeout 300.0 41 GEO002-4 theorem 0.0 2 1 13 0 3 0 3 0 2 13 57 31 1 GEO079-1 theorem 0.0 2 1 3 0 2 0 0 0 2 3 6 1 1 GRP001-5 theorem 0.0 2 1 7 0 5 0 0 0 2 7 96 79 1 GRP003-1 theorem 0.0 2 1 5 0 3 0 0 0 3 5 48 31 0 GRP003-2 theorem 0.0 2 1 24 0 4 0 0 0 2 24 860 785 0 GRP004-1 theorem 0.0 2 1 11 0 3 0 0 0 2 11 160 23 0 GRP004-2 theorem 0.0 2 1 22 0 4 0 0 0 2 22 824 785 0 GRP005-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 72 62 0 GRP006-1 theorem 0.0 2 1 7 0 6 0 0 0 2 7 74 63 1 GRP028-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 5 1 0 GRP028-3 theorem 0.0 2 1 4 0 4 0 0 0 2 4 9 4 0 GRP028-4 theorem 0.0 2 1 3 0 3 0 0 0 2 3 6 2 0 GRP029-2 theorem 0.4 2 1 11 0 5 0 0 0 3 11 281 247 1 GRP031-2 theorem 0.0 2 1 11 0 4 0 0 0 2 11 176 67 0 GRP033-3 theorem 0.0 2 1 8 0 7 0 0 0 2 8 155 142 1 GRP034-4 theorem 0.0 2 1 7 0 6 0 0 0 2 7 78 67 1 GRP041-2 theorem 0.0 2 1 3 0 3 0 0 0 2 3 20 14 0 GRP042-2 theorem 0.0 2 1 6 0 5 0 0 0 2 6 34 24 1 GRP043-2 theorem 0.0 2 1 15 0 6 0 0 0 2 15 156 85 1 GRP044-2 theorem 0.0 2 1 7 0 6 0 0 0 2 7 62 44 1 GRP045-2 theorem 0.0 2 1 17 0 6 0 0 0 2 17 428 375 1 GRP046-2 theorem 0.0 2 1 16 0 5 0 0 0 2 16 394 375 1 GRP047-2 theorem 0.0 2 1 16 0 5 0 0 0 2 16 425 404 1 GRP048-2 theorem 4.8 5 1 45 0 5 0 0 0 3 45 9873 9837 1 GRP394-2 timeout 300.0 226 KRS004-1 theorem 0.0 2 1 2 0 1 0 0 0 2 2 5 1 1 LAT005-1 theorem 4.7 7 1 405 0 17 0 14 0 2 405 95285 5034 1 LAT005-2 theorem 3.3 6 1 403 0 21 0 14 0 2 403 75398 3960 1 LCL001-1 timeout 300.0 37 LCL002-1 timeout 300.0 79 LCL003-1 timeout 300.0 93 LCL004-1 theorem 3.4 9 1 310 0 2 0 198 0 8 310 29297 28336 1 LCL005-1 timeout 300.0 106 LCL006-1 theorem 0.7 3 1 132 0 3 0 0 0 5 132 5234 5106 1 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 19 1 LCL009-1 theorem 0.0 2 1 23 0 2 0 2 0 5 23 263 228 1 LCL010-1 theorem 0.0 2 1 11 0 2 0 0 0 5 11 81 69 1 LCL011-1 theorem 0.0 2 1 24 0 2 0 0 0 5 24 292 253 1 LCL012-1 theorem 33.8 16 1 410 0 2 0 0 0 7 410 71592 70969 1 LCL013-1 theorem 0.0 2 1 3 0 2 0 0 0 6 3 4 0 0 LCL014-1 theorem 10.5 9 1 245 0 2 0 1 0 7 245 29886 29480 1 LCL015-1 theorem 141.0 20 1 402 0 2 0 0 0 8 402 78866 77010 1 LCL016-1 theorem 122.2 35 1 635 0 2 0 0 0 8 635 188208 187037 1 LCL017-1 timeout 300.0 26 LCL018-1 theorem 106.5 19 1 349 0 2 0 0 0 9 349 66924 65589 1 LCL019-1 timeout 300.0 84 LCL020-1 timeout 300.0 57 LCL021-1 timeout 300.0 59 LCL022-1 theorem 0.0 2 1 10 0 2 0 2 0 5 10 82 59 1 LCL023-1 theorem 0.0 2 1 14 0 2 0 2 0 5 14 109 86 1 LCL024-1 timeout 300.0 87 LCL025-1 theorem 5.7 6 1 270 0 4 0 4 0 5 270 18828 8241 1 LCL026-1 theorem 24.9 8 1 458 0 4 0 4 0 5 458 45121 24600 1 LCL027-1 theorem 0.0 2 1 32 0 4 0 2 0 4 32 230 109 0 LCL028-1 timeout 300.0 21 LCL029-1 theorem 0.8 3 1 138 0 5 0 0 0 5 138 6542 4151 1 LCL030-1 theorem 49.3 10 1 496 0 5 0 14 0 5 496 59839 35947 1 LCL031-1 theorem 183.1 17 1 838 0 5 0 27 0 5 838 151755 108608 0 LCL032-1 timeout 300.0 41 LCL033-1 theorem 0.0 2 1 14 0 2 0 2 0 5 14 108 61 1 LCL034-1 theorem 21.8 10 1 349 0 2 0 15 0 7 349 50552 19842 1 LCL035-1 theorem 0.0 2 1 8 0 2 0 0 0 5 8 48 34 1 LCL036-1 theorem 5.5 5 1 153 0 2 0 7 0 7 153 9617 3836 1 LCL037-1 timeout 300.0 43 LCL038-1 timeout 300.0 27 LCL039-1 theorem 67.9 15 1 1062 0 6 0 4 0 5 1062 115810 81228 0 LCL040-1 theorem 29.9 10 1 946 0 6 0 14 0 5 946 60040 24049 1 LCL041-1 theorem 0.0 2 1 47 0 6 0 0 0 4 47 427 211 0 LCL042-1 theorem 202.7 21 1 1298 0 6 0 29 0 5 1298 181161 102511 1 LCL043-1 theorem 0.0 2 1 37 0 6 0 0 0 4 37 313 185 0 LCL044-1 theorem 0.2 2 1 11 0 6 0 0 0 5 11 87 66 1 LCL045-1 theorem 180.6 20 1 1197 0 6 0 28 0 5 1197 168394 108059 1 LCL046-1 theorem 0.0 2 1 5 0 4 0 0 0 5 5 12 3 1 LCL047-1 theorem 0.1 2 1 86 0 4 0 2 0 5 86 2048 1275 1 LCL048-1 theorem 0.2 2 1 98 0 4 0 2 0 5 98 2352 1275 1 LCL049-1 theorem 0.5 3 1 139 0 4 0 6 0 5 139 4871 2996 1 LCL050-1 theorem 0.6 3 1 141 0 4 0 6 0 5 141 5038 2996 1 LCL051-1 theorem 0.6 3 1 131 0 4 0 6 0 5 131 4764 3190 1 LCL052-1 theorem 0.6 3 1 134 0 4 0 7 0 5 134 5093 3529 1 LCL053-1 theorem 0.9 3 1 156 0 4 0 9 0 5 156 6485 3979 1 LCL054-1 theorem 154.6 19 1 1170 0 4 0 27 0 5 1170 155100 87174 1 LCL055-1 theorem 1.2 3 1 185 0 4 0 6 0 5 185 6852 3253 1 LCL056-1 theorem 0.6 3 1 136 0 4 0 7 0 5 136 5122 3540 1 LCL057-1 theorem 0.4 2 1 120 0 4 0 7 0 5 120 4607 3653 1 LCL058-1 theorem 54.1 13 1 789 0 4 0 17 0 5 789 89959 62304 1 LCL059-1 theorem 1.1 3 1 164 0 4 0 9 0 5 164 6603 4155 1 LCL060-1 timeout 300.0 24 LCL061-1 timeout 300.0 25 LCL062-1 timeout 300.0 27 LCL063-1 timeout 300.0 24 LCL064-1 theorem 21.1 10 1 716 0 4 0 17 0 5 716 58528 30413 1 LCL064-2 theorem 0.9 3 1 137 0 3 0 2 0 5 137 5086 2936 1 LCL065-1 theorem 0.4 2 1 133 0 4 0 1 0 5 133 4748 3567 1 LCL066-1 theorem 0.6 3 1 146 0 4 0 1 0 5 146 5169 2629 1 LCL067-1 timeout 300.0 28 LCL068-1 theorem 17.3 8 1 612 0 4 0 18 0 5 612 45060 35187 1 LCL069-1 theorem 3.8 6 1 451 0 4 0 6 0 5 451 21025 9982 0 LCL070-1 theorem 31.7 11 1 966 0 4 0 56 0 5 966 68707 32995 1 LCL071-1 theorem 17.9 8 1 621 0 4 0 21 0 5 621 46437 36432 1 LCL072-1 theorem 8.8 8 1 574 0 4 0 13 0 5 574 32921 17163 0 LCL073-1 timeout 300.0 44 LCL074-1 timeout 300.0 43 LCL075-1 theorem 0.0 2 1 34 0 2 0 2 0 6 34 605 328 1 LCL076-1 theorem 0.2 2 1 94 0 4 0 1 0 5 94 3082 2384 1 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 470 0 LCL077-1 theorem 0.3 2 1 109 0 4 0 1 0 5 109 3206 2384 1 LCL077-2 theorem 0.0 2 1 26 0 4 0 1 0 4 26 308 200 1 LCL078-1 timeout 300.0 22 LCL079-1 theorem 0.0 2 1 17 0 6 0 1 0 3 17 76 41 1 LCL080-1 theorem 1.1 3 1 144 0 4 0 1 0 5 144 6520 4187 1 LCL080-2 theorem 1.1 3 1 144 0 5 0 1 0 5 144 6521 4187 1 LCL081-1 theorem 0.0 2 1 37 0 2 0 4 0 5 37 297 173 1 LCL082-1 theorem 0.0 2 1 36 0 2 0 7 0 5 36 353 214 1 LCL083-1 theorem 2.0 3 1 189 0 2 0 68 0 6 189 7274 3543 1 LCL083-2 theorem 1.1 3 1 89 0 3 0 1 0 6 89 2953 1319 1 LCL084-2 timeout 300.0 26 LCL084-3 timeout 300.0 24 LCL085-1 timeout 300.0 23 LCL086-1 theorem 0.0 2 1 28 0 2 0 7 0 6 28 443 306 1 LCL087-1 theorem 0.0 2 1 12 0 2 0 2 0 6 12 109 76 1 LCL088-1 theorem 0.2 2 1 64 0 2 0 9 0 6 64 2130 1533 1 LCL089-1 theorem 0.4 2 1 86 0 2 0 11 0 6 86 2992 1533 1 LCL090-1 theorem 0.1 2 1 42 0 2 0 15 0 6 42 485 337 0 LCL091-1 theorem 0.1 2 1 47 0 2 0 9 0 6 47 791 546 1 LCL092-1 theorem 0.8 3 1 109 0 2 0 12 0 6 109 4568 3248 1 LCL093-1 theorem 64.7 11 1 423 0 2 0 19 0 6 423 63419 38483 1 LCL094-1 theorem 0.6 2 1 78 0 2 0 8 0 6 78 3632 2851 1 LCL095-1 theorem 0.5 3 1 121 0 2 0 14 0 6 121 4145 2159 1 LCL096-1 theorem 10.5 12 1 538 0 4 0 1 0 5 538 127303 127004 0 LCL097-1 theorem 2.4 5 1 278 0 3 0 1 0 5 278 32082 31967 0 LCL098-1 theorem 0.6 2 1 207 0 2 0 0 0 6 207 531 127 0 LCL099-1 timeout 300.0 131 LCL100-1 timeout 300.0 126 LCL101-1 theorem 0.0 2 1 14 0 3 0 1 0 5 14 81 66 0 LCL102-1 theorem 0.5 3 1 139 0 4 0 1 0 5 139 9651 9565 0 LCL103-1 theorem 4.9 9 1 347 0 3 0 0 0 6 347 52313 52202 1 LCL104-1 theorem 0.0 2 1 16 0 3 0 0 0 5 16 94 81 0 LCL105-1 timeout 300.0 170 LCL106-1 theorem 0.0 2 1 22 0 3 0 0 0 6 22 45 10 0 LCL107-1 theorem 0.0 2 1 15 0 2 0 0 0 8 15 114 84 1 LCL108-1 theorem 0.0 2 1 11 0 2 0 0 0 8 11 60 39 1 LCL109-1 timeout 300.0 21 LCL110-1 theorem 0.1 2 1 46 0 5 0 0 0 5 46 1016 681 1 LCL111-1 theorem 0.1 2 1 61 0 5 0 0 0 5 61 1452 803 1 LCL112-1 theorem 0.5 3 1 155 0 5 0 0 0 5 155 6342 4751 1 LCL113-1 theorem 37.3 11 1 800 0 5 0 11 0 5 800 67077 43840 0 LCL114-1 theorem 50.2 12 1 869 0 5 0 24 0 5 869 80481 54338 1 LCL115-1 theorem 0.8 3 1 202 0 5 0 0 0 5 202 8306 4835 1 LCL116-1 theorem 95.0 16 1 1037 0 5 0 14 0 5 1037 123260 100844 1 LCL117-1 theorem 0.0 2 1 4 0 2 0 0 0 5 4 9 3 1 LCL118-1 theorem 0.0 2 1 12 0 2 0 0 0 6 12 81 60 1 LCL119-1 timeout 300.0 90 LCL120-1 theorem 0.1 2 1 40 0 2 0 0 0 6 40 624 560 1 LCL121-1 theorem 5.5 7 1 183 0 2 0 3 0 7 183 20094 19783 1 LCL122-1 theorem 62.8 52 1 894 0 2 0 3 0 7 894 370005 369361 0 LCL123-1 theorem 49.1 15 1 362 0 2 0 3 0 7 362 69980 69178 1 LCL124-1 timeout 300.0 68 LCL125-1 timeout 300.0 148 LCL126-1 theorem 0.0 2 1 6 0 3 0 0 0 5 6 15 8 1 LCL127-1 theorem 3.2 6 1 127 0 2 0 5 0 7 127 10172 9954 1 LCL128-1 theorem 0.2 2 1 48 0 2 0 1 0 7 48 1587 1529 1 LCL129-1 timeout 300.0 108 LCL130-1 timeout 300.0 118 LCL131-1 theorem 0.6 3 1 150 0 2 0 1 0 5 150 10311 10234 0 LCL166-1 timeout 300.0 60 LCL167-1 timeout 300.0 53 LCL168-1 timeout 300.0 96 LCL169-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 7 0 0 LCL170-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 LCL171-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 LCL172-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 LCL173-1 theorem 0.0 2 1 6 0 6 0 0 0 2 6 6 0 0 LCL174-1 theorem 0.4 3 1 807 0 6 0 0 0 5 807 2568 2548 0 LCL175-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 7 0 0 LCL176-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 17 3 1 LCL177-1 theorem 0.0 2 1 11 0 6 0 0 0 4 11 31 16 1 LCL178-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 30 16 1 LCL179-1 timeout 300.0 112 LCL180-1 timeout 300.0 110 LCL181-1 timeout 300.0 102 LCL182-1 theorem 0.4 3 1 636 0 6 0 0 0 5 636 2295 1999 0 LCL183-1 timeout 300.0 75 LCL184-1 timeout 300.0 114 LCL185-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 18 3 1 LCL186-1 theorem 0.0 2 1 19 0 6 0 0 0 4 19 58 44 0 LCL187-1 theorem 0.0 2 1 20 0 6 0 0 0 4 20 64 50 1 LCL188-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 27 16 1 LCL189-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 26 16 0 LCL190-1 theorem 0.0 2 1 7 0 6 0 0 0 4 7 14 5 1 LCL191-1 theorem 23.4 11 1 4435 0 6 0 0 0 6 4435 22814 16399 1 LCL192-1 theorem 0.2 2 1 282 0 6 0 0 0 5 282 1119 947 1 LCL193-1 theorem 0.1 2 1 247 0 6 0 0 0 5 247 974 942 0 LCL194-1 theorem 21.8 11 1 4866 0 6 0 0 0 6 4866 22017 18321 1 LCL195-1 theorem 18.8 11 1 5032 0 6 0 0 0 6 5032 26402 18654 1 LCL196-1 theorem 0.6 3 1 787 0 6 0 0 0 5 787 2704 2218 0 LCL197-1 theorem 0.0 2 1 9 0 6 0 0 0 5 9 37 19 1 LCL198-1 theorem 0.5 3 1 764 0 6 0 0 0 5 764 2618 2218 0 LCL199-1 theorem 0.2 2 1 308 0 6 0 0 0 5 308 1220 1143 1 LCL200-1 theorem 0.0 2 1 13 0 6 0 0 0 5 13 52 35 1 LCL201-1 theorem 10.5 6 1 1516 0 6 0 0 0 6 1516 9378 6189 1 LCL202-1 theorem 8.7 6 1 220 0 6 0 0 0 6 220 1851 1080 1 LCL203-1 theorem 13.8 7 1 210 0 6 0 0 0 6 210 1590 1080 1 LCL204-1 theorem 3.8 6 1 1478 0 6 0 0 0 6 1478 7687 6189 0 LCL205-1 theorem 14.3 7 1 691 0 6 0 0 0 6 691 5382 3145 0 LCL206-1 theorem 5.4 5 1 665 0 6 0 0 0 6 665 4071 3145 0 LCL207-1 theorem 9.5 7 1 529 0 6 0 0 0 6 529 3733 2307 0 LCL208-1 theorem 0.3 3 1 626 0 6 0 0 0 5 626 2142 2001 1 LCL209-1 timeout 300.0 106 LCL210-1 theorem 0.4 3 1 638 0 6 0 0 0 5 638 2205 2011 1 LCL211-1 theorem 0.3 2 1 589 0 6 0 0 0 5 589 2056 1928 1 LCL212-1 theorem 3.6 5 1 1688 0 6 0 0 0 6 1688 8314 7058 0 LCL213-1 theorem 2.5 4 1 1401 0 6 0 0 0 6 1401 6106 6085 0 LCL214-1 theorem 5.9 5 1 1398 0 6 0 0 0 6 1398 6762 5913 1 LCL215-1 theorem 6.0 6 1 1451 0 6 0 0 0 6 1451 7696 6094 1 LCL216-1 theorem 0.3 2 1 584 0 6 0 0 0 5 584 1999 1930 1 LCL217-1 theorem 0.3 2 1 587 0 6 0 0 0 5 587 2012 1997 0 LCL218-1 timeout 300.0 75 LCL219-1 timeout 300.0 108 LCL220-1 timeout 300.0 108 LCL221-1 theorem 38.8 33 1 18689 0 6 0 0 0 6 18689 65074 64905 1 LCL222-1 theorem 43.6 35 1 19631 0 6 0 0 0 6 19631 67543 67371 1 LCL223-1 theorem 39.8 41 1 21633 0 6 0 0 0 6 21633 73813 73711 1 LCL224-1 theorem 18.5 9 1 3424 0 6 0 0 0 6 3424 14060 13891 1 LCL225-1 theorem 18.9 8 1 3424 0 6 0 0 0 6 3424 13993 13891 1 LCL226-1 theorem 0.0 2 1 7 0 6 0 0 0 5 7 16 7 1 LCL227-1 timeout 300.0 113 LCL228-1 timeout 300.0 119 LCL229-1 timeout 300.0 120 LCL230-1 timeout 300.0 73 LCL231-1 timeout 300.0 65 LCL234-1 theorem 6.5 6 1 2607 0 6 0 0 0 6 2607 10879 10847 0 LCL235-1 timeout 300.0 65 LCL236-1 theorem 0.0 2 1 9 0 6 0 0 0 4 9 25 16 0 LCL237-1 theorem 6.4 7 1 2608 0 6 0 0 0 6 2608 10884 10851 1 LCL238-1 theorem 0.1 2 1 298 0 6 0 0 0 5 298 1157 1141 0 LCL239-1 timeout 300.0 121 LCL240-1 timeout 300.0 117 LCL241-1 timeout 300.0 117 LCL242-1 timeout 300.0 65 LCL243-1 timeout 300.0 116 LCL244-1 timeout 300.0 75 LCL245-1 timeout 300.0 73 LCL246-1 timeout 300.0 114 LCL247-1 timeout 300.0 125 LCL248-1 timeout 300.0 74 LCL249-1 timeout 300.0 118 LCL250-1 theorem 8.1 13 1 6335 0 6 0 0 0 6 6335 24523 24484 0 LCL251-1 timeout 300.0 84 LCL252-1 timeout 300.0 104 LCL253-1 timeout 300.0 123 LCL254-1 timeout 300.0 118 LCL255-1 timeout 300.0 90 LCL256-1 theorem 0.3 2 1 110 0 4 0 7 0 5 110 4117 3623 0 LCL257-1 theorem 0.0 2 1 28 0 2 0 2 0 5 28 369 359 1 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 57 0 LCL357-1 theorem 0.0 2 1 20 0 4 0 1 0 5 20 105 57 0 LCL358-1 theorem 0.0 2 1 25 0 4 0 2 0 5 25 136 84 0 LCL359-1 theorem 0.0 2 1 21 0 4 0 1 0 5 21 109 62 1 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 76 0 LCL362-1 theorem 0.0 0 1 31 0 4 0 2 0 5 31 217 146 0 LCL363-1 theorem 0.0 2 1 31 0 4 0 2 0 5 31 220 146 0 LCL364-1 theorem 0.0 2 1 40 0 4 0 2 0 5 40 455 334 1 LCL365-1 theorem 0.1 2 1 70 0 4 0 2 0 5 70 1547 1228 1 LCL366-1 theorem 0.0 2 1 9 0 4 0 0 0 5 9 40 16 1 LCL367-1 theorem 0.1 2 1 78 0 4 0 3 0 5 78 1863 1303 1 LCL368-1 theorem 0.8 2 1 157 0 4 0 6 0 5 157 5688 3150 1 LCL369-1 theorem 0.8 3 1 155 0 4 0 11 0 5 155 6421 4502 0 LCL370-1 theorem 1.0 3 1 169 0 4 0 12 0 5 169 7234 4612 1 LCL371-1 theorem 1.0 3 1 169 0 4 0 12 0 5 169 7234 4612 1 LCL372-1 theorem 3.6 5 1 298 0 4 0 15 0 5 298 17990 10922 1 LCL373-1 theorem 5.6 7 1 352 0 4 0 19 0 5 352 22638 10512 1 LCL374-1 theorem 10.2 8 1 452 0 4 0 17 0 5 452 31319 15676 1 LCL375-1 timeout 300.0 24 LCL376-1 timeout 300.0 24 LCL377-1 timeout 300.0 24 LCL378-1 theorem 1.0 3 1 165 0 4 0 6 0 5 165 6057 3190 1 LCL379-1 theorem 0.5 2 1 124 0 4 0 7 0 5 124 4762 3653 1 LCL380-1 theorem 0.8 3 1 156 0 4 0 7 0 5 156 5716 3458 1 LCL381-1 theorem 1.0 3 1 172 0 4 0 7 0 5 172 6459 3540 1 LCL382-1 theorem 1.3 3 1 196 0 4 0 10 0 5 196 9813 6787 1 LCL383-1 theorem 29.6 11 1 661 0 4 0 13 0 5 661 70075 49639 1 LCL384-1 theorem 0.4 2 1 125 0 4 0 6 0 5 125 4277 2967 1 LCL385-1 theorem 1.2 3 1 182 0 4 0 10 0 5 182 9270 6787 1 LCL386-1 theorem 1.5 3 1 194 0 4 0 13 0 5 194 8600 5049 1 LCL387-1 theorem 5.7 6 1 368 0 4 0 16 0 5 368 22439 12826 1 LCL388-1 theorem 123.9 17 1 1053 0 4 0 21 0 5 1053 143278 91828 1 LCL389-1 theorem 32.0 11 1 662 0 4 0 13 0 5 662 74347 49639 1 LCL390-1 theorem 4.5 6 1 332 0 4 0 17 0 5 332 19832 11707 1 LCL391-1 timeout 300.0 26 LCL392-1 timeout 300.0 24 LCL393-1 timeout 300.0 25 LCL394-1 timeout 300.0 24 LCL395-1 timeout 300.0 24 LCL396-1 theorem 0.8 3 1 151 0 4 0 7 0 5 151 5921 3653 1 LCL397-1 theorem 0.0 2 1 39 0 4 0 2 0 5 39 321 146 1 LCL398-1 theorem 0.0 2 1 6 0 4 0 0 0 5 6 16 3 1 LCL399-1 theorem 0.0 2 1 42 0 4 0 2 0 5 42 539 420 1 LCL400-1 theorem 1.5 3 1 181 0 4 0 9 0 5 181 7344 4058 1 LCL401-1 theorem 2.4 4 1 225 0 4 0 12 0 5 225 11731 6635 1 LCL402-1 theorem 1.8 4 1 206 0 4 0 12 0 5 206 10548 6576 0 LCL403-1 theorem 99.5 16 1 955 0 4 0 18 0 5 955 126640 91828 1 LCL404-1 theorem 25.8 11 1 606 0 4 0 13 0 5 606 65695 49723 0 LCL405-1 theorem 0.6 3 1 160 0 4 0 10 0 5 160 7551 6781 0 LCL411-1 timeout 300.0 117 LCL414-1 theorem 0.0 2 1 6 0 4 0 0 0 3 6 9 1 0 LCL415-1 timeout 300.0 125 LCL416-1 theorem 0.7 3 1 37 0 2 0 0 0 10 37 659 251 1 LCL417-1 timeout 300.0 73 LCL418-1 timeout 300.0 51 LCL419-1 timeout 300.0 35 LCL420-1 timeout 300.0 25 LCL421-1 timeout 300.0 33 LCL422-1 timeout 300.0 35 LCL423-1 timeout 300.0 214 LCL424-1 timeout 300.0 151 LCL425-1 timeout 300.0 51 LCL426-1 timeout 300.0 63 LCL427-1 timeout 300.0 19 LCL428-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 6 0 0 MGT001-1 theorem 0.0 2 1 19 0 10 0 0 0 2 19 30 10 1 MGT002-1 theorem 0.0 2 1 12 0 7 0 0 0 2 12 26 9 1 MGT003-1 theorem 0.0 2 1 12 0 7 0 0 0 2 12 26 9 1 MGT006-1 theorem 0.0 2 1 13 0 9 1 0 0 2 13 23 5 1 MGT008-1 theorem 0.0 2 1 15 0 12 0 0 0 2 15 25 3 1 MGT009-1 theorem 0.0 2 1 15 0 12 0 0 0 2 15 25 3 1 MGT010-1 theorem 0.0 2 1 18 0 14 1 0 0 2 18 28 5 1 MGT015-1 theorem 0.0 2 1 17 0 13 0 0 0 2 17 27 4 1 MGT017-1 theorem 0.0 2 1 17 0 13 0 0 0 2 17 27 4 1 MGT032-2 theorem 0.0 2 1 7 0 2 0 0 0 4 7 11 4 1 MGT036-3 theorem 0.0 2 1 6 0 4 0 0 0 2 6 9 1 1 MSC005-1 theorem 0.0 2 1 15 0 3 0 0 0 4 15 175 169 1 NLP104-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 NLP105-1 non_thm 0.0 2 0 1 0 1 0 0 0 2 0 1 0 0 NLP106-1 non_thm 0.0 2 0 24 0 2 0 0 0 2 0 25 12 0 NLP107-1 non_thm 0.0 2 0 46 0 3 0 0 0 2 0 48 23 0 NLP108-1 non_thm 0.0 2 0 99 0 10 0 0 0 2 0 105 41 0 NLP109-1 non_thm 0.0 2 0 46 0 3 0 0 0 2 0 48 23 0 NLP110-1 non_thm 0.0 2 0 77 0 9 0 0 0 2 0 82 30 0 NLP111-1 non_thm 0.0 2 0 99 0 10 0 0 0 2 0 105 41 0 NLP112-1 non_thm 0.0 2 0 99 0 10 0 0 0 2 0 105 41 0 NLP113-1 non_thm 0.0 2 0 23 0 2 0 0 0 2 0 24 11 0 NUM001-1 theorem 0.0 2 1 26 0 8 0 0 0 3 26 347 326 1 NUM002-1 theorem 0.0 2 1 27 0 8 0 0 0 3 27 356 336 1 NUM003-1 theorem 0.0 2 1 25 0 8 0 0 0 3 25 341 319 1 NUM004-1 theorem 0.0 2 1 27 0 8 0 0 0 3 27 356 336 1 NUM017-1 timeout 300.0 67 NUM019-1 theorem 0.0 2 1 3 0 3 0 0 0 2 3 18 5 0 NUM020-1 theorem 0.0 2 1 9 0 8 0 0 0 3 9 48 26 1 NUM023-1 theorem 0.0 2 1 5 0 5 0 0 0 2 5 20 8 0 NUM024-1 theorem 0.0 2 1 38 0 8 0 1 0 3 38 314 154 0 NUM025-1 theorem 0.0 2 1 4 0 4 0 0 0 2 4 17 4 0 NUM026-1 timeout 300.0 24 NUM283-1.005 theorem 0.4 2 1 155 0 4 0 0 0 25 155 158 110 0 NUM284-1.014 timeout 300.0 3 NUM286-1 timeout 300.0 4 NUM286-2 timeout 300.0 140 NUM287-1 timeout 300.0 15 PLA001-1 theorem 0.0 2 1 23 0 12 0 0 0 2 23 41 2 0 PLA003-1 theorem 0.0 2 1 15 0 5 2 3 0 2 15 34 1 1 PLA004-1 timeout 300.0 37 PLA004-2 timeout 300.0 37 PLA005-1 timeout 300.0 36 PLA005-2 timeout 300.0 36 PLA006-1 theorem 0.0 2 1 21 0 20 0 0 0 2 21 38 11 0 PLA007-1 timeout 300.0 37 PLA008-1 timeout 300.0 37 PLA009-1 timeout 300.0 36 PLA009-2 timeout 300.0 36 PLA010-1 timeout 300.0 37 PLA011-1 timeout 300.0 37 PLA011-2 timeout 300.0 37 PLA012-1 timeout 300.0 36 PLA013-1 timeout 300.0 37 PLA014-1 timeout 300.0 37 PLA014-2 timeout 300.0 37 PLA015-1 timeout 300.0 37 PLA016-1 timeout 300.0 37 PLA017-1 theorem 0.0 2 1 68 0 20 0 0 0 3 68 216 187 1 PLA018-1 timeout 300.0 37 PLA019-1 timeout 300.0 37 PLA020-1 theorem 0.0 2 1 18 0 18 0 0 0 2 18 43 11 0 PLA021-1 timeout 300.0 37 PLA022-1 theorem 4.2 9 1 1066 0 20 0 0 0 4 1066 20905 20850 1 PLA022-2 theorem 4.2 9 1 1066 0 20 0 0 0 4 1066 20905 20850 1 PLA023-1 timeout 300.0 37 PLA029-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 PLA030-1 timeout 300.0 37 PUZ003-1 theorem 0.0 2 1 9 0 6 0 0 0 2 9 18 5 1 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 8 1 PUZ008-3 theorem 0.0 2 1 37 0 4 0 0 0 6 37 69 31 1 PUZ011-1 theorem 0.0 2 1 18 0 18 0 0 0 2 18 55 0 0 PUZ022-1 theorem 0.0 2 1 38 0 31 0 0 0 2 38 64 22 1 PUZ036-1.005 theorem 0.0 2 1 61 0 2 0 0 0 2 61 184 90 1 PUZ037-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 28 18 0 PUZ037-2 theorem 0.0 2 1 6 0 2 0 0 0 2 6 102 63 1 PUZ037-3 theorem 0.9 13 1 173 0 2 0 0 0 2 173 3105 1590 1 PUZ038-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 2 0 0 PUZ039-1 timeout 300.0 185 PUZ040-1 timeout 300.0 195 PUZ041-1 timeout 300.0 213 PUZ042-1 timeout 300.0 196 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 1 1 PUZ048-1 timeout 300.0 189 PUZ049-1 timeout 300.0 210 PUZ050-1 timeout 300.0 287 PUZ051-1 timeout 300.0 207 RNG001-2 theorem 1.3 3 1 64 0 7 0 0 0 2 64 16590 16394 1 RNG001-3 theorem 0.0 2 1 9 0 4 0 0 0 2 9 93 77 1 RNG001-5 theorem 0.9 3 1 57 0 8 0 0 0 2 57 12262 11915 1 RNG004-3 timeout 300.0 405 RNG005-2 theorem 0.0 2 1 11 0 11 0 0 0 2 11 585 537 0 RNG006-2 theorem 0.0 0 1 14 0 13 0 0 0 2 14 695 662 1 RNG037-2 theorem 0.0 2 1 10 0 9 0 0 0 2 10 310 282 1 RNG038-2 theorem 0.0 2 1 11 0 9 0 0 0 2 11 321 295 1 RNG039-2 theorem 2.1 6 1 64 0 50 0 6 0 2 64 31718 31589 1 ROB025-1 timeout 300.0 176 SWV010-1 non_thm 0.0 2 0 8 0 5 0 0 0 6 0 8 3 0 SWV011-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 2 0 0 SWV012-1 timeout 300.0 381 SWV013-1 timeout 300.0 381 SWV014-1 timeout 300.0 379 SWV015-1 timeout 300.0 378 SWV016-1 timeout 300.0 321 SWV017-1 timeout 300.0 2 SWV018-1 timeout 300.0 10 SYN003-1.006 theorem 0.0 4 1 18 0 18 18 0 0 2 18 26 16 1 SYN004-1.007 theorem 0.0 4 1 14 0 14 14 0 0 2 14 17 12 1 SYN005-1.010 theorem 0.0 4 1 10 0 10 0 0 0 2 10 20 0 0 SYN010-1.005.005 theorem 0.0 4 1 26 0 26 26 0 0 2 26 32 20 1 SYN033-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 5 1 0 SYN035-1 theorem 0.0 4 1 2 0 2 6 0 0 2 2 6 1 0 SYN040-1 theorem 0.0 4 1 2 0 4 2 0 0 2 2 4 1 0 SYN041-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 4 0 0 SYN046-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 4 0 0 SYN048-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 0 SYN049-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 4 0 0 SYN050-1 theorem 0.0 4 1 3 0 3 1 0 0 2 3 7 1 0 SYN057-1 theorem 0.0 4 1 7 0 4 0 0 0 2 7 12 3 1 SYN058-1 theorem 0.0 4 1 5 0 6 1 0 0 2 5 8 2 1 SYN062-1 theorem 0.0 4 1 5 0 3 0 0 0 2 5 8 2 1 SYN063-2 theorem 0.0 4 1 2 0 2 2 0 0 2 2 4 0 0 SYN064-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 0 SYN065-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 6 0 0 SYN068-1 theorem 0.0 4 1 5 0 1 0 0 0 2 5 9 6 1 SYN079-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 6 0 0 SYN085-1.010 theorem 0.0 4 1 11 0 11 11 0 0 2 11 22 1 0 SYN086-1.003 non_thm 0.0 4 0 1 0 1 1 0 0 2 0 1 0 0 SYN087-1.003 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 0 SYN088-1.010 theorem 0.0 4 1 21 0 21 0 0 0 2 21 1055 1024 0 SYN089-1.002 theorem 0.0 4 1 5 0 10 5 0 0 2 5 11 4 0 SYN090-1.008 theorem 0.0 4 1 34 0 36 58 0 0 2 34 65 58 1 SYN095-1.002 theorem 0.0 4 1 4 0 5 1 0 0 2 4 10 1 0 SYN096-1.008 theorem 0.0 4 1 34 0 4 0 0 0 2 34 67 60 1 SYN101-1.002.002 theorem 0.0 4 1 10 0 5 0 0 0 2 10 24 16 1 SYN102-1.007.007 theorem 0.9 5 1 3727 0 15 1 0 0 2 3727 7185 7168 1 SYN103-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN104-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN105-1 theorem 0.0 4 1 22 0 29 31 0 0 2 22 209 168 0 SYN106-1 theorem 0.0 4 1 17 0 24 30 0 0 2 17 167 126 0 SYN107-1 theorem 0.0 4 1 34 0 41 36 0 0 2 34 327 285 1 SYN108-1 theorem 0.0 4 1 34 0 41 35 0 0 2 34 327 285 1 SYN109-1 theorem 0.0 4 1 58 0 91 87 0 0 2 58 475 433 1 SYN110-1 theorem 0.0 2 1 55 0 92 85 0 0 2 55 457 412 1 SYN111-1 theorem 0.0 4 1 59 0 91 88 0 0 2 59 490 444 1 SYN112-1 theorem 0.0 4 1 34 0 40 36 0 0 2 34 328 285 1 SYN113-1 theorem 0.0 4 1 56 0 90 85 0 0 2 56 463 419 1 SYN114-1 theorem 0.0 4 1 35 0 47 36 0 0 2 35 357 310 1 SYN115-1 theorem 0.1 4 1 184 0 112 149 3 0 2 184 1580 1529 1 SYN116-1 theorem 0.0 4 1 53 0 108 86 0 0 2 53 465 405 1 SYN117-1 theorem 0.0 4 1 53 0 107 85 0 0 2 53 464 405 1 SYN118-1 theorem 0.0 2 1 1 0 1 0 0 0 2 1 39 0 0 SYN119-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN120-1 theorem 0.0 4 1 17 0 24 30 0 0 2 17 168 125 0 SYN121-1 theorem 0.0 4 1 70 0 94 101 1 0 2 70 551 503 1 SYN122-1 theorem 0.0 4 1 69 0 92 92 0 0 2 69 531 484 1 SYN123-1 theorem 0.0 4 1 34 0 39 35 0 0 2 34 328 285 1 SYN124-1 theorem 0.0 4 1 37 0 56 47 0 0 2 37 369 327 1 SYN125-1 theorem 0.1 4 1 237 0 122 156 6 0 2 237 1967 1925 1 SYN126-1 theorem 0.0 4 1 40 0 62 60 0 0 2 40 393 352 1 SYN127-1 theorem 0.0 4 1 40 0 62 60 0 0 2 40 394 352 1 SYN128-1 theorem 0.0 4 1 52 0 87 83 0 0 2 52 446 405 1 SYN129-1 theorem 0.0 4 1 52 0 87 83 0 0 2 52 446 405 1 SYN130-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN131-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN132-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 96 0 SYN133-1 theorem 0.0 4 1 5 0 4 9 0 0 2 5 52 13 0 SYN134-1 theorem 0.0 4 1 34 0 58 36 0 0 2 34 343 285 1 SYN135-1 theorem 0.0 4 1 35 0 48 36 0 0 2 35 350 308 1 SYN136-1 theorem 0.0 4 1 35 0 47 36 0 0 2 35 350 308 1 SYN137-1 theorem 0.0 4 1 83 0 100 121 1 0 2 83 654 608 1 SYN138-1 theorem 0.1 4 1 182 0 113 147 3 0 2 182 1571 1518 1 SYN139-1 theorem 0.1 4 1 195 0 119 150 4 0 2 195 1639 1586 1 SYN140-1 theorem 0.1 4 1 195 0 119 150 4 0 2 195 1640 1586 1 SYN141-1 theorem 0.1 4 1 186 0 113 149 3 0 2 186 1592 1529 1 SYN142-1 theorem 0.1 4 1 232 0 124 154 4 0 2 232 1924 1848 1 SYN143-1 theorem 0.1 4 1 232 0 124 154 4 0 2 232 1924 1848 1 SYN144-1 theorem 0.0 4 1 139 0 104 137 1 0 2 139 980 930 1 SYN145-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN146-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 50 4 0 SYN147-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 68 20 0 SYN148-1 theorem 0.0 4 1 119 0 102 134 1 0 2 119 812 769 1 SYN149-1 theorem 0.0 4 1 12 0 20 30 0 0 2 12 140 96 0 SYN150-1 theorem 0.0 4 1 34 0 42 38 0 0 2 34 334 285 1 SYN151-1 theorem 0.0 4 1 34 0 39 35 0 0 2 34 331 285 1 SYN152-1 theorem 0.0 4 1 34 0 42 37 0 0 2 34 327 285 1 SYN153-1 theorem 0.0 4 1 35 0 48 36 0 0 2 35 350 309 1 SYN154-1 theorem 0.0 4 1 35 0 48 36 0 0 2 35 350 309 1 SYN155-1 theorem 0.0 4 1 99 0 105 132 1 0 2 99 754 709 1 SYN156-1 theorem 0.1 4 1 190 0 116 148 3 0 2 190 1620 1575 1 SYN157-1 theorem 0.0 4 1 46 0 81 73 0 0 2 46 441 395 1 SYN158-1 theorem 0.0 4 1 46 0 81 72 0 0 2 46 439 395 1 SYN159-1 theorem 0.1 4 1 174 0 113 150 3 0 2 174 1381 1316 1 SYN160-1 theorem 0.0 4 1 46 0 81 72 0 0 2 46 439 395 1 SYN161-1 theorem 0.0 4 1 46 0 81 72 0 0 2 46 439 395 1 SYN162-1 theorem 0.0 4 1 46 0 81 72 0 0 2 46 439 395 1 SYN163-1 theorem 0.1 4 1 174 0 113 151 3 0 2 174 1378 1316 1 SYN164-1 theorem 0.0 4 1 7 0 10 16 0 0 2 7 78 39 0 SYN165-1 theorem 0.0 4 1 5 0 6 10 0 0 2 5 56 8 0 SYN166-1 theorem 0.1 4 1 141 0 105 137 2 0 2 141 1042 995 1 SYN167-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 140 96 0 SYN168-1 theorem 0.0 4 1 37 0 60 52 0 0 2 37 374 327 1 SYN169-1 theorem 0.0 4 1 35 0 44 36 0 0 2 35 350 307 1 SYN170-1 theorem 0.0 4 1 40 0 66 61 0 0 2 40 394 351 1 SYN171-1 theorem 0.1 4 1 178 0 112 147 3 0 2 178 1494 1444 1 SYN172-1 theorem 0.0 4 1 6 0 7 12 0 0 2 6 71 32 0 SYN173-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 272 231 0 SYN174-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 272 231 0 SYN175-1 theorem 0.0 4 1 34 0 46 38 0 0 2 34 332 285 1 SYN176-1 theorem 0.0 4 1 69 0 92 92 0 0 2 69 535 484 1 SYN177-1 theorem 0.0 4 1 37 0 57 47 0 0 2 37 378 327 1 SYN178-1 theorem 0.0 4 1 43 0 70 66 0 0 2 43 431 385 1 SYN179-1 theorem 0.0 4 1 83 0 100 121 1 0 2 83 666 608 1 SYN180-1 theorem 0.0 4 1 46 0 79 71 0 0 2 46 448 394 1 SYN181-1 theorem 0.0 4 1 46 0 79 71 0 0 2 46 439 394 1 SYN182-1 theorem 0.0 4 1 46 0 81 72 0 0 2 46 437 394 1 SYN183-1 theorem 0.0 4 1 46 0 81 72 0 0 2 46 437 394 1 SYN184-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN185-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN186-1 theorem 0.0 4 1 34 0 40 35 0 0 2 34 332 285 1 SYN187-1 theorem 0.0 4 1 34 0 40 35 0 0 2 34 333 285 1 SYN188-1 theorem 0.0 4 1 34 0 41 36 0 0 2 34 327 285 1 SYN189-1 theorem 0.0 4 1 38 0 61 52 0 0 2 38 380 338 1 SYN190-1 theorem 0.0 4 1 83 0 100 121 1 0 2 83 658 614 1 SYN191-1 theorem 0.0 4 1 130 0 103 134 1 0 2 130 911 867 1 SYN192-1 theorem 0.0 4 1 47 0 85 79 0 0 2 47 444 395 1 SYN193-1 theorem 0.0 4 1 47 0 84 79 0 0 2 47 445 395 1 SYN194-1 theorem 0.1 4 1 97 0 104 129 1 0 2 97 729 669 1 SYN195-1 theorem 0.0 4 1 60 0 90 89 0 0 2 60 494 450 1 SYN196-1 theorem 0.0 4 1 34 0 40 36 0 0 2 34 338 289 1 SYN197-1 theorem 0.0 4 1 8 0 15 20 0 0 2 8 82 40 0 SYN198-1 theorem 0.0 4 1 34 0 46 36 1 0 2 34 327 285 1 SYN199-1 theorem 0.0 4 1 34 0 40 36 0 0 2 34 339 289 1 SYN200-1 theorem 0.0 4 1 34 0 46 36 1 0 2 34 327 285 1 SYN201-1 theorem 0.0 4 1 43 0 71 66 0 0 2 43 429 385 1 SYN202-1 theorem 0.0 4 1 69 0 93 92 0 0 2 69 528 484 1 SYN203-1 theorem 0.0 4 1 50 0 89 81 0 0 2 50 446 399 1 SYN204-1 theorem 0.1 4 1 150 0 108 138 3 0 2 150 1176 1132 1 SYN205-1 theorem 0.1 4 1 150 0 108 138 3 0 2 150 1176 1132 1 SYN206-1 theorem 0.0 4 1 69 0 92 92 0 0 2 69 529 484 1 SYN207-1 theorem 0.0 4 1 85 0 101 121 1 0 2 85 653 609 1 SYN208-1 theorem 0.0 4 1 70 0 94 102 1 0 2 70 547 503 1 SYN209-1 theorem 0.0 4 1 48 0 83 78 0 0 2 48 447 397 1 SYN210-1 theorem 0.0 4 1 48 0 83 78 0 0 2 48 442 397 1 SYN211-1 theorem 0.0 4 1 48 0 82 78 0 0 2 48 443 397 1 SYN212-1 theorem 0.0 4 1 48 0 84 78 0 0 2 48 446 397 1 SYN213-1 theorem 0.0 4 1 55 0 97 86 0 0 2 55 456 405 1 SYN214-1 theorem 0.0 4 1 55 0 97 86 0 0 2 55 456 405 1 SYN215-1 theorem 0.0 4 1 55 0 97 86 0 0 2 55 456 405 1 SYN216-1 theorem 0.0 4 1 34 0 40 36 0 0 2 34 336 285 1 SYN217-1 theorem 0.0 4 1 34 0 39 35 0 0 2 34 331 285 1 SYN218-1 theorem 0.0 4 1 34 0 41 37 0 0 2 34 333 285 1 SYN219-1 theorem 0.0 4 1 70 0 94 101 1 0 2 70 551 503 1 SYN220-1 theorem 0.0 4 1 35 0 47 36 0 0 2 35 358 313 1 SYN221-1 theorem 0.0 4 1 37 0 56 49 0 0 2 37 372 327 1 SYN222-1 theorem 0.0 4 1 37 0 56 48 0 0 2 37 372 327 1 SYN223-1 theorem 0.0 4 1 35 0 48 36 0 0 2 35 359 314 1 SYN224-1 theorem 0.0 4 1 37 0 56 47 0 0 2 37 369 327 1 SYN225-1 theorem 0.0 4 1 63 0 93 90 0 0 2 63 517 474 1 SYN226-1 theorem 0.0 4 1 35 0 47 36 0 0 2 35 358 313 1 SYN227-1 theorem 0.1 4 1 235 0 122 155 6 0 2 235 1939 1897 1 SYN228-1 theorem 0.1 4 1 128 0 104 134 1 0 2 128 884 841 1 SYN229-1 theorem 0.0 4 1 37 0 56 48 0 0 2 37 370 327 1 SYN230-1 theorem 0.0 4 1 37 0 56 48 0 0 2 37 370 327 1 SYN231-1 theorem 0.0 2 1 37 0 56 49 0 0 2 37 370 327 1 SYN232-1 theorem 0.0 4 1 37 0 56 48 0 0 2 37 370 327 1 SYN233-1 theorem 0.0 4 1 35 0 47 36 0 0 2 35 358 314 1 SYN234-1 theorem 0.0 2 1 63 0 92 90 0 0 2 63 517 474 1 SYN235-1 theorem 0.0 4 1 130 0 103 134 1 0 2 130 934 891 1 SYN236-1 theorem 0.0 4 1 35 0 47 36 0 0 2 35 358 313 1 SYN237-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 80 26 0 SYN238-1 theorem 0.0 4 1 4 0 4 6 0 0 2 4 53 3 0 SYN239-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 53 5 0 SYN240-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 138 96 0 SYN241-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 138 96 0 SYN242-1 theorem 0.0 4 1 27 0 33 35 0 0 2 27 272 231 0 SYN243-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 273 231 0 SYN244-1 theorem 0.0 4 1 4 0 4 9 0 0 2 4 53 5 0 SYN245-1 theorem 0.0 4 1 12 0 18 31 0 0 2 12 138 96 0 SYN246-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 274 231 0 SYN247-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 78 26 0 SYN248-1 theorem 0.0 4 1 55 0 91 84 0 0 2 55 456 412 1 SYN249-1 theorem 0.0 4 1 55 0 92 84 0 0 2 55 456 412 1 SYN250-1 theorem 0.1 4 1 263 0 123 161 7 0 2 263 2106 2046 1 SYN251-1 theorem 0.0 4 1 30 0 36 34 0 0 2 30 301 257 0 SYN252-1 theorem 0.0 4 1 151 0 109 138 3 0 2 151 1182 1132 1 SYN253-1 theorem 0.1 4 1 195 0 120 150 4 0 2 195 1640 1586 1 SYN254-1 theorem 0.1 4 1 195 0 119 150 4 0 2 195 1638 1586 1 SYN255-1 theorem 0.0 2 1 34 0 41 38 0 0 2 34 329 285 1 SYN256-1 theorem 0.0 4 1 34 0 39 37 0 0 2 34 335 285 1 SYN257-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 96 0 SYN258-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 89 37 0 SYN259-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 89 37 0 SYN260-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 140 96 0 SYN261-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 141 96 0 SYN262-1 theorem 0.0 4 1 34 0 39 35 0 0 2 34 331 287 1 SYN263-1 theorem 0.0 4 1 37 0 57 47 0 0 2 37 373 328 1 SYN264-1 theorem 0.0 4 1 34 0 39 35 0 0 2 34 333 287 1 SYN265-1 theorem 0.0 4 1 37 0 60 51 0 0 2 37 370 327 1 SYN266-1 theorem 0.0 4 1 131 0 104 134 1 0 2 131 890 844 1 SYN267-1 theorem 0.0 4 1 40 0 67 60 0 0 2 40 396 351 1 SYN268-1 theorem 0.0 4 1 40 0 66 60 0 0 2 40 394 351 1 SYN269-1 theorem 0.1 4 1 178 0 112 147 3 0 2 178 1494 1444 1 SYN270-1 theorem 0.1 4 1 156 0 108 139 3 0 2 156 1256 1214 1 SYN271-1 theorem 0.1 4 1 178 0 112 147 3 0 2 178 1494 1444 1 SYN272-1 theorem 0.0 4 1 77 0 99 114 1 0 2 77 606 564 1 SYN273-1 theorem 0.0 4 1 88 0 100 126 1 0 2 88 706 665 1 SYN274-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN275-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 0 SYN276-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 96 0 SYN277-1 theorem 0.0 4 1 6 0 10 11 0 0 2 6 69 13 0 SYN278-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 63 6 0 SYN279-1 theorem 0.0 4 1 13 0 19 29 0 0 2 13 142 96 0 SYN280-1 theorem 0.0 2 1 4 0 4 10 0 0 2 4 65 7 0 SYN281-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 137 96 0 SYN282-1 theorem 0.0 4 1 6 0 9 12 0 0 2 6 73 13 0 SYN283-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 276 231 0 SYN284-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 274 231 0 SYN285-1 theorem 0.0 4 1 34 0 39 35 0 0 2 34 331 285 1 SYN286-1 theorem 0.0 4 1 17 0 23 30 0 0 2 17 167 120 0 SYN287-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 64 7 0 SYN288-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 272 231 0 SYN289-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 276 231 0 SYN290-1 theorem 0.0 4 1 6 0 10 10 0 0 2 6 69 13 0 SYN291-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 69 13 0 SYN292-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 272 231 0 SYN293-1 theorem 0.0 2 1 34 0 39 36 0 0 2 34 334 288 1 SYN294-1 theorem 0.0 4 1 34 0 39 37 0 0 2 34 335 288 1 SYN295-1 theorem 0.0 4 1 27 0 34 35 0 0 2 27 272 231 0 SYN296-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 276 231 0 SYN297-1 theorem 0.0 4 1 27 0 34 34 0 0 2 27 272 231 0 SYN298-1 theorem 0.0 4 1 69 0 92 92 0 0 2 69 538 484 1 SYN299-1 theorem 0.0 4 1 69 0 92 92 0 0 2 69 533 484 1 SYN300-1 theorem 0.0 4 1 69 0 92 92 0 0 2 69 529 484 1 SYN301-1 theorem 0.0 4 1 48 0 82 78 0 0 2 48 444 397 1 SYN302-1.003 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 0 SYN303-1 timeout 300.0 4 SYN310-1 theorem 0.2 4 1 1101 0 2 0 0 0 3 1101 3584 5 1 SYN311-1 theorem 4.5 15 1 13067 0 2 0 0 0 3 13067 40552 40544 1 SYN312-1 theorem 13.2 9 1 2818 0 3 0 0 0 3 2818 47015 47008 1 SYN318-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 6 1 0 SYN322-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 0 SYN329-1 non_thm 0.0 2 0 3 0 4 0 0 0 2 0 4 0 0 SYN333-1 theorem 0.0 4 1 2 0 2 6 0 0 2 2 6 1 0 SYN336-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 5 0 0 SYN337-1 non_thm 0.0 4 0 4 0 5 0 0 0 2 0 5 0 0 SYN338-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 3 0 0 SYN339-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 0 SYN340-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 0 SYN341-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 0 SYN342-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 0 2 0 0 SYN346-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 4 0 0 SYN553-1 theorem 0.0 4 1 14 0 7 0 0 0 3 14 103 85 0 SYN555-1 theorem 0.0 4 1 9 0 6 0 0 0 2 9 28 15 0 SYN556-1 timeout 300.0 14 SYN557-1 theorem 21.7 18 1 560 0 7 0 0 0 4 560 120412 119751 1 SYN558-1 theorem 0.0 4 1 32 0 6 0 2 0 2 32 108 21 1 SYN559-1 theorem 0.0 4 1 10 0 6 0 0 0 3 10 114 103 1 SYN561-1 theorem 0.2 4 1 14 0 6 0 0 0 4 14 307 296 1 SYN562-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 31 14 0 SYN563-1 theorem 0.0 4 1 58 0 6 0 0 0 3 58 404 127 1 SYN564-1 theorem 0.0 4 1 30 0 7 0 0 0 4 30 299 276 1 SYN565-1 theorem 0.0 4 1 30 0 7 0 0 0 4 30 299 276 1 SYN566-1 theorem 0.0 4 1 19 0 8 0 0 0 3 19 69 30 1 SYN569-1 theorem 0.0 4 1 35 0 7 0 0 0 3 35 176 166 1 SYN570-1 theorem 0.0 4 1 14 0 10 0 0 0 3 14 45 26 1 SYN572-1 theorem 0.8 4 1 141 0 9 0 0 0 5 141 4216 4070 1 SYN577-1 theorem 0.1 4 1 80 0 12 0 0 0 3 80 905 887 1 SYN584-1 theorem 0.0 4 1 10 0 9 0 0 0 8 10 34 19 1 SYN588-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 30 15 0 SYN589-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 30 15 0 SYN590-1 theorem 0.0 4 1 144 0 8 0 0 0 4 144 786 188 1 SYN596-1 theorem 0.0 4 1 12 0 11 0 0 0 5 12 37 21 1 SYN597-1 theorem 0.5 5 1 214 0 11 0 0 0 4 214 5232 5220 0 SYN598-1 timeout 300.0 38 SYN599-1 timeout 300.0 38 SYN600-1 timeout 300.0 202 SYN601-1 theorem 0.6 5 1 241 0 12 0 0 0 4 241 5656 5643 0 SYN602-1 theorem 0.2 4 1 89 0 7 0 0 0 3 89 620 606 1 SYN603-1 theorem 27.8 27 1 863 0 7 0 0 0 4 863 81397 81380 1 SYN614-1 timeout 300.0 212 SYN615-1 timeout 300.0 248 SYN616-1 theorem 0.7 4 1 156 0 13 0 0 0 3 156 5731 5712 0 SYN617-1 timeout 300.0 73 SYN618-1 theorem 0.0 4 1 28 0 16 0 0 0 3 28 114 79 1 SYN628-1 theorem 0.4 5 1 111 0 15 0 0 0 3 111 3904 3888 0 SYN629-1 theorem 0.4 5 1 111 0 15 0 0 0 3 111 3904 3888 0 SYN631-1 timeout 300.0 92 SYN632-1 theorem 0.0 4 1 26 0 12 0 0 0 7 26 76 34 1 SYN637-1 theorem 0.0 4 1 24 0 14 0 0 0 7 24 108 67 1 SYN638-1 theorem 0.0 4 1 24 0 14 0 0 0 7 24 108 67 1 SYN639-1 timeout 300.0 92 SYN640-1 timeout 300.0 92 SYN646-1 timeout 300.0 95 SYN647-1 timeout 300.0 94 SYN649-1 timeout 300.0 85 SYN651-1 theorem 0.0 4 1 23 0 15 0 0 0 6 23 73 49 1 SYN652-1 theorem 0.0 4 1 26 0 20 0 0 0 3 26 86 56 1 SYN653-1 timeout 300.0 4 SYN654-1 timeout 300.0 4 SYN655-1 timeout 300.0 4 SYN688-1 theorem 0.0 4 1 40 0 28 0 0 0 3 40 95 52 1 SYN689-1 theorem 0.0 4 1 40 0 28 0 0 0 3 40 95 52 1 SYN691-1 theorem 0.0 4 1 33 0 24 0 1 0 8 33 96 43 1 SYN702-1 theorem 0.0 4 1 31 0 28 0 0 0 9 31 90 51 1 SYN703-1 theorem 0.0 4 1 37 0 29 0 1 0 9 37 114 51 1 SYN704-1 timeout 300.0 110 SYN705-1 theorem 0.0 4 1 37 0 29 0 1 0 9 37 114 51 1 SYN706-1 theorem 0.0 4 1 41 0 31 0 0 0 6 41 130 87 1 SYN707-1 timeout 300.0 24 SYN708-1 timeout 300.0 24 SYN709-1 theorem 0.0 4 1 41 0 35 0 0 0 4 41 113 71 1 SYN711-1 timeout 300.0 31 SYN712-1 theorem 0.0 4 1 42 0 36 0 1 0 10 42 127 66 1 SYN715-1 theorem 0.1 4 1 40 0 36 0 0 0 10 40 117 72 1 SYN716-1 theorem 0.1 4 1 41 0 36 0 0 0 10 41 122 66 1 SYN719-1 theorem 0.0 4 1 49 0 46 0 0 0 3 49 133 78 0 SYN720-1 non_thm 0.1 3 0 423 0 132 171 6 0 2 0 3108 3070 0 SYN721-1 theorem 0.0 4 1 3 0 1 0 0 0 2 3 5 2 1 SYN727-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 4 0 0 SYN729-1 theorem 0.0 4 1 34 0 1 0 0 0 4 34 71 40 1 SYN731-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 0