Darbe pateiktas sekvencinis skaičiavimas skaidaus laiko logikai su until operatoriumi, kuris naudoja efektyvų ciklų radimo mechanizmą. Darbe įrodyta, kad ciklų radimui gali būti naudojamos ne visos, o tiktam tikros specialios išvedimo medžio sekvencijos. Mes naudojame specialius indeksus toms specialioms sekvencijoms aptikti. Šie apribojimai leidžia mums sukonstruoti efektyvią išvedimo paieškos procedūrą, paremtą pristatytu sekvenciniu skaičiavimu.