IBM_FV_2004_rule_batch_30_SAT_dat.k35.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
70924	294099	77.24	74.50	71.41	9.48	8.58

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	77.06	72.73	69.18	8.90	9.51	0	22134	8	22134	8	99387077	80.7097	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	78.45	74.12	71.04	8.36	9.18	0	4539	2	4539	2	19810027	15.5336	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	77.29	74.52	71.47	9.71	9.04	0	252	0	252	0	17862616	14.1299	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	77.30	74.50	71.46	9.71	9.04	0	210	0	210	0	10527251	8.09477	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	77.41	73.16	69.66	8.77	9.36	0	17741	6	17741	6	63607466	50.1434	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	78.44	74.13	71.03	8.37	9.17	0	4502	2	4502	2	19772527	15.3747	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	77.29	74.52	71.47	9.72	9.04	0	215	0	215	0	17579661	14.1249	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	1657.66

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	77.29	74.51	71.46	9.72	9.04	0	173	0	173	0	10491658	8.59969	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut