Аннотация:Рассматриваются логико-автоматные формулы, построенные с помощью логических связок из равенств автоматных термов. Для формул данного типа формулируется проблема выполнимости по функциональным (автоматным) переменным. При этом предполагается, что все предметные переменные (по двоичным сверхсловам) находятся под кванторами общности. Строится алгоритм, основанный на переборе частичных недетерминированных автоматов, который решает данную проблему.