php-040-040.shuffled-as.sat05-1166.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
1600	31240	73.19	76.68	99.87	26.68	23.19

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1249600	0.581911	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	291360	0.137979	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1600	0.016997	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1600	0.010998	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1600	0.019996	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1600	0.011998	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1600	0.015997	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	73.19	76.68	99.87	26.68	23.19	0	0	0	0	0	1600	0.014997	UNKNOWN

zChaff	minisat	SatELite
0.015997	TimeOut	TimeOut