-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv true Problems list file : casc19_ept-problems Output file : casc19_ept-output Summary file : casc19_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 [0.33] GRP127-2.006 theorem 2.4 3 81 2988 135 57 0 0 5073 2 272 19423 66768 28 [0.33] SYN448-1 theorem 4.1 2 394 5611 502 5370 2672 0 0 2 94 20784 171004 109 [0.33] SYN451-1 theorem 5.1 2 383 5304 531 5157 2372 0 0 2 81 22896 341018 149 [0.33] SYN454-1 theorem 10.3 3 331 5124 413 4811 2259 0 0 2 84 20582 874761 83 [0.33] SYN469-1 theorem 5.3 2 399 6289 499 5853 2850 0 0 2 81 26347 363161 101 [0.33] SYN478-1 theorem 4.3 3 222 3854 279 3602 1830 0 0 2 82 16447 264591 58 [0.33] SYN483-1 theorem 3.3 3 217 3252 257 3118 1640 0 0 2 75 12670 245727 41 [0.33] SYN485-1 theorem 2.3 2 239 3648 327 3630 1821 0 0 2 77 13265 215067 89 [0.33] SYN506-1 theorem 5.5 4 166 3532 176 3185 1557 0 0 2 95 14329 422055 11 [0.33] SYN850-1 timeout 500.0 38 [0.33] SYN861-1 theorem 360.1 48 1348 696 55203 72 939 0 11765 2 1649 2668 166722 1171 [0.33] SYN865-1 theorem 12.4 17 36 696 1522 72 939 0 95 2 1076 1356 5572 39 [0.33] SYN866-1 timeout 500.0 43 [0.50] PUZ037-3 theorem 2.7 9 1 560 0 2 0 0 0 2 560 10069 0 0 [0.50] SYN436-1 theorem 150.3 10 2153 20484 3264 21111 9534 0 10672 2 96 130431 7701032 1010 [0.50] SYN442-1 theorem 13.4 3 935 15016 1197 14218 6899 0 0 2 89 60933 810203 263 [0.50] SYN447-1 timeout 500.0 8 [0.50] SYN450-1 theorem 24.1 4 733 11473 915 11032 5164 0 0 2 87 46673 2045203 183 [0.50] SYN452-1 theorem 4.3 2 451 6247 626 6040 2959 0 0 2 80 28940 231251 176 [0.50] SYN465-1 theorem 37.6 6 820 13355 1118 12678 6350 0 0 2 95 60043 3330496 299 [0.50] SYN466-1 timeout 500.0 13 [0.50] SYN467-1 theorem 7.2 3 382 5501 496 5346 2728 0 0 2 72 26465 615791 115 [0.50] SYN473-1 theorem 30.8 5 1316 18402 1845 17498 9934 0 0 2 81 89646 2845279 530 [0.50] SYN476-1 theorem 60.1 8 1376 26165 1650 23931 11477 0 0 2 110 103613 4857530 275 [0.50] SYN486-1 theorem 2.6 3 175 2445 242 2354 1249 0 0 2 72 11737 193866 68 [0.50] SYN488-1 theorem 24.7 4 838 16055 963 14689 7110 0 0 2 96 79429 1518836 126 [0.50] SYN489-1 theorem 7.2 3 145 2149 195 2064 1076 0 0 2 94 10601 514470 51 [0.50] SYN498-1 theorem 2.4 3 143 2369 165 2230 1201 0 0 2 72 9673 249274 23 [0.50] SYN499-1 theorem 18.2 6 605 9557 765 9185 4796 0 0 2 96 48382 1359426 161 [0.50] SYN500-1 theorem 4.4 3 213 3401 265 3247 1766 0 0 2 72 15525 389081 53 [0.50] SYN503-1 theorem 9.6 3 203 2674 274 2587 1451 0 0 2 75 15088 928943 72 [0.50] SYN507-1 theorem 20.2 4 829 18208 959 16566 7690 0 0 2 103 72707 1521179 131 [0.50] SYN508-1 theorem 37.4 4 748 11023 1012 10634 5607 0 0 2 98 65400 2092429 265 [0.67] GRP128-2.006 theorem 5.2 4 408 15736 425 56 0 0 12901 2 262 70474 159334 16 [0.67] SYN457-1 timeout 500.0 10