-------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------- Rating Problem Result CPU Memory Close Assert Split Subsume Resolve Compact Prod. D.Bound Ct.Size Ass.Cd. Spl.Cd. Debug [0.00] SYN312-1 theorem 5.2 6 1 2445 0 3 0 0 0 3 2445 38856 0 0 [0.12] LCL195-1 theorem 14.3 7 1 5038 0 6 0 0 0 6 5038 26441 0 0 [0.12] SYN597-1 theorem 0.3 4 1 135 0 11 0 0 0 4 135 3760 0 0 [0.12] SYN602-1 theorem 0.1 2 1 81 0 7 0 0 0 3 81 565 0 0 [0.25] LCL068-1 theorem 14.7 5 1 612 0 4 0 18 0 5 612 45060 0 0 [0.25] LCL225-1 theorem 14.1 5 1 3123 0 6 0 0 0 6 3123 12887 0 0 [0.25] PLA004-2 timeout 500.0 59 [0.25] PLA005-2 timeout 500.0 59 [0.25] PLA009-2 timeout 500.0 59 [0.25] PLA011-1 timeout 500.0 59 [0.25] PLA021-1 timeout 500.0 59 [0.25] PUZ039-1 timeout 500.0 467 [0.25] PUZ040-1 timeout 500.0 472 [0.25] PUZ042-1 timeout 500.1 452 [0.25] RNG001-5 theorem 0.5 2 1 55 0 8 0 0 0 2 55 11718 0 0 [0.25] SYN311-1 theorem 2.1 11 1 13067 0 2 0 0 0 3 13067 40554 0 0 [0.25] SYN603-1 theorem 18.5 23 1 859 0 7 0 0 0 4 859 80480 0 0 [0.25] SYN653-1 timeout 500.0 4 [0.25] SYN704-1 timeout 500.0 117 [0.25] SYN708-1 timeout 500.0 27 [0.38] LCL052-1 theorem 0.5 2 1 130 0 4 0 7 0 5 130 5009 0 0 [0.38] PLA023-1 timeout 500.0 59 [0.38] RNG001-2 theorem 1.1 3 1 73 0 7 0 3 0 2 73 23415 0 0 [0.38] RNG004-3 timeout 500.0 270 [0.38] SWV014-1 timeout 500.0 304 [0.38] SYN711-1 timeout 500.0 42 [0.50] ANA003-2 timeout 500.0 129 [0.50] LCL012-1 theorem 31.1 11 1 410 0 2 0 0 0 7 410 71592 0 0 [0.50] LCL018-1 theorem 95.6 14 1 349 0 2 0 0 0 9 349 66924 0 0 [0.50] LCL191-1 theorem 18.4 8 1 4378 0 6 0 0 0 6 4378 22649 0 0 [0.50] LCL227-1 timeout 500.0 82 [0.50] PLA012-1 timeout 500.0 58 [0.62] LCL166-1 timeout 500.0 83 [0.75] LCL221-1 theorem 27.9 16 1 18689 0 6 0 0 0 6 18689 65074 0 0 [0.75] LCL253-1 timeout 500.0 83