IBM_FV_2004_rule_batch_30_SAT_dat.k25.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
50004	206879	77.36	74.65	71.55	9.43	8.51

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	77.20	72.91	69.36	8.97	9.63	0	15384	7	15384	7	67472087	52.516	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	78.57	74.28	71.18	8.43	9.30	0	3169	2	3169	2	13513827	10.8983	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	77.42	74.67	71.61	9.77	9.16	0	182	0	182	0	12158541	9.42257	UNKNOWN

zChaff	minisat	SatELite
TimeOut	8550.13	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	77.42	74.66	71.60	9.77	9.16	0	150	0	150	0	7163901	5.69413	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	77.55	73.34	69.83	8.84	9.48	0	12301	6	12301	6	43355701	33.8958	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	78.56	74.29	71.17	8.44	9.30	0	3142	2	3142	2	13487397	10.8114	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	77.41	74.67	71.60	9.78	9.16	0	155	0	155	0	11966496	9.45956	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	77.41	74.66	71.59	9.78	9.16	0	123	0	123	0	7139378	5.71313	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut