php-050-050.shuffled-as.sat05-1168.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
2500	61300	75.06	74.98	99.92	24.86	24.94

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	3065000	1.82172	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	764500	0.469928	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	2500	0.030995	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	2500	0.022996	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	2500	0.040993	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	2500	0.024996	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	2500	0.034994	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	75.06	74.98	99.92	24.86	24.94	0	0	0	0	0	2500	0.025996	UNKNOWN

zChaff	minisat	SatELite
0.017998	TimeOut	TimeOut