-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv false Problems list file : casc18_sne-problems Output file : casc18_sne-output Summary file : casc18_sne-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.00] PUZ045-1 non_thm 0.0 2 0 0 1 0 0 0 0 2 1 0 1 0 [0.00] SWV016-1 timeout 500.0 183 [0.00] SYN330-1 timeout 500.0 47 [0.00] SYN351-1 timeout 500.0 29 [0.20] HWV035-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 2 2 0 0 [0.20] HWV036-1 non_thm 0.0 2 0 2 0 2 0 0 0 2 2 2 0 0 [0.20] PUZ046-1 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.20] SYN303-1 timeout 500.0 7 [0.20] SYN754-1 non_thm 0.3 2 0 1 29 1 0 0 498 7 30 1 963 0 [0.40] GRP394-2 timeout 500.0 198 [0.40] HWV036-2 non_thm 0.0 2 0 0 0 0 0 0 0 2 0 0 0 0 [0.40] LCL415-1 memory 299.7 499 [0.40] NLP026-1 non_thm 0.0 2 0 4 5 5 3 0 0 2 9 4 9 0 [0.40] NUM287-1 timeout 500.0 128 [0.40] SYN736-1 non_thm 130.1 3 12 1 74 1 0 0 78868 21 68 1 171235 0 [0.40] TOP010-1 timeout 500.0 110 [0.40] TOP011-1 timeout 500.0 87 [0.40] TOP014-1 timeout 500.0 101 [0.40] TOP016-1 timeout 500.0 97 [0.60] NLP191-1 non_thm 0.0 2 0 33 4 34 4 0 0 2 37 33 66 0 [0.60] NUM288-1 timeout 500.0 149 [0.60] SYN786-1 timeout 500.0 10 [0.60] SYN904-1 timeout 500.0 18 [0.60] SYN907-1 timeout 500.0 27 [0.60] TOP018-1 timeout 500.0 75 [0.80] LCL240-1 timeout 500.0 320 [0.80] LCL248-1 timeout 500.0 179 [0.80] SYN770-1 timeout 500.0 8 [0.80] SYN776-1 timeout 500.0 8 [0.80] SYN806-1 timeout 500.0 11 [0.80] SYN912-1 timeout 500.0 45 [0.80] TOP006-1 timeout 500.0 101 [0.80] TOP009-1 timeout 500.0 306 [0.80] TOP012-1 timeout 500.0 65 [0.80] TOP013-1 timeout 500.0 89