-------------------------------------------------------------------------------- Execute format string : ../darwin -umx true Problems list file : cascj2_hne-problems Output file : cascj2_hne-output Summary file : cascj2_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 129 LCL012-1 theorem 31.1 11 1 410 0 2 0 0 0 7 410 71592 0 0 LCL018-1 theorem 95.6 14 1 349 0 2 0 0 0 9 349 66924 0 0 LCL052-1 theorem 0.5 2 1 130 0 4 0 7 0 5 130 5009 0 0 LCL068-1 theorem 14.7 5 1 612 0 4 0 18 0 5 612 45060 0 0 LCL166-1 timeout 500.0 83 LCL191-1 theorem 18.4 8 1 4378 0 6 0 0 0 6 4378 22649 0 0 LCL195-1 theorem 14.3 7 1 5038 0 6 0 0 0 6 5038 26441 0 0 LCL221-1 theorem 27.9 16 1 18689 0 6 0 0 0 6 18689 65074 0 0 LCL225-1 theorem 14.1 5 1 3123 0 6 0 0 0 6 3123 12887 0 0 LCL227-1 timeout 500.0 82 LCL253-1 timeout 500.0 83 PLA004-2 timeout 500.0 59 PLA005-2 timeout 500.0 59 PLA009-2 timeout 500.0 59 PLA011-1 timeout 500.0 59 PLA012-1 timeout 500.0 58 PLA021-1 timeout 500.0 59 PLA023-1 timeout 500.0 59 PUZ039-1 timeout 500.0 467 PUZ040-1 timeout 500.0 472 PUZ042-1 timeout 500.1 452 RNG001-2 theorem 1.1 3 1 73 0 7 0 3 0 2 73 23415 0 0 RNG001-5 theorem 0.5 2 1 55 0 8 0 0 0 2 55 11718 0 0 RNG004-3 timeout 500.0 270 SWV014-1 timeout 500.0 304 SYN311-1 theorem 2.1 11 1 13067 0 2 0 0 0 3 13067 40554 0 0 SYN312-1 theorem 5.2 6 1 2445 0 3 0 0 0 3 2445 38856 0 0 SYN597-1 theorem 0.3 4 1 135 0 11 0 0 0 4 135 3760 0 0 SYN602-1 theorem 0.1 2 1 81 0 7 0 0 0 3 81 565 0 0 SYN603-1 theorem 18.5 23 1 859 0 7 0 0 0 4 859 80480 0 0 SYN653-1 timeout 500.0 4 SYN704-1 timeout 500.0 117 SYN708-1 timeout 500.0 27 SYN711-1 timeout 500.0 42