Algorithm 5
Input:
W.l.o.g assume:, ,.
For and
do begin
If or...or is satisfiable,
then output and halt.
end
output “failure”.
, 
,
. 
and 
do begin 
or...or 
is satisfiable, 
and halt.