php-035-035.shuffled-as.sat05-1165.cnf

variables	clauses	Horn %	ReverseHorn %	Binaire %	Pos %	Neg %
1225	20860	74.77	75.01	99.83	25.06	24.82

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rc	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	730100	0.316951	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcn	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	182420	0.082987	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcb	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	1225	0.009998	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcnb	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	1225	0.008998	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcw	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	1225	0.014997	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwn	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	1225	0.007998	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwb	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	1225	0.012998	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut

simplif	% horn	% Rhorn	Binaire %	Pos %	Neg %	var sup	cla sup	%	cla red	%	pu	time	resultat
rcwnb	74.77	75.01	99.83	25.06	24.82	0	0	0	0	0	1225	0.007998	UNKNOWN

zChaff	minisat	SatELite
0.009998	TimeOut	TimeOut