column 1 = type of benchmark column 2 = benchmark name column 3 = machine column 4 = algorithm column 5 = time in m.secs to convert .v to .qdimacs column 6 = sat/unsat column 7 = time by bloqqer in m.secs to generate Skolem functions from qdimacs file column 8 = total time in m.secs NA = Qrat-trim could not solve (Bloqqer could not solve this completely) generated bobsm5378d2_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 36 sat 9191 9229 generated bobsm9234_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 40 sat 5346 5416 generated bobsmcodic_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 182 sat 4175985 4176167 generated bobsmfpu_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 247 sat NA NA generated bobsmhdlc1_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 39 sat 29838 29879 generated eijkbs4863_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 88 sat 43811 43901 generated neclaftp2001_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 385 sat NA NA generated neclaftp2002_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 340 sat NA NA generated neclaftp3001_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 281 sat NA NA generated neclaftp3002_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 215 sat NA NA generated neclaftp4001_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 85 sat NA NA generated neclaftp4002_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 84 sat NA NA generated pdtpmsgigamax_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 32 sat NA NA generated pdtpmsmiim_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 31 sat 7131 7163 generated pdtpmsns3_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 88 sat NA NA generated pdtpmsrotate32_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 33 sat 4872 4906 generated pdtpmssfeistel_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 96 sat NA NA generated pdtpmsvsa16a_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 55 sat 4363 4463 generated pdtvismiim0_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 3273 3297 generated pdtvissoap0_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 38 sat NA NA generated pdtvissoap1_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat NA NA generated pdtvissoap2_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat NA NA generated texasifetch1p1_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 249 270 generated viselevatorp1_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 21 sat 792 814 generated visprodcellp01_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 2350 2374 generated bobsmhdlc2_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 57 sat 20185 20244 generated bobsmhdlc3_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 40 sat 19872 19913 generated bobsmhdlc_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 39 sat 19015 19056 generated eijkbs1512_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 33 sat 7255 7289 generated pdtvismiim1_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 3631 3654 generated pdtvismiim2_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 3260 3284 generated pdtvismiim3_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 3612 3636 generated pdtvismiim4_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 3243 3266 generated pdtvismiim5_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 22 sat 3589 3612 generated pdtvismiim6_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 3258 3281 generated pdtvissfeistel_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 56 sat 192199 192257 generated pdtvisvsa16a00_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1905 1957 generated pdtvisvsa16a01_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1866 1919 generated pdtvisvsa16a02_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1906 1958 generated pdtvisvsa16a03_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 38 sat 2075 2129 generated texasifetch1p2_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 265 286 generated texasifetch1p3_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 21 sat 266 288 generated texasifetch1p4_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 258 280 generated texasifetch1p5_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 268 290 generated texasifetch1p8_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 260 282 generated viselevatorp2_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 969 989 generated viselevatorp3_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 20 sat 602 622 generated visprodcellp03_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 24 sat 1235 1262 generated visprodcellp07_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 23 sat 779 805 generated visprodcellp22_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 24 sat 787 814 generated pdtvisvsa16a04_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 36 sat 1911 1963 generated pdtvisvsa16a05_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1968 2021 generated pdtvisvsa16a06_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1855 1907 generated pdtvisvsa16a07_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1855 1908 generated pdtvisvsa16a08_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 36 sat 1953 2005 generated pdtvisvsa16a09_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1912 1964 generated pdtvisvsa16a10_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1922 1975 generated pdtvisvsa16a11_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1854 1907 generated pdtvisvsa16a12_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1879 1932 generated pdtvisvsa16a13_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1927 1980 generated pdtvisvsa16a14_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1934 1987 generated pdtvisvsa16a15_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1914 1968 generated pdtvisvsa16a16_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1880 1933 generated pdtvisvsa16a17_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1962 2014 generated pdtvisvsa16a18_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1875 1927 generated pdtvisvsa16a19_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1959 2012 generated pdtvisvsa16a20_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1990 2043 generated pdtvisvsa16a21_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1850 1903 generated pdtvisvsa16a22_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1929 1982 generated pdtvisvsa16a23_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1904 1956 generated pdtvisvsa16a24_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1904 1957 generated pdtvisvsa16a25_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1977 2030 generated pdtvisvsa16a26_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1881 1934 generated pdtvisvsa16a27_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1847 1900 generated pdtvisvsa16a29_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1868 1920 generated pdtvisvsa16a31_sat_-1_extra_bit_differing_from_cycle_tseitin.v prolient bloqqer 37 sat 1876 1928