\setlength{\unitlength}{0.00058300in}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(4909,2204)(884,-1953)
\thicklines
\put(1201,-511){\circle{618}}
\put(4876,-511){\circle{618}}
\put(5476,-1636){\circle{618}}
\put(4276,-1636){\circle{618}}
\put(1201,-211){\line( 0, 1){450}}
\put(4876,-211){\line( 0, 1){450}}
\put(4426,-1336){\line( 1, 2){300}}
\put(5401,-1336){\line(-3, 5){363.971}}
\put(2551,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}becomes}}}
\put(5326,-1711){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}REJ}}}
\put(4126,-1711){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}ACC}}}
\put(4801,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\exists$}}}
\put(1051,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}REJ}}}
\end{picture}
