IBM_FV_2004_rule_batch_30_SAT_dat.k55.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
112764	468539	77.14	74.36	71.30	9.52	8.64

zChaff	minisat	SatELite
TimeOut	4504.05	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	76.93	72.56	69.02	8.84	9.40	0	35634	8	35634	8	164265257	134.77	UNKNOWN

zChaff	minisat	SatELite
TimeOut	5313.74	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	78.35	73.98	70.91	8.30	9.07	0	7279	2	7279	2	32459427	28.4787	UNKNOWN

zChaff	minisat	SatELite
TimeOut	8181.16	1597.49

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	77.19	74.38	71.36	9.66	8.93	0	392	0	392	0	29328666	25.2512	UNKNOWN

zChaff	minisat	SatELite
TimeOut	2443	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	77.19	74.37	71.35	9.66	8.93	0	330	0	330	0	17309151	14.9887	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	77.29	73.00	69.50	8.71	9.25	0	28621	6	28621	6	104276296	89.7874	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	78.34	73.99	70.91	8.31	9.07	0	7222	2	7222	2	32399787	28.3757	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	77.18	74.38	71.35	9.67	8.93	0	335	0	335	0	28863891	24.8822	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	1683.72

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	77.18	74.37	71.34	9.67	8.93	0	273	0	273	0	17251418	15.1427	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut