benchmark type = generated benchmark name = ../benchmarks/avgceiling/128.v problem = variable_elimination machine = prolient number of factors = 1 number of variables to eliminate = 128 number of variables = 384 aig sizes of factors = 2677, variables in factors = 384, variables to eliminate in factors = 128, i: index of variable to be eliminated v: name of variable to be eliminated F_v: Number of factors with the variable to be eliminated T_v: Time (in milliseconds) to eliminate the variable N_v: Size of the skolem function psi_i = interpolant between alpha_i and beta_i Q_v: Size of the quantified result q_i = conjunction of factors with variable substituted by skolem function A_v: Size of alpha_i B_v: Size of beta_i I_T: Time consumed in computing interpolant between alpha_i and beta_i cmp_v: Number of composes in elimination of the variable cmp_T: Time consumed in composes in elimination of the variable B_v: Number of boolean operations in elimination of the variable B_T: Time consumed in boolean operations in elimination of the variable S_v: Number of support operations in elimination of the variable S_T: Time consumed in support operations in elimination of the variable I_v: Indices of factors containing the variable to be eliminated X_v: Sizes of factors containing the variable to be eliminated i v F_v T_v N_v A_v B_v I_T Q_v cmp_v cmp_T B_v B_T S_v S_T I_v X_v 1 i_1 1 6 15 3036 3036 4 2683 3 0 4 0 1 1 1, 2677, 2 i_10 1 8 34 3021 3021 7 2707 3 1 4 0 1 0 1, 2683, 3 i_100 1 6 42 2798 2798 5 2739 3 1 4 0 1 0 1, 2707, 4 i_101 1 7 67 2827 2827 5 2789 3 2 4 0 1 0 1, 2739, 5 i_102 1 6 75 2874 2874 5 2843 3 0 4 0 1 0 1, 2789, 6 i_103 1 8 164 2926 2926 7 2980 3 0 4 0 1 1 1, 2843, 7 i_104 1 30 127 3060 3060 28 3075 3 1 4 0 1 1 1, 2980, 8 i_105 1 15 142 3152 3152 14 3186 3 1 4 0 1 0 1, 3075, 9 i_106 1 23 123 3260 3260 23 3269 3 0 4 0 1 0 1, 3186, 10 i_107 1 25 221 3341 3341 23 3445 3 1 4 0 1 1 1, 3269, 11 i_108 1 23 192 3514 3514 22 3585 3 1 4 0 1 0 1, 3445, 12 i_109 1 36 398 3651 3651 35 3928 3 0 4 0 1 1 1, 3585, 13 i_11 1 20 100 4264 4264 18 4011 3 0 4 0 1 1 1, 3928, 14 i_110 1 48 333 4074 4074 46 4275 3 1 4 0 1 1 1, 4011, 15 i_111 1 44 251 4336 4336 42 4459 3 1 4 0 1 1 1, 4275, 16 i_112 1 53 330 4517 4517 52 4719 3 0 4 0 1 1 1, 4459, 17 i_113 1 47 453 4774 4774 44 5101 3 1 4 0 1 1 1, 4719, 18 i_114 1 75 424 5153 5153 73 5438 3 2 4 0 1 0 1, 5101, 19 i_115 1 64 491 5488 5488 61 5845 3 0 4 0 1 1 1, 5438, 20 i_116 1 73 556 5892 5892 68 6308 3 1 4 0 1 0 1, 5845, 21 i_117 1 92 624 6352 6352 90 6826 3 1 4 0 1 0 1, 6308, 22 i_118 1 128 744 6867 6867 121 7456 3 2 4 0 1 0 1, 6826, 23 i_119 1 101 548 7494 7494 98 7889 3 2 4 0 1 1 1, 7456, 24 i_12 1 46 114 8222 8222 37 7985 3 3 4 0 1 1 1, 7889, 25 i_120 1 89 575 8020 8020 86 8423 3 2 4 0 1 1 1, 7985, 26 i_121 1 136 813 8455 8455 128 9087 3 2 4 0 1 1 1, 8423, 27 i_122 1 195 834 9116 9116 183 9794 3 3 4 0 1 1 1, 9087, 28 i_123 1 134 777 9819 9819 126 10418 3 4 4 0 1 0 1, 9794, 29 i_124 1 168 1304 10439 10439 164 11572 3 2 4 0 1 1 1, 10418, 30 i_125 1 183 568 11589 11589 178 12000 3 2 4 0 1 1 1, 11572, 31 i_126 1 212 790 12013 12013 208 12641 3 3 4 0 1 0 1, 12000, 32 i_127 1 216 1015 12651 12651 210 13513 3 2 4 0 1 1 1, 12641, 33 i_128 1 126 441 14001 14001 121 13766 3 3 4 0 1 0 1, 13513, 34 i_13 1 61 102 14096 14096 55 13844 3 3 4 0 1 1 1, 13766, 35 i_14 1 68 141 14171 14171 62 13954 3 3 4 0 1 0 1, 13844, 36 i_15 1 69 236 14279 14279 60 14155 3 4 4 0 1 0 1, 13954, 37 i_16 1 87 161 14477 14477 71 14275 3 4 4 0 1 1 1, 14155, 38 i_17 1 72 185 14594 14594 66 14419 3 4 4 0 1 1 1, 14275, 39 i_18 1 84 347 14735 14735 72 14708 3 6 4 0 1 0 1, 14419, 40 i_19 1 84 239 15022 15022 72 14888 3 3 4 0 1 1 1, 14708, 41 i_2 1 69 32 15249 15249 59 14906 3 4 4 0 1 1 1, 14888, 42 i_20 1 105 296 15227 15227 100 15139 3 3 4 0 1 0 1, 14906, 43 i_21 1 100 419 15447 15447 90 15482 3 4 4 0 1 1 1, 15139, 44 i_22 1 125 328 15787 15787 115 15740 3 3 4 0 1 0 1, 15482, 45 i_23 1 93 204 16043 16043 83 15866 3 3 4 0 1 1 1, 15740, 46 i_24 1 108 479 16181 16181 101 16253 3 5 4 0 1 1 1, 15866, 47 i_25 1 127 266 16550 16550 111 16423 3 3 4 0 1 2 1, 16253, 48 i_26 1 115 369 16757 16757 104 16696 3 9 4 0 1 1 1, 16423, 49 i_27 1 179 810 17124 17124 165 17390 3 4 4 0 1 1 1, 16696, 50 i_28 1 161 625 17679 17679 147 17906 3 6 4 0 1 1 1, 17390, 51 i_29 1 175 562 18192 18192 157 18345 3 13 4 0 1 1 1, 17906, 52 i_3 1 96 78 18703 18703 81 18402 3 5 4 0 1 1 1, 18345, 53 i_30 1 226 690 18685 18685 185 18978 3 5 4 0 1 1 1, 18402, 54 i_31 1 244 540 19259 19259 233 19401 3 9 4 0 1 1 1, 18978, 55 i_32 1 246 603 19679 19679 224 19862 3 15 4 0 1 1 1, 19401, 56 i_33 1 313 1382 20137 20137 303 21096 3 6 4 0 1 2 1, 19862, 57 i_34 1 294 1609 21368 21368 280 22548 3 8 4 0 1 0 1, 21096, 58 i_35 1 345 715 22818 22818 324 23118 3 11 4 0 1 2 1, 22548, 59 i_36 1 303 1334 23385 23385 261 24306 3 37 4 0 1 2 1, 23118, 60 i_37 1 353 1407 24570 24570 336 25529 3 9 4 0 1 1 1, 24306, 61 i_38 1 422 1480 25790 25790 403 26833 3 15 4 0 1 1 1, 25529, 62 i_39 1 484 3205 27092 27092 465 29855 3 13 4 0 1 1 1, 26833, 63 i_4 1 163 120 30231 30231 133 29952 3 18 4 0 1 1 1, 29855, 64 i_40 1 583 1398 30208 30208 556 31172 3 12 4 0 1 1 1, 29952, 65 i_41 1 590 1859 31425 31425 561 32823 3 20 4 0 1 2 1, 31172, 66 i_42 1 487 1155 33073 33073 458 33796 3 14 4 0 1 3 1, 32823, 67 i_43 1 565 1546 34847 34847 535 35155 3 11 4 0 1 2 1, 33796, 68 i_44 1 561 919 35400 35400 499 35873 3 35 4 0 1 20 1, 35155, 69 i_45 1 598 1262 36672 36672 566 36922 3 22 4 0 1 2 1, 35873, 70 i_46 1 750 2129 37161 37161 709 38812 3 20 4 0 1 2 1, 36922, 71 i_47 1 651 1788 39049 39049 619 40356 3 24 4 0 1 2 1, 38812, 72 i_48 1 873 839 40590 40590 835 40969 3 28 4 0 1 1 1, 40356, 73 i_49 1 856 1877 41200 41200 820 42602 3 15 4 0 1 2 1, 40969, 74 i_5 1 283 113 43600 43600 241 42686 3 36 4 0 1 2 1, 42602, 75 i_50 1 925 1056 42914 42914 879 43517 3 24 4 0 1 2 1, 42686, 76 i_51 1 818 1246 43743 43743 772 44553 3 32 4 0 1 3 1, 43517, 77 i_52 1 938 1389 44776 44776 888 45699 3 25 4 0 1 3 1, 44553, 78 i_53 1 903 1946 46358 46358 866 47351 3 26 4 0 1 2 1, 45699, 79 i_54 1 830 1961 47568 47568 778 49048 3 36 4 0 1 2 1, 47351, 80 i_55 1 1252 2363 49263 49263 1206 51149 3 36 4 0 1 3 1, 49048, 81 i_56 1 1089 2402 51361 51361 1046 53245 3 30 4 0 1 3 1, 51149, 82 i_57 1 1258 1599 53454 53454 1207 54574 3 25 4 0 1 9 1, 53245, 83 i_58 1 1370 2928 54780 54780 1317 57241 3 30 4 0 1 10 1, 54574, 84 i_59 1 1271 1650 57445 57445 1219 58602 3 37 4 0 1 9 1, 57241, 85 i_6 1 330 103 59596 59596 270 58671 3 46 4 0 1 9 1, 58602, 86 i_60 1 1569 4003 58872 58872 1516 62372 3 38 4 0 1 2 1, 58671, 87 i_61 1 1377 1883 62570 62570 1303 63987 3 38 4 6 1 9 1, 62372, 88 i_62 1 1254 1367 64182 64182 1177 65070 3 54 4 0 1 4 1, 63987, 89 i_63 1 1720 1553 65263 65263 1663 66347 3 42 4 0 1 4 1, 65070, 90 i_64 1 1362 1414 66537 66537 1303 67480 3 44 4 0 1 8 1, 66347, 91 i_65 1 1449 1221 67667 67667 1404 68390 3 32 4 0 1 3 1, 67480, 92 i_66 1 2347 3262 68574 68574 2268 71324 3 51 4 0 1 9 1, 68390, 93 i_67 1 2460 3450 71506 71506 2381 74478 3 51 4 0 1 12 1, 71324, 94 i_68 1 2135 2844 74657 74657 2054 76956 3 60 4 0 1 3 1, 74478, 95 i_69 1 2029 2982 77132 77132 1945 79639 3 50 4 0 1 4 1, 76956, 96 i_7 1 447 103 80628 80628 358 79703 3 58 4 0 1 4 1, 79639, 97 i_70 1 2050 1469 79876 79876 1960 80870 3 61 4 0 1 4 1, 79703, 98 i_71 1 2627 3269 81041 81041 2524 83808 3 76 4 0 1 8 1, 80870, 99 i_72 1 1596 2082 83976 83976 1503 85589 3 67 4 0 1 9 1, 83808, 100 i_73 1 2759 2947 87218 87218 2656 88182 3 59 4 0 1 12 1, 85589, 101 i_74 1 2692 2220 88344 88344 2593 89972 3 65 4 0 1 4 1, 88182, 102 i_75 1 2525 2893 90132 90132 2425 92436 3 71 4 1 1 4 1, 89972, 103 i_76 1 2631 5318 92593 92593 2525 97365 3 75 4 0 1 9 1, 92436, 104 i_77 1 2879 1969 97519 97519 2763 99003 3 74 4 0 1 8 1, 97365, 105 i_78 1 3099 2055 99154 99154 2976 100676 3 81 4 0 1 13 1, 99003, 106 i_79 1 2580 1440 100825 100825 2442 101762 3 91 4 0 1 10 1, 100676, 107 i_8 1 621 210 103592 103592 486 101931 3 95 4 0 1 13 1, 101762, 108 i_80 1 3938 3377 102077 102077 3811 104912 3 98 4 0 1 4 1, 101931, 109 i_81 1 3281 2537 105055 105055 3140 107027 3 96 4 0 1 10 1, 104912, 110 i_82 1 3334 2015 107167 107167 3206 108691 3 90 4 0 1 5 1, 107027, 111 i_83 1 3432 1603 108829 108829 3276 109917 3 116 4 0 1 12 1, 108691, 112 i_84 1 3977 3374 110052 110052 3794 112910 3 131 4 0 1 7 1, 109917, 113 i_85 1 4255 1917 113042 113042 4102 114424 3 118 4 0 1 6 1, 112910, 114 i_86 1 3397 3250 114553 114553 3250 117272 3 101 4 0 1 11 1, 114424, 115 i_87 1 4976 3910 117399 117399 4834 120741 3 108 4 0 1 10 1, 117272, 116 i_88 1 4962 2515 120865 120865 4824 122881 3 95 4 0 1 16 1, 120741, 117 i_89 1 5735 5174 123002 123002 5578 127584 3 120 4 0 1 6 1, 122881, 118 i_9 1 1107 254 191811 191811 769 127784 3 272 4 0 1 14 1, 127584, 119 i_90 1 4165 1728 127902 127902 4010 129077 3 101 4 0 1 15 1, 127784, 120 i_91 1 5280 3171 129583 129583 5126 131802 3 109 4 0 1 17 1, 129077, 121 i_92 1 5021 4259 131915 131915 4837 135584 3 138 4 0 1 18 1, 131802, 122 i_93 1 5739 3120 135694 135694 5577 138247 3 114 4 0 1 18 1, 135584, 123 i_94 1 6396 6762 138354 138354 6196 144521 3 144 4 0 1 14 1, 138247, 124 i_95 1 3688 1753 144626 144626 3476 145853 3 149 4 0 1 15 1, 144521, 125 i_96 1 6340 2929 146474 146474 6127 148313 3 154 4 0 1 10 1, 145853, 126 i_97 1 6844 3424 148412 148412 6619 151225 3 159 4 0 1 15 1, 148313, 127 i_98 1 6441 3848 151321 151321 6211 154555 3 170 4 0 1 15 1, 151225, 128 i_99 1 6764 3323 162580 162580 6596 154555 2 107 4 0 1 16 1, 154555, total_number_of_compose_operations_in_initial_skolem_function_generation = 383 total_ComposeTime_in_initial_skolem_function_generation = 4887 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 512 total_BooleanOpTime_in_initial_skolem_function_generation = 7 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 128 total_FactorFindingTime_in_initial_skolem_function_generation = 551 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 167194 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 2 total-time-in-initial-skolem-function-generation-without-size-computation-time = 167194 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 4461 milliseconds total-time-without-size-computation-time = 171655 milliseconds total-time-in-interpolant-computation = 161681 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 1 milliseconds total time in compute-size = 1755 total time in compute-support = 149 total time in initialization of skolem function generator-without-size-computation-time = 2 total time in sat solving = 0 solver used = abc number of cegar iterations = 0 Compose Details: Hit_1 = 0 Miss_1 = 0 Hit_2 = 0 Miss_2 = 0 Leaves = 0 Non-leaves = 0 No-create-expr = 0 Create-expr = 0 Create-expr/Miss_2 = -nan size_computation_time_in_initialization = 0 milliseconds size_computation_time_in_initial_abstraction_generation_in_cegar = 1723 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 32 milliseconds size_computation_time_in_cegar_loops_in_cegar = 0 milliseconds size_computation_time_in_connection_substitution_in_cegar = 0 milliseconds total_time_in_compute_size = 1755 milliseconds compose-in-reverse-substitution = 8128 time-in-reverse-substitution = 4117 final-skolem-function-sizes = 15, 283, 3360, 3385, 3393, 3482, 3445, 3457, 3441, 3539, 3505, 3716, 349, 3646, 3569, 3648, 3771, 3739, 3805, 3874, 3938, 4062, 3866, 363, 3891, 4131, 4152, 4090, 4622, 3881, 4106, 4650, 3759, 351, 390, 485, 410, 434, 591, 728, 32, 545, 668, 577, 858, 724, 1690, 1503, 1220, 874, 806, 177, 939, 784, 848, 1627, 1853, 964, 1583, 1651, 1724, 3449, 120, 1642, 2108, 2793, 1792, 2265, 1511, 2739, 2032, 1088, 2287, 113, 1300, 1490, 3358, 2190, 2205, 2607, 2646, 1843, 3177, 1894, 103, 4241, 2127, 1609, 1797, 1659, 1465, 3506, 3699, 3093, 3231, 103, 1713, 3513, 4997, 3191, 2467, 3137, 5567, 2213, 2299, 1684, 210, 3626, 2781, 2259, 1848, 3623, 2166, 3494, 4159, 2759, 5423, 254, 4519, 3171, 4259, 3120, 6762, 4284, 2929, 3424, 3848, 3323,