generated bobsm5378d2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 189 33 377 1850 38.608467 14.899471 5.222222 88 7 13 1 27.909090 931.515137 60614 968 1139 16272.606445 least-occurring-first 1 0 0 0 0 187 59288 27267 27150 117 generated bobsm5378d2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 131 33 277 1314 38.702290 15.679389 5.793893 80 3 13 1 20.484848 563.454529 15582 435 672 9648.242188 least-occurring-first 0 0 0 0 0 111 14799 7291 7155 136 generated bobsm9234_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 230 33 551 3353 49.086956 16.647825 2.517391 303 5 8 1 16.757576 1367.121216 270221 2536 801 12507.788086 least-occurring-first 0 0 0 0 0 242 269178 184112 183332 780 generated bobsm9234_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 220 33 517 3628 57.318180 17.450001 2.672727 306 5 8 1 17.000000 1240.242432 235701 2111 547 9550.272461 least-occurring-first 0 0 0 0 0 217 234939 176200 173383 2817 generated bobsmcodic_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 2533 33 3733 31379 66.608368 18.206079 1.139755 188 9 17 1 87.484848 1028.787842 54233 0 1898 29695.818359 least-occurring-first 0 0 0 0 0 2509 49834 49073 0 49073 generated bobsmcodic_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 2512 33 3733 31358 66.333595 18.158041 1.117436 190 9 17 1 85.060608 255.454544 14739 0 198 4907.303223 least-occurring-first 0 0 0 0 0 2484 12068 11339 0 11339 generated bobsmfpu_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 354 117 596 17789 1838.940674 20.700565 1.132768 14611 7 48 1 3.427351 6014.187988 9138 0 2567 6014.187988 least-occurring-first 1 0 0 0 0 3709 2899 2011 0 2011 generated bobsmfpu_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 254 117 409 16301 1076.720459 14.118111 1.185039 14549 3 48 1 2.572649 633.358948 2767 0 289 633.358948 least-occurring-first 0 0 0 0 0 1758 735 250 0 250 generated bobsmhdlc1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 197 48 464 2531 34.461929 12.822335 1.781726 238 9 7 1 7.208333 265.166656 3723 5 680 4963.041504 least-occurring-first 0 0 0 0 0 192 2851 2634 1294 1340 generated bobsmhdlc1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 234 48 447 2560 32.692307 12.153846 1.666667 234 9 7 1 7.916667 243.416672 2108 7 586 4091.750000 least-occurring-first 0 0 0 0 0 207 1315 1125 803 322 generated bobsmhdlc2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 199 48 464 2527 36.190956 13.587939 1.738693 237 10 7 1 7.208333 262.416656 4081 9 639 4887.520996 least-occurring-first 1 0 0 0 0 200 3232 3035 1793 1242 generated bobsmhdlc2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 194 48 447 2598 36.067009 13.036082 1.768041 233 9 7 1 7.145833 247.666672 2075 5 583 4227.020996 least-occurring-first 0 0 0 0 0 188 1302 1129 787 342 generated bobsmhdlc3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 200 48 476 2564 34.180000 12.675000 1.750000 259 9 8 1 7.270833 269.291656 4043 3 663 5287.416504 least-occurring-first 0 0 0 0 0 290 3089 2834 1076 1758 generated bobsmhdlc3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 200 48 459 2572 35.215000 12.790000 1.825000 259 5 8 1 7.395833 243.770828 2095 3 601 4331.666504 least-occurring-first 0 0 0 0 0 186 1309 1149 885 264 generated bobsmhdlc_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 199 48 465 2535 34.351757 12.834171 1.768844 238 10 7 1 7.125000 267.229156 3817 5 662 4980.562500 least-occurring-first 0 0 0 0 0 192 2964 2786 1340 1446 generated bobsmhdlc_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 209 48 448 2586 34.918659 12.636364 1.751196 233 9 7 1 7.500000 250.604172 2406 5 615 4288.104004 least-occurring-first 0 0 0 0 0 197 1594 1421 1162 259 generated bobtuint00_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 72 70 379 2138 114.805557 37.527779 4.472222 352 9 16 1 4.600000 6001.842773 116491 41 44956 111308.671875 least-occurring-first 0 0 0 0 0 495 71041 68867 66028 2839 generated bobtuint04_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 138898 40 48791 113989.656250 least-occurring-first 0 0 0 0 0 634 89473 86757 84096 2661 generated bobtuint05_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 72 70 379 2138 120.333336 39.347221 4.833333 350 9 16 1 4.971428 6035.957031 161521 41 56912 112584.468750 least-occurring-first 1 0 0 0 0 581 104028 101520 95642 5878 generated bobtuint06_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 74 70 379 2151 111.824326 36.337837 4.202703 352 9 16 1 4.442857 6884.571289 174188 52 58773 127571.375000 least-occurring-first 1 0 0 0 0 649 114766 111800 104751 7049 generated bobtuint07_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 72 70 379 2139 119.513885 39.083332 4.819445 350 9 16 1 4.871428 6019.643066 130762 37 46720 112449.031250 least-occurring-first 1 0 0 0 0 577 83465 81085 72138 8947 generated bobtuint08_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2149 108.136986 35.027397 4.273973 352 7 16 1 4.371428 6728.942871 155985 38 48124 124482.960938 least-occurring-first 0 0 0 0 0 523 107337 104845 96585 8260 generated bobtuint09_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 133004 42 44416 112479.882812 least-occurring-first 1 0 0 0 0 632 87958 85452 79792 5660 generated eijkbs1512_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 164 29 345 2059 90.396339 26.189024 3.030488 264 12 7 1 16.655172 451.655182 3756 44 147 3850.689697 least-occurring-first 0 0 0 0 0 204 3406 2990 1740 1250 generated eijkbs4863_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 372 49 561 4851 83.338707 15.717742 6.623656 510 9 14 1 - 47.979591 7200000 2716 - - least-occurring-first 0 0 0 0 0 1005 0 7040450 7040450 0 generated kenflashp02_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 54 33 102 783 17.333334 3.833333 1.240741 539 7 14 1 2.030303 3402.000000 42451 0 2232 39357.847656 least-occurring-first 0 0 0 0 0 88 40130 39359 0 39359 generated kenflashp02_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 58 33 100 873 15.137931 2.793103 1.224138 689 3 14 1 2.151515 4435.151367 198882 0 2538 51776.910156 least-occurring-first 0 0 0 0 0 161 196181 194977 0 194977 generated neclaftp2001_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3655 32 3369 18511 38.755131 17.920931 1.000000 117 23 1 1 114.218750 165.000000 21444 0 7 165.000000 least-occurring-first 0 0 0 0 0 2914 18526 17819 0 17819 generated neclaftp2002_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3956 32 5963 31073 45.806877 19.553337 1.000000 122 27 1 1 123.625000 1310.125000 50333 0 77 1310.125000 least-occurring-first 0 0 0 0 0 3985 46273 45181 0 45181 generated neclaftp2002_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3721 32 3370 18429 38.590164 17.915613 1.000000 118 23 1 1 116.281250 165.000000 48270 0 8 165.000000 least-occurring-first 1 0 0 0 0 2888 45381 44702 0 44702 generated neclaftp3001_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3230 32 4778 23707 29.091022 13.056966 1.000000 92 27 1 1 100.937500 738.000000 28402 0 41 738.000000 least-occurring-first 0 0 0 0 0 2109 26257 25403 0 25403 generated neclaftp3001_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3108 32 2506 14470 24.967503 12.051802 1.000000 84 23 1 1 97.125000 143.000000 12643 0 7 143.000000 least-occurring-first 0 0 0 0 0 1657 10984 10471 0 10471 generated neclaftp3002_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3353 32 4778 23705 28.796301 13.052490 1.000000 82 27 1 1 104.781250 736.000000 36236 0 42 736.000000 least-occurring-first 0 0 0 0 0 2234 33964 33133 0 33133 generated neclaftp3002_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3190 32 2506 14466 24.857054 12.051724 1.000000 82 23 1 1 99.687500 143.000000 17862 0 6 143.000000 least-occurring-first 0 0 0 0 0 1645 16212 15706 0 15706 generated neclaftp4001_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 568 32 810 3950 29.839788 13.000000 1.000000 35 27 1 1 17.750000 162.000000 874 0 9 162.000000 least-occurring-first 0 0 0 0 0 361 504 379 0 379 generated neclaftp4001_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 558 32 426 2335 26.023298 12.005377 1.000000 32 23 1 1 17.437500 23.000000 530 0 2 23.000000 least-occurring-first 1 0 0 0 0 270 258 179 0 179 generated neclaftp4002_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 557 32 810 3951 29.931778 13.000000 1.000000 36 27 1 1 17.406250 163.000000 851 0 9 163.000000 least-occurring-first 0 0 0 0 0 364 478 352 0 352 generated neclaftp4002_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 561 32 426 2337 25.495544 12.003565 1.000000 32 23 1 1 17.531250 23.000000 521 0 2 23.000000 least-occurring-first 0 0 0 0 0 271 249 169 0 169 generated pdtpmsgigamax_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 115 22 230 1404 270.730438 72.026085 10.913043 433 9 17 1 55.590908 11391.590820 41284 0 6902 129489.093750 least-occurring-first 1 0 0 0 0 816 33568 31769 0 31769 generated pdtpmsgigamax_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 98 22 214 1188 254.418365 67.265305 11.091837 431 5 17 1 45.681820 10411.636719 37402 0 7232 118770.632812 least-occurring-first 0 0 0 0 0 660 29512 27907 0 27907 generated pdtpmsmiim_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 133 40 295 1499 28.127819 10.864661 2.060150 89 7 8 1 6.200000 120.925003 675 2 104 1146.875000 least-occurring-first 0 0 0 0 0 95 476 370 154 216 generated pdtpmsmiim_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 99 40 249 1128 28.747475 11.868687 2.272727 88 3 8 1 5.075000 95.050003 333 2 44 565.549988 least-occurring-first 0 0 0 0 0 75 215 149 77 72 generated pdtpmsns3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 480 21 836 5512 179.368744 53.370834 4.947917 582 9 21 1 109.333336 15586.619141 3059338 3121 9635 188106.093750 least-occurring-first 0 0 0 0 0 1407 3048300 2860990 2518286 342704 generated pdtpmsns3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 407 21 783 4798 189.029480 55.950859 4.921376 581 3 21 1 89.142860 12283.571289 1446562 2729 6591 138113.718750 least-occurring-first 0 0 0 0 0 1066 1438908 1304458 1206128 98330 generated pdtpmsrotate32_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 210 37 295 2061 57.076191 17.161905 2.819048 138 7 5 1 - 16.000000 7200000 20482 - - least-occurring-first 0 0 0 0 0 217 0 3595166 3595166 0 generated pdtpmsrotate32_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 158 37 198 1641 70.221519 20.462025 3.360759 137 3 5 1 - 14.351352 7200000 21289 - - least-occurring-first 0 0 0 0 0 188 0 3441393 3441393 0 generated pdtpmssfeistel_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1008 68 1546 10614 53.975197 17.389881 3.363095 699 12 68 1 49.852940 1263.352905 92939 94 15819 38436.234375 least-occurring-first 0 0 0 0 0 1970 75155 66836 47119 19717 generated pdtpmssfeistel_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 890 68 1546 10584 59.498875 19.040449 3.611236 702 9 68 1 47.264706 1259.044067 74836 188 13360 37382.218750 least-occurring-first 0 0 0 0 0 1848 59632 45973 45649 324 generated pdtpmsvsa16a_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 100 32 166 708 17.280001 7.500000 1.000000 24 13 1 1 3.125000 29.000000 116 0 2 29.000000 least-occurring-first 0 0 0 0 0 53 60 32 0 32 generated pdtpmsvsa16a_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 85 32 108 457 13.752941 6.552941 1.000000 20 9 1 1 2.656250 3.000000 57 0 1 3.000000 least-occurring-first 0 0 0 0 0 29 27 7 0 7 generated pdtvismiim0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 100 40 206 1111 29.360001 11.990000 2.220000 74 9 8 1 5.450000 126.824997 726 32 84 1074.074951 least-occurring-first 0 0 0 0 0 77 564 361 223 138 generated pdtvismiim0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.750000 13.154762 2.238095 72 5 8 1 4.525000 103.599998 503 33 48 599.025024 least-occurring-first 0 0 0 0 0 66 388 200 171 29 generated pdtvismiim1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 97 40 206 1107 28.979382 11.835052 2.175258 74 9 8 1 5.225000 127.849998 755 38 85 1077.300049 least-occurring-first 0 0 0 0 0 70 600 355 292 63 generated pdtvismiim1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.750000 13.154762 2.238095 72 5 8 1 4.525000 103.974998 531 35 47 601.174988 least-occurring-first 0 0 0 0 0 67 417 202 176 26 generated pdtvismiim2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 100 40 206 1111 29.360001 11.990000 2.220000 74 9 8 1 5.450000 126.824997 726 32 85 1074.074951 least-occurring-first 0 0 0 0 0 77 564 358 220 138 generated pdtvismiim2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.750000 13.154762 2.238095 72 5 8 1 4.525000 103.599998 501 33 48 599.025024 least-occurring-first 0 0 0 0 0 68 385 197 168 29 generated pdtvismiim3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 97 40 206 1107 28.979382 11.835052 2.175258 74 9 8 1 5.225000 127.849998 755 38 85 1077.300049 least-occurring-first 0 0 0 0 0 74 596 358 294 64 generated pdtvismiim3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.750000 13.154762 2.238095 72 5 8 1 4.525000 103.974998 607 35 48 601.174988 least-occurring-first 0 0 0 0 0 108 451 204 177 27 generated pdtvismiim4_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 100 40 206 1116 28.879999 11.790000 2.220000 74 9 8 1 5.475000 129.425003 855 45 87 1088.849976 least-occurring-first 0 0 0 0 0 76 692 417 378 39 generated pdtvismiim4_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.452381 13.059524 2.226191 72 5 8 1 4.500000 104.525002 487 35 47 601.825012 least-occurring-first 0 0 0 0 0 64 376 184 178 6 generated pdtvismiim5_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 97 40 206 1107 28.979382 11.835052 2.175258 74 9 8 1 5.225000 127.849998 752 38 86 1077.300049 least-occurring-first 0 0 0 0 0 74 591 351 289 62 generated pdtvismiim5_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.750000 13.154762 2.238095 72 5 8 1 4.525000 103.974998 710 35 48 601.174988 least-occurring-first 0 0 0 0 0 67 596 200 174 26 generated pdtvismiim6_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 100 40 206 1111 29.360001 11.990000 2.220000 74 9 8 1 5.450000 126.824997 731 32 85 1074.074951 least-occurring-first 1 0 0 0 0 78 569 341 206 135 generated pdtvismiim6_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 84 40 187 923 30.750000 13.154762 2.238095 72 5 8 1 4.525000 103.599998 497 33 48 599.025024 least-occurring-first 0 0 0 0 0 68 380 195 167 28 generated pdtvissfeistel_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 610 68 790 5705 51.229507 16.552460 3.447541 612 14 68 1 - 30.926470 7200000 6914 - - least-occurring-first 0 0 0 0 0 1119 0 4442259 4442259 0 generated pdtvissfeistel_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 514 68 790 5847 45.447472 14.992218 3.661479 612 11 68 1 27.676470 691.338257 13921 6 7308 21211.412109 least-occurring-first 0 0 0 0 0 811 5803 5035 2983 2052 generated pdtvissoap0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 185 21 315 2841 49.740540 13.356757 1.140541 135 15 2 1 10.047619 60.428570 338 0 4 407.380951 least-occurring-first 0 0 0 0 0 88 246 204 0 204 generated pdtvissoap0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 174 21 315 2573 46.706898 13.770115 1.166667 134 11 2 1 9.666667 27.952381 193 0 1 144.142853 least-occurring-first 1 0 0 0 0 84 108 71 0 71 generated pdtvissoap1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 176 21 315 2845 50.698864 13.357955 1.136364 135 14 2 1 9.523809 60.428570 352 0 3 407.238098 least-occurring-first 1 0 0 0 0 86 263 221 0 221 generated pdtvissoap1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 172 21 315 2573 46.837208 13.843023 1.191860 133 11 2 1 9.761905 27.952381 187 0 1 144.142853 least-occurring-first 0 0 0 0 0 86 100 64 0 64 generated pdtvissoap2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 182 21 315 2840 52.318680 13.461538 1.120879 135 14 2 1 9.714286 60.428570 360 0 4 407.666656 least-occurring-first 0 0 0 0 0 88 268 227 0 227 generated pdtvissoap2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 178 21 315 2574 46.443821 13.887640 1.157303 134 11 2 1 9.809524 27.952381 187 0 1 144.142853 least-occurring-first 0 0 0 0 0 85 101 65 0 65 generated pdtvisvsa16a00_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 52 0 1 14.000000 least-occurring-first 0 0 0 0 0 27 24 9 0 9 generated pdtvisvsa16a00_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 1 1.000000 least-occurring-first 0 0 0 0 0 15 13 1 0 1 generated pdtvisvsa16a01_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 51 0 1 14.000000 least-occurring-first 0 0 0 0 0 26 24 9 0 9 generated pdtvisvsa16a01_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 2 0 2 generated pdtvisvsa16a02_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 73 0 2 14.000000 least-occurring-first 0 0 0 0 0 28 24 8 0 8 generated pdtvisvsa16a02_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 31 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a03_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.916666 7.625000 1.000000 21 13 1 1 1.500000 14.000000 49 0 2 14.000000 least-occurring-first 0 0 0 0 0 26 21 6 0 6 generated pdtvisvsa16a03_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 31 0 1 1.000000 least-occurring-first 0 0 0 0 0 17 13 1 0 1 generated pdtvisvsa16a04_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 49 0 1 14.000000 least-occurring-first 0 0 0 0 0 26 21 6 0 6 generated pdtvisvsa16a04_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 2 0 2 generated pdtvisvsa16a05_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.916666 7.625000 1.000000 21 13 1 1 1.500000 14.000000 49 0 1 14.000000 least-occurring-first 1 0 0 0 0 27 21 7 0 7 generated pdtvisvsa16a05_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 45 32 70 236 12.911111 6.533333 1.000000 17 9 1 1 1.406250 1.000000 32 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 2 0 2 generated pdtvisvsa16a06_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.541666 7.437500 1.000000 21 13 1 1 1.500000 14.000000 50 0 2 14.000000 least-occurring-first 1 0 0 0 0 26 21 6 0 6 generated pdtvisvsa16a06_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 15 13 1 0 1 generated pdtvisvsa16a07_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 46 32 99 361 17.043478 7.630435 1.000000 21 13 1 1 1.437500 14.000000 45 0 1 14.000000 least-occurring-first 0 0 0 0 0 25 19 5 0 5 generated pdtvisvsa16a07_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 2 0 2 generated pdtvisvsa16a08_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 32 99 361 17.046511 7.534883 1.000000 21 13 1 1 1.343750 14.000000 46 0 1 14.000000 least-occurring-first 0 0 0 0 0 25 20 4 0 4 generated pdtvisvsa16a08_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 12 2 0 2 generated pdtvisvsa16a09_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 46 32 99 361 17.043478 7.630435 1.000000 21 13 1 1 1.437500 14.000000 45 0 2 14.000000 least-occurring-first 0 0 0 0 0 25 18 5 0 5 generated pdtvisvsa16a09_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 2 1.000000 least-occurring-first 0 0 0 0 0 15 12 1 0 1 generated pdtvisvsa16a10_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 46 0 1 14.000000 least-occurring-first 1 0 0 0 0 25 21 6 0 6 generated pdtvisvsa16a10_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 12 2 0 2 generated pdtvisvsa16a11_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 53 32 99 361 16.698112 7.641510 1.000000 21 13 1 1 1.656250 14.000000 49 0 1 14.000000 least-occurring-first 0 0 0 0 0 29 19 5 0 5 generated pdtvisvsa16a11_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 45 32 70 236 12.911111 6.533333 1.000000 17 9 1 1 1.406250 1.000000 31 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 3 0 3 generated pdtvisvsa16a12_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 50 0 1 14.000000 least-occurring-first 0 0 0 0 0 26 23 8 0 8 generated pdtvisvsa16a12_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a13_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 47 32 99 361 16.531916 7.404255 1.000000 21 13 1 1 1.468750 14.000000 44 0 1 14.000000 least-occurring-first 0 0 0 0 0 25 18 4 0 4 generated pdtvisvsa16a13_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 28 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 12 2 0 2 generated pdtvisvsa16a14_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 99 361 16.909090 7.500000 1.000000 21 13 1 1 1.375000 14.000000 44 0 1 14.000000 least-occurring-first 0 0 0 0 0 24 19 4 0 4 generated pdtvisvsa16a14_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a15_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 99 361 16.909090 7.500000 1.000000 21 13 1 1 1.375000 14.000000 44 0 1 14.000000 least-occurring-first 0 0 0 0 0 24 19 4 0 4 generated pdtvisvsa16a15_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 12 2 0 2 generated pdtvisvsa16a16_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 51 0 1 14.000000 least-occurring-first 0 0 0 0 0 26 23 9 0 9 generated pdtvisvsa16a16_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 1 1.000000 least-occurring-first 1 0 0 0 0 16 12 2 0 2 generated pdtvisvsa16a17_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 50 32 99 361 16.559999 7.500000 1.000000 21 13 1 1 1.562500 14.000000 46 0 1 14.000000 least-occurring-first 0 0 0 0 0 27 18 4 0 4 generated pdtvisvsa16a17_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a18_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 45 32 99 361 16.911112 7.533333 1.000000 21 13 1 1 1.406250 14.000000 45 0 2 14.000000 least-occurring-first 0 0 0 0 0 24 18 4 0 4 generated pdtvisvsa16a18_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 15 12 1 0 1 generated pdtvisvsa16a19_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 49 32 99 361 16.918367 7.653061 1.000000 21 13 1 1 1.531250 14.000000 48 0 1 14.000000 least-occurring-first 0 0 0 0 0 27 20 5 0 5 generated pdtvisvsa16a19_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a20_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 32 99 361 16.767443 7.395349 1.000000 21 13 1 1 1.343750 14.000000 44 0 2 14.000000 least-occurring-first 0 0 0 0 0 24 18 4 0 4 generated pdtvisvsa16a20_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 15 13 1 0 1 generated pdtvisvsa16a21_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 51 0 2 14.000000 least-occurring-first 0 0 0 0 0 25 23 9 0 9 generated pdtvisvsa16a21_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 29 0 1 1.000000 least-occurring-first 0 0 0 0 0 15 13 1 0 1 generated pdtvisvsa16a22_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 75 0 2 14.000000 least-occurring-first 0 0 0 0 0 51 22 7 0 7 generated pdtvisvsa16a22_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 2 0 2 generated pdtvisvsa16a23_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 50 0 2 14.000000 least-occurring-first 0 0 0 0 0 26 23 9 0 9 generated pdtvisvsa16a23_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 31 0 2 1.000000 least-occurring-first 0 0 0 0 0 17 12 1 0 1 generated pdtvisvsa16a24_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 50 0 1 14.000000 least-occurring-first 0 0 0 0 0 25 24 8 0 8 generated pdtvisvsa16a24_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 31 0 1 1.000000 least-occurring-first 0 0 0 0 0 17 13 1 0 1 generated pdtvisvsa16a25_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 93 0 1 14.000000 least-occurring-first 0 0 0 0 0 70 22 7 0 7 generated pdtvisvsa16a25_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a26_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 32 99 361 16.666666 7.500000 1.000000 21 13 1 1 1.500000 14.000000 50 0 2 14.000000 least-occurring-first 0 0 0 0 0 25 23 9 0 9 generated pdtvisvsa16a26_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 31 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a27_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 47 32 99 361 16.404255 7.340425 1.000000 21 13 1 1 1.468750 14.000000 47 0 2 14.000000 least-occurring-first 0 0 0 0 0 25 20 6 0 6 generated pdtvisvsa16a27_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 1 0 0 0 0 16 13 1 0 1 generated pdtvisvsa16a29_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 47 32 99 361 17.042553 7.659575 1.000000 21 13 1 1 1.468750 14.000000 47 0 2 14.000000 least-occurring-first 0 0 0 0 0 26 19 5 0 5 generated pdtvisvsa16a29_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 2 1.000000 least-occurring-first 0 0 0 0 0 15 13 2 0 2 generated pdtvisvsa16a31_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 99 361 16.909090 7.500000 1.000000 21 13 1 1 1.375000 14.000000 45 0 2 14.000000 least-occurring-first 0 0 0 0 0 24 19 4 0 4 generated pdtvisvsa16a31_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 32 70 236 13.045455 6.568182 1.000000 17 9 1 1 1.375000 1.000000 30 0 1 1.000000 least-occurring-first 0 0 0 0 0 16 13 2 0 2 generated texasifetch1p1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 106 462 20.184210 7.894737 2.210526 50 9 11 1 3.230769 42.576923 59 0 3 93.038460 least-occurring-first 0 0 0 0 0 17 39 23 0 23 generated texasifetch1p1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 39 26 93 385 17.512821 7.102564 1.974359 46 5 11 1 2.923077 32.730770 44 0 2 72.692307 least-occurring-first 0 0 0 0 0 15 27 13 0 13 generated texasifetch1p2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 106 462 20.184210 7.815790 2.210526 50 9 11 1 3.230769 42.461540 62 0 3 96.076920 least-occurring-first 0 0 0 0 0 17 42 24 0 24 generated texasifetch1p2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 93 385 17.052631 6.921052 1.947368 46 5 11 1 2.846154 32.884617 46 0 2 73.346153 least-occurring-first 0 0 0 0 0 15 29 15 0 15 generated texasifetch1p3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 39 26 106 462 19.846153 7.717949 2.153846 50 9 11 1 3.230769 42.461540 70 0 2 96.076920 least-occurring-first 0 0 0 0 0 15 53 37 0 37 generated texasifetch1p3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 93 385 17.052631 6.921052 1.947368 46 5 11 1 2.846154 32.884617 46 0 2 73.346153 least-occurring-first 0 0 0 0 0 14 30 15 0 15 generated texasifetch1p4_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 40 26 106 462 19.200001 7.525000 1.925000 50 9 11 1 2.961539 40.730770 59 0 3 88.346153 least-occurring-first 0 0 0 0 0 15 42 26 0 26 generated texasifetch1p4_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 93 385 17.052631 6.921052 1.947368 46 5 11 1 2.846154 32.884617 43 0 2 73.346153 least-occurring-first 1 0 0 0 0 14 27 13 0 13 generated texasifetch1p5_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 106 461 20.736841 7.947369 2.210526 49 9 11 1 3.230769 42.000000 60 0 2 95.423080 least-occurring-first 0 0 0 0 0 16 42 26 0 26 generated texasifetch1p5_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 93 384 17.026316 6.921052 1.947368 45 5 11 1 2.846154 32.730770 45 0 2 73.076920 least-occurring-first 0 0 0 0 0 15 29 15 0 15 generated texasifetch1p8_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 106 462 20.184210 7.815790 2.210526 50 9 11 1 3.230769 42.461540 60 0 2 96.076920 least-occurring-first 0 0 0 0 0 16 42 24 0 24 generated texasifetch1p8_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 38 26 93 385 17.342106 7.052631 2.131579 46 5 11 1 3.115385 33.884617 48 0 2 77.730766 least-occurring-first 0 0 0 0 0 16 30 17 0 17 generated viselevatorp1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 42 28 99 547 22.857143 8.071428 1.261905 151 7 12 1 1.892857 137.714279 143 0 17 725.607117 least-occurring-first 0 0 0 0 0 19 107 81 0 81 generated viselevatorp1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 42 28 93 469 16.714285 6.238095 1.261905 169 3 12 1 1.892857 316.642853 186 0 31 1504.714233 least-occurring-first 0 0 0 0 0 15 140 109 0 109 generated viselevatorp2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 37 28 99 545 24.891891 8.567568 1.297297 151 7 12 1 1.714286 204.428574 222 0 24 1106.250000 least-occurring-first 0 0 0 0 0 18 180 154 0 154 generated viselevatorp2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 42 28 93 469 16.714285 6.238095 1.261905 169 3 12 1 1.892857 316.642853 189 0 30 1504.714233 least-occurring-first 0 0 0 0 0 19 140 109 0 109 generated viselevatorp3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 36 28 99 545 23.944445 8.166667 1.305556 151 7 12 1 1.678571 177.142853 199 0 17 854.642883 least-occurring-first 0 0 0 0 0 17 165 138 0 138 generated viselevatorp3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 42 28 93 470 16.714285 6.238095 1.261905 169 3 12 1 1.892857 240.464279 243 0 33 1540.857178 least-occurring-first 0 0 0 0 0 16 193 161 0 161 generated visprodcellp01_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 30 108 509 12.750000 4.250000 1.604167 257 7 30 1 2.566667 76692.164062 3892716 0 269179 1562343.125000 least-occurring-first 0 0 0 0 0 4491 3619046 3589362 0 3589362 generated visprodcellp03_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 48 30 108 509 12.750000 4.250000 1.604167 257 7 30 1 2.566667 76692.164062 3712551 0 270356 1562343.125000 least-occurring-first 0 0 0 0 0 4335 3437860 3408840 0 3408840 generated visprodcellp07_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 49 30 108 510 12.612245 4.224490 1.591837 258 7 30 1 2.600000 107076.765625 3435406 0 301480 1934536.875000 least-occurring-first 0 0 0 0 0 5374 3128552 3085952 0 3085952 generated visprodcellp22_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 49 30 108 510 12.612245 4.224490 1.591837 258 7 30 1 2.600000 107076.765625 3683532 0 304559 1934536.875000 least-occurring-first 0 0 0 0 0 5966 3373006 3327089 0 3327089 generated bobsynth00_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 232642 32 3340 31031.294922 least-occurring-first 0 0 0 0 0 2827 226479 222951 180342 42609 generated bobsynth00_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 207286 32 3255 30555.955078 least-occurring-first 0 0 0 0 0 2582 201454 198016 139034 58982 generated bobsynth01_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 191671 32 3173 31031.294922 least-occurring-first 0 0 0 0 0 2682 185821 182455 145749 36706 generated bobsynth01_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 211234 32 3362 30555.955078 least-occurring-first 0 0 0 0 0 2581 205297 201779 140266 61513 generated bobsynth02_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 263187 32 3602 31031.294922 least-occurring-first 1 0 0 0 0 2840 256753 253190 202488 50702 generated bobsynth02_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 263997 32 4094 30555.955078 least-occurring-first 1 0 0 0 0 2674 257238 253546 171115 82431 generated bobsynth04_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 208097 32 3169 31031.294922 least-occurring-first 0 0 0 0 0 2735 202200 198780 158727 40053 generated bobsynth04_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 228525 32 3486 30555.955078 least-occurring-first 0 0 0 0 0 2672 222370 218793 151345 67448 generated bobsynth05_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 244461 32 3874 31031.294922 least-occurring-first 0 0 0 0 0 2786 237806 234273 181942 52331 generated bobsynth05_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 275135 32 3525 30555.955078 least-occurring-first 0 0 0 0 0 2850 268764 264900 191577 73323 generated bobsynth06_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 223616 32 3150 31031.294922 least-occurring-first 0 0 0 0 0 2881 217589 214024 176719 37305 generated bobsynth06_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 218527 32 3505 30555.955078 least-occurring-first 0 0 0 0 0 2576 212452 208970 136650 72320 generated bobsynth07_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 242178 32 3254 31031.294922 least-occurring-first 0 0 0 0 0 2805 236125 232564 192829 39735 generated bobsynth07_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 235281 32 3392 30555.955078 least-occurring-first 0 0 0 0 0 2629 229271 225696 160333 65363 generated bobsynth08_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 209100 32 3192 31031.294922 least-occurring-first 0 0 0 0 0 2779 203135 199728 160653 39075 generated bobsynth08_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 230403 32 3361 30555.955078 least-occurring-first 0 0 0 0 0 2670 224378 220824 154896 65928 generated bobsynth09_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 149008 32 3007 31031.294922 least-occurring-first 0 0 0 0 0 2669 143337 140111 109769 30342 generated bobsynth09_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 215583 32 3259 30555.955078 least-occurring-first 0 0 0 0 0 2671 209656 206142 146431 59711 generated bobsynth10_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 201487 32 3156 31031.294922 least-occurring-first 0 0 0 0 0 2785 195552 192150 155314 36836 generated bobsynth10_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 209928 32 3314 30555.955078 least-occurring-first 0 0 0 0 0 2639 203981 200452 139191 61261 generated bobsynth11_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1360 44 2860 15219 70.086761 24.286030 2.684559 2650 9 14 1 81.386360 2830.022705 323744 32 4468 31031.294922 least-occurring-first 0 0 0 0 0 2929 316354 312569 248991 63578 generated bobsynth11_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1428 44 2841 15333 74.254906 23.282213 2.661765 2680 7 14 1 84.250000 2791.477295 237515 32 3515 30555.955078 least-occurring-first 0 0 0 0 0 2666 231336 227709 161436 66273 generated bobsynth12_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1450 44 2860 15219 71.401382 24.646896 2.723448 2649 11 14 1 87.386360 2960.818115 266732 43 3477 32503.705078 least-occurring-first 0 0 0 0 0 3017 260242 255706 186389 69317 generated bobsynth12_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1456 44 2841 15341 73.951233 23.271978 2.636676 2680 7 14 1 85.022728 2642.386475 191265 23 3217 28917.455078 least-occurring-first 0 0 0 0 0 2735 185321 182547 158467 24080 generated bobsynth13_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1450 44 2860 15219 71.401382 24.646896 2.723448 2649 11 14 1 87.386360 2960.818115 260777 43 3411 32503.705078 least-occurring-first 0 0 0 0 0 3042 254331 249875 180557 69318 generated bobsynth13_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1456 44 2841 15341 73.951233 23.271978 2.636676 2680 7 14 1 85.022728 2642.386475 233032 23 3649 28917.455078 least-occurring-first 1 0 0 0 0 2705 226685 223754 191312 32442 generated bobsynthand_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1369 44 2860 15219 71.396637 24.608473 2.728269 2650 11 14 1 82.613640 2638.431885 289686 13 3392 30856.431641 least-occurring-first 0 0 0 0 0 2838 283463 281364 125035 156329 generated bobsynthand_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1448 44 2841 15322 74.335632 23.376381 2.667127 2680 5 14 1 84.954544 2641.795410 153600 21 3225 29345.273438 least-occurring-first 0 0 0 0 0 2595 147782 145134 86812 58322 generated bobsynthetic2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 91 66 600 10067 8777.922852 402.758240 66.000000 9000 8671 66 66 - 76.681816 7200000 713 - - least-occurring-first 0 0 0 0 0 114809 0 6205496 6205496 0 generated bobsynthetic2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 24 66 424 9016 8760.583008 401.125000 66.000000 8848 8461 66 66 - 23.045454 7200000 928 - - least-occurring-first 0 0 0 0 0 38588 0 6263329 6263329 0 generated bobsynthor_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1438 44 2860 15219 70.853966 24.550764 2.701669 2649 9 14 1 86.363640 2725.931885 231641 24 3174 30466.091797 least-occurring-first 0 0 0 0 0 2931 225540 222555 157797 64758 generated bobsynthor_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1470 44 2841 15324 73.706123 23.267347 2.664626 2680 7 14 1 86.272728 2681.931885 161855 24 3081 29193.044922 least-occurring-first 1 0 0 0 0 2614 156166 153382 125396 27986 generated bobtuint10_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2139 112.773331 36.973331 4.600000 350 9 16 1 4.928571 6036.928711 206525 48 72810 112593.398438 least-occurring-first 0 0 0 0 0 578 133137 130519 128618 1901 generated bobtuint11_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 148000 42 47185 112479.882812 least-occurring-first 0 0 0 0 0 630 100155 97605 91559 6046 generated bobtuint12_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 129210 40 48995 113989.656250 least-occurring-first 0 0 0 0 0 600 79615 77203 75180 2023 generated bobtuint13_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 139497 42 46815 112479.882812 least-occurring-first 0 0 0 0 0 736 91946 89562 83627 5935 generated bobtuint14_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 130454 40 50923 113989.656250 least-occurring-first 0 0 0 0 0 608 78923 76493 74447 2046 generated bobtuint15_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 165037 42 61082 112479.882812 least-occurring-first 0 0 0 0 0 635 103321 100861 92078 8783 generated bobtuint16_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 135333 40 49267 113989.656250 least-occurring-first 0 0 0 0 0 614 85452 83007 80844 2163 generated bobtuint17_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.428711 157803 46 49809 112482.125000 least-occurring-first 0 0 0 0 0 592 107403 104829 101802 3027 generated bobtuint18_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 141451 40 52205 113989.656250 least-occurring-first 0 0 0 0 0 667 88580 86111 83872 2239 generated bobtuint19_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 149925 42 48980 112479.882812 least-occurring-first 0 0 0 0 0 622 100323 97919 91146 6773 generated bobtuint20_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 159776 40 67004 113989.656250 least-occurring-first 0 0 0 0 0 627 92144 89672 86902 2770 generated bobtuint21_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 174520 42 49577 112479.882812 least-occurring-first 0 0 0 0 0 651 124293 121616 115095 6521 generated bobtuint22_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2137 119.333336 39.080002 4.906667 352 7 16 1 5.257143 6133.214355 151565 40 61155 113989.656250 least-occurring-first 0 0 0 0 0 648 89761 87254 84595 2659 generated bobtuint23_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 143573 42 47676 112479.882812 least-occurring-first 1 0 0 0 0 594 95303 92862 86915 5947 generated bobtuint27_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 70 379 2139 112.773331 36.973331 4.600000 350 9 16 1 4.928571 6036.500000 185191 39 70711 112584.617188 least-occurring-first 0 0 0 0 0 642 113837 111188 97078 14110 generated bobtuint28_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 213089 42 70057 112479.882812 least-occurring-first 0 0 0 0 0 681 142351 139709 130232 9477 generated bobtuint29_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2138 117.643837 38.438354 4.575343 350 9 16 1 4.771429 6023.371582 171004 42 48471 112479.882812 least-occurring-first 0 0 0 0 0 689 121843 119276 112598 6678 generated bobtuint30_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 70 379 2150 111.164383 36.465752 4.232877 352 9 16 1 4.414286 6409.856934 168571 42 55081 119736.570312 least-occurring-first 0 0 0 0 0 550 112941 110432 97313 13119 generated bobtuint31_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 78 70 379 2138 103.282051 34.217949 4.115385 352 7 16 1 4.585714 6302.114258 187277 44 64373 118342.328125 least-occurring-first 0 0 0 0 0 559 122347 119796 119432 364 generated bobtuintand_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 74 70 379 2138 109.175674 35.824326 4.270270 352 9 16 1 4.500000 5979.485840 178642 43 57147 110945.968750 least-occurring-first 0 0 0 0 0 572 120922 118388 117851 537 generated bobtuintor_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 76 70 379 2138 109.934212 36.026318 4.381579 352 7 16 1 4.757143 5918.457031 143270 43 54084 109123.312500 least-occurring-first 0 0 0 0 0 514 88672 86225 85389 836 generated kenflashp12_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 31 21 98 878 30.677420 4.935484 1.225806 717 7 8 1 1.809524 360.571442 235 0 12 857.047607 least-occurring-first 0 0 0 0 0 12 211 188 0 188 generated kenflashp12_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 39 21 97 1020 26.256411 3.564103 1.179487 902 3 8 1 2.190476 426.142853 256 0 16 900.428589 least-occurring-first 0 0 0 0 0 12 227 201 0 201 generated kenoopp1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 39 24 121 601 28.333334 7.000000 1.410256 412 7 9 1 2.291667 299.875000 150 0 13 1286.166626 least-occurring-first 0 0 0 0 0 20 117 81 0 81 generated kenoopp1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 24 120 547 12.790698 3.837209 1.186046 412 3 9 1 2.125000 325.375000 156 0 25 1403.041626 least-occurring-first 0 0 0 0 0 14 117 82 0 82 generated pdtvishuffman0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 20 5 39 307 59.549999 15.200000 4.800000 104 28 5 4 19.200001 506.799988 247 25 4 1255.400024 least-occurring-first 0 0 0 0 0 11 231 145 132 13 generated pdtvishuffman0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 18 5 31 237 53.777779 14.888889 4.888889 98 27 5 4 16.600000 314.799988 113 20 2 815.200012 least-occurring-first 0 0 0 0 0 9 101 45 40 5 generated pdtvishuffman1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 22 5 39 307 59.363636 15.318182 4.863636 102 30 5 4 21.400000 510.399994 245 27 3 1277.599976 least-occurring-first 0 0 0 0 0 12 230 124 122 2 generated pdtvishuffman1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 19 5 31 237 53.842106 14.894737 4.894737 98 27 5 4 17.799999 315.399994 103 19 2 818.000000 least-occurring-first 0 0 0 0 0 10 91 41 34 7 generated pdtvishuffman2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 19 5 39 308 56.684212 15.368421 4.842105 102 30 5 4 18.400000 510.399994 234 28 3 1259.599976 least-occurring-first 1 0 0 0 0 13 218 126 104 22 generated pdtvishuffman2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 18 5 31 237 55.055557 14.888889 4.888889 98 27 5 4 17.000000 314.399994 113 19 2 812.799988 least-occurring-first 0 0 0 0 0 10 101 40 35 5 generated pdtvishuffman3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 19 5 39 308 58.105263 15.315789 4.842105 102 30 5 4 18.400000 502.200012 219 32 3 1242.000000 least-occurring-first 0 0 0 0 0 45 170 97 87 10 generated pdtvishuffman3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 17 5 31 254 57.235294 15.882353 4.882353 98 29 5 4 16.400000 329.000000 89 15 2 832.200012 least-occurring-first 0 0 0 0 0 10 77 33 30 3 generated pdtvishuffman4_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 17 5 39 307 59.941177 15.294118 4.823529 104 30 5 4 16.400000 493.600006 154 25 2 1204.599976 least-occurring-first 0 0 0 0 0 9 143 77 67 10 generated pdtvishuffman4_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 21 5 31 253 53.095238 15.666667 4.904762 98 27 5 4 18.200001 324.200012 75 16 2 826.000000 least-occurring-first 0 0 0 0 0 7 66 28 27 1 generated pdtvishuffman5_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 20 5 39 308 60.299999 15.250000 4.800000 103 28 5 4 19.200001 504.000000 161 26 3 1249.000000 least-occurring-first 0 0 0 0 0 8 149 87 81 6 generated pdtvishuffman5_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 17 5 31 254 57.235294 15.882353 4.882353 98 29 5 4 16.400000 329.000000 68 15 2 832.200012 least-occurring-first 0 0 0 0 0 7 59 25 23 2 generated pdtvishuffman6_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 19 5 39 308 58.842106 15.368421 4.842105 102 30 5 4 18.400000 501.399994 159 25 3 1233.599976 least-occurring-first 0 0 0 0 0 9 147 87 81 6 generated pdtvishuffman6_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 17 5 31 254 57.235294 15.882353 4.882353 98 29 5 4 16.400000 329.000000 99 15 2 832.200012 least-occurring-first 0 0 0 0 0 10 87 37 34 3 generated pdtvishuffman7_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 18 5 39 308 61.666668 15.277778 4.833333 100 30 5 4 17.400000 497.600006 194 26 4 1218.000000 least-occurring-first 0 0 0 0 0 9 181 104 93 11 generated pdtvishuffman7_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 19 5 31 253 55.526318 15.736842 4.894737 98 27 5 4 17.400000 324.399994 124 18 2 823.000000 least-occurring-first 0 0 0 0 0 12 110 53 48 5 generated pdtvistictactoe00_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 31 4 52 522 195.870972 20.322580 3.612903 253 9 4 2 27.250000 543.000000 272 0 2 1004.250000 least-occurring-first 0 0 0 0 0 22 249 223 0 223 generated pdtvistictactoe00_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 48 486 186.933334 19.266666 3.600000 268 5 4 2 24.750000 433.000000 156 0 2 711.750000 least-occurring-first 0 0 0 0 0 24 130 113 0 113 generated pdtvistictactoe01_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 28 4 52 517 187.357147 19.821428 3.571429 249 9 4 2 24.250000 530.750000 261 0 2 982.000000 least-occurring-first 0 0 0 0 0 22 238 211 0 211 generated pdtvistictactoe01_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 33 4 48 476 187.212128 19.787878 3.636364 257 5 4 2 26.500000 420.750000 124 0 2 697.000000 least-occurring-first 0 0 0 0 0 19 103 87 0 87 generated pdtvistictactoe02_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 4 52 506 190.586212 20.000000 3.586207 252 9 4 2 25.250000 530.750000 262 0 1 967.000000 least-occurring-first 0 0 0 0 0 15 246 230 0 230 generated pdtvistictactoe02_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 4 48 489 190.206894 19.827587 3.655172 260 5 4 2 25.250000 507.000000 148 0 1 970.250000 least-occurring-first 0 0 0 0 0 13 133 115 0 115 generated pdtvistictactoe03_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 4 52 498 184.517242 20.000000 3.586207 244 9 4 2 25.250000 521.500000 195 0 1 958.250000 least-occurring-first 0 0 0 0 0 12 183 166 0 166 generated pdtvistictactoe03_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 48 483 185.866669 20.000000 3.666667 253 5 4 2 25.000000 499.000000 151 0 2 956.000000 least-occurring-first 0 0 0 0 0 20 129 105 0 105 generated pdtvistictactoe04_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 4 52 499 188.965515 20.000000 3.586207 249 9 4 2 25.250000 507.500000 312 0 2 909.000000 least-occurring-first 0 0 0 0 0 22 289 264 0 264 generated pdtvistictactoe04_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 32 4 49 500 186.250000 20.375000 3.625000 257 5 4 2 25.500000 439.000000 122 0 2 711.000000 least-occurring-first 0 0 0 0 0 19 102 84 0 84 generated pdtvistictactoe05_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 4 52 518 186.000000 19.629629 3.555556 250 9 4 2 23.250000 552.500000 319 0 2 1041.250000 least-occurring-first 0 0 0 0 0 22 296 268 0 268 generated pdtvistictactoe05_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 48 480 183.133331 19.266666 3.600000 262 5 4 2 24.750000 426.250000 138 0 2 707.750000 least-occurring-first 0 0 0 0 0 19 116 98 0 98 generated pdtvistictactoe06_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 28 4 52 520 189.785721 19.892857 3.642857 253 9 4 2 24.250000 529.750000 327 0 2 983.250000 least-occurring-first 0 0 0 0 0 22 304 278 0 278 generated pdtvistictactoe06_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 32 4 48 479 188.156250 19.625000 3.625000 258 5 4 2 26.250000 424.250000 125 0 1 702.750000 least-occurring-first 0 0 0 0 0 21 103 86 0 86 generated pdtvistictactoe07_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 31 4 52 505 194.193542 20.322580 3.612903 252 9 4 2 27.250000 524.250000 210 0 2 940.000000 least-occurring-first 0 0 0 0 0 20 188 167 0 167 generated pdtvistictactoe07_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 39 4 49 515 199.512817 21.205128 3.692308 257 5 4 2 32.250000 540.500000 248 0 1 1027.750000 least-occurring-first 0 0 0 0 0 28 220 191 0 191 generated pdtvistictactoe08_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 52 503 190.266663 20.166666 3.600000 248 9 4 2 26.250000 541.750000 358 0 2 1007.000000 least-occurring-first 0 0 0 0 0 24 333 306 0 306 generated pdtvistictactoe08_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 34 4 48 489 188.911758 19.941177 3.647059 258 5 4 2 28.250000 515.750000 221 0 1 994.000000 least-occurring-first 0 0 0 0 0 24 196 173 0 173 generated pdtvistictactoe09_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 33 4 52 500 197.818176 20.606060 3.636364 252 9 4 2 29.250000 527.500000 309 0 2 957.500000 least-occurring-first 0 0 0 0 0 28 281 254 0 254 generated pdtvistictactoe09_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 35 4 48 492 194.085709 20.085714 3.657143 259 5 4 2 29.750000 520.750000 196 0 1 1012.250000 least-occurring-first 0 0 0 0 0 26 169 142 0 142 generated pdtvistictactoe10_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 4 52 518 188.620697 20.000000 3.586207 248 9 4 2 25.250000 543.000000 260 0 2 1020.750000 least-occurring-first 0 0 0 0 0 21 238 215 0 215 generated pdtvistictactoe10_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 48 476 181.866669 19.266666 3.600000 258 5 4 2 24.750000 419.500000 138 0 1 693.250000 least-occurring-first 0 0 0 0 0 18 120 100 0 100 generated pdtvistictactoe11_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 31 4 52 523 196.000000 20.322580 3.612903 253 9 4 2 27.250000 542.500000 218 0 1 1004.750000 least-occurring-first 0 0 0 0 0 14 202 183 0 183 generated pdtvistictactoe11_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 48 486 186.933334 19.266666 3.600000 268 5 4 2 25.000000 431.750000 120 0 1 709.500000 least-occurring-first 0 0 0 0 0 20 100 84 0 84 generated pdtvistictactoe12_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 52 516 188.866669 20.166666 3.600000 246 9 4 2 26.250000 543.000000 208 0 1 1015.250000 least-occurring-first 0 0 0 0 0 17 192 174 0 174 generated pdtvistictactoe12_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 4 49 506 187.166672 20.066668 3.600000 263 5 4 2 24.750000 448.000000 151 0 2 726.000000 least-occurring-first 0 0 0 0 0 22 127 108 0 108 generated pdtvistictactoe13_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 33 4 52 498 195.545456 20.606060 3.636364 248 9 4 2 29.250000 512.250000 207 0 2 912.250000 least-occurring-first 0 0 0 0 0 19 185 169 0 169 generated pdtvistictactoe13_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 33 4 48 488 195.363632 20.454546 3.696970 256 5 4 2 27.750000 513.500000 131 0 1 988.000000 least-occurring-first 0 0 0 0 0 16 113 96 0 96 generated pdtvistimeout0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 10 74 624 47.534885 13.093023 4.139535 148 9 10 1 17.600000 1151.500000 942 17 35 6503.700195 least-occurring-first 0 0 0 0 0 21 885 782 688 94 generated pdtvistimeout0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 10 73 708 56.431820 14.181818 4.545455 156 5 10 1 20.000000 1018.099976 652 0 32 5356.299805 least-occurring-first 1 0 0 0 0 26 594 530 0 530 generated pdtvistimeout1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 10 74 624 47.488373 13.093023 4.139535 148 9 10 1 17.600000 1153.300049 1017 22 35 6517.700195 least-occurring-first 0 0 0 0 0 22 960 838 318 520 generated pdtvistimeout1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 45 10 73 708 57.311111 14.400000 4.644444 156 5 10 1 20.900000 1025.099976 562 0 41 5420.899902 least-occurring-first 0 0 0 0 0 26 496 436 0 436 generated pdtvistimeout2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 10 74 615 49.930233 13.767442 4.232558 148 9 10 1 18.100000 1146.000000 1292 34 33 6487.600098 least-occurring-first 0 0 0 0 0 31 1227 1027 539 488 generated pdtvistimeout2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 44 10 73 707 57.659092 14.068182 4.545455 156 5 10 1 20.000000 1016.599976 821 0 40 5339.600098 least-occurring-first 1 0 0 0 0 40 741 659 0 659 generated pdtvistimeout3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 10 74 624 47.488373 13.093023 4.139535 148 9 10 1 17.600000 1153.300049 1016 22 34 6517.700195 least-occurring-first 0 0 0 0 0 21 961 848 316 532 generated pdtvistimeout3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 45 10 73 708 57.311111 14.400000 4.644444 156 5 10 1 20.900000 1025.099976 639 0 30 5420.899902 least-occurring-first 0 0 0 0 0 42 567 487 0 487 generated pdtvistwo0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 7 6 18 59 8.428572 3.000000 1.000000 9 7 1 1 1.166667 5.000000 19 0 0 5.000000 least-occurring-first 0 0 0 0 0 17 2 0 0 0 generated pdtvistwo0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 10 6 12 35 3.400000 2.000000 1.000000 5 3 1 1 1.666667 1.000000 5 0 0 1.000000 least-occurring-first 0 0 0 0 0 2 2 0 0 0 generated pdtvistwo1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 7 6 18 59 8.428572 3.000000 1.000000 9 7 1 1 1.166667 5.000000 6 0 0 5.000000 least-occurring-first 0 0 0 0 0 2 3 0 0 0 generated pdtvistwo1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 10 6 12 35 3.400000 2.000000 1.000000 5 3 1 1 1.666667 1.000000 4 0 0 1.000000 least-occurring-first 0 0 0 0 0 1 2 1 0 1 generated pdtvistwoall0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 9 6 18 59 7.666667 3.000000 1.000000 9 7 1 1 1.500000 5.000000 7 0 0 5.000000 least-occurring-first 1 0 0 0 0 4 3 1 0 1 generated pdtvistwoall0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 10 6 12 35 3.400000 2.000000 1.000000 5 3 1 1 1.666667 1.000000 6 0 0 1.000000 least-occurring-first 0 0 0 0 0 3 2 0 0 0 generated pdtvistwoall1_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 9 6 18 59 7.666667 3.000000 1.000000 9 7 1 1 1.500000 5.000000 6 0 0 5.000000 least-occurring-first 0 0 0 0 0 3 2 1 0 1 generated pdtvistwoall1_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 10 6 12 35 3.400000 2.000000 1.000000 5 3 1 1 1.666667 1.000000 4 0 0 1.000000 least-occurring-first 0 0 0 0 0 1 2 0 0 0 generated pdtvistwoall2_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 9 6 18 59 7.666667 3.000000 1.000000 9 7 1 1 1.500000 5.000000 6 0 0 5.000000 least-occurring-first 0 0 0 0 0 3 3 0 0 0 generated pdtvistwoall2_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 10 6 12 35 3.400000 2.000000 1.000000 5 3 1 1 1.666667 1.000000 3 0 0 1.000000 least-occurring-first 0 0 0 0 0 1 2 0 0 0 generated pdtvistwoall3_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 9 6 18 59 7.666667 3.000000 1.000000 9 7 1 1 1.500000 5.000000 7 0 0 5.000000 least-occurring-first 0 0 0 0 0 4 3 0 0 0 generated pdtvistwoall3_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 10 6 12 35 3.400000 2.000000 1.000000 5 3 1 1 1.666667 1.000000 5 0 0 1.000000 least-occurring-first 0 0 0 0 0 2 2 1 0 1 generated pdtvisvending00_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 32 2 53 403 73.250000 15.312500 1.968750 98 54 2 1 31.500000 408.000000 54 0 0 532.500000 least-occurring-first 0 0 0 0 0 11 43 32 0 32 generated pdtvisvending00_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 28 2 54 385 72.250000 15.464286 1.928571 138 44 2 1 26.000000 359.000000 80 0 0 483.500000 least-occurring-first 1 0 0 0 0 9 71 59 0 59 generated pdtvisvending01_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 53 436 74.103447 15.275862 1.965517 100 54 2 1 28.000000 444.000000 48 0 0 571.500000 least-occurring-first 0 0 0 0 0 8 39 29 0 29 generated pdtvisvending01_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 54 384 72.896553 15.551724 1.965517 138 46 2 1 27.500000 364.500000 74 0 0 485.500000 least-occurring-first 0 0 0 0 0 6 67 59 0 59 generated pdtvisvending02_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 28 2 53 423 73.392860 15.285714 1.964286 100 54 2 1 27.000000 429.500000 34 0 0 555.000000 least-occurring-first 0 0 0 0 0 5 28 20 0 20 generated pdtvisvending02_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 2 54 375 73.666664 15.555555 1.962963 138 46 2 1 26.000000 352.500000 69 0 0 470.500000 least-occurring-first 0 0 0 0 0 6 63 55 0 55 generated pdtvisvending03_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 53 427 74.379311 15.517241 1.965517 98 54 2 1 28.000000 431.000000 39 0 0 555.000000 least-occurring-first 0 0 0 0 0 5 34 26 0 26 generated pdtvisvending03_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 31 2 54 374 70.645164 15.354838 1.935484 138 44 2 1 28.500000 349.000000 85 0 0 464.500000 least-occurring-first 0 0 0 0 0 7 78 71 0 71 generated pdtvisvending04_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 2 53 437 73.666664 15.600000 1.966667 100 54 2 1 28.500000 440.500000 59 0 0 565.000000 least-occurring-first 0 0 0 0 0 9 50 40 0 40 generated pdtvisvending04_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 28 2 54 384 66.714287 15.464286 1.964286 140 46 2 1 25.500000 363.000000 86 0 0 480.500000 least-occurring-first 0 0 0 0 0 9 77 68 0 68 generated pdtvisvending05_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 2 53 437 74.111115 15.296296 1.962963 100 54 2 1 26.000000 444.500000 51 0 0 572.000000 least-occurring-first 0 0 0 0 0 8 43 32 0 32 generated pdtvisvending05_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 2 54 380 72.037041 15.518518 1.962963 138 46 2 1 25.500000 363.000000 90 0 1 481.500000 least-occurring-first 0 0 0 0 0 8 81 72 0 72 generated pdtvisvending06_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 2 53 435 73.333336 15.259259 1.962963 100 54 2 1 26.500000 445.000000 64 0 1 570.000000 least-occurring-first 0 0 0 0 0 9 53 42 0 42 generated pdtvisvending06_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 26 2 54 385 68.769234 15.346154 1.923077 140 44 2 1 24.000000 372.000000 81 0 0 492.000000 least-occurring-first 0 0 0 0 0 7 74 64 0 64 generated pdtvisvending07_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 32 2 53 449 72.781250 15.281250 1.968750 100 54 2 1 30.000000 450.500000 54 0 0 574.500000 least-occurring-first 0 0 0 0 0 9 45 32 0 32 generated pdtvisvending07_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 2 54 388 69.481483 15.555555 1.962963 140 46 2 1 25.500000 372.500000 87 0 0 494.000000 least-occurring-first 0 0 0 0 0 8 79 68 0 68 generated pdtvisvending08_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 53 427 74.241379 15.482759 1.965517 100 54 2 1 28.500000 436.000000 54 0 1 563.000000 least-occurring-first 0 0 0 0 0 9 44 33 0 33 generated pdtvisvending08_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 2 54 390 68.633331 15.266666 1.933333 138 44 2 1 27.500000 371.000000 124 0 1 488.500000 least-occurring-first 0 0 0 0 0 8 116 105 0 105 generated pdtvisvending09_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 53 436 74.103447 15.275862 1.965517 100 54 2 1 28.000000 444.000000 37 0 1 571.500000 least-occurring-first 0 0 0 0 0 6 30 22 0 22 generated pdtvisvending09_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 54 384 72.896553 15.551724 1.965517 138 46 2 1 27.500000 364.500000 104 0 0 485.500000 least-occurring-first 0 0 0 0 0 9 95 85 0 85 generated pdtvisvending10_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 29 2 53 436 74.103447 15.275862 1.965517 100 54 2 1 28.000000 444.000000 36 0 0 571.500000 least-occurring-first 0 0 0 0 0 5 30 22 0 22 generated pdtvisvending10_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 27 2 54 401 75.407410 16.407408 1.925926 138 44 2 1 25.000000 370.000000 54 0 0 495.000000 least-occurring-first 1 0 0 0 0 5 49 42 0 42 generated ringp0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 26 15 59 306 15.000000 5.230769 1.653846 141 7 11 1 2.866667 354.666656 175 0 29 2353.600098 least-occurring-first 0 0 0 0 0 12 134 94 0 94 generated ringp0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 30 15 59 269 11.033334 4.366667 1.600000 150 3 11 1 3.066667 449.133331 183 0 39 3110.399902 least-occurring-first 0 0 0 0 0 13 131 78 0 78 generated ringp0neg_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 26 15 59 306 15.000000 5.230769 1.653846 141 7 11 1 2.866667 371.733337 169 0 31 2469.000000 least-occurring-first 0 0 0 0 0 10 128 85 0 85 generated ringp0neg_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 28 15 59 269 11.035714 4.214286 1.571429 150 3 11 1 2.933333 456.200012 196 0 39 3128.333252 least-occurring-first 0 0 0 0 0 14 142 85 0 85 generated shortp0_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 16 10 38 179 15.125000 5.375000 1.500000 91 7 8 1 2.400000 125.900002 36 0 3 430.799988 least-occurring-first 0 0 0 0 0 6 27 16 0 16 generated shortp0_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 18 10 35 154 9.888889 4.055555 1.388889 93 3 8 1 2.500000 123.199997 25 0 3 483.700012 least-occurring-first 0 0 0 0 0 4 17 7 0 7 generated shortp0neg_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 15 10 34 162 13.800000 4.600000 1.466667 91 7 8 1 2.200000 116.300003 46 0 2 380.500000 least-occurring-first 0 0 0 0 0 27 16 9 0 9 generated shortp0neg_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 18 10 35 154 9.888889 4.055555 1.388889 93 3 8 1 2.500000 123.400002 27 0 3 484.799988 least-occurring-first 0 0 0 0 0 5 18 8 0 8 generated kenflashp01_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 37 24 133 699 21.783783 5.675676 1.513514 530 7 20 1 2.333333 72644.835938 1694761 0 113438 1239021.625000 least-occurring-first 0 0 0 0 0 3143 1578180 1549997 0 1549997 generated kenflashp01_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 43 24 130 690 16.372093 4.325582 1.441860 566 3 20 1 2.583333 131561.578125 2657853 0 172210 1829179.875000 least-occurring-first 1 0 0 0 0 3801 2481842 2450732 0 2450732 generated kenflashp04_all_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 47 31 160 825 20.340425 5.361702 1.382979 602 7 19 1 2.096774 52964.968750 308459 0 54596 656019.437500 least-occurring-first 0 0 0 0 0 3040 250823 233484 0 233484 generated kenflashp04_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 56 31 157 826 14.964286 4.000000 1.321429 659 3 19 1 2.387097 48943.257812 938747 0 118528 844312.500000 least-occurring-first 0 0 0 0 0 2920 817299 789181 0 789181 generated visprodcellp01_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 54 30 93 420 8.203704 3.129630 1.537037 270 3 30 1 2.766667 120139.101562 2619057 0 317840 2217064.250000 least-occurring-first 0 0 0 0 0 6662 2294554 2243131 0 2243131 generated visprodcellp03_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 54 30 93 420 8.203704 3.129630 1.537037 270 3 30 1 2.766667 120139.101562 2619519 0 317816 2217064.250000 least-occurring-first 0 0 0 0 0 6645 2295058 2243586 0 2243586 generated visprodcellp07_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 54 30 93 420 8.203704 3.129630 1.537037 270 3 30 1 2.766667 120139.101562 2637240 0 318870 2217064.250000 least-occurring-first 0 0 0 0 0 7584 2310761 2256664 0 2256664 generated visprodcellp22_all_bit_differing_from_true_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 54 30 93 420 8.203704 3.129630 1.537037 270 3 30 1 2.766667 120139.101562 2619044 0 317777 2217064.250000 least-occurring-first 0 0 0 0 0 6667 2294600 2243190 0 2243190 generated bobsm5378d2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 422 290 546 4374 33.620853 11.689573 4.421801 2134 3 257 1 3.486207 250.199997 814145 1027 13234 2934.448242 least-occurring-first 0 0 0 0 0 1435 799475 485281 483197 2084 generated bobsm9234_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 433 377 720 5070 41.383373 13.951501 3.120092 687 1 344 1 1.535809 60.753315 12175 10 7161 673.761292 least-occurring-first 0 0 0 0 0 2148 2867 802 794 8 generated bobsmcodic_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 2671 1884 3734 36046 75.312988 19.440659 2.848746 22266 9 1851 1 1.424098 73.643845 137716 0 20561 98.989388 least-occurring-first 4 0 0 0 0 81783 35391 9996 0 9996 generated bobsmfpu_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1413 1024 1930 41752 1695.535034 31.099787 1.907290 35247 3 907 1 1.526367 1700.121094 221630 16 120239 1927.080078 least-occurring-first 2 0 0 0 0 76782 24781 9698 6766 2932 generated bobsmhdlc1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 442 339 629 5000 38.782806 13.160633 2.558824 2223 7 291 1 1.598820 51.867256 9339 0 6324 579.834778 least-occurring-first 0 0 0 0 0 1688 1328 348 0 348 generated bobsmhdlc2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 449 338 627 5042 38.391983 13.115813 2.601336 2270 7 290 1 1.775148 55.946747 9441 0 6346 772.769226 least-occurring-first 1 0 0 0 0 1729 1366 372 0 372 generated bobsmhdlc3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 450 349 649 5256 39.908890 13.306666 2.653333 2425 5 301 1 1.719198 56.346706 10694 0 7145 807.805176 least-occurring-first 1 0 0 0 0 1828 1722 602 0 602 generated bobsmhdlc_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 450 340 631 5150 37.284443 12.686666 2.548889 2398 3 292 1 1.594118 51.044117 7833 0 4796 518.732361 least-occurring-first 1 0 0 0 0 1633 1404 350 0 350 generated eijkbs1512_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 253 188 346 3731 79.750992 22.438736 4.462451 1863 11 159 2 2.436170 143.680847 12505 24 9773 3364.893555 least-occurring-first 1 0 0 0 0 1012 1720 1032 952 80 generated eijkbs4863_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 385 306 562 12090 108.792206 17.257143 8.366234 7307 9 257 1 7.901961 620.026123 164962 37 97176 11154.839844 least-occurring-first 0 0 0 0 0 2687 65102 60805 60196 609 generated neclaftp2001_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 7034 4751 9782 68036 63.227039 23.271112 2.234717 11055 1 4719 1 1.480530 65.561142 1127674 0 116429 63.454010 least-occurring-first 10 0 0 0 0 603431 407856 163902 0 163902 generated neclaftp2002_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 7013 4751 9782 72628 66.440041 23.949522 2.244974 19532 1 4719 1 1.476110 67.535889 1100238 0 110432 65.469162 least-occurring-first 10 0 0 0 0 645086 344751 130419 0 130419 generated neclaftp3001_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3904 2828 5654 48872 75.911888 23.656250 2.558658 20606 1 2796 1 1.387907 79.974892 385789 0 65467 108.690948 least-occurring-first 6 0 0 0 0 198851 121494 42838 0 42838 generated neclaftp3002_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 3973 2828 5654 56832 78.728668 23.701485 2.543670 30689 1 2796 1 1.448373 83.900284 445338 0 82492 143.549149 least-occurring-first 6 0 0 0 0 212300 150567 49394 0 49394 generated neclaftp4001_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1545 1004 2098 15713 51.941746 17.822653 1.995469 6813 1 972 1 1.540837 53.436256 32249 0 3906 52.159363 least-occurring-first 2 0 0 0 0 19459 8891 3550 0 3550 generated neclaftp4002_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1502 1004 2098 13446 49.646473 17.182423 1.378163 4697 1 2 1 1.503984 50.582668 30957 0 3888 49.985062 least-occurring-first 2 0 0 0 0 19249 7802 3194 0 3194 generated pdtpmsgigamax_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 185 146 269 3072 192.183777 50.389191 8.821622 1721 3 124 1 - 6.698630 7200000 1136 - - least-occurring-first 0 0 0 0 0 1823 0 6567876 6567876 0 generated pdtpmsmiim_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 269 250 459 2666 31.089220 11.078067 2.925651 419 1 210 1 1.552000 37.023998 2732 2 806 156.707993 least-occurring-first 1 0 0 0 0 819 1107 297 241 56 generated pdtpmsns3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 763 494 966 14151 150.003937 43.262123 5.321101 9017 7 473 1 - 4.781376 7200000 1921 - - least-occurring-first 1 0 0 0 0 18331 0 6195808 6195808 0 generated pdtpmsrotate32_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 227 168 298 3957 68.546257 18.889868 4.427313 1888 3 131 1 4.160714 118.982140 10222 10 7747 4341.416504 least-occurring-first 1 0 0 0 0 831 1644 1105 1082 23 generated pdtpmssfeistel_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 1116 824 1579 17579 68.839607 20.190861 4.977599 9159 11 756 1 - - MO - - - - - - - - - - - - - - generated pdtpmsvsa16a_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 603 423 844 7946 53.451077 15.681592 1.179104 1074 1 5 1 1.456265 49.725769 6212 8 672 49.243500 least-occurring-first 0 0 0 0 0 3360 2183 785 598 187 generated pdtvismiim0_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 108 127 213 1455 33.157406 12.972222 3.805556 371 7 87 1 1.551181 44.472443 683 2 248 201.283463 least-occurring-first 0 0 0 0 0 179 255 64 47 17 generated pdtvismiim1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 105 127 213 1479 33.771427 13.066667 3.904762 430 9 87 1 1.472441 47.291340 717 6 268 216.503937 least-occurring-first 1 0 0 0 0 170 279 83 81 2 generated pdtvismiim2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 108 127 213 1455 33.157406 12.972222 3.805556 371 7 87 1 1.551181 44.472443 682 2 249 201.283463 least-occurring-first 0 0 0 0 0 180 253 64 47 17 generated pdtvismiim3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 105 127 213 1479 33.771427 13.066667 3.904762 430 9 87 1 1.472441 47.291340 737 6 270 216.503937 least-occurring-first 1 0 0 0 0 169 298 86 84 2 generated pdtvismiim4_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 125 127 213 1481 32.824001 12.968000 3.824000 424 7 87 1 1.551181 42.503937 419 0 20 4.393701 least-occurring-first 0 0 0 0 0 187 212 49 0 49 generated pdtvismiim5_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 105 127 213 1479 33.771427 13.066667 3.904762 430 9 87 1 1.472441 47.291340 717 6 268 216.503937 least-occurring-first 0 0 0 0 0 171 279 84 81 3 generated pdtvismiim6_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 108 127 213 1455 33.157406 12.972222 3.805556 371 7 87 1 1.551181 44.472443 685 2 248 201.283463 least-occurring-first 1 0 0 0 0 183 253 66 49 17 generated pdtvissfeistel_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 654 430 791 9223 60.310398 17.706423 5.029052 4781 14 362 1 - 2.906977 7200000 120 - - least-occurring-first 1 0 0 0 0 5060 0 1515352 1515352 0 generated pdtvissoap0_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 378 242 462 4570 45.433861 11.973545 2.277778 2639 3 221 1 2.020661 272.214874 15288 11 11307 3022.785156 least-occurring-first 1 0 0 0 0 1013 2967 1230 346 884 generated pdtvissoap1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 366 242 462 4557 45.959015 11.991803 2.289618 2628 3 221 1 2.041322 258.566101 15467 11 10827 2959.690186 least-occurring-first 0 0 0 0 0 1006 3635 1964 1720 244 generated pdtvissoap2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 379 242 462 4563 45.517151 12.021109 2.284961 2632 3 221 1 2.082645 223.954544 12021 11 8687 2626.603271 least-occurring-first 0 0 0 0 0 1054 2281 747 572 175 generated pdtvisvsa16a00_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2523 28 195 46.795277 least-occurring-first 1 0 0 0 0 1044 1284 403 386 17 generated pdtvisvsa16a01_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2513 28 196 46.795277 least-occurring-first 0 0 0 0 0 1039 1277 398 381 17 generated pdtvisvsa16a02_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2571 28 196 46.795277 least-occurring-first 0 0 0 0 0 1073 1302 420 403 17 generated pdtvisvsa16a03_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 305 254 490 4308 44.468853 15.327868 1.229508 334 1 2 1 1.456693 45.133858 2701 34 204 46.586613 least-occurring-first 0 0 0 0 0 1086 1413 449 426 23 generated texasifetch1p1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 77 86 145 789 17.402597 7.038961 2.883117 119 1 60 1 1.267442 14.220930 116 0 13 17.465117 least-occurring-first 0 0 0 0 0 46 56 9 0 9 generated texasifetch1p2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 77 86 145 731 15.610390 6.233766 2.012987 50 1 12 1 0.976744 10.988372 93 0 11 10.313953 least-occurring-first 0 0 0 0 0 42 40 7 0 7 generated texasifetch1p3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 86 145 731 16.260275 6.410959 2.068493 50 1 12 1 1.000000 12.325582 102 0 14 18.860466 least-occurring-first 0 0 0 0 0 41 46 8 0 8 generated texasifetch1p4_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 75 86 145 791 17.546667 7.133333 2.920000 119 1 60 1 1.209302 13.337210 129 2 11 9.465117 least-occurring-first 0 0 0 0 0 47 70 13 12 1 generated texasifetch1p5_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 73 86 145 730 16.534246 6.465754 2.136986 49 1 12 1 1.011628 12.546512 101 0 16 21.709303 least-occurring-first 0 0 0 0 0 42 43 9 0 9 generated texasifetch1p8_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 76 86 145 730 16.157894 6.381579 2.157895 50 1 12 1 1.058140 12.558140 100 0 15 21.500000 least-occurring-first 0 0 0 0 0 42 43 9 0 9 generated viselevatorp1_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 55 69 109 882 34.018181 10.127273 2.709091 439 3 41 1 1.289855 135.014496 365 0 215 1392.594238 least-occurring-first 0 0 0 0 0 46 103 40 0 40 generated viselevatorp2_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 49 69 109 842 37.346939 10.918367 2.857143 398 3 41 1 1.101449 166.144928 368 0 224 1397.536255 least-occurring-first 0 0 0 0 0 43 102 38 0 38 generated viselevatorp3_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 55 69 109 877 34.963634 10.436363 2.636364 415 3 41 1 1.289855 128.275360 360 0 196 1382.869507 least-occurring-first 0 0 0 0 0 50 114 51 0 51 generated visprodcellp01_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 127 109 187 1658 41.716534 10.015748 2.433071 917 3 79 1 1.715596 39028.027344 3379003 1 2997330 1862119.000000 least-occurring-first 1 0 0 0 0 7648 374004 273731 232510 41221 generated visprodcellp03_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 115 109 187 1644 43.026089 10.278261 2.539130 903 3 79 1 1.642202 52654.726562 5898186 1 5232625 2689744.250000 least-occurring-first 0 0 0 0 0 10554 655007 450853 246228 204625 generated visprodcellp07_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 115 109 187 1644 43.026089 10.278261 2.539130 903 3 79 1 1.642202 52654.726562 5936700 1 5270496 2689744.250000 least-occurring-first 0 0 0 0 0 10546 655658 451104 246414 204690 generated visprodcellp22_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 115 109 187 1644 43.026089 10.278261 2.539130 903 3 79 1 1.642202 52654.726562 5927429 1 5260132 2689744.250000 least-occurring-first 1 0 0 0 0 10592 656704 451874 246881 204993 generated pdtvisvsa16a04_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4306 45.559322 15.298306 1.237288 332 1 3 1 1.425197 45.149605 2430 26 193 46.799213 least-occurring-first 1 0 0 0 0 1038 1199 341 324 17 generated pdtvisvsa16a05_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 305 254 490 4304 45.003277 15.222951 1.219672 332 1 3 1 1.444882 45.062992 2639 28 197 46.566929 least-occurring-first 0 0 0 0 0 1088 1347 435 397 38 generated pdtvisvsa16a06_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 290 254 490 4300 45.620689 15.548276 1.206897 334 1 2 1 1.362205 44.948818 2583 28 193 46.291340 least-occurring-first 1 0 0 0 0 1084 1307 378 361 17 generated pdtvisvsa16a07_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 302 254 490 4309 45.645695 15.516557 1.195364 332 1 2 1 1.409449 44.771652 2734 30 193 45.870079 least-occurring-first 0 0 0 0 0 1143 1398 447 423 24 generated pdtvisvsa16a08_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 312 254 490 4305 45.205128 15.339744 1.214744 333 1 2 1 1.472441 44.952755 2603 28 196 46.303150 least-occurring-first 1 0 0 0 0 1098 1309 386 384 2 generated pdtvisvsa16a09_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 291 254 490 4306 45.714775 15.553265 1.237113 335 1 2 1 1.389764 45.106300 2522 26 193 46.279526 least-occurring-first 1 0 0 0 0 1053 1276 400 376 24 generated pdtvisvsa16a10_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 299 254 490 4313 46.936455 15.882943 1.204013 332 1 2 1 1.405512 44.732285 2553 26 191 45.685040 least-occurring-first 1 0 0 0 0 1126 1236 342 300 42 generated pdtvisvsa16a11_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2456 26 192 46.795277 least-occurring-first 0 0 0 0 0 1039 1225 374 353 21 generated pdtvisvsa16a12_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2530 28 192 46.795277 least-occurring-first 0 0 0 0 0 1049 1265 394 377 17 generated pdtvisvsa16a13_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 306 254 490 4303 45.836601 15.503268 1.222222 332 1 2 1 1.456693 45.161419 2843 38 195 46.618111 least-occurring-first 0 0 0 0 0 1127 1523 519 512 7 generated pdtvisvsa16a14_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 301 254 490 4308 46.986710 15.956811 1.202658 332 1 2 1 1.413386 45.007874 2764 30 187 46.303150 least-occurring-first 1 0 0 0 0 1168 1409 431 424 7 generated pdtvisvsa16a15_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 301 254 490 4308 46.986710 15.956811 1.202658 332 1 2 1 1.413386 45.007874 2746 30 187 46.303150 least-occurring-first 0 0 0 0 0 1152 1407 429 423 6 generated pdtvisvsa16a16_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2509 27 194 46.795277 least-occurring-first 0 0 0 0 0 1040 1276 407 385 22 generated pdtvisvsa16a17_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 293 254 490 4298 46.583618 15.706485 1.245734 333 1 3 1 1.425197 45.224411 2579 30 195 46.692913 least-occurring-first 0 0 0 0 0 1062 1323 437 395 42 generated pdtvisvsa16a18_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 289 254 490 4299 46.934258 15.809689 1.238754 332 1 4 1 1.393701 45.968502 2979 30 194 49.645668 least-occurring-first 0 0 0 0 0 1117 1668 458 420 38 generated pdtvisvsa16a19_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 303 254 490 4308 47.280529 16.168316 1.227723 332 1 2 1 1.452756 44.980316 2701 30 193 46.192913 least-occurring-first 1 0 0 0 0 1176 1332 424 410 14 generated pdtvisvsa16a20_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4307 45.925423 15.454237 1.247458 332 1 3 1 1.437008 45.094490 2592 28 194 46.653542 least-occurring-first 1 0 0 0 0 1039 1359 483 467 16 generated pdtvisvsa16a21_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2490 28 195 46.795277 least-occurring-first 0 0 0 0 0 1034 1264 392 376 16 generated pdtvisvsa16a22_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2502 26 194 46.795277 least-occurring-first 1 0 0 0 0 1080 1228 365 351 14 generated pdtvisvsa16a23_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2589 28 194 46.795277 least-occurring-first 1 0 0 0 0 1085 1252 381 370 11 generated pdtvisvsa16a24_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2487 28 193 46.795277 least-occurring-first 0 0 0 0 0 1035 1261 395 379 16 generated pdtvisvsa16a25_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2486 26 193 46.795277 least-occurring-first 0 0 0 0 0 1034 1261 388 353 35 generated pdtvisvsa16a26_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2492 28 193 46.795277 least-occurring-first 0 0 0 0 0 1037 1262 401 385 16 generated pdtvisvsa16a27_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 295 254 490 4303 45.555931 15.298306 1.237288 332 1 3 1 1.425197 45.145668 2527 28 193 46.795277 least-occurring-first 1 0 0 0 0 1057 1278 396 379 17 generated pdtvisvsa16a29_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 304 254 490 4301 44.575657 15.361842 1.194079 334 1 2 1 1.417323 44.799213 2611 30 196 45.897636 least-occurring-first 1 0 0 0 0 1078 1339 401 390 11 generated pdtvisvsa16a31_sat_-1_flattened_extra_bit_differing_from_cycle_tseitin.v prolient cegar_unoptimized_withnegf_withaccumulate 290 254 490 4296 46.437931 15.565517 1.251724 333 1 4 1 1.417323 45.614174 2649 34 199 47.748032 least-occurring-first 0 0 0 0 0 1049 1401 415 389 26