IBM_FV_2004_rule_batch_30_SAT_dat.k40.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
81384	337709	77.21	74.45	71.37	9.50	8.61

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	77.02	72.67	69.13	8.88	9.47	0	25509	8	25509	8	115475597	97.7381	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	78.42	74.07	71.00	8.34	9.14	0	5224	2	5224	2	22965252	18.2152	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	77.26	74.47	71.43	9.69	9.00	0	287	0	287	0	20721891	16.8994	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	77.26	74.46	71.42	9.69	9.00	0	240	0	240	0	12215826	9.54155	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	77.37	73.10	69.60	8.75	9.32	0	20461	6	20461	6	73754011	58.6371	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	78.41	74.08	70.99	8.35	9.14	0	5182	2	5182	2	22922217	19.812	UNKNOWN

zChaff	minisat	SatELite
TimeOut	2420.23	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	77.25	74.47	71.42	9.70	9.00	0	245	0	245	0	20393481	16.8604	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	6021.4

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	77.25	74.46	71.41	9.70	9.00	0	198	0	198	0	12174698	12.5131	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut