vmpc_34.renamed-as.sat05-1926.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
1156	194072	99.96	0.09	39.37	0.04	39.31

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	99.93	0.16	33.25	0.07	33.16	0	89794	46	89794	46	59703367	523.826	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	99.96	0.09	39.37	0.04	39.31	0	0	0	0	0	2520	0.108983	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	99.95	0.12	52.33	0.05	52.26	0	48073	25	48073	25	48625453	466.864	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	99.96	0.09	39.37	0.04	39.31	0	0	0	0	0	2520	0.104984	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	99.95	0.12	49.94	0.05	49.87	0	55038	28	55038	28	50680472	461.151	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	99.96	0.09	39.37	0.04	39.31	0	0	0	0	0	2520	0.113982	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	99.95	0.12	52.33	0.05	52.26	0	48073	25	48073	25	48625453	468.066	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	99.96	0.09	39.37	0.04	39.31	0	0	0	0	0	2520	0.113982	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut