-------------------------------------------------------------------------------- Execute format string : ./darwin --horn-candidates Ignore Problems list file : hne_ignore-problems Output file : hne_ignore-output Summary file : hne_ignore-summary Time limit : 300 s Memory limit : 400 MB -------------------------------------------------------------------------------- Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. ANA003-2 timeout 299.0 49 ANA004-2 timeout 299.0 51 ANA005-2 timeout 299.0 50 COM001-1 theorem 0.0 4 1 10 0 7 0 0 0 2 10 13 0 COM002-1 theorem 0.0 4 1 30 0 15 0 0 0 2 30 56 0 GEO001-4 timeout 298.9 51 GEO002-4 theorem 0.0 4 1 15 0 3 0 5 0 2 15 46 0 GEO079-1 theorem 0.0 4 1 3 0 2 0 0 0 2 3 4 0 GRP001-5 theorem 0.0 4 1 8 0 5 0 0 0 2 8 94 0 GRP003-1 theorem 0.0 4 1 5 0 3 0 0 0 3 5 36 0 GRP003-2 theorem 0.1 4 1 11 0 4 0 0 0 3 11 282 0 GRP004-1 theorem 0.0 4 1 5 0 3 0 0 0 3 5 36 0 GRP004-2 theorem 0.1 4 1 10 0 4 0 0 0 3 10 157 0 GRP005-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 69 0 GRP006-1 theorem 0.0 4 1 7 0 6 0 0 0 2 7 72 0 GRP028-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 4 0 GRP028-3 theorem 0.0 4 1 4 0 4 0 0 0 2 4 8 0 GRP028-4 theorem 0.0 4 1 3 0 3 0 0 0 2 3 5 0 GRP029-2 theorem 0.2 4 1 11 0 5 0 0 0 3 11 339 0 GRP031-2 theorem 0.1 4 1 10 0 4 0 0 0 3 10 173 0 GRP033-3 theorem 0.0 4 1 8 0 7 0 0 0 2 8 149 0 GRP034-4 theorem 0.0 4 1 7 0 6 0 0 0 2 7 74 0 GRP041-2 theorem 0.0 4 1 3 0 3 0 0 0 2 3 18 0 GRP042-2 theorem 0.0 4 1 15 0 5 0 0 0 2 15 341 0 GRP043-2 theorem 0.0 4 1 24 0 6 0 0 0 2 24 883 0 GRP044-2 theorem 0.0 4 1 16 0 6 0 0 0 2 16 341 0 GRP045-2 theorem 0.0 4 1 24 0 6 0 0 0 2 24 929 0 GRP046-2 theorem 0.0 4 1 20 0 5 0 0 0 2 20 658 0 GRP047-2 theorem 0.0 4 1 18 0 5 0 0 0 2 18 500 0 GRP048-2 theorem 13.2 17 1 169 0 5 0 0 0 3 169 186334 0 GRP394-2 timeout 299.0 144 KRS004-1 theorem 0.0 4 1 2 0 1 0 0 0 2 2 2 0 LAT005-1 theorem 0.4 4 1 150 0 17 0 0 0 2 150 7301 0 LAT005-2 theorem 0.3 4 1 146 0 21 0 0 0 2 146 5862 0 LCL001-1 timeout 299.0 24 LCL002-1 theorem 72.7 13 1 2482 0 2 0 411 0 8 2482 1812116 0 LCL003-1 theorem 69.9 13 1 2442 0 2 0 406 0 8 2442 1771827 0 LCL004-1 theorem 1.7 7 1 305 0 2 0 197 0 8 305 28445 0 LCL005-1 timeout 299.0 41 LCL006-1 theorem 0.8 4 1 248 0 3 0 0 0 5 248 16687 0 LCL007-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 3 0 LCL008-1 theorem 0.0 4 1 8 0 2 0 1 0 5 8 38 0 LCL009-1 theorem 0.5 4 1 184 0 2 0 2 0 5 184 10838 0 LCL010-1 theorem 0.0 4 1 33 0 2 0 0 0 5 33 591 0 LCL011-1 theorem 0.0 4 1 47 0 2 0 0 0 5 47 983 0 LCL012-1 theorem 8.3 12 1 477 0 2 0 0 0 7 477 95045 0 LCL013-1 theorem 0.0 4 1 3 0 2 0 0 0 8 3 5 0 LCL014-1 theorem 3.9 8 1 340 0 2 0 1 0 7 340 51187 0 LCL015-1 theorem 21.5 23 1 617 0 2 0 0 0 8 617 190649 0 LCL016-1 theorem 22.4 23 1 692 0 2 0 0 0 8 692 223976 0 LCL017-1 theorem 26.3 35 1 627 0 2 0 0 0 9 627 220982 0 LCL018-1 theorem 16.6 22 1 530 0 2 0 0 0 9 530 159506 0 LCL019-1 theorem 239.4 110 1 1880 0 2 0 0 0 8 1880 1503600 0 LCL020-1 timeout 299.0 84 LCL021-1 theorem 101.0 78 1 1166 0 2 0 0 0 10 1166 719458 0 LCL022-1 theorem 0.0 4 1 44 0 2 0 2 0 5 44 845 0 LCL023-1 theorem 0.2 4 1 115 0 2 0 2 0 5 115 4499 0 LCL024-1 theorem 164.8 76 1 1628 0 2 0 0 0 8 1628 1096804 0 LCL025-1 theorem 0.8 4 1 257 0 4 0 3 0 5 257 24981 0 LCL026-1 theorem 1.0 4 1 282 0 4 0 3 0 5 282 29757 0 LCL027-1 theorem 0.1 4 1 64 0 4 0 2 0 5 64 2211 0 LCL028-1 theorem 8.2 6 1 740 0 4 0 66 0 5 740 154737 0 LCL029-1 theorem 0.2 4 1 120 0 5 0 1 0 5 120 7237 0 LCL030-1 theorem 1.5 4 1 323 0 5 0 9 0 5 323 38604 0 LCL031-1 theorem 5.7 5 1 590 0 5 0 23 0 5 590 108633 0 LCL032-1 timeout 299.0 40 LCL033-1 theorem 0.0 4 1 11 0 2 0 2 0 5 11 71 0 LCL034-1 theorem 0.5 4 1 182 0 2 0 9 0 7 182 20408 0 LCL035-1 theorem 0.0 4 1 8 0 2 0 0 0 5 8 43 0 LCL036-1 theorem 0.1 4 1 74 0 2 0 5 0 7 74 3977 0 LCL037-1 timeout 299.0 41 LCL038-1 theorem 133.2 22 1 2051 0 2 0 134 0 7 2051 2232852 0 LCL039-1 theorem 2.3 4 1 684 0 6 0 4 0 5 684 81313 0 LCL040-1 theorem 1.6 4 1 481 0 6 0 51 0 5 481 40195 0 LCL041-1 theorem 0.0 4 1 26 0 6 0 0 0 4 26 223 0 LCL042-1 theorem 4.6 5 1 719 0 6 0 16 0 5 719 103348 0 LCL043-1 theorem 0.0 4 1 23 0 6 0 0 0 4 23 199 0 LCL044-1 theorem 0.1 4 1 74 0 6 0 0 0 5 74 2097 0 LCL045-1 theorem 4.9 5 1 742 0 6 0 16 0 5 742 108312 0 LCL046-1 theorem 0.0 4 1 5 0 4 0 0 0 5 5 9 0 LCL047-1 theorem 0.0 4 1 56 0 4 0 4 0 5 56 1319 0 LCL048-1 theorem 0.1 4 1 55 0 4 0 3 0 5 55 1285 0 LCL049-1 theorem 0.1 4 1 88 0 4 0 6 0 5 88 3037 0 LCL050-1 theorem 0.1 4 1 89 0 4 0 6 0 5 89 3151 0 LCL051-1 theorem 0.1 4 1 93 0 4 0 6 0 5 93 3462 0 LCL052-1 theorem 0.1 4 1 100 0 4 0 9 0 5 100 3893 0 LCL053-1 theorem 0.1 4 1 101 0 4 0 9 0 5 101 4020 0 LCL054-1 theorem 4.9 5 1 746 0 4 0 15 0 5 746 109398 0 LCL055-1 theorem 0.1 4 1 94 0 4 0 7 0 5 94 3500 0 LCL056-1 theorem 0.1 4 1 95 0 4 0 7 0 5 95 3540 0 LCL057-1 theorem 0.2 4 1 139 0 4 0 10 0 5 139 6785 0 LCL058-1 theorem 3.9 5 1 674 0 4 0 14 0 5 674 91831 0 LCL059-1 theorem 0.2 4 1 136 0 4 0 10 0 5 136 6580 0 LCL060-1 theorem 6.1 5 1 824 0 4 0 17 0 5 824 127911 0 LCL061-1 theorem 30.0 10 1 1764 0 4 0 20 0 5 1764 431586 0 LCL062-1 theorem 56.3 13 1 2472 0 4 0 30 0 5 2472 733048 0 LCL063-1 timeout 299.0 31 LCL064-1 theorem 1.6 4 1 455 0 4 0 8 0 5 455 48836 0 LCL064-2 theorem 0.2 4 1 131 0 3 0 1 0 5 131 6999 0 LCL065-1 theorem 0.1 4 1 90 0 4 0 1 0 5 90 3614 0 LCL066-1 theorem 0.1 4 1 79 0 4 0 1 0 5 79 3054 0 LCL067-1 theorem 28.8 9 1 2025 0 4 0 101 0 5 2025 485845 0 LCL068-1 theorem 1.3 4 1 419 0 4 0 9 0 5 419 39517 0 LCL069-1 theorem 1.0 4 1 368 0 4 0 7 0 5 368 31084 0 LCL070-1 theorem 1.3 4 1 404 0 4 0 7 0 5 404 36972 0 LCL071-1 theorem 1.6 4 1 447 0 4 0 7 0 5 447 44473 0 LCL072-1 theorem 1.1 4 1 381 0 4 0 7 0 5 381 32887 0 LCL073-1 timeout 299.0 11 LCL074-1 timeout 299.0 11 LCL075-1 theorem 0.1 4 1 56 0 2 0 2 0 6 56 1879 0 LCL076-1 theorem 0.1 4 1 73 0 4 0 1 0 5 73 2632 0 LCL076-2 theorem 0.0 4 1 4 0 4 0 0 0 2 4 5 0 LCL076-3 theorem 0.0 4 1 27 0 4 0 1 0 4 27 481 0 LCL077-1 theorem 0.1 4 1 72 0 4 0 1 0 5 72 2604 0 LCL077-2 theorem 0.0 4 1 25 0 4 0 1 0 4 25 409 0 LCL078-1 timeout 298.9 23 LCL079-1 theorem 0.0 4 1 14 0 6 0 1 0 3 14 71 0 LCL080-1 theorem 0.2 4 1 123 0 4 0 2 0 5 123 7081 0 LCL080-2 theorem 0.2 4 1 123 0 5 0 2 0 5 123 7082 0 LCL081-1 theorem 0.0 4 1 21 0 2 0 6 0 5 21 216 0 LCL082-1 theorem 0.0 4 1 24 0 2 0 10 0 5 24 284 0 LCL083-1 theorem 0.1 4 1 89 0 2 0 41 0 6 89 3710 0 LCL083-2 theorem 0.1 4 1 40 0 3 0 0 0 6 40 1361 0 LCL084-2 theorem 118.3 19 1 1900 0 3 0 57 0 7 1900 2044579 0 LCL084-3 theorem 121.2 20 1 1923 0 4 0 48 0 7 1923 2121256 0 LCL085-1 theorem 18.6 4 1 750 0 2 0 98 0 7 750 335245 0 LCL086-1 theorem 0.0 4 1 23 0 2 0 5 0 6 23 325 0 LCL087-1 theorem 0.0 4 1 12 0 2 0 2 0 6 12 104 0 LCL088-1 theorem 0.1 4 1 50 0 2 0 8 0 6 50 1576 0 LCL089-1 theorem 0.1 4 1 61 0 2 0 8 0 6 61 2440 0 LCL090-1 theorem 0.0 4 1 32 0 2 0 8 0 6 32 406 0 LCL091-1 theorem 0.0 4 1 36 0 2 0 8 0 6 36 575 0 LCL092-1 theorem 0.1 4 1 83 0 2 0 12 0 6 83 3303 0 LCL093-1 theorem 1.5 4 1 278 0 2 0 12 0 6 278 39731 0 LCL094-1 theorem 0.2 4 1 92 0 2 0 8 0 6 92 5728 0 LCL095-1 theorem 0.1 4 1 70 0 2 0 12 0 6 70 2218 0 LCL096-1 theorem 6.3 4 1 538 0 4 0 1 0 5 538 127303 0 LCL097-1 theorem 1.5 4 1 278 0 3 0 1 0 5 278 32079 0 LCL098-1 theorem 0.9 4 1 191 0 2 0 0 0 7 191 2562 0 LCL099-1 timeout 299.0 44 LCL100-1 timeout 299.0 41 LCL101-1 theorem 0.0 4 1 14 0 3 0 1 0 5 14 78 0 LCL102-1 theorem 0.3 4 1 139 0 4 0 1 0 5 139 9646 0 LCL103-1 theorem 3.8 6 1 358 0 3 0 0 0 6 358 55769 0 LCL104-1 theorem 0.0 4 1 16 0 3 0 0 0 5 16 91 0 LCL105-1 timeout 299.0 49 LCL106-1 theorem 0.0 4 1 9 0 3 0 0 0 7 9 26 0 LCL107-1 theorem 0.0 4 1 17 0 2 0 0 0 8 17 118 0 LCL108-1 theorem 0.0 4 1 11 0 2 0 0 0 8 11 44 0 LCL109-1 timeout 299.0 21 LCL110-1 theorem 0.1 4 1 111 0 5 0 0 0 5 111 4756 0 LCL111-1 theorem 0.6 4 1 269 0 5 0 3 0 5 269 18156 0 LCL112-1 theorem 0.1 4 1 112 0 5 0 0 0 5 112 4791 0 LCL113-1 theorem 1.9 4 1 476 0 5 0 4 0 5 476 43924 0 LCL114-1 theorem 5.3 5 1 781 0 5 0 14 0 5 781 100559 0 LCL115-1 theorem 0.3 4 1 206 0 5 0 2 0 5 206 12252 0 LCL116-1 theorem 5.5 5 1 783 0 5 0 14 0 5 783 100935 0 LCL117-1 theorem 0.0 4 1 4 0 2 0 0 0 5 4 7 0 LCL118-1 theorem 0.2 4 1 93 0 2 0 3 0 6 93 3274 0 LCL119-1 timeout 299.0 93 LCL120-1 theorem 0.1 4 1 74 0 2 0 0 0 6 74 1997 0 LCL121-1 theorem 4.0 8 1 318 0 2 0 3 0 7 318 55034 0 LCL122-1 theorem 48.9 32 1 894 0 2 0 3 0 7 894 369981 0 LCL123-1 theorem 16.6 15 1 556 0 2 0 3 0 7 556 155678 0 LCL124-1 timeout 299.0 111 LCL125-1 timeout 299.0 49 LCL126-1 theorem 0.0 4 1 8 0 3 0 1 0 5 8 29 0 LCL127-1 theorem 83.0 40 1 1107 0 2 0 5 0 7 1107 559576 0 LCL128-1 theorem 0.6 4 1 126 0 2 0 1 0 7 126 10177 0 LCL129-1 theorem 73.5 7 1 479 0 2 0 2 0 6 479 93570 0 LCL130-1 theorem 233.2 46 1 2303 0 2 0 3 0 6 2303 1919978 0 LCL131-1 theorem 0.4 4 1 150 0 2 0 1 0 5 150 10311 0 LCL166-1 theorem 51.3 45 1 901 0 2 0 0 0 10 901 393021 0 LCL167-1 timeout 299.0 85 LCL168-1 timeout 299.0 107 LCL169-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 LCL170-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 6 0 LCL171-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 LCL172-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 LCL173-1 theorem 0.0 4 1 6 0 6 0 0 0 2 6 6 0 LCL174-1 theorem 0.2 4 1 805 0 6 0 0 0 5 805 2555 0 LCL175-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 6 0 LCL176-1 theorem 0.0 4 1 8 0 6 0 0 0 4 8 18 0 LCL177-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 25 0 LCL178-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 25 0 LCL179-1 timeout 299.0 80 LCL180-1 timeout 299.0 77 LCL181-1 timeout 299.0 78 LCL182-1 theorem 0.2 4 1 587 0 6 0 0 0 5 587 2007 0 LCL183-1 timeout 299.0 80 LCL184-1 timeout 299.0 77 LCL185-1 theorem 0.0 4 1 19 0 6 0 0 0 4 19 52 0 LCL186-1 theorem 0.0 4 1 19 0 6 0 0 0 4 19 52 0 LCL187-1 theorem 0.0 4 1 20 0 6 0 0 0 4 20 60 0 LCL188-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 25 0 LCL189-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 25 0 LCL190-1 theorem 0.0 4 1 19 0 6 0 0 0 4 19 53 0 LCL191-1 theorem 3.1 6 1 4171 0 6 0 0 0 6 4171 16414 0 LCL192-1 theorem 0.1 4 1 271 0 6 0 0 0 5 271 1041 0 LCL193-1 theorem 0.1 4 1 247 0 6 0 0 0 5 247 952 0 LCL194-1 theorem 3.5 6 1 4728 0 6 0 0 0 6 4728 18445 0 LCL195-1 theorem 3.9 7 1 5123 0 6 0 0 0 6 5123 20027 0 LCL196-1 theorem 0.2 4 1 669 0 6 0 0 0 5 669 2225 0 LCL197-1 theorem 0.0 4 1 85 0 6 0 0 0 5 85 371 0 LCL198-1 theorem 0.2 4 1 669 0 6 0 0 0 5 669 2225 0 LCL199-1 theorem 0.1 4 1 297 0 6 0 0 0 5 297 1150 0 LCL200-1 theorem 0.0 4 1 134 0 6 0 0 0 5 134 571 0 LCL201-1 theorem 1.1 4 1 1415 0 6 0 0 0 6 1415 6197 0 LCL202-1 theorem 0.9 4 1 643 0 6 0 0 0 6 643 3154 0 LCL203-1 theorem 0.8 4 1 643 0 6 0 0 0 6 643 3154 0 LCL204-1 theorem 1.2 4 1 1415 0 6 0 0 0 6 1415 6197 0 LCL205-1 theorem 0.9 4 1 643 0 6 0 0 0 6 643 3154 0 LCL206-1 theorem 0.9 4 1 643 0 6 0 0 0 6 643 3154 0 LCL207-1 theorem 0.8 4 1 486 0 6 0 0 0 6 486 2315 0 LCL208-1 theorem 0.2 4 1 589 0 6 0 0 0 5 589 2011 0 LCL209-1 timeout 299.0 79 LCL210-1 theorem 0.2 4 1 591 0 6 0 0 0 5 591 2020 0 LCL211-1 theorem 0.2 4 1 586 0 6 0 0 0 5 586 2003 0 LCL212-1 theorem 1.3 4 1 1626 0 6 0 0 0 6 1626 7066 0 LCL213-1 theorem 1.2 4 1 1400 0 6 0 0 0 6 1400 6094 0 LCL214-1 theorem 1.2 4 1 1400 0 6 0 0 0 6 1400 6094 0 LCL215-1 theorem 1.3 4 1 1626 0 6 0 0 0 6 1626 7066 0 LCL216-1 theorem 0.2 4 1 586 0 6 0 0 0 5 586 2004 0 LCL217-1 theorem 0.1 4 1 586 0 6 0 0 0 5 586 2004 0 LCL218-1 timeout 299.0 78 LCL219-1 timeout 299.0 78 LCL220-1 timeout 299.0 78 LCL221-1 theorem 24.8 18 1 19817 0 6 0 0 0 6 19817 68181 0 LCL222-1 theorem 27.0 18 1 21122 0 6 0 0 0 6 21122 71819 0 LCL223-1 theorem 30.7 20 1 23044 0 6 0 0 0 6 23044 78004 0 LCL224-1 theorem 28.0 20 1 21624 0 6 0 0 0 6 21624 73710 0 LCL225-1 theorem 28.0 19 1 21624 0 6 0 0 0 6 21624 73710 0 LCL226-1 theorem 0.2 4 1 805 0 6 0 0 0 5 805 2555 0 LCL227-1 timeout 299.0 80 LCL228-1 timeout 299.0 78 LCL229-1 timeout 299.0 79 LCL230-1 timeout 299.0 78 LCL231-1 timeout 299.0 79 LCL234-1 theorem 1.9 5 1 2604 0 6 0 0 0 6 2604 10856 0 LCL235-1 timeout 299.0 78 LCL236-1 theorem 0.0 4 1 9 0 6 0 0 0 4 9 25 0 LCL237-1 theorem 1.9 5 1 2605 0 6 0 0 0 6 2605 10860 0 LCL238-1 theorem 0.1 4 1 296 0 6 0 0 0 5 296 1148 0 LCL239-1 timeout 299.0 78 LCL240-1 timeout 299.0 78 LCL241-1 timeout 299.0 78 LCL242-1 timeout 299.0 77 LCL243-1 timeout 299.0 77 LCL244-1 timeout 299.0 77 LCL245-1 timeout 299.0 78 LCL246-1 timeout 299.0 77 LCL247-1 timeout 299.0 78 LCL248-1 timeout 299.0 78 LCL249-1 timeout 299.0 79 LCL250-1 theorem 5.2 8 1 6332 0 6 0 0 0 6 6332 24493 0 LCL251-1 timeout 299.0 79 LCL252-1 timeout 299.0 77 LCL253-1 timeout 299.0 79 LCL254-1 timeout 299.0 77 LCL255-1 timeout 299.0 77 LCL256-1 theorem 0.1 4 1 96 0 4 0 7 0 5 96 3657 0 LCL257-1 theorem 0.0 4 1 38 0 2 0 2 0 5 38 620 0 LCL355-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 4 0 LCL356-1 theorem 0.0 4 1 13 0 4 0 1 0 5 13 66 0 LCL357-1 theorem 0.0 4 1 13 0 4 0 1 0 5 13 66 0 LCL358-1 theorem 0.0 4 1 18 0 4 0 2 0 5 18 96 0 LCL359-1 theorem 0.0 4 1 18 0 4 0 2 0 5 18 88 0 LCL360-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 4 0 LCL361-1 theorem 0.0 4 1 17 0 4 0 2 0 5 17 83 0 LCL362-1 theorem 0.0 4 1 24 0 4 0 2 0 5 24 164 0 LCL363-1 theorem 0.0 4 1 24 0 4 0 2 0 5 24 164 0 LCL364-1 theorem 0.0 4 1 53 0 4 0 2 0 5 53 1217 0 LCL365-1 theorem 0.1 4 1 86 0 4 0 6 0 5 86 2968 0 LCL366-1 theorem 0.0 4 1 8 0 4 0 0 0 5 8 25 0 LCL367-1 theorem 0.0 4 1 56 0 4 0 4 0 5 56 1319 0 LCL368-1 theorem 0.1 4 1 107 0 4 0 9 0 5 107 4506 0 LCL369-1 theorem 0.1 4 1 107 0 4 0 9 0 5 107 4577 0 LCL370-1 theorem 0.4 4 1 192 0 4 0 10 0 5 192 10830 0 LCL371-1 theorem 0.3 4 1 192 0 4 0 10 0 5 192 10830 0 LCL372-1 theorem 0.4 4 1 201 0 4 0 10 0 5 201 11634 0 LCL373-1 theorem 0.5 4 1 231 0 4 0 11 0 5 231 13968 0 LCL374-1 theorem 35.5 11 1 1933 0 4 0 23 0 5 1933 497295 0 LCL375-1 theorem 29.7 10 1 1761 0 4 0 19 0 5 1761 429400 0 LCL376-1 theorem 7.9 6 1 915 0 4 0 17 0 5 915 154140 0 LCL377-1 theorem 13.2 7 1 1174 0 4 0 17 0 5 1174 225386 0 LCL378-1 theorem 0.1 4 1 93 0 4 0 6 0 5 93 3462 0 LCL379-1 theorem 0.2 4 1 136 0 4 0 10 0 5 136 6639 0 LCL380-1 theorem 0.1 4 1 94 0 4 0 7 0 5 94 3500 0 LCL381-1 theorem 0.1 4 1 96 0 4 0 7 0 5 96 3657 0 LCL382-1 theorem 2.0 4 1 450 0 4 0 12 0 5 450 49546 0 LCL383-1 theorem 2.6 4 1 527 0 4 0 12 0 5 527 62290 0 LCL384-1 theorem 0.2 4 1 148 0 4 0 10 0 5 148 7451 0 LCL385-1 theorem 1.9 4 1 450 0 4 0 12 0 5 450 49546 0 LCL386-1 theorem 0.4 4 1 215 0 4 0 10 0 5 215 12829 0 LCL387-1 theorem 0.5 4 1 240 0 4 0 12 0 5 240 14805 0 LCL388-1 theorem 4.0 5 1 676 0 4 0 14 0 5 676 92257 0 LCL389-1 theorem 2.0 4 1 452 0 4 0 12 0 5 452 49837 0 LCL390-1 theorem 6.1 5 1 823 0 4 0 17 0 5 823 127742 0 LCL391-1 theorem 19.2 8 1 1452 0 4 0 18 0 5 1452 306246 0 LCL392-1 theorem 6.3 5 1 824 0 4 0 17 0 5 824 127911 0 LCL393-1 theorem 21.7 9 1 1524 0 4 0 18 0 5 1524 333554 0 LCL394-1 theorem 33.0 11 1 1853 0 4 0 22 0 5 1853 464642 0 LCL395-1 theorem 43.9 12 1 2150 0 4 0 24 0 5 2150 601375 0 LCL396-1 theorem 0.2 4 1 140 0 4 0 10 0 5 140 6839 0 LCL397-1 theorem 0.0 4 1 24 0 4 0 2 0 5 24 164 0 LCL398-1 theorem 0.0 4 1 6 0 4 0 0 0 5 6 12 0 LCL399-1 theorem 0.0 4 1 40 0 4 0 2 0 5 40 705 0 LCL400-1 theorem 0.2 4 1 117 0 4 0 9 0 5 117 5053 0 LCL401-1 theorem 0.4 4 1 222 0 4 0 10 0 5 222 13325 0 LCL402-1 theorem 0.2 4 1 136 0 4 0 10 0 5 136 6639 0 LCL403-1 theorem 4.0 5 1 676 0 4 0 14 0 5 676 92257 0 LCL404-1 theorem 2.0 4 1 452 0 4 0 12 0 5 452 49837 0 LCL405-1 theorem 0.2 4 1 139 0 4 0 10 0 5 139 6791 0 LCL411-1 timeout 299.0 78 LCL414-1 theorem 0.0 4 1 5 0 4 0 0 0 3 5 6 0 LCL415-1 crash 62.1 97 LCL416-1 theorem 14.7 19 1 507 0 2 0 1 0 10 507 113271 0 LCL417-1 timeout 299.0 107 LCL418-1 timeout 299.0 17 LCL419-1 timeout 299.0 21 LCL420-1 timeout 299.0 20 LCL421-1 timeout 299.0 20 LCL422-1 timeout 299.0 21 LCL423-1 timeout 299.0 21 LCL424-1 timeout 299.0 11 LCL425-1 timeout 299.0 38 LCL426-1 timeout 299.0 18 LCL427-1 timeout 299.0 69 LCL428-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 5 0 MGT001-1 theorem 0.0 4 1 19 0 10 0 0 0 2 19 22 0 MGT002-1 theorem 0.0 4 1 12 0 7 0 0 0 2 12 17 0 MGT003-1 theorem 0.0 4 1 12 0 7 0 0 0 2 12 17 0 MGT006-1 theorem 0.0 4 1 13 0 8 2 0 0 2 13 13 0 MGT008-1 theorem 0.0 4 1 15 0 12 0 0 0 2 15 16 0 MGT009-1 theorem 0.0 4 1 15 0 12 0 0 0 2 15 16 0 MGT010-1 theorem 0.0 4 1 18 0 13 2 0 0 2 18 18 0 MGT015-1 theorem 0.0 4 1 17 0 13 0 0 0 2 17 18 0 MGT017-1 theorem 0.0 4 1 17 0 13 0 0 0 2 17 18 0 MGT032-2 theorem 0.0 4 1 7 0 2 0 0 0 4 7 7 0 MGT036-3 theorem 0.0 4 1 6 0 4 0 0 0 2 6 7 0 MSC005-1 theorem 0.1 4 1 50 0 3 0 0 0 4 50 1447 0 NLP001-1 theorem 0.0 4 2 28 1 48 5 0 0 2 19 32 30 NLP104-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 NLP105-1 non_thm 0.0 4 0 1 0 1 0 0 0 2 1 1 0 NLP106-1 non_thm 0.0 4 0 14 0 2 0 0 0 2 14 14 0 NLP107-1 non_thm 0.0 4 0 26 0 3 0 0 0 2 26 26 0 NLP108-1 non_thm 0.0 4 0 49 0 10 0 0 0 2 49 51 0 NLP109-1 non_thm 0.0 4 0 26 0 3 0 0 0 2 26 26 0 NLP110-1 non_thm 0.0 4 0 37 0 9 0 0 0 2 37 39 0 NLP111-1 non_thm 0.0 4 0 49 0 10 0 0 0 2 49 51 0 NLP112-1 non_thm 0.0 4 0 49 0 10 0 0 0 2 49 51 0 NLP113-1 non_thm 0.0 4 0 13 0 2 0 0 0 2 13 13 0 NUM001-1 theorem 0.1 4 1 38 0 8 0 0 0 3 38 549 0 NUM002-1 theorem 0.0 4 1 34 0 8 0 0 0 3 34 481 0 NUM003-1 theorem 0.0 4 1 40 0 8 0 0 0 3 40 594 0 NUM004-1 theorem 0.0 4 1 33 0 8 0 0 0 3 33 464 0 NUM017-1 timeout 299.0 71 NUM019-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 14 0 NUM020-1 theorem 0.0 4 1 12 0 8 0 0 0 3 12 61 0 NUM023-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 16 0 NUM024-1 theorem 5.9 8 1 1892 0 8 0 44 0 4 1892 54335 0 NUM025-1 theorem 0.0 4 1 4 0 4 0 0 0 2 4 14 0 NUM026-1 timeout 299.0 50 NUM283-1.005 theorem 24.8 7 1 601 0 4 0 0 0 121 601 625 0 NUM284-1.014 theorem 170.1 12 1 249 0 4 0 0 0 378 249 250 0 NUM286-1 timeout 299.0 24 NUM286-2 timeout 299.0 100 NUM287-1 timeout 299.0 42 PLA001-1 theorem 2.0 8 1 3066 0 12 0 0 0 10 3066 8182 0 PLA003-1 theorem 0.0 4 1 8 0 4 2 3 0 2 8 15 0 PLA004-1 timeout 298.9 49 PLA004-2 timeout 299.0 49 PLA005-1 timeout 299.0 50 PLA005-2 timeout 299.0 49 PLA006-1 theorem 0.0 4 1 64 0 20 0 0 0 3 64 198 0 PLA007-1 timeout 299.0 45 PLA008-1 timeout 299.0 46 PLA009-1 timeout 299.0 46 PLA009-2 timeout 299.0 45 PLA010-1 timeout 299.0 49 PLA011-1 timeout 299.0 49 PLA011-2 timeout 299.0 50 PLA012-1 timeout 299.0 48 PLA013-1 timeout 299.0 48 PLA014-1 timeout 299.0 50 PLA014-2 timeout 299.0 50 PLA015-1 timeout 299.0 46 PLA016-1 timeout 299.0 45 PLA017-1 theorem 0.0 4 1 93 0 20 0 0 0 3 93 407 0 PLA018-1 timeout 299.0 49 PLA019-1 timeout 298.9 48 PLA020-1 theorem 0.0 4 1 18 0 18 0 0 0 2 18 31 0 PLA021-1 timeout 299.0 50 PLA022-1 theorem 24.5 16 1 3177 0 20 0 0 0 4 3177 53020 0 PLA022-2 theorem 24.3 15 1 3177 0 20 0 0 0 4 3177 53029 0 PLA023-1 timeout 299.0 46 PLA029-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 PLA030-1 timeout 299.0 45 PUZ003-1 theorem 0.0 4 1 14 0 6 0 0 0 2 14 27 0 PUZ008-1 theorem 0.0 4 1 5 0 5 0 0 0 2 5 6 0 PUZ008-2 theorem 0.0 4 1 13 0 28 13 0 0 3 13 16 0 PUZ008-3 theorem 0.0 4 1 27 0 4 0 0 0 6 27 46 0 PUZ011-1 theorem 0.0 4 1 18 0 18 0 0 0 2 18 26 0 PUZ015-3 timeout 299.0 267 PUZ022-1 theorem 0.0 4 1 34 0 31 0 0 0 2 34 53 0 PUZ036-1.005 theorem 0.2 4 1 605 0 2 0 0 0 2 605 1812 0 PUZ037-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 20 0 PUZ037-2 theorem 0.5 4 1 118 0 2 0 0 0 2 118 2100 0 PUZ037-3 memory 120.8 399 PUZ038-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 2 0 PUZ039-1 theorem 8.8 30 1 10655 0 2 0 0 0 6 10655 28569 0 PUZ040-1 theorem 0.1 4 1 67 0 2 0 0 0 6 67 194 0 PUZ041-1 memory 253.6 398 PUZ042-1 theorem 62.9 141 1 63506 0 2 0 0 0 6 63506 173714 0 PUZ046-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 PUZ047-1 theorem 0.0 4 1 36 0 2 0 0 0 7 36 73 0 PUZ048-1 memory 237.8 399 PUZ049-1 non_thm 1.4 7 0 1897 0 2 0 0 0 6 1897 5126 0 PUZ050-1 memory 250.6 399 PUZ051-1 memory 244.2 399 PUZ052-1 memory 121.2 399 PUZ053-1 memory 120.7 399 PUZ054-1 non_thm 0.0 4 0 75 0 2 0 0 0 15 75 180 0 RNG001-2 theorem 19.5 18 1 163 0 7 0 18 0 2 163 344049 0 RNG001-3 theorem 0.0 4 1 18 0 4 0 1 0 2 18 557 0 RNG001-5 theorem 1.0 4 1 66 0 8 0 3 0 2 66 19176 0 RNG004-3 timeout 299.0 208 RNG005-2 theorem 0.0 4 1 11 0 11 0 0 0 2 11 554 0 RNG006-2 theorem 88.7 94 1 209 0 13 0 9 0 2 209 1968859 0 RNG037-2 theorem 0.0 4 1 15 0 9 0 0 0 2 15 898 0 RNG038-2 theorem 2.2 5 1 69 0 9 0 0 0 2 69 58084 0 RNG039-2 theorem 1.6 6 1 64 0 50 0 7 0 2 64 31717 0 ROB025-1 timeout 298.9 56 SWV010-1 non_thm 0.0 4 0 8 0 5 0 0 0 6 8 8 0 SWV011-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 2 0 SWV012-1 timeout 299.0 265 SWV013-1 timeout 299.0 267 SWV014-1 timeout 299.0 266 SWV015-1 timeout 299.0 276 SWV016-1 timeout 299.0 272 SWV017-1 timeout 298.9 4 SWV018-1 timeout 299.0 4 SYN003-1.006 theorem 0.0 4 1 18 0 22 18 0 0 2 18 23 0 SYN004-1.007 theorem 0.0 4 1 14 0 14 14 0 0 2 14 14 0 SYN005-1.010 theorem 0.0 4 1 10 0 10 0 0 0 2 10 10 0 SYN010-1.005.005 theorem 0.0 4 1 26 0 26 26 0 0 2 26 27 0 SYN033-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 4 0 SYN035-1 theorem 0.0 4 1 2 0 2 6 0 0 2 2 2 0 SYN040-1 theorem 0.0 4 1 2 0 3 2 0 0 2 2 3 0 SYN041-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 4 0 SYN046-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 3 0 SYN048-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 SYN049-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 3 0 SYN050-1 theorem 0.0 4 1 3 0 3 1 0 0 2 3 5 0 SYN057-1 theorem 0.0 4 1 7 0 4 0 0 0 2 7 8 0 SYN058-1 theorem 0.0 4 1 5 0 8 1 0 0 2 5 6 0 SYN062-1 theorem 0.0 4 1 5 0 3 0 0 0 2 5 6 0 SYN063-2 theorem 0.0 4 1 2 0 2 2 0 0 2 2 3 0 SYN064-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 SYN065-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 3 0 SYN068-1 theorem 0.0 4 1 6 0 1 0 0 0 2 6 7 0 SYN079-1 theorem 0.0 4 1 3 0 3 0 0 0 2 3 4 0 SYN085-1.010 theorem 0.0 4 1 11 0 11 11 0 0 2 11 12 0 SYN086-1.003 non_thm 0.0 4 0 1 0 1 1 0 0 2 1 1 0 SYN087-1.003 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 SYN088-1.010 theorem 0.0 4 1 21 0 21 0 0 0 2 21 1045 0 SYN089-1.002 theorem 0.0 4 1 5 0 9 5 0 0 2 5 9 0 SYN090-1.008 theorem 0.0 4 1 34 0 64 58 0 0 2 34 62 0 SYN095-1.002 theorem 0.0 4 1 4 0 6 1 0 0 2 4 7 0 SYN096-1.008 theorem 0.0 4 1 34 0 4 0 0 0 2 34 64 0 SYN101-1.002.002 theorem 0.0 4 1 17 0 5 0 0 0 2 17 29 0 SYN102-1.007.007 theorem 0.6 4 1 3854 0 14 2 0 0 2 3854 7182 0 SYN103-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN104-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN105-1 theorem 0.0 4 1 22 0 29 31 0 0 2 22 208 0 SYN106-1 theorem 0.0 4 1 17 0 24 30 0 0 2 17 166 0 SYN107-1 theorem 0.0 4 1 37 0 116 51 0 0 2 37 370 0 SYN108-1 theorem 0.0 4 1 37 0 117 51 0 0 2 37 370 0 SYN109-1 theorem 0.0 4 1 129 0 234 134 1 0 2 129 900 0 SYN110-1 theorem 0.1 4 1 252 0 255 159 6 0 2 252 2060 0 SYN111-1 theorem 0.1 4 1 234 0 255 155 6 0 2 234 1917 0 SYN112-1 theorem 0.0 4 1 37 0 115 52 0 0 2 37 370 0 SYN113-1 theorem 0.0 4 1 60 0 218 89 0 0 2 60 493 0 SYN114-1 theorem 0.0 4 1 39 0 119 60 0 0 2 39 388 0 SYN115-1 theorem 0.1 4 1 208 0 252 155 4 0 2 208 1846 0 SYN116-1 theorem 0.1 4 1 93 0 231 127 1 0 2 93 707 0 SYN117-1 theorem 0.0 4 1 93 0 231 126 1 0 2 93 707 0 SYN118-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN119-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN120-1 theorem 0.0 4 1 17 0 25 30 0 0 2 17 165 0 SYN121-1 theorem 0.0 4 1 70 0 225 109 1 0 2 70 549 0 SYN122-1 theorem 0.1 4 1 70 0 225 109 1 0 2 70 549 0 SYN123-1 theorem 0.0 4 1 34 0 57 35 0 0 2 34 326 0 SYN124-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 SYN125-1 theorem 0.1 4 1 274 0 256 162 6 0 2 274 2213 0 SYN126-1 theorem 0.0 4 1 47 0 189 78 0 0 2 47 435 0 SYN127-1 theorem 0.0 4 1 47 0 189 78 0 0 2 47 435 0 SYN128-1 theorem 0.0 4 1 57 0 218 87 0 0 2 57 470 0 SYN129-1 theorem 0.0 4 1 56 0 218 86 0 0 2 56 463 0 SYN130-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN131-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN132-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 SYN133-1 theorem 0.0 4 1 5 0 4 9 0 0 2 5 52 0 SYN134-1 theorem 0.0 4 1 59 0 219 89 0 0 2 59 486 0 SYN135-1 theorem 0.0 4 1 40 0 124 64 0 0 2 40 391 0 SYN136-1 theorem 0.0 4 1 40 0 123 64 0 0 2 40 391 0 SYN137-1 theorem 0.0 4 1 85 0 231 122 1 0 2 85 662 0 SYN138-1 theorem 0.1 4 1 237 0 254 156 6 0 2 237 1951 0 SYN139-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 SYN140-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 SYN141-1 theorem 0.1 4 1 209 0 253 154 4 0 2 209 1858 0 SYN142-1 theorem 0.1 4 1 296 0 259 167 6 0 2 296 2374 0 SYN143-1 theorem 0.1 4 1 296 0 259 167 6 0 2 296 2374 0 SYN144-1 theorem 0.1 4 1 227 0 254 154 4 0 2 227 1887 0 SYN145-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN146-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 44 0 SYN147-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 60 0 SYN148-1 theorem 0.0 4 1 133 0 234 135 1 0 2 133 954 0 SYN149-1 theorem 0.0 4 1 12 0 20 30 0 0 2 12 135 0 SYN150-1 theorem 0.0 4 1 36 0 94 45 0 0 2 36 358 0 SYN151-1 theorem 0.0 4 1 36 0 94 45 0 0 2 36 358 0 SYN152-1 theorem 0.0 4 1 36 0 95 46 0 0 2 36 358 0 SYN153-1 theorem 0.0 4 1 41 0 143 65 0 0 2 41 397 0 SYN154-1 theorem 0.0 4 1 41 0 143 65 0 0 2 41 397 0 SYN155-1 theorem 0.1 4 1 188 0 245 147 3 0 2 188 1578 0 SYN156-1 theorem 0.1 4 1 203 0 252 152 4 0 2 203 1839 0 SYN157-1 theorem 0.0 4 1 51 0 206 83 0 0 2 51 443 0 SYN158-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 SYN159-1 theorem 0.1 4 1 189 0 248 147 3 0 2 189 1609 0 SYN160-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 SYN161-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 SYN162-1 theorem 0.0 4 1 51 0 206 82 0 0 2 51 443 0 SYN163-1 theorem 0.1 4 1 189 0 248 147 3 0 2 189 1609 0 SYN164-1 theorem 0.0 4 1 7 0 10 16 0 0 2 7 78 0 SYN165-1 theorem 0.0 4 1 5 0 6 10 0 0 2 5 48 0 SYN166-1 theorem 0.1 4 1 141 0 236 137 2 0 2 141 1037 0 SYN167-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 SYN168-1 theorem 0.0 4 1 39 0 119 61 0 0 2 39 387 0 SYN169-1 theorem 0.0 4 1 39 0 119 61 0 0 2 39 387 0 SYN170-1 theorem 0.0 4 1 43 0 164 67 0 0 2 43 424 0 SYN171-1 theorem 0.1 4 1 386 0 264 170 6 0 2 386 2976 0 SYN172-1 theorem 0.0 4 1 6 0 7 12 0 0 2 6 71 0 SYN173-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN174-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN175-1 theorem 0.0 4 1 35 0 77 38 0 0 2 35 347 0 SYN176-1 theorem 0.0 4 1 70 0 225 107 1 0 2 70 547 0 SYN177-1 theorem 0.1 4 1 148 0 240 138 3 0 2 148 1157 0 SYN178-1 theorem 0.0 4 1 77 0 229 114 1 0 2 77 604 0 SYN179-1 theorem 0.1 4 1 164 0 242 145 3 0 2 164 1272 0 SYN180-1 theorem 0.0 4 1 78 0 229 115 1 0 2 78 608 0 SYN181-1 theorem 0.0 4 1 75 0 229 113 1 0 2 75 583 0 SYN182-1 theorem 0.0 4 1 49 0 198 80 0 0 2 49 438 0 SYN183-1 theorem 0.1 4 1 49 0 198 80 0 0 2 49 438 0 SYN184-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN185-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN186-1 theorem 0.0 4 1 37 0 116 51 0 0 2 37 371 0 SYN187-1 theorem 0.0 4 1 37 0 117 51 0 0 2 37 371 0 SYN188-1 theorem 0.0 4 1 37 0 116 51 0 0 2 37 371 0 SYN189-1 theorem 0.0 4 1 38 0 119 52 0 0 2 38 377 0 SYN190-1 theorem 0.1 4 1 177 0 244 147 3 0 2 177 1476 0 SYN191-1 theorem 0.1 4 1 155 0 239 138 3 0 2 155 1240 0 SYN192-1 theorem 0.1 4 1 161 0 239 141 3 0 2 161 1265 0 SYN193-1 theorem 0.0 4 1 161 0 239 141 3 0 2 161 1265 0 SYN194-1 theorem 0.1 4 1 119 0 233 134 1 0 2 119 808 0 SYN195-1 theorem 0.1 4 1 93 0 231 126 1 0 2 93 701 0 SYN196-1 theorem 0.0 4 1 68 0 221 92 0 0 2 68 522 0 SYN197-1 theorem 0.0 4 1 8 0 15 20 0 0 2 8 80 0 SYN198-1 theorem 0.0 4 1 68 0 222 92 0 0 2 68 522 0 SYN199-1 theorem 0.0 4 1 68 0 221 92 0 0 2 68 522 0 SYN200-1 theorem 0.0 4 1 68 0 220 92 0 0 2 68 522 0 SYN201-1 theorem 0.0 4 1 68 0 220 92 0 0 2 68 511 0 SYN202-1 theorem 0.0 4 1 78 0 229 116 1 0 2 78 612 0 SYN203-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 SYN204-1 theorem 0.1 4 1 294 0 257 163 6 0 2 294 2354 0 SYN205-1 theorem 0.1 4 1 294 0 257 163 6 0 2 294 2354 0 SYN206-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 SYN207-1 theorem 0.1 4 1 288 0 257 163 6 0 2 288 2301 0 SYN208-1 theorem 0.0 4 1 82 0 231 121 1 0 2 82 645 0 SYN209-1 theorem 0.0 4 1 122 0 233 134 1 0 2 122 815 0 SYN210-1 theorem 0.1 4 1 118 0 233 133 1 0 2 118 794 0 SYN211-1 theorem 0.0 4 1 59 0 218 88 0 0 2 59 483 0 SYN212-1 theorem 0.0 4 1 114 0 233 130 1 0 2 114 779 0 SYN213-1 theorem 0.1 4 1 162 0 240 142 3 0 2 162 1271 0 SYN214-1 theorem 0.1 4 1 162 0 240 142 3 0 2 162 1271 0 SYN215-1 theorem 0.1 4 1 162 0 240 142 3 0 2 162 1271 0 SYN216-1 theorem 0.0 4 1 68 0 220 92 0 0 2 68 516 0 SYN217-1 theorem 0.0 4 1 69 0 222 101 1 0 2 69 541 0 SYN218-1 theorem 0.0 4 1 68 0 222 93 0 0 2 68 516 0 SYN219-1 theorem 0.0 4 1 70 0 226 109 1 0 2 70 549 0 SYN220-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 SYN221-1 theorem 0.0 4 1 41 0 142 67 0 0 2 41 396 0 SYN222-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 SYN223-1 theorem 0.0 4 1 41 0 143 65 0 0 2 41 396 0 SYN224-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 SYN225-1 theorem 0.0 4 1 74 0 230 113 1 0 2 74 582 0 SYN226-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 SYN227-1 theorem 0.1 4 1 272 0 256 162 6 0 2 272 2196 0 SYN228-1 theorem 0.0 4 1 128 0 235 134 1 0 2 128 881 0 SYN229-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 SYN230-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 SYN231-1 theorem 0.0 4 1 41 0 142 67 0 0 2 41 396 0 SYN232-1 theorem 0.0 4 1 41 0 142 66 0 0 2 41 396 0 SYN233-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 SYN234-1 theorem 0.0 4 1 74 0 229 113 1 0 2 74 582 0 SYN235-1 theorem 0.0 4 1 130 0 234 134 1 0 2 130 931 0 SYN236-1 theorem 0.0 4 1 41 0 142 65 0 0 2 41 396 0 SYN237-1 theorem 0.0 4 1 6 0 8 13 0 0 2 6 66 0 SYN238-1 theorem 0.0 4 1 4 0 4 6 0 0 2 4 43 0 SYN239-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 45 0 SYN240-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 135 0 SYN241-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 135 0 SYN242-1 theorem 0.0 4 1 27 0 33 35 0 0 2 27 269 0 SYN243-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN244-1 theorem 0.0 4 1 4 0 4 9 0 0 2 4 45 0 SYN245-1 theorem 0.0 4 1 12 0 18 31 0 0 2 12 135 0 SYN246-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN247-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 66 0 SYN248-1 theorem 0.0 4 1 57 0 218 87 0 0 2 57 468 0 SYN249-1 theorem 0.0 4 1 56 0 218 86 0 0 2 56 461 0 SYN250-1 theorem 0.1 4 1 257 0 254 161 6 0 2 257 2097 0 SYN251-1 theorem 0.0 4 1 30 0 36 34 0 0 2 30 297 0 SYN252-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 SYN253-1 theorem 0.1 4 1 295 0 258 164 6 0 2 295 2366 0 SYN254-1 theorem 0.1 4 1 295 0 257 164 6 0 2 295 2366 0 SYN255-1 theorem 0.0 4 1 36 0 94 46 0 0 2 36 358 0 SYN256-1 theorem 0.0 4 1 36 0 94 46 0 0 2 36 358 0 SYN257-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 SYN258-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 77 0 SYN259-1 theorem 0.0 4 1 7 0 11 16 0 0 2 7 77 0 SYN260-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 SYN261-1 theorem 0.0 4 1 12 0 19 30 0 0 2 12 135 0 SYN262-1 theorem 0.0 4 1 61 0 219 89 0 0 2 61 500 0 SYN263-1 theorem 0.0 4 1 140 0 236 136 1 0 2 140 1015 0 SYN264-1 theorem 0.1 4 1 247 0 254 158 6 0 2 247 2028 0 SYN265-1 theorem 0.0 4 1 40 0 123 64 0 0 2 40 390 0 SYN266-1 theorem 0.0 4 1 170 0 243 146 3 0 2 170 1333 0 SYN267-1 theorem 0.0 4 1 43 0 165 66 0 0 2 43 424 0 SYN268-1 theorem 0.0 4 1 43 0 164 66 0 0 2 43 424 0 SYN269-1 theorem 0.1 4 1 384 0 264 170 6 0 2 384 2958 0 SYN270-1 theorem 0.1 4 1 173 0 244 147 3 0 2 173 1386 0 SYN271-1 theorem 0.1 4 1 386 0 264 170 6 0 2 386 2976 0 SYN272-1 theorem 0.0 4 1 97 0 233 128 1 0 2 97 736 0 SYN273-1 theorem 0.1 4 1 96 0 233 128 1 0 2 96 723 0 SYN274-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN275-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 39 0 SYN276-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 SYN277-1 theorem 0.0 4 1 6 0 10 11 0 0 2 6 53 0 SYN278-1 theorem 0.0 4 1 4 0 5 9 0 0 2 4 47 0 SYN279-1 theorem 0.0 4 1 13 0 19 29 0 0 2 13 136 0 SYN280-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 47 0 SYN281-1 theorem 0.0 4 1 12 0 18 29 0 0 2 12 135 0 SYN282-1 theorem 0.0 4 1 6 0 9 12 0 0 2 6 53 0 SYN283-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN284-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN285-1 theorem 0.1 4 1 144 0 238 138 3 0 2 144 1096 0 SYN286-1 theorem 0.0 4 1 17 0 23 30 0 0 2 17 160 0 SYN287-1 theorem 0.0 4 1 4 0 4 10 0 0 2 4 47 0 SYN288-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN289-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN290-1 theorem 0.0 4 1 6 0 10 10 0 0 2 6 53 0 SYN291-1 theorem 0.0 4 1 6 0 10 12 0 0 2 6 53 0 SYN292-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN293-1 theorem 0.0 4 1 55 0 218 85 0 0 2 55 455 0 SYN294-1 theorem 0.0 4 1 55 0 218 86 0 0 2 55 455 0 SYN295-1 theorem 0.0 4 1 27 0 34 35 0 0 2 27 269 0 SYN296-1 theorem 0.0 4 1 27 0 33 34 0 0 2 27 269 0 SYN297-1 theorem 0.0 4 1 27 0 34 34 0 0 2 27 269 0 SYN298-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 SYN299-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 SYN300-1 theorem 0.0 4 1 81 0 229 120 1 0 2 81 638 0 SYN301-1 theorem 0.1 4 1 110 0 233 130 1 0 2 110 759 0 SYN302-1.003 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 SYN303-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 5 0 SYN310-1 theorem 0.0 4 1 14 0 2 0 0 0 3 14 34 0 SYN311-1 theorem 3.1 13 1 15758 0 2 0 0 0 3 15758 47201 0 SYN312-1 theorem 37.8 11 1 6733 0 3 0 0 0 3 6733 142417 0 SYN318-1 theorem 0.0 4 1 2 0 2 2 0 0 2 2 4 0 SYN322-1 non_thm 0.0 4 0 0 0 0 0 0 0 2 0 0 0 SYN329-1 non_thm 0.0 4 0 3 0 4 0 0 0 2 3 4 0 SYN333-1 theorem 0.0 4 1 2 0 2 6 0 0 2 2 2 0 SYN336-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 5 0 SYN337-1 non_thm 0.0 4 0 4 0 5 0 0 0 2 4 5 0 SYN338-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 3 0 SYN339-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 SYN340-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 SYN341-1 theorem 0.0 4 1 1 0 0 0 0 0 2 1 2 0 SYN342-1 non_thm 0.0 4 0 2 0 2 0 0 0 2 2 2 0 SYN346-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0 SYN553-1 theorem 0.0 4 1 14 0 7 0 0 0 3 14 98 0 SYN555-1 theorem 0.0 4 1 8 0 6 0 0 0 2 8 22 0 SYN556-1 timeout 298.9 12 SYN557-1 timeout 299.0 54 SYN558-1 theorem 0.0 4 1 16 0 6 0 0 0 2 16 80 0 SYN559-1 theorem 0.0 4 1 40 0 6 0 0 0 3 40 303 0 SYN561-1 theorem 0.4 4 1 76 0 6 0 0 0 4 76 5020 0 SYN562-1 theorem 0.0 4 1 7 0 7 0 0 0 2 7 21 0 SYN563-1 theorem 0.0 4 1 42 0 6 0 0 0 3 42 236 0 SYN564-1 theorem 0.0 4 1 38 0 7 0 0 0 4 38 423 0 SYN565-1 theorem 0.0 4 1 56 0 7 0 0 0 4 56 611 0 SYN566-1 theorem 0.0 4 1 16 0 8 0 0 0 3 16 56 0 SYN569-1 theorem 0.0 4 1 36 0 7 0 0 0 3 36 178 0 SYN570-1 theorem 0.0 4 1 16 0 10 0 0 0 3 16 47 0 SYN572-1 theorem 0.6 4 1 141 0 9 0 0 0 5 141 4505 0 SYN577-1 theorem 0.1 4 1 80 0 12 0 0 0 3 80 905 0 SYN584-1 theorem 0.0 4 1 10 0 9 0 0 0 8 10 29 0 SYN588-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 27 0 SYN589-1 theorem 0.0 4 1 12 0 12 0 0 0 2 12 27 0 SYN590-1 theorem 0.0 4 1 57 0 8 0 0 0 4 57 204 0 SYN596-1 theorem 0.0 4 1 12 0 11 0 0 0 5 12 33 0 SYN597-1 theorem 0.4 4 1 214 0 11 0 0 0 4 214 5231 0 SYN598-1 timeout 299.0 39 SYN599-1 timeout 299.0 38 SYN600-1 timeout 299.0 175 SYN601-1 theorem 0.5 5 1 241 0 12 0 0 0 4 241 5655 0 SYN602-1 theorem 0.2 4 1 114 0 7 0 0 0 3 114 793 0 SYN603-1 theorem 238.4 41 1 3200 0 7 0 0 0 4 3200 190451 0 SYN614-1 timeout 299.0 296 SYN615-1 timeout 299.0 297 SYN616-1 theorem 0.6 4 1 155 0 13 0 0 0 3 155 5725 0 SYN617-1 timeout 299.0 112 SYN618-1 theorem 0.0 4 1 32 0 16 0 0 0 3 32 118 0 SYN628-1 theorem 0.3 5 1 111 0 15 0 0 0 3 111 3903 0 SYN629-1 theorem 0.3 5 1 111 0 15 0 0 0 3 111 3903 0 SYN631-1 timeout 299.0 74 SYN632-1 theorem 0.0 4 1 24 0 12 0 0 0 7 24 107 0 SYN637-1 theorem 0.1 4 1 25 0 14 0 0 0 7 25 219 0 SYN638-1 theorem 0.0 4 1 25 0 14 0 0 0 7 25 219 0 SYN639-1 timeout 299.0 94 SYN640-1 timeout 299.0 98 SYN646-1 timeout 299.0 40 SYN647-1 timeout 298.9 41 SYN649-1 timeout 299.0 78 SYN651-1 theorem 0.0 4 1 25 0 15 0 0 0 6 25 69 0 SYN652-1 theorem 0.0 4 1 27 0 20 0 0 0 3 27 86 0 SYN653-1 timeout 298.9 4 SYN654-1 timeout 299.0 4 SYN655-1 timeout 299.0 4 SYN688-1 theorem 0.0 4 1 41 0 28 0 0 0 3 41 93 0 SYN689-1 theorem 0.0 4 1 41 0 28 0 0 0 3 41 93 0 SYN691-1 theorem 0.0 4 1 32 0 24 0 0 0 8 32 94 0 SYN702-1 theorem 0.0 4 1 34 0 28 0 0 0 9 34 98 0 SYN703-1 theorem 0.0 4 1 37 0 29 0 0 0 9 37 107 0 SYN704-1 timeout 299.0 67 SYN705-1 theorem 0.0 4 1 37 0 29 0 0 0 9 37 107 0 SYN706-1 theorem 0.0 4 1 56 0 31 0 1 0 6 56 196 0 SYN707-1 timeout 299.0 24 SYN708-1 timeout 299.0 24 SYN709-1 theorem 0.0 4 1 47 0 35 0 0 0 4 47 132 0 SYN711-1 timeout 299.0 40 SYN712-1 theorem 0.0 4 1 44 0 36 0 0 0 10 44 129 0 SYN715-1 theorem 0.0 4 1 44 0 36 0 0 0 10 44 131 0 SYN716-1 theorem 0.0 4 1 43 0 36 0 0 0 10 43 126 0 SYN719-1 theorem 0.0 4 1 49 0 46 0 0 0 3 49 126 0 SYN720-1 non_thm 0.1 4 0 423 0 264 171 6 0 2 423 3107 0 SYN721-1 theorem 0.0 4 1 3 0 1 0 0 0 2 3 3 0 SYN727-1 theorem 0.0 4 1 2 0 2 0 0 0 2 2 3 0 SYN729-1 theorem 0.0 4 1 41 0 1 0 0 0 4 41 41 0 SYN731-1 theorem 0.0 4 1 1 0 1 0 0 0 2 1 2 0