Results

(Luka5, Z22, KB-comm, jimc)  

 

Table: Equality Formulation of Luka5

	otter	roo8	roo16	roo24
run time	3953.73	608.74	316.40	204.87
generated	538331	614588	637223	606136
kept	2493	2484	2419	2414
memory (K)	2554	3353	6003	10378
gen/sec	136	1009	2016	2957
speedups:
proof	1.0	6.5	12.5	19.4
gen/sec	1.0	7.4	14.8	21.7