-------------------------------------------------------------------------------- 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 82 [0.25] ANA004-4 timeout 500.0 213 [0.25] SET012-2 theorem 0.1 4 3 215 6 6 0 0 1 2 150 2617 1988 1 [0.25] SET015-1 timeout 500.0 21 [0.25] SYN036-3 theorem 0.0 4 10 69 9 100 156 8 0 2 18 116 79 0 [0.25] SYN037-1 theorem 0.0 4 9 69 8 100 170 11 0 2 17 112 76 0 [0.25] SYN690-1 timeout 500.0 25 [0.38] ANA002-1 timeout 500.0 69 [0.38] COM003-1 theorem 4.0 4 895 7849 5795 312 178 0 0 2 422 29440 154151 4890 [0.38] FLD041-4 theorem 0.5 4 1 425 0 10 0 0 0 2 425 14906 5433 0 [0.38] FLD062-3 theorem 120.0 33 1 1215 0 7 0 0 0 2 1215 325953 109262 0 [0.38] SYN784-1 theorem 3.2 4 60 2 342 2 0 0 21364 4 31 2 61373 6 [0.38] SYN796-1 theorem 0.9 4 36 2 157 2 0 0 4493 3 16 2 21426 0 [0.50] SYN067-1 theorem 14.3 4 420 5258 528 551 1090 0 58769 2 54 18405 409772 100 [0.62] SYN067-2 theorem 27.7 4 732 10527 875 955 969 0 94165 2 60 29932 831895 135 [0.62] SYN067-3 theorem 6.1 4 451 6823 555 600 503 0 30681 2 72 16174 332702 96 [0.62] SYN762-1 theorem 20.7 4 173 1 964 1 0 0 149757 8 30 1 335459 8 [0.75] FLD028-1 timeout 500.0 22 [0.75] SYN802-1 timeout 500.0 8 [0.88] FLD050-3 timeout 500.0 51