-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv false Problems list file : casc19_nne-problems Output file : casc19_nne-output Summary file : casc19_nne-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.25] ANA002-2 timeout 500.0 83 [0.25] ANA004-4 timeout 500.0 242 [0.25] SET012-2 theorem 0.1 2 3 215 6 6 0 0 1 2 150 2617 1988 0 [0.25] SET015-1 timeout 500.0 28 [0.25] SYN036-3 theorem 0.0 2 10 69 9 100 156 8 0 2 18 116 79 0 [0.25] SYN037-1 theorem 0.0 2 9 69 8 100 170 11 0 2 17 112 76 0 [0.25] SYN690-1 timeout 500.0 33 [0.38] ANA002-1 timeout 500.0 71 [0.38] COM003-1 theorem 4.1 4 895 7849 5795 312 178 0 0 2 422 29440 154151 0 [0.38] FLD041-4 theorem 0.5 3 1 425 0 10 0 0 0 2 425 14906 5433 0 [0.38] FLD062-3 theorem 107.9 35 1 1173 0 7 0 0 0 2 1173 305943 96641 197616 [0.38] SYN784-1 theorem 3.0 3 60 2 342 2 0 0 21364 4 31 2 61373 0 [0.38] SYN796-1 theorem 0.8 2 36 2 157 2 0 0 4493 3 16 2 21426 0 [0.50] SYN067-1 theorem 14.1 2 420 5258 528 551 1090 0 58769 2 54 18405 409772 0 [0.62] SYN067-2 theorem 27.6 2 732 10527 875 955 969 0 94165 2 60 29932 831895 0 [0.62] SYN067-3 theorem 6.2 2 451 6823 555 600 503 0 30681 2 72 16174 332702 0 [0.62] SYN762-1 theorem 19.4 3 173 1 964 1 0 0 149757 8 30 1 335459 0 [0.75] FLD028-1 timeout 500.0 23 [0.75] SYN802-1 theorem 219.7 16 518 2 3485 2 0 0 1290873 6 98 2 2816843 115035 [0.88] FLD050-3 timeout 500.0 67