-------------------------------------------------------------------------------- Execute format string : ../darwin -b 2 -ubj true -uv false Problems list file : casc18_hne-problems Output file : casc18_hne-output Summary file : casc18_hne-summary Time limit : 500 s Memory limit : 500 MB -------------------------------------------------------------------------------- Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug ANA003-2 timeout 500.0 109 GEO002-4 theorem 0.0 2 1 16 0 3 0 5 0 2 16 73 0 0 GRP048-2 theorem 14.0 19 1 156 0 5 0 0 0 3 156 200231 0 130800 LCL012-1 theorem 8.5 15 1 507 0 2 0 0 0 7 507 105286 0 43216 LCL024-1 theorem 140.3 86 1 1622 0 2 0 0 0 8 1622 1096514 0 667102 LCL030-1 theorem 27.4 10 1 573 0 5 0 14 0 5 573 73990 0 7147 LCL048-1 theorem 0.2 2 1 125 0 4 0 3 0 5 125 3155 0 0 LCL191-1 theorem 21.2 16 1 4390 0 6 0 0 0 6 4390 22438 0 0 LCL223-1 theorem 40.6 70 1 22869 0 6 0 0 0 6 22869 77454 0 0 LCL224-1 theorem 109.8 72 1 21798 0 6 0 67 0 6 21798 104514 0 27018 LCL225-1 theorem 46.4 58 1 20344 0 6 0 0 0 6 20344 70277 0 0 LCL227-1 timeout 500.0 328 LCL249-1 timeout 500.0 318 LCL253-1 timeout 500.0 330 LCL402-1 theorem 0.7 3 1 188 0 4 0 11 0 5 188 8613 0 0 LCL416-1 theorem 25.6 18 1 365 0 2 0 0 0 10 365 68100 0 41875 LCL417-1 timeout 500.0 188 NUM017-1 timeout 500.0 120 PLA008-1 timeout 500.0 56 PLA010-1 timeout 500.0 56 PLA015-1 timeout 500.0 56 PLA018-1 timeout 500.0 56 PUZ042-1 timeout 500.0 275 RNG001-5 theorem 1.0 3 1 70 0 8 0 0 0 2 70 18027 0 0 RNG004-3 timeout 500.0 278 RNG039-2 theorem 1.1 4 1 64 0 50 0 11 0 2 64 23226 0 0 SYN556-1 timeout 500.0 11 SYN597-1 theorem 0.3 3 1 193 0 11 0 0 0 4 193 4841 0 0 SYN600-1 timeout 500.0 176 SYN601-1 theorem 0.2 3 1 127 0 12 0 0 0 4 127 3595 0 0 SYN602-1 theorem 0.2 2 1 114 0 7 0 0 0 3 114 791 0 0 SYN616-1 theorem 0.2 3 1 85 0 13 0 0 0 3 85 3860 0 0 SYN628-1 theorem 0.1 2 1 66 0 15 0 0 0 3 66 2584 0 0 SYN631-1 timeout 500.0 92 SYN653-1 timeout 500.0 2