-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv false Problems list file : casc18_ept-problems Output file : casc18_ept-output Summary file : casc18_ept-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 GRP127-2.006 theorem 0.1 2 3 332 2 57 0 0 0 2 260 1449 1416 0 GRP128-2.006 theorem 0.1 2 8 516 7 56 0 0 0 2 255 2007 1838 0 GRP128-3.005 theorem 0.1 2 8 409 7 46 0 0 0 2 209 1551 905 0 PUZ010-1 theorem 1.0 2 337 7192 350 1303 420 0 0 2 204 19149 29173 0 PUZ017-1 theorem 0.1 2 5 306 4 85 1 5 0 2 231 1196 1624 0 PUZ037-2 theorem 0.1 2 1 19 0 2 0 0 0 2 19 338 0 0 PUZ037-3 theorem 2.5 9 1 560 0 2 0 0 0 2 560 10069 0 0 SYN440-1 theorem 117.5 5 1087 13368 1283 13038 4949 0 0 2 130 223514 5767922 0 SYN447-1 theorem 15.5 10 100 2482 126 2207 859 0 0 2 127 9563 1538466 0 SYN454-1 theorem 2.7 3 100 1398 116 1351 614 0 0 2 80 5427 175857 0 SYN457-1 theorem 77.7 7 808 14076 1032 13105 4537 0 0 2 154 115929 3150057 3644 SYN462-1 theorem 0.9 3 38 738 39 666 292 0 0 2 79 2999 102482 0 SYN466-1 theorem 1.7 2 108 1481 114 1437 650 0 0 2 85 7497 98924 0 SYN470-1 theorem 1.3 3 67 1262 80 1182 543 0 0 2 88 4342 84564 0 SYN475-1 theorem 1.9 3 57 899 64 858 414 0 0 2 62 3481 218483 0 SYN483-1 theorem 1.5 3 86 1568 89 1443 691 0 0 2 66 6292 121337 0 SYN487-1 theorem 3.7 3 106 1914 120 1795 790 0 0 2 99 9714 170073 0 SYN498-1 theorem 2.3 3 55 846 57 791 387 0 0 2 77 4187 221843 0 SYN500-1 theorem 1.2 3 49 778 50 720 343 0 0 2 56 3768 140471 0 SYN501-1 theorem 0.6 2 25 386 25 371 176 0 0 2 55 1506 53578 0 SYN504-1 theorem 3.1 3 54 614 62 635 311 0 0 2 80 6130 229387 0 SYN507-1 theorem 2.4 3 62 1212 68 1122 496 0 0 2 78 4650 166517 0 SYN510-1 theorem 0.8 2 68 1152 75 1098 549 0 0 2 64 3733 60206 0 SYN813-1 theorem 2.9 5 41 188 1709 36 269 0 1203 2 744 389 6491 0 SYN820-1 theorem 1.8 5 27 188 1453 36 269 0 297 2 467 375 4060 0 SYN834-1 theorem 0.9 5 31 188 624 36 269 0 10 2 384 371 1762 0 SYN844-1 timeout 500.0 35 SYN845-1 theorem 318.1 30 4932 188 93140 36 269 0 80749 2 803 5272 718816 13151 SYN848-1 timeout 500.0 56 SYN859-1 theorem 28.4 12 284 376 6465 52 489 0 4874 2 872 984 32517 0 SYN876-1 theorem 1.9 3 42 52 243 52 487 0 219 2 102 94 1936 0 SYN883-1 theorem 1.0 4 14 52 117 52 491 0 79 2 96 66 1045 0 SYN886-1 theorem 0.4 3 4 72 22 72 909 0 0 2 81 76 144 0 SYN887-1 theorem 0.4 3 5 72 19 72 938 0 0 2 81 77 132 0 SYN900-1 theorem 1.3 4 26 72 110 72 923 0 66 2 116 98 531 0