IBM_FV_2004_rule_batch_30_SAT_dat.k75.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
154604	642979	77.09	74.30	71.24	9.54	8.67

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	76.88	72.48	68.95	8.81	9.35	0	49134	8	49134	8	230541037	193.361	UNKNOWN

zChaff	minisat	SatELite
TimeOut	5666.77	8813.08

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	78.31	73.92	70.86	8.27	9.02	0	10019	2	10019	2	45184827	38.4072	UNKNOWN

zChaff	minisat	SatELite
TimeOut	9503.74	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	77.14	74.32	71.30	9.63	8.89	0	532	0	532	0	40871916	36.4155	UNKNOWN

zChaff	minisat	SatELite
TimeOut	4382.1	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	77.14	74.31	71.29	9.63	8.88	0	450	0	450	0	24164651	21.1858	UNKNOWN

zChaff	minisat	SatELite
TimeOut	800.225	2570.88

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	77.23	72.92	69.43	8.68	9.20	0	39501	6	39501	6	145165526	128.207	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	78.30	73.92	70.85	8.28	9.02	0	9942	2	9942	2	45103047	39.702	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	77.13	74.32	71.29	9.64	8.88	0	455	0	455	0	40225321	35.8895	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	478.64

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	77.13	74.31	71.28	9.64	8.88	0	373	0	373	0	24084778	21.6217	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	1303.3