-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv true 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 2.3 9 81 2988 135 57 0 0 5073 2 272 19423 66768 28 GRP128-2.006 theorem 5.0 4 408 15736 425 56 0 0 12901 2 262 70474 159334 16 GRP128-3.005 theorem 0.2 3 8 562 8 46 0 0 0 2 209 1876 15925 1 PUZ010-1 theorem 3.1 3 138 2941 210 494 268 0 0 2 205 6438 268732 73 PUZ017-1 memory 378.2 499 PUZ037-2 theorem 0.1 3 1 19 0 2 0 0 0 2 19 338 0 0 PUZ037-3 theorem 2.6 9 1 560 0 2 0 0 0 2 560 10069 0 0 SYN440-1 timeout 500.0 18 SYN447-1 timeout 500.0 8 SYN454-1 theorem 10.0 3 331 5124 413 4811 2259 0 0 2 84 20582 874761 83 SYN457-1 timeout 500.0 11 SYN462-1 theorem 3.8 3 170 2823 238 2777 1382 0 0 2 78 11424 309363 69 SYN466-1 timeout 500.0 13 SYN470-1 theorem 17.8 3 817 13566 1071 12513 6106 0 0 2 117 61750 1136420 255 SYN475-1 theorem 3.9 3 318 4955 402 4803 2540 0 0 2 72 18410 426073 85 SYN483-1 theorem 3.2 3 217 3252 257 3118 1640 0 0 2 75 12670 245727 41 SYN487-1 theorem 66.1 8 1235 21279 1473 19200 9492 0 0 2 110 101997 4759310 239 SYN498-1 theorem 2.3 3 143 2369 165 2230 1201 0 0 2 72 9673 249274 23 SYN500-1 theorem 4.4 4 213 3401 265 3247 1766 0 0 2 72 15525 389081 53 SYN501-1 theorem 2.6 3 165 2176 207 2129 1170 0 0 2 73 10062 236967 43 SYN504-1 theorem 5.5 3 351 5533 516 5378 2989 0 0 2 90 23714 462231 166 SYN507-1 theorem 20.1 4 829 18208 959 16566 7690 0 0 2 103 72707 1521179 131 SYN510-1 theorem 4.1 3 219 2837 278 2782 1593 0 0 2 96 12267 285993 60 SYN813-1 timeout 500.0 27 SYN820-1 theorem 12.4 7 154 188 7912 36 269 0 4570 2 1204 502 27932 99 SYN834-1 theorem 3.7 6 113 188 1943 36 269 0 403 2 495 453 7322 76 SYN844-1 theorem 5.5 7 112 188 2830 36 269 0 1045 2 497 452 13083 193 SYN845-1 timeout 500.0 38 SYN848-1 theorem 3.5 8 26 376 1046 52 489 0 58 2 663 726 3552 50 SYN859-1 theorem 6.2 9 47 376 1912 52 489 0 360 2 709 747 6542 88 SYN876-1 theorem 6.6 5 98 52 626 52 487 0 823 2 127 150 4288 159 SYN883-1 theorem 0.8 4 11 52 70 52 491 0 16 2 85 63 740 4 SYN886-1 theorem 0.8 4 6 72 36 72 909 0 0 2 86 78 542 0 SYN887-1 theorem 1.1 4 5 72 22 72 938 0 0 2 83 77 622 0 SYN900-1 theorem 1.2 4 6 72 57 72 923 0 10 2 106 78 757 12