Performance Darwin 1.1

The following tests were run on a Pentium IV 2.4 Ghz with 512 MB RAM under SUSe Linux 9.0 on the TPTP version 2.7. The Time/Memory columns give the average time spent on the solved problems - but due to sharing the test computer with other processes these results are not highly reliable. The detailed results are given sorted by name and rating in the Details column. Detailed explanations for the configurations and results are to be published soon.

Darwin configurations

Horn problems without equality

The following tests were run on the 758 Horn problems without equality. The time limit is 300 s, the memory limit 400 MB.

Configuration	Solved	Time	Memory	Theorem	Non Theorem	Out of Memory	Details
Default	626	4.8	5.8	602	24	7	name/rating
--horn-candidates Lookahead	621	4.8	5.0	597	24	6	name/rating
--horn-candidates Use	600	5.3	4.6	579	21	1	name/rating
--restart Reluctant	621	6.7	10.0	597	24	11	name/rating
--lookahead-all true	624	6.5	7.3	600	24	7	name/rating
--iterative-deepening TermWeight	626	8.4	6.3	602	24	6	name/rating

non-Horn problems without equality

The following tests were run on the 1172 non-Horn problems without equality. The time limit is 300 s, the memory limit 400 MB.

Configuration	Solved	Time	Memory	Theorem	Non Theorem	Out of Memory	Details
Darwin (Default)	900	5.0	6.4	555	345	1	name/rating
--restart Eager	887	4.6	6.4	555	332	1	name/rating
--restart Reluctant	872	4.6	7.3	530	342	15	name/rating
--restart Exhaustive	873	4.8	7.4	531	342	13	name/rating
--lookahead-all true	907	4.8	7.6	561	346	9	name/rating
--iterative-deepening TermWeight	833	5.3	6.3	498	335	1	name/rating

Other provers

Horn problems without equality

The following tests were run on the 758 Horn problems without equality. The time limit is 300 s, the memory limit 500 MB (400MB for Darwin).

Configuration	Solved	Time	Memory	Theorem	Non Theorem	Out of Memory	Details
Darwin	626	4.8	5.8	602	24	7	name/rating
DCTP 1.31	572	4.8	8.5	538	34	8	name/rating
DCTP 10.21p	634	7.4	3.6	599	35	0	name/rating
Vampire 7.0	693	14.7	36.8	663	30	8	name/rating
E 0.82	676	2.8	15.2	644	32	42	name/rating
SPASS 2.1	568	9.4	4.2	539	29	0	name/rating

non-Horn problems without equality

The following tests were run on the 1172 non-Horn problems without equality. The time limit is 300 s, the memory limit 500 MB (400MB for Darwin).

Configuration	Solved	Time	Memory	Theorem	Non Theorem	Out of Memory	Details
Darwin	901	4.9	6.4	555	346	1	name/rating
DCTP 1.31	800	6.9	10.0	510	290	32	name/rating
DCTP 10.21p	931	6.2	4.6	589	342	0	name/rating
Vampire 7.0	812	11.6	32.7	636	176	0	name/rating
E 0.82	838	6.5	10.6	604	234	148	name/rating
SPASS 2.1	741	11.7	6.2	521	220	0	name/rating