-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true Problems list file : cascj2_ept-problems Output file : cascj2_ept-output Summary file : cascj2_ept-summary Time limit : 500 s Memory limit : 500 MB -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug [None] SYN914-1 timeout 500.0 3 [0.00] LAT005-1 theorem 3.5 6 1 428 0 17 0 16 0 2 428 96665 0 0 [0.00] PUZ036-1.005 theorem 0.0 2 1 53 0 2 0 0 0 2 53 160 0 0 [0.00] PUZ037-1 theorem 0.0 2 1 2 0 2 0 0 0 2 2 35 0 0 [0.00] PUZ037-2 theorem 0.0 2 1 7 0 2 0 0 0 2 7 124 0 0 [0.00] SYN885-1 theorem 4.7 5 56 72 367 72 1094 0 813 2 155 128 1900 0 [0.00] SYN886-1 theorem 0.3 3 2 72 8 72 1108 0 56 2 77 74 89 0 [0.00] SYN887-1 theorem 0.4 3 5 72 18 72 1159 0 61 2 81 77 130 0 [0.00] SYN897-1 theorem 391.5 13 760 72 13661 72 1180 275 88337 2 233 832 173793 0 [0.00] SYN898-1 theorem 8.3 5 110 72 905 72 1161 8 1366 2 154 182 4161 0 [0.00] SYN899-1 theorem 1.0 4 14 72 95 72 1185 0 125 2 105 86 380 0 [0.00] SYN900-1 theorem 1.4 4 24 72 92 72 1166 0 219 2 112 96 515 0 [0.17] GRP128-3.005 theorem 0.1 2 7 385 6 46 0 0 62 2 207 1428 868 0 [0.17] SYN480-1 theorem 1.8 3 75 1227 81 1128 728 0 12227 2 66 3853 181860 0 [0.17] SYN820-1 theorem 1.0 5 12 188 504 36 433 71 814 2 371 360 1588 0 [0.17] SYN846-1 theorem 6.8 9 41 376 1590 52 829 24 2473 2 763 741 4584 0 [0.17] SYN862-1 theorem 21.4 19 48 696 2791 72 1648 23 4594 2 1200 1368 8014 0 [0.17] SYN901-1 theorem 1.3 6 11 101 46 101 2051 0 122 2 130 112 230 0 [0.33] SYN448-1 theorem 1.3 3 101 1323 107 1246 889 0 16863 2 84 3447 99834 0 [0.33] SYN850-1 theorem 35.8 18 78 696 5543 72 1649 85 8624 2 1342 1398 15578 0 [0.33] SYN861-1 theorem 25.1 18 59 696 3750 72 1654 47 5206 2 1152 1379 10119 0 [0.33] SYN866-1 theorem 149.5 21 337 696 19985 72 1659 177 34492 2 1172 1657 63770 0 [0.50] PUZ037-3 theorem 0.8 15 1 207 0 2 0 0 0 2 207 3717 0 0 [0.50] SYN447-1 theorem 19.9 9 125 3070 163 2644 1480 0 134513 2 117 10230 1752487 0 [0.50] SYN460-1 theorem 7.4 4 129 2056 143 1875 1131 0 118919 2 99 9600 443131 0 [0.50] SYN470-1 theorem 3.2 3 121 2149 126 1948 1262 0 34294 2 106 6746 192312 0 [0.50] SYN472-1 theorem 3.6 3 89 1537 91 1367 871 0 38259 2 76 6256 318041 0 [0.50] SYN473-1 theorem 3.0 3 91 1444 94 1282 831 0 24522 2 81 6744 279623 0 [0.50] SYN474-1 theorem 1.8 3 82 1406 86 1234 803 0 15857 2 71 4949 143118 0 [0.50] SYN476-1 theorem 1.1 3 75 1612 81 1460 934 0 5607 2 88 4796 59786 0 [0.50] SYN481-1 theorem 1.4 3 63 900 72 818 543 0 17987 2 70 2958 125717 0 [0.50] SYN487-1 theorem 7.1 4 250 4223 273 3758 2449 0 76860 2 95 17236 373891 0 [0.50] SYN488-1 theorem 4.9 4 159 2826 174 2542 1572 0 40381 2 91 11641 317102 0 [0.50] SYN489-1 theorem 0.6 3 50 1139 52 1018 729 0 3134 2 77 3735 32838 0 [0.50] SYN498-1 theorem 1.6 3 64 886 66 820 563 0 12910 2 63 3378 157244 0 [0.50] SYN503-1 theorem 0.7 3 44 495 50 473 343 0 8027 2 68 2162 38687 0 [0.50] SYN511-1 theorem 1.4 3 85 1085 96 984 677 0 13969 2 87 7692 42096 0 [0.67] GRP128-2.006 theorem 0.1 2 8 466 7 56 0 0 143 2 252 1745 1754 0 [0.67] SYN440-1 theorem 49.3 4 507 7374 711 6828 3876 0 683930 2 118 86750 2306224 0 [0.67] SYN457-1 theorem 40.5 6 389 7742 519 6897 3924 0 609262 2 136 34335 1492965 0