IBM_FV_2004_rule_batch_30_SAT_dat.k65.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
133684	555759	77.11	74.33	71.26	9.54	8.66

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	76.90	72.51	68.98	8.82	9.37	0	42384	8	42384	8	197228447	165.282	UNKNOWN

zChaff	minisat	SatELite
TimeOut	3535.92	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	78.33	73.95	70.88	8.28	9.04	0	8649	2	8649	2	38812627	34.6687	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	77.16	74.34	71.32	9.64	8.91	0	462	0	462	0	35090641	30.0814	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	1173.23

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	77.16	74.33	71.31	9.64	8.91	0	390	0	390	0	20727701	18.4172	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	4125.77

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	77.26	72.95	69.46	8.69	9.22	0	34061	6	34061	6	124693361	111.53	UNKNOWN

zChaff	minisat	SatELite
TimeOut	10803.2	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	78.32	73.95	70.87	8.29	9.04	0	8582	2	8582	2	38741917	34.3528	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	77.15	74.35	71.31	9.65	8.91	0	395	0	395	0	34534956	29.8845	UNKNOWN

zChaff	minisat	SatELite
TimeOut	3485.45	1738.11

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	77.15	74.34	71.31	9.65	8.90	0	323	0	323	0	20658898	18.4932	UNKNOWN

zChaff	minisat	SatELite
TimeOut	8552.73	876.791