benchmark type = generated benchmark name = ../benchmarks/equalization/8.v problem = variable_elimination machine = prolient number of factors = 13 number of variables to eliminate = 16 number of variables = 32 aig sizes of factors = 93, 95, 95, 85, 71, 71, 61, 37, 47, 47, 25, 11, 11, variables in factors = 32, 32, 32, 28, 24, 24, 20, 12, 16, 16, 8, 4, 4, variables to eliminate in factors = 16, 16, 16, 14, 12, 12, 10, 6, 8, 8, 4, 2, 2, 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_8 3 1 121 124 124 0 163 9 0 57 0 13 0 1,2,3, 93,95,95, 2 i_2_8 1 1 195 188 188 1 320 3 0 4 0 13 0 3, 163, 3 i_1_7 2 5 350 419 419 5 622 6 0 21 0 13 0 3,4, 320,85, 4 i_2_7 1 48 958 789 789 42 1539 3 0 4 0 13 0 4, 622, 5 i_1_6 3 18 146 2431 2431 17 1643 9 0 45 0 13 1 4,5,6, 1539,71,71, 6 i_2_6 1 201 5675 2555 2555 197 7242 3 0 4 0 13 0 6, 1643, 7 i_1_5 2 54 112 9143 9143 50 7312 6 2 21 0 13 0 6,7, 7242,61, 8 i_2_5 1 546 1165 9345 9345 542 8430 3 3 4 0 13 0 7, 7312, 9 i_1_4 3 98 143 12625 12625 92 8541 9 5 45 0 13 1 7,9,10, 8430,47,47, 10 i_2_4 1 1424 7860 14407 14407 1411 16349 3 9 4 0 13 1 10, 8541, 11 i_1_3 2 185 135 25068 25068 159 16470 6 11 21 0 13 1 8,10, 37,16349, 12 i_2_3 1 3777 3792 26331 26331 3744 20222 3 24 4 0 13 1 10, 16470, 13 i_1_2 2 308 64 30110 30110 268 20283 6 16 21 0 13 1 10,11, 20222,25, 14 i_2_2 1 5560 49396 31603 31603 5518 69415 3 20 4 0 13 0 11, 20283, 15 i_1_1 3 548 17 82604 82604 443 69434 9 84 45 0 13 7 11,12,13, 69415,11,11, 16 i_2_1 1 22269 78100 82434 82434 22196 69434 2 52 4 0 13 8 13, 69434, total_number_of_compose_operations_in_initial_skolem_function_generation = 83 total_ComposeTime_in_initial_skolem_function_generation = 226 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 308 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 208 total_FactorFindingTime_in_initial_skolem_function_generation = 21 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 34963 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 4 total-time-in-initial-skolem-function-generation-without-size-computation-time = 34963 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 5046 milliseconds total-time-without-size-computation-time = 40009 milliseconds total-time-in-interpolant-computation = 34685 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 3 milliseconds total time in compute-size = 244 total time in compute-support = 5 total time in initialization of skolem function generator-without-size-computation-time = 4 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 = 92 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 152 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 = 244 milliseconds compose-in-reverse-substitution = 120 time-in-reverse-substitution = 5028 final-skolem-function-sizes = 144792, 144733, 144583, 144301, 143415, 143323, 137840, 137768, 136642, 136531, 128860, 128747, 125319, 125265, 78114, 78100,