IBM_FV_2004_rule_batch_23_SAT_dat.k80.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
165606	686695	81.66	77.08	77.96	5.47	9.82

zChaff	minisat	SatELite
TimeOut	TimeOut	2293

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	80.40	75.65	76.09	5.80	10.34	2	59116	9	59116	9	156059800	123.968	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	8093.07

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	82.12	77.12	78.02	5.20	10.00	0	3837	1	3837	1	32787470	27.4628	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	81.81	77.21	78.10	5.55	9.96	0	1277	0	1277	0	16952698	15.1857	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	5474.48

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	81.81	77.21	78.10	5.55	9.96	0	1275	0	1275	0	14898480	12.6961	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	5840.25

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	81.61	77.23	77.49	5.40	9.58	2	19904	3	19904	3	107484681	90.4642	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	10525.4

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	82.12	77.12	78.02	5.20	10.00	0	3837	1	3837	1	32530010	27.2859	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	81.81	77.21	78.10	5.55	9.96	0	1277	0	1277	0	16952698	14.7178	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	5546.82

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	81.81	77.21	78.10	5.55	9.96	0	1275	0	1275	0	14898480	12.2941	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	5937.58