-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv false Problems list file : casc19_hne-problems Output file : casc19_hne-output Summary file : casc19_hne-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] LCL225-1 theorem 46.1 58 1 20344 0 6 0 0 0 6 20344 70277 0 0 [0.25] LCL256-1 theorem 0.2 2 1 116 0 4 0 7 0 5 116 4228 0 0 [0.25] PLA009-2 timeout 500.0 57 [0.25] PLA021-1 timeout 500.0 56 [0.25] PUZ039-1 timeout 500.0 271 [0.25] PUZ040-1 timeout 500.0 290 [0.25] PUZ042-1 timeout 500.0 277 [0.25] RNG001-5 theorem 0.9 3 1 70 0 8 0 0 0 2 70 18027 0 0 [0.25] SYN311-1 theorem 3.7 13 1 13067 0 2 0 0 0 3 13067 40552 0 0 [0.38] LCL016-1 theorem 18.1 24 1 677 0 2 0 0 0 8 677 214615 0 119307 [0.38] LCL389-1 theorem 97.5 13 1 1050 0 4 0 18 0 5 1050 143573 0 22907 [0.38] PLA016-1 timeout 500.0 57 [0.38] RNG001-2 theorem 37.2 45 1 182 0 7 0 20 0 2 182 758445 0 383626 [0.38] RNG004-3 timeout 500.0 285 [0.38] SWV014-1 timeout 500.0 222 [0.38] SYN617-1 timeout 500.0 209 [0.50] LCL127-1 theorem 51.6 34 1 945 0 2 0 5 0 7 945 399790 0 213682 [0.50] LCL223-1 theorem 39.8 70 1 22869 0 6 0 0 0 6 22869 77454 0 0 [0.62] LCL222-1 theorem 43.4 62 1 20763 0 6 0 0 0 6 20763 71531 0 0 [0.62] SYN614-1 timeout 500.0 270