-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv false Problems list file : casc18_heq-problems Output file : casc18_heq-output Summary file : casc18_heq-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] BOO017-1 timeout 500.0 289 [0.00] CAT002-1 theorem 0.7 2 1 297 0 11 0 0 0 2 297 14241 0 0 [0.00] HEN003-1 theorem 61.2 44 1 124 0 5 0 3 0 3 124 1642972 0 167955 [0.00] HEN003-2 theorem 74.9 52 1 130 0 7 0 4 0 3 130 2176594 0 191609 [0.00] HEN005-4 theorem 22.6 11 1 1227 0 12 0 39 0 3 1227 172790 0 45571 [0.00] HEN006-1 timeout 500.0 227 [0.00] HEN006-2 timeout 500.0 281 [0.00] HEN006-6 timeout 500.0 60 [0.00] HEN006-7 timeout 500.0 228 [0.00] HEN007-1 timeout 500.0 216 [0.00] HEN010-7 timeout 500.0 288 [0.00] HEN012-1 theorem 40.2 24 1 117 0 5 0 0 0 3 117 833106 0 91297 [0.00] HWC001-1 timeout 500.0 136 [0.00] LCL109-5 theorem 0.1 2 1 142 0 17 7 102 0 3 142 3020 0 0 [0.00] RNG005-1 theorem 8.5 12 1 182 0 10 0 3 0 2 182 144490 0 65056 [0.00] RNG008-6 timeout 500.0 299 [0.17] BOO008-1 timeout 500.0 160 [0.17] BOO015-1 timeout 500.0 193 [0.17] CAT011-4 theorem 1.0 4 1 411 0 6 0 0 0 4 411 11358 0 0 [0.17] CAT018-4 theorem 9.0 10 1 1380 0 7 0 2 0 4 1380 59959 0 18860 [0.17] COL003-2 timeout 500.0 69 [0.17] COL042-5 timeout 500.0 78 [0.17] GRP002-1 timeout 500.0 89 [0.17] HEN004-2 timeout 500.0 128 [0.17] LAT005-5 timeout 500.0 252 [0.33] COL044-2 timeout 500.0 100 [0.33] COL044-3 timeout 500.0 101 [0.33] HWC003-2 timeout 500.0 258 [0.50] LCL300-3 timeout 500.0 313 [0.67] ANA004-1 timeout 500.0 56 [0.67] COL006-3 timeout 500.0 65 [0.67] COL044-5 timeout 500.0 101 [0.67] HWV002-1 timeout 500.0 231 [0.67] LCL152-1 timeout 500.0 123 [0.83] LAT002-1 timeout 500.0 94