php-070-070.shuffled-as.sat05-1170.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
4900	169120	75.29	74.56	99.96	24.67	25.40

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	11838400	11.6382	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	2925230	2.90356	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	4900	0.103984	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	4900	0.068989	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	4900	0.116982	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	4900	0.069989	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	4900	0.104984	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	75.29	74.56	99.96	24.67	25.40	0	0	0	0	0	4900	0.075988	UNKNOWN

zChaff	minisat	SatELite
0.120982	TimeOut	TimeOut