benchmark type = generated benchmark name = ../benchmarks/min/32.v problem = variable_elimination machine = prolient number of factors = 5 number of variables to eliminate = 32 number of variables = 96 aig sizes of factors = 188, 188, 3, 3, 351, variables in factors = 64, 64, 2, 2, 96, variables to eliminate in factors = 32, 32, 1, 1, 32, 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 7 260 502 502 7 518 9 0 49 0 5 0 1,2,5, 188,188,351, 2 i_10 1 6 270 681 681 5 696 3 0 4 0 5 1 5, 518, 3 i_11 1 8 259 998 998 7 867 3 0 4 0 5 1 5, 696, 4 i_12 1 9 246 1303 1303 8 1029 3 0 4 0 5 0 5, 867, 5 i_13 1 11 235 1586 1586 11 1184 3 0 4 0 5 0 5, 1029, 6 i_14 1 15 222 1862 1862 15 1330 3 0 4 0 5 0 5, 1184, 7 i_15 1 20 211 2123 2123 19 1469 3 1 4 0 5 0 5, 1330, 8 i_16 1 21 198 2372 2372 19 1599 3 2 4 0 5 0 5, 1469, 9 i_17 1 29 187 2609 2609 27 1722 3 2 4 0 5 0 5, 1599, 10 i_18 1 27 174 2828 2828 26 1836 3 1 4 0 5 0 5, 1722, 11 i_19 1 37 163 3037 3037 36 1943 3 0 4 0 5 0 5, 1836, 12 i_2 1 42 541 2053 2053 39 2353 3 0 4 0 5 1 5, 1943, 13 i_20 1 37 150 3815 3815 35 2451 3 2 4 0 5 0 5, 2353, 14 i_21 1 44 139 3993 3993 38 2542 3 1 4 0 5 0 5, 2451, 15 i_22 1 58 126 4168 4168 56 2624 3 2 4 0 5 0 5, 2542, 16 i_23 1 99 115 4328 4328 96 2699 3 2 4 0 5 1 5, 2624, 17 i_24 1 111 102 4469 4469 90 2765 3 19 4 0 5 0 5, 2699, 18 i_25 1 82 91 4605 4605 79 2824 3 3 4 0 5 0 5, 2765, 19 i_26 1 122 74 4726 4726 106 2871 3 15 4 0 5 0 5, 2824, 20 i_27 1 91 67 4825 4825 89 2914 3 1 4 0 5 1 5, 2871, 21 i_28 1 104 52 4920 4920 94 2946 3 2 4 0 5 1 5, 2914, 22 i_29 1 111 41 4996 4996 104 2971 3 1 4 0 5 0 5, 2946, 23 i_3 1 134 471 3483 3483 131 3358 3 2 4 0 5 1 5, 2971, 24 i_30 1 148 23 5696 5696 145 3370 3 2 4 0 5 0 5, 3358, 25 i_31 1 136 10 5722 5722 134 3372 3 2 4 0 5 0 5, 3370, 26 i_4 1 138 459 4256 4256 137 3757 3 1 4 0 5 0 5, 3372, 27 i_5 1 162 444 4983 4983 159 4130 3 2 4 0 5 1 5, 3757, 28 i_6 1 138 433 5692 5692 135 4496 3 3 4 0 5 0 5, 4130, 29 i_7 1 180 594 6385 6385 178 5027 3 2 4 0 5 0 5, 4496, 30 i_8 1 195 411 7349 7349 187 5378 3 3 4 0 5 0 5, 5027, 31 i_9 1 216 439 8022 8022 208 5762 3 4 4 0 5 1 5, 5378, 32 i_32 3 222 3 10203 10207 217 5762 6 2 41 0 5 1 3,4,5, 3,3,5762, total_number_of_compose_operations_in_initial_skolem_function_generation = 105 total_ComposeTime_in_initial_skolem_function_generation = 77 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 210 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 160 total_FactorFindingTime_in_initial_skolem_function_generation = 10 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 2757 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 1 total-time-in-initial-skolem-function-generation-without-size-computation-time = 2757 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 87 milliseconds total-time-without-size-computation-time = 2844 milliseconds total-time-in-interpolant-computation = 2637 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 12 total time in compute-support = 7 total time in initialization of skolem function generator-without-size-computation-time = 1 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 = 11 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 1 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 = 12 milliseconds compose-in-reverse-substitution = 496 time-in-reverse-substitution = 49 final-skolem-function-sizes = 5515, 2160, 1978, 1802, 1636, 1476, 1326, 1182, 1048, 920, 802, 3951, 690, 588, 492, 406, 326, 256, 192, 141, 93, 57, 2878, 26, 10, 2466, 2079, 1701, 1331, 795, 439, 3,