F=QFFRD(V)
[Quantifier-free formula read.  V is a variable list of length 
r>=1.  A q.f.f. whose variables all occur in V is read from the 
input stream and assigned to F.]
     const ANDOP=10, OROP=11, EQOP=1.
     safe C.
(1)  [Read first term.]  C=CREADB();  if BEGAF(C)==1
     then { BKSP;  F#=QFFRDA(V) } else if C=='(' then
     {  F#=QFFRD(V); if CREADB()~=')' then
     { print "right parenthesis expected";  go to 5 }  }
     else { print "unexpected character";  go to 5 };
     F=LIST1(F#);  C=CREADB().
(2)  [Next disjunct.]  if C==')'|C=='$' then go to 4;
     if C=='&' then { ADV(F;G#,F);  G=LIST1(G#);  go to 3 };
     if C=='|' then {   C=CREADB();  if BEGAF(C)==1 then
     { BKSP;  F#=QFFRDA(V) } else if C=='(' then
     {  F#=QFFRD(V);  if CREADB()~=')' then
     { print "right parenthesis expected";  go to 5 }  }
     else { print "unexpected character";  go to 5 };
     F=COMP(F#,F);  C=CREADB();  go to 2   };  
     print "unexpected character";  go to 5.
(3)  [Next conjunct.]  if C=='|'|C=')'|C='$' then
     { G=INV(G);  G=COMP(ANDOP,G);  F=COMP(G,F);
     go to 2 };  if C=='&' then {   C=CREADB();
     if BEGAF(C)==1 then { BKSP;  G#=QFFRDA(V) } else
     if C=='(' then {  G#=QFFRD(V);  
     if CREADB()~=')' then 
     { print "right parenthesis expected";  go to 5 }  }
     else { print "unexpected character";  go to 5 };
     G=COMP(G#,G);  C=CREADB();
     go to 3   };  print "unexpected character";  go to 5.
(4)  [Exit.]  if C==')' then BKSP;  if LENGTH(F)==1 then
     F=FIRST(F) else { F=INV(F); F=COMP(OROP,F) };
     return.
(5)  [Error exit.]  DIBUFF;  print "reading through next $";
     while C~='$' do C=CREADB();
     print "the q.f.f. 0=0 returned";  F=LIST2(EQOP,0);
     return..