column1 = benchmark name column2 = Average size of Skolem function in CEGARSKOLEMGEN column3 = Average size of Skolem function in MONOCOMPSKOLEMGEN bobsm5378d2_all_bit_differing_from_cycle_tseitin.v 16272.606445 114401.210938 bobsm5378d2_all_bit_differing_from_true_tseitin.v 9648.242188 90855.390625 bobsm9234_all_bit_differing_from_cycle_tseitin.v 12507.788086 25135.818359 bobsm9234_all_bit_differing_from_true_tseitin.v 9550.272461 197678.781250 bobsmcodic_all_bit_differing_from_cycle_tseitin.v 29695.818359 31684.363281 bobsmcodic_all_bit_differing_from_true_tseitin.v 4907.303223 6264.242188 bobsmfpu_all_bit_differing_from_cycle_tseitin.v 6014.187988 6546.461426 bobsmfpu_all_bit_differing_from_true_tseitin.v 633.358948 4375.880371 bobsmhdlc1_all_bit_differing_from_cycle_tseitin.v 4963.041504 47143.394531 bobsmhdlc1_all_bit_differing_from_true_tseitin.v 4091.750000 40482.187500 bobsmhdlc2_all_bit_differing_from_cycle_tseitin.v 4887.520996 30827.333984 bobsmhdlc2_all_bit_differing_from_true_tseitin.v 4227.020996 28871.875000 bobsmhdlc3_all_bit_differing_from_cycle_tseitin.v 5287.416504 36650.937500 bobsmhdlc3_all_bit_differing_from_true_tseitin.v 4331.666504 30417.125000 bobsmhdlc_all_bit_differing_from_cycle_tseitin.v 4980.562500 32195.937500 bobsmhdlc_all_bit_differing_from_true_tseitin.v 4288.104004 22563.875000 bobtuint00_all_bit_differing_from_cycle_tseitin.v 111308.671875 7763982.500000 bobtuint04_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint05_all_bit_differing_from_cycle_tseitin.v 112584.468750 2407081.500000 bobtuint06_all_bit_differing_from_cycle_tseitin.v 127571.375000 5145786.000000 bobtuint07_all_bit_differing_from_cycle_tseitin.v 112449.031250 2418487.750000 bobtuint08_all_bit_differing_from_cycle_tseitin.v 124482.960938 50000000 bobtuint09_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 eijkbs1512_all_bit_differing_from_cycle_tseitin.v 3850.689697 4929.137695 eijkbs4863_all_bit_differing_from_cycle_tseitin.v 50000000 3353031.500000 kenflashp02_all_bit_differing_from_cycle_tseitin.v 39357.847656 372283.906250 kenflashp02_all_bit_differing_from_true_tseitin.v 51776.910156 224034.609375 neclaftp2001_all_bit_differing_from_true_tseitin.v 165.000000 165.000000 neclaftp2002_all_bit_differing_from_cycle_tseitin.v 1310.125000 1310.125000 neclaftp2002_all_bit_differing_from_true_tseitin.v 165.000000 165.000000 neclaftp3001_all_bit_differing_from_cycle_tseitin.v 738.000000 738.000000 neclaftp3001_all_bit_differing_from_true_tseitin.v 143.000000 143.000000 neclaftp3002_all_bit_differing_from_cycle_tseitin.v 736.000000 736.000000 neclaftp3002_all_bit_differing_from_true_tseitin.v 143.000000 143.000000 neclaftp4001_all_bit_differing_from_cycle_tseitin.v 162.000000 162.000000 neclaftp4001_all_bit_differing_from_true_tseitin.v 23.000000 23.000000 neclaftp4002_all_bit_differing_from_cycle_tseitin.v 163.000000 163.000000 neclaftp4002_all_bit_differing_from_true_tseitin.v 23.000000 23.000000 pdtpmsgigamax_all_bit_differing_from_cycle_tseitin.v 129489.093750 191628.265625 pdtpmsgigamax_all_bit_differing_from_true_tseitin.v 118770.632812 179942.859375 pdtpmsmiim_all_bit_differing_from_cycle_tseitin.v 1146.875000 2138.449951 pdtpmsmiim_all_bit_differing_from_true_tseitin.v 565.549988 1374.824951 pdtpmsns3_all_bit_differing_from_cycle_tseitin.v 188106.093750 9897577.000000 pdtpmsns3_all_bit_differing_from_true_tseitin.v 138113.718750 8937092.000000 pdtpmsrotate32_all_bit_differing_from_cycle_tseitin.v 50000000 1573.324341 pdtpmsrotate32_all_bit_differing_from_true_tseitin.v 50000000 1544.621582 pdtpmssfeistel_all_bit_differing_from_cycle_tseitin.v 38436.234375 65434.574219 pdtpmssfeistel_all_bit_differing_from_true_tseitin.v 37382.218750 53457.132812 pdtpmsvsa16a_all_bit_differing_from_cycle_tseitin.v 29.000000 29.000000 pdtpmsvsa16a_all_bit_differing_from_true_tseitin.v 3.000000 3.000000 pdtvismiim0_all_bit_differing_from_cycle_tseitin.v 1074.074951 1571.324951 pdtvismiim0_all_bit_differing_from_true_tseitin.v 599.025024 999.500000 pdtvismiim1_all_bit_differing_from_cycle_tseitin.v 1077.300049 1612.925049 pdtvismiim1_all_bit_differing_from_true_tseitin.v 601.174988 999.500000 pdtvismiim2_all_bit_differing_from_cycle_tseitin.v 1074.074951 1571.324951 pdtvismiim2_all_bit_differing_from_true_tseitin.v 599.025024 999.500000 pdtvismiim3_all_bit_differing_from_cycle_tseitin.v 1077.300049 1612.925049 pdtvismiim3_all_bit_differing_from_true_tseitin.v 601.174988 999.500000 pdtvismiim4_all_bit_differing_from_cycle_tseitin.v 1088.849976 1650.824951 pdtvismiim4_all_bit_differing_from_true_tseitin.v 601.825012 987.424988 pdtvismiim5_all_bit_differing_from_cycle_tseitin.v 1077.300049 1612.925049 pdtvismiim5_all_bit_differing_from_true_tseitin.v 601.174988 999.500000 pdtvismiim6_all_bit_differing_from_cycle_tseitin.v 1074.074951 1571.324951 pdtvismiim6_all_bit_differing_from_true_tseitin.v 599.025024 999.500000 pdtvissfeistel_all_bit_differing_from_cycle_tseitin.v 50000000 29243.367188 pdtvissfeistel_all_bit_differing_from_true_tseitin.v 21211.412109 27375.353516 pdtvissoap0_all_bit_differing_from_cycle_tseitin.v 407.380951 407.380951 pdtvissoap0_all_bit_differing_from_true_tseitin.v 144.142853 144.142853 pdtvissoap1_all_bit_differing_from_cycle_tseitin.v 407.238098 407.238098 pdtvissoap1_all_bit_differing_from_true_tseitin.v 144.142853 144.142853 pdtvissoap2_all_bit_differing_from_cycle_tseitin.v 407.666656 407.666656 pdtvissoap2_all_bit_differing_from_true_tseitin.v 144.142853 144.142853 pdtvisvsa16a00_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a00_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a01_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a01_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a02_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a02_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a03_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a03_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a04_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a04_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a05_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a05_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a06_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a06_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a07_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a07_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a08_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a08_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a09_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a09_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a10_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a10_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a11_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a11_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a12_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a12_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a13_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a13_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a14_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a14_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a15_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a15_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a16_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a16_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a17_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a17_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a18_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a18_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a19_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a19_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a20_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a20_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a21_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a21_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a22_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a22_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a23_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a23_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a24_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a24_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a25_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a25_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a26_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a26_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a27_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a27_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a29_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a29_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 pdtvisvsa16a31_all_bit_differing_from_cycle_tseitin.v 14.000000 14.000000 pdtvisvsa16a31_all_bit_differing_from_true_tseitin.v 1.000000 1.000000 texasifetch1p1_all_bit_differing_from_cycle_tseitin.v 93.038460 287.038452 texasifetch1p1_all_bit_differing_from_true_tseitin.v 72.692307 273.576935 texasifetch1p2_all_bit_differing_from_cycle_tseitin.v 96.076920 302.961548 texasifetch1p2_all_bit_differing_from_true_tseitin.v 73.346153 273.884613 texasifetch1p3_all_bit_differing_from_cycle_tseitin.v 96.076920 302.961548 texasifetch1p3_all_bit_differing_from_true_tseitin.v 73.346153 273.884613 texasifetch1p4_all_bit_differing_from_cycle_tseitin.v 88.346153 303.038452 texasifetch1p4_all_bit_differing_from_true_tseitin.v 73.346153 273.884613 texasifetch1p5_all_bit_differing_from_cycle_tseitin.v 95.423080 314.115387 texasifetch1p5_all_bit_differing_from_true_tseitin.v 73.076920 273.730774 texasifetch1p8_all_bit_differing_from_cycle_tseitin.v 96.076920 302.961548 texasifetch1p8_all_bit_differing_from_true_tseitin.v 77.730766 264.576935 viselevatorp1_all_bit_differing_from_cycle_tseitin.v 725.607117 18408.072266 viselevatorp1_all_bit_differing_from_true_tseitin.v 1504.714233 19021.927734 viselevatorp2_all_bit_differing_from_cycle_tseitin.v 1106.250000 21876.035156 viselevatorp2_all_bit_differing_from_true_tseitin.v 1504.714233 19021.927734 viselevatorp3_all_bit_differing_from_cycle_tseitin.v 854.642883 21904.322266 viselevatorp3_all_bit_differing_from_true_tseitin.v 1540.857178 20423.357422 visprodcellp01_all_bit_differing_from_cycle_tseitin.v 1562343.125000 50000000 visprodcellp03_all_bit_differing_from_cycle_tseitin.v 1562343.125000 50000000 visprodcellp07_all_bit_differing_from_cycle_tseitin.v 1934536.875000 50000000 visprodcellp22_all_bit_differing_from_cycle_tseitin.v 1934536.875000 50000000 bobsynth00_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth00_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth01_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth01_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth02_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth02_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth04_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth04_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth05_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth05_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth06_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth06_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth07_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth07_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth08_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth08_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth09_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth09_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth10_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth10_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth11_all_bit_differing_from_cycle_tseitin.v 31031.294922 2988632.250000 bobsynth11_all_bit_differing_from_true_tseitin.v 30555.955078 3051950.500000 bobsynth12_all_bit_differing_from_cycle_tseitin.v 32503.705078 3035126.750000 bobsynth12_all_bit_differing_from_true_tseitin.v 28917.455078 3115964.000000 bobsynth13_all_bit_differing_from_cycle_tseitin.v 32503.705078 3035126.750000 bobsynth13_all_bit_differing_from_true_tseitin.v 28917.455078 3115964.000000 bobsynthand_all_bit_differing_from_cycle_tseitin.v 30856.431641 3387289.750000 bobsynthand_all_bit_differing_from_true_tseitin.v 29345.273438 2920478.750000 bobsynthetic2_all_bit_differing_from_cycle_tseitin.v 50000000 167933.265625 bobsynthetic2_all_bit_differing_from_true_tseitin.v 50000000 141692.421875 bobsynthor_all_bit_differing_from_cycle_tseitin.v 30466.091797 3016269.500000 bobsynthor_all_bit_differing_from_true_tseitin.v 29193.044922 3149146.250000 bobtuint10_all_bit_differing_from_cycle_tseitin.v 112593.398438 2422456.500000 bobtuint11_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint12_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint13_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint14_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint15_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint16_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint17_all_bit_differing_from_cycle_tseitin.v 112482.125000 2400489.500000 bobtuint18_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint19_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint20_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint21_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint22_all_bit_differing_from_cycle_tseitin.v 113989.656250 2470492.000000 bobtuint23_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint27_all_bit_differing_from_cycle_tseitin.v 112584.617188 2422456.500000 bobtuint28_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint29_all_bit_differing_from_cycle_tseitin.v 112479.882812 2414585.250000 bobtuint30_all_bit_differing_from_cycle_tseitin.v 119736.570312 8836504.000000 bobtuint31_all_bit_differing_from_cycle_tseitin.v 118342.328125 6101854.500000 bobtuintand_all_bit_differing_from_cycle_tseitin.v 110945.968750 6017271.500000 bobtuintor_all_bit_differing_from_cycle_tseitin.v 109123.312500 7803540.000000 kenflashp12_all_bit_differing_from_cycle_tseitin.v 857.047607 3521.333252 kenflashp12_all_bit_differing_from_true_tseitin.v 900.428589 2841.047607 kenoopp1_all_bit_differing_from_cycle_tseitin.v 1286.166626 4086.541748 kenoopp1_all_bit_differing_from_true_tseitin.v 1403.041626 4656.333496 kenflashp01_all_bit_differing_from_cycle_tseitin.v 1239021.625000 9130125.000000 kenflashp01_all_bit_differing_from_true_tseitin.v 1829179.875000 10080623.000000 kenflashp04_all_bit_differing_from_cycle_tseitin.v 656019.437500 2052766.625000 kenflashp04_all_bit_differing_from_true_tseitin.v 844312.500000 2198642.500000 visprodcellp01_all_bit_differing_from_true_tseitin.v 2217064.250000 50000000 visprodcellp03_all_bit_differing_from_true_tseitin.v 2217064.250000 50000000 visprodcellp07_all_bit_differing_from_true_tseitin.v 2217064.250000 50000000 visprodcellp22_all_bit_differing_from_true_tseitin.v 2217064.250000 50000000 bobsm5378d2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 2934.448242 50000000 bobsm9234_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 673.761292 50000000 bobsmcodic_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 98.989388 50000000 bobsmfpu_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 1927.080078 50000000 bobsmhdlc1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 579.834778 50000000 bobsmhdlc2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 772.769226 50000000 bobsmhdlc3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 807.805176 50000000 bobsmhdlc_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 518.732361 50000000 eijkbs1512_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 3364.893555 50000000 eijkbs4863_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 11154.839844 50000000 neclaftp2001_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 63.454010 50000000 neclaftp2002_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 65.469162 50000000 neclaftp3001_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 108.690948 50000000 neclaftp3002_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 143.549149 50000000 neclaftp4001_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 52.159363 50000000 neclaftp4002_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 49.985062 50.088646 pdtpmsmiim_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 156.707993 50000000 pdtpmsrotate32_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 4341.416504 50000000 pdtpmsvsa16a_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 49.243500 51.193855 pdtvismiim0_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 201.283463 50000000 pdtvismiim1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 216.503937 50000000 pdtvismiim2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 201.283463 50000000 pdtvismiim3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 216.503937 50000000 pdtvismiim4_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 4.393701 50000000 pdtvismiim5_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 216.503937 50000000 pdtvismiim6_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 201.283463 50000000 pdtvissfeistel_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 50000000 50000000 pdtvissoap0_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 3022.785156 50000000 pdtvissoap1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 2959.690186 50000000 pdtvissoap2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 2626.603271 50000000 pdtvisvsa16a00_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a01_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a02_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a03_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.586613 46.263779 pdtvisvsa16a04_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.799213 48.035435 pdtvisvsa16a05_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.566929 47.055119 pdtvisvsa16a06_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.291340 46.818897 pdtvisvsa16a07_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 45.870079 45.799213 pdtvisvsa16a08_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.303150 46.980316 pdtvisvsa16a09_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.279526 45.972443 pdtvisvsa16a10_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 45.685040 45.330708 pdtvisvsa16a11_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a12_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a13_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.618111 46.114174 pdtvisvsa16a14_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.303150 46.275589 pdtvisvsa16a15_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.303150 46.275589 pdtvisvsa16a16_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a17_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.692913 46.645668 pdtvisvsa16a18_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 49.645668 50.870079 pdtvisvsa16a19_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.192913 46.047245 pdtvisvsa16a20_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.653542 46.586613 pdtvisvsa16a21_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a22_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a23_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a24_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a25_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a26_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a27_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 46.795277 48.031498 pdtvisvsa16a29_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 45.897636 45.826771 pdtvisvsa16a31_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 47.748032 48.196850 texasifetch1p1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 17.465117 23.116280 texasifetch1p2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 10.313953 22.127907 texasifetch1p3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 18.860466 32.627907 texasifetch1p4_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 9.465117 50000000 texasifetch1p5_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 21.709303 28.255814 texasifetch1p8_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 21.500000 28.523256 viselevatorp1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 1392.594238 50000000 viselevatorp2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 1397.536255 5468988.500000 viselevatorp3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 1382.869507 5003501.000000 visprodcellp01_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 1862119.000000 50000000 visprodcellp03_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 2689744.250000 50000000 visprodcellp07_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 2689744.250000 50000000 visprodcellp22_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v 2689744.250000 50000000