benchmark type = generated benchmark name = ../benchmarks/min/128.v problem = variable_elimination machine = prolient number of factors = 5 number of variables to eliminate = 128 number of variables = 384 aig sizes of factors = 764, 764, 3, 3, 1407, variables in factors = 256, 256, 2, 2, 384, variables to eliminate in factors = 128, 128, 1, 1, 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 3 78 1305 1944 1944 77 2326 9 0 49 0 5 1 1,2,5, 764,764,1407, 2 i_10 1 89 1103 2707 2707 89 2867 3 0 4 0 5 0 5, 2326, 3 i_100 1 20 342 3972 3972 19 3093 3 0 4 0 5 1 5, 2867, 4 i_101 1 38 331 4372 4372 32 3312 3 2 4 0 5 1 5, 3093, 5 i_102 1 33 318 4757 4757 26 3522 3 1 4 0 5 0 5, 3312, 6 i_103 1 37 307 5124 5124 35 3725 3 2 4 0 5 0 5, 3522, 7 i_104 1 43 294 5495 5495 42 3919 3 1 4 0 5 0 5, 3725, 8 i_105 1 61 283 5843 5843 54 4106 3 2 4 0 5 1 5, 3919, 9 i_106 1 55 270 6177 6177 52 4284 3 2 4 0 5 0 5, 4106, 10 i_107 1 94 259 6498 6498 64 4455 3 28 4 0 5 1 5, 4284, 11 i_108 1 86 246 6805 6805 77 4617 3 5 4 0 5 0 5, 4455, 12 i_109 1 85 235 7100 7100 82 4772 3 3 4 0 5 0 5, 4617, 13 i_11 1 281 1193 5626 5626 278 5408 3 2 4 0 5 1 5, 4772, 14 i_110 1 111 222 8784 8784 107 5554 3 2 4 0 5 0 5, 5408, 15 i_111 1 124 211 9058 9058 114 5693 3 3 4 0 5 1 5, 5554, 16 i_112 1 158 198 9325 9325 153 5823 3 4 4 0 5 1 5, 5693, 17 i_113 1 173 187 9571 9571 168 5946 3 3 4 0 5 0 5, 5823, 18 i_114 1 212 174 9798 9798 201 6060 3 2 4 0 5 1 5, 5946, 19 i_115 1 191 163 10014 10014 184 6167 3 4 4 0 5 1 5, 6060, 20 i_116 1 242 150 10221 10221 231 6265 3 8 4 0 5 1 5, 6167, 21 i_117 1 320 139 10411 10411 310 6356 3 6 4 0 5 0 5, 6265, 22 i_118 1 353 126 10586 10586 338 6438 3 13 4 0 5 1 5, 6356, 23 i_119 1 396 115 10750 10750 384 6513 3 10 4 0 5 0 5, 6438, 24 i_12 1 620 1410 7520 7520 602 7350 3 12 4 0 5 1 5, 6513, 25 i_120 1 316 102 11996 11996 255 7416 3 58 4 0 5 1 5, 7350, 26 i_121 1 342 91 12139 12139 332 7475 3 4 4 0 5 0 5, 7416, 27 i_122 1 431 78 12263 12263 425 7525 3 3 4 0 5 1 5, 7475, 28 i_123 1 388 70 12374 12374 379 7569 3 4 4 0 5 0 5, 7525, 29 i_124 1 334 52 12475 12475 323 7601 3 9 4 0 5 1 5, 7569, 30 i_125 1 378 41 12558 12558 367 7626 3 5 4 0 5 0 5, 7601, 31 i_126 1 496 23 12622 12622 490 7638 3 5 4 0 5 1 5, 7626, 32 i_127 1 511 10 12646 12646 505 7640 3 4 4 0 5 1 5, 7638, 33 i_13 1 699 2240 9122 9122 690 9373 3 5 4 0 5 0 5, 7640, 34 i_14 1 660 1758 11648 11648 649 10580 3 8 4 0 5 0 5, 9373, 35 i_15 1 898 1966 13383 13383 891 12018 3 6 4 0 5 1 5, 10580, 36 i_16 1 745 1471 15812 15812 727 12941 3 15 4 0 5 1 5, 12018, 37 i_17 1 818 1621 17172 17172 802 14012 3 12 4 0 5 0 5, 12941, 38 i_18 1 685 1678 18791 18791 672 15096 3 8 4 0 5 1 5, 14012, 39 i_19 1 1047 1374 20543 20543 1025 15889 3 16 4 0 5 1 5, 15096, 40 i_2 1 994 2121 16643 16643 974 17321 3 17 4 0 5 1 5, 15889, 41 i_20 1 1085 1373 24131 24131 1043 18147 3 37 4 0 5 2 5, 17321, 42 i_21 1 974 1565 25477 25477 939 19134 3 23 4 0 5 1 5, 18147, 43 i_22 1 878 1688 26989 26989 854 20296 3 21 4 0 5 1 5, 19134, 44 i_23 1 963 1519 28786 28786 933 21214 3 26 4 0 5 2 5, 20296, 45 i_24 1 1108 1398 30187 30187 1064 22097 3 36 4 1 5 3 5, 21214, 46 i_25 1 1274 1467 31554 31554 1228 23006 3 29 4 0 5 8 5, 22097, 47 i_26 1 1157 1689 32924 32924 1117 24187 3 26 4 0 5 2 5, 23006, 48 i_27 1 1271 1288 34767 34767 1215 24937 3 46 4 0 5 1 5, 24187, 49 i_28 1 1354 1591 35866 35866 1312 25927 3 37 4 0 5 1 5, 24937, 50 i_29 1 1264 1391 37574 37574 1230 26823 3 28 4 0 5 3 5, 25927, 51 i_3 1 1606 3258 28295 28295 1565 29381 3 30 4 0 5 1 5, 26823, 52 i_30 1 1601 1625 42329 42329 1530 30474 3 59 4 0 5 1 5, 29381, 53 i_31 1 1866 1627 43948 43948 1349 31512 3 505 4 0 5 1 5, 30474, 54 i_32 1 1250 1338 45614 45614 1209 32391 3 33 4 0 5 2 5, 31512, 55 i_33 1 1458 1568 47006 47006 1397 33442 3 41 4 0 5 8 5, 32391, 56 i_34 1 1686 1278 48830 48830 1620 34242 3 38 4 1 5 8 5, 33442, 57 i_35 1 1802 1496 50058 50058 1728 35301 3 49 4 0 5 2 5, 34242, 58 i_36 1 1857 1675 51914 51914 1797 36447 3 44 4 0 5 3 5, 35301, 59 i_37 1 1871 1518 53783 53783 1821 37457 3 39 4 0 5 1 5, 36447, 60 i_38 1 2162 1355 55262 55262 2093 38284 3 52 4 0 5 2 5, 37457, 61 i_39 1 1825 1911 56668 56668 1750 39663 3 55 4 0 5 2 5, 38284, 62 i_4 1 2615 3027 41182 41182 2547 42095 3 47 4 0 5 3 5, 39663, 63 i_40 1 2354 2116 61987 61987 2269 43695 3 61 4 0 5 3 5, 42095, 64 i_41 1 2439 1905 64129 64129 2352 45109 3 62 4 0 5 3 5, 43695, 65 i_42 1 2396 1797 66208 66208 2304 46429 3 76 4 0 5 2 5, 45109, 66 i_43 1 2517 1205 68383 68383 2425 47182 3 69 4 0 5 3 5, 46429, 67 i_44 1 2674 990 69668 69668 2560 47765 3 82 4 0 5 7 5, 47182, 68 i_45 1 2709 1363 70675 70675 2617 48680 3 72 4 0 5 3 5, 47765, 69 i_46 1 3063 1785 72092 72092 2958 49941 3 79 4 0 5 10 5, 48680, 70 i_47 1 3109 2325 74295 74295 3000 51840 3 83 4 0 5 3 5, 49941, 71 i_48 1 2817 1616 77526 77526 2723 53032 3 74 4 0 5 3 5, 51840, 72 i_49 1 2952 1670 79498 79498 2870 54252 3 72 4 0 5 3 5, 53032, 73 i_5 1 4763 3364 55798 55798 4650 56898 3 91 4 0 5 3 5, 54252, 74 i_50 1 3264 1167 85574 85574 3140 57635 3 98 4 0 5 3 5, 56898, 75 i_51 1 3237 965 86636 86636 3103 58179 3 110 4 0 5 3 5, 57635, 76 i_52 1 3100 1007 87739 87739 2971 58825 3 111 4 0 5 3 5, 58179, 77 i_53 1 3243 1027 88957 88957 3111 59444 3 106 4 0 5 8 5, 58825, 78 i_54 1 3574 1087 90017 90017 3439 60120 3 105 4 0 5 3 5, 59444, 79 i_55 1 3937 925 91106 91106 3803 60616 3 105 4 0 5 7 5, 60120, 80 i_56 1 4185 1381 92013 92013 4043 61584 3 114 4 0 5 7 5, 60616, 81 i_57 1 3948 1267 93615 93615 3790 62464 3 125 4 0 5 3 5, 61584, 82 i_58 1 4466 1420 95087 95087 4300 63498 3 140 4 0 5 5 5, 62464, 83 i_59 1 3825 1441 96657 96657 3668 64543 3 122 4 0 5 13 5, 63498, 84 i_6 1 4573 4318 67689 67689 4455 68200 3 102 4 0 5 4 5, 64543, 85 i_60 1 4118 1603 103144 103144 3931 69392 3 156 4 0 5 3 5, 68200, 86 i_61 1 5455 1511 105137 105137 4254 70447 3 1172 4 0 5 4 5, 69392, 87 i_62 1 4444 1309 107047 107047 4295 71436 3 111 4 0 5 6 5, 70447, 88 i_63 1 4758 1287 108813 108813 4622 72377 3 99 4 0 5 4 5, 71436, 89 i_64 1 4579 1381 110282 110282 4434 73366 3 117 4 0 5 3 5, 72377, 90 i_65 1 4547 947 111811 111811 4435 74011 3 89 4 0 5 4 5, 73366, 91 i_66 1 4984 835 112826 112826 4879 74473 3 77 4 0 5 4 5, 74011, 92 i_67 1 5088 1008 113370 113370 4906 75134 3 137 4 0 5 14 5, 74473, 93 i_68 1 5437 1233 114902 114902 5288 76034 3 119 4 0 5 6 5, 75134, 94 i_69 1 5223 1510 116479 116479 5073 77192 3 108 4 0 5 13 5, 76034, 95 i_7 1 6140 2642 82311 82311 6003 79209 3 109 4 0 5 9 5, 77192, 96 i_70 1 5756 1017 122330 122330 5586 79937 3 138 4 0 5 12 5, 79209, 97 i_71 1 6110 992 123856 123856 5940 80581 3 125 4 0 5 10 5, 79937, 98 i_72 1 6097 1229 125136 125136 5932 81478 3 113 4 0 5 10 5, 80581, 99 i_73 1 6255 1084 126710 126710 6094 82282 3 120 4 0 5 4 5, 81478, 100 i_74 1 6289 1075 128098 128098 6111 83119 3 131 4 0 5 5 5, 82282, 101 i_75 1 6744 1129 129461 129461 6563 83964 3 129 4 0 5 4 5, 83119, 102 i_76 1 6702 956 130845 130845 6558 84685 3 110 4 0 5 5 5, 83964, 103 i_77 1 6787 784 132039 132039 6617 85242 3 139 4 0 5 4 5, 84685, 104 i_78 1 6555 901 133016 133016 6390 85927 3 117 4 0 5 8 5, 85242, 105 i_79 1 6700 865 134310 134310 6515 86556 3 138 4 0 5 9 5, 85927, 106 i_8 1 7876 3181 92761 92761 7712 89174 3 126 4 0 5 9 5, 86556, 107 i_80 1 6954 849 139193 139193 6758 89819 3 146 4 0 5 5 5, 89174, 108 i_81 1 7181 821 140423 140423 6972 90463 3 155 4 0 5 9 5, 89819, 109 i_82 1 7481 821 141609 141609 7260 91095 3 158 4 0 5 11 5, 90463, 110 i_83 1 7343 694 142734 142734 7124 91619 3 151 4 0 5 5 5, 91095, 111 i_84 1 7842 635 144424 144424 7629 92107 3 160 4 0 5 5 5, 91619, 112 i_85 1 8061 711 145334 145334 7852 92671 3 156 4 0 5 7 5, 92107, 113 i_86 1 8206 707 146534 146534 7985 93234 3 153 4 0 5 9 5, 92671, 114 i_87 1 8145 600 147612 147612 7933 93709 3 170 4 0 5 8 5, 93234, 115 i_88 1 8900 620 148648 148648 8673 94206 3 167 4 0 5 9 5, 93709, 116 i_89 1 8764 611 149723 149723 8512 94700 3 193 4 0 5 10 5, 94206, 117 i_9 1 10297 3419 101976 101976 10090 97518 3 158 4 0 5 15 5, 94700, 118 i_90 1 8983 633 155107 155107 8736 98037 3 184 4 0 5 5 5, 97518, 119 i_91 1 8790 565 156229 156229 8563 98496 3 184 4 0 5 7 5, 98037, 120 i_92 1 9385 639 157196 157196 9140 99029 3 198 4 0 5 6 5, 98496, 121 i_93 1 9801 595 158243 158243 9517 99523 3 214 4 0 5 24 5, 99029, 122 i_94 1 11271 560 159299 159299 11034 99989 3 192 4 0 5 10 5, 99523, 123 i_95 1 11038 549 160217 160217 10782 100446 3 210 4 0 5 10 5, 99989, 124 i_96 1 32881 547 161214 161214 17351 100905 3 15471 4 0 5 9 5, 100446, 125 i_97 1 47521 516 162070 162070 36158 101336 3 11185 4 0 5 16 5, 100905, 126 i_98 1 28535 585 162879 162879 25554 101837 3 2722 4 0 5 90 5, 101336, 127 i_99 1 124460 537 163947 163947 37593 102307 3 86539 4 0 5 94 5, 101837, 128 i_128 3 34833 3 174992 174996 28978 102307 6 5139 41 0 5 72 3,4,5, 3,3,102307, total_number_of_compose_operations_in_initial_skolem_function_generation = 393 total_ComposeTime_in_initial_skolem_function_generation = 131339 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 594 total_BooleanOpTime_in_initial_skolem_function_generation = 2 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 640 total_FactorFindingTime_in_initial_skolem_function_generation = 769 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 661354 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 8 total-time-in-initial-skolem-function-generation-without-size-computation-time = 661354 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 145961 milliseconds total-time-without-size-computation-time = 807335 milliseconds total-time-in-interpolant-computation = 527449 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 5 milliseconds total time in compute-size = 3122 total time in compute-support = 279 total time in initialization of skolem function generator-without-size-computation-time = 8 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 = 2302 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 820 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 = 3122 milliseconds compose-in-reverse-substitution = 8128 time-in-reverse-substitution = 145838 final-skolem-function-sizes = 101440, 80624, 3432, 3202, 2978, 2764, 2556, 2358, 2166, 1984, 1808, 1642, 78144, 1482, 1332, 1188, 1054, 926, 808, 696, 594, 498, 412, 76401, 332, 262, 198, 144, 93, 57, 26, 10, 75301, 73641, 72492, 71086, 70208, 69191, 68152, 87579, 67398, 66604, 65629, 64482, 63575, 62698, 61789, 60619, 59885, 58899, 76865, 58015, 56930, 55890, 55012, 53962, 53161, 52100, 50946, 49951, 49123, 64110, 47738, 46136, 44712, 43383, 42638, 42043, 41121, 39841, 37931, 36730, 49496, 35491, 34743, 34166, 33509, 32870, 32184, 31670, 30677, 29783, 28731, 39086, 27651, 26437, 25351, 24342, 23349, 22331, 21661, 21132, 20443, 19525, 26205, 18322, 17571, 16888, 15942, 15098, 14233, 13349, 12599, 12011, 11302, 16555, 10635, 9955, 9289, 8624, 8079, 7579, 6999, 6422, 5940, 5434, 8236, 4934, 4406, 3941, 3399, 2896, 2426, 1961, 1498, 1056, 537, 3,