OKgenerator_s0=32s1=18n=12000l=3cp=50400-Dnr0=0nr1=2-o.shuffled-as.sat05-1660.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
12000	50400	49.90	50.10	0.00	12.69	12.73

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	151286	0.320951	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	75500	0.172973	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	151286	0.315951	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	75500	0.164974	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	0	0.049992	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	0	0.036994	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	0	0.045993	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	49.90	50.10	0.00	12.69	12.73	0	0	0	0	0	0	0.033994	UNKNOWN

zChaff	minisat	SatELite
TimeOut	TimeOut	TimeOut