benchmark type = generated benchmark name = ../benchmarks/decomposition/8.v problem = variable_elimination machine = prolient number of factors = 14 number of variables to eliminate = 16 number of variables = 24 aig sizes of factors = 39, 43, 43, 13, 19, 13, 25, 25, 9, 19, 31, 31, 49, 49, variables in factors = 13, 15, 15, 5, 7, 5, 9, 9, 3, 7, 11, 11, 17, 17, variables to eliminate in factors = 12, 14, 14, 4, 6, 4, 8, 8, 2, 6, 10, 10, 16, 16, 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 2 1 156 60 60 1 173 6 0 34 0 14 0 13,14, 49,49, 2 i_2_8 1 2 1 203 203 2 156 3 0 4 0 14 0 14, 173, 3 i_1_7 3 1 66 220 220 1 202 9 0 45 0 14 0 2,3,14, 43,43,156, 4 i_2_7 1 2 146 252 252 2 333 3 0 4 0 14 0 14, 202, 5 i_1_6 2 2 107 456 456 2 423 6 0 21 0 14 0 1,14, 39,333, 6 i_2_6 1 22 700 565 565 22 1089 3 0 4 0 14 0 14, 423, 7 i_1_5 3 11 71 1546 1546 9 1146 9 0 45 0 14 1 11,12,14, 31,31,1089, 8 i_2_5 1 29 3315 1572 1572 27 4371 3 0 4 0 14 1 14, 1146, 9 i_1_4 3 40 37 5791 5791 38 4396 9 2 45 0 14 0 7,8,14, 25,25,4371, 10 i_2_4 1 211 1 5479 5479 208 2999 3 2 4 0 14 1 14, 4396, 11 i_1_3 3 23 38 4676 4676 21 3032 9 2 45 0 14 0 5,10,14, 19,19,2999, 12 i_2_3 1 115 1610 4708 4708 108 4574 3 3 4 0 14 0 14, 3032, 13 i_1_2 3 69 26 6646 6646 59 4602 9 2 45 0 14 0 4,6,14, 13,13,4574, 14 i_2_2 1 277 23646 6669 6669 269 28151 3 3 4 0 14 0 14, 4602, 15 i_1_1 2 112 12 31279 31279 76 28167 6 33 21 0 14 1 9,14, 9,28151, 16 i_2_1 1 1409 74556 31264 31264 1386 28167 2 17 4 0 14 1 14, 28167, total_number_of_compose_operations_in_initial_skolem_function_generation = 86 total_ComposeTime_in_initial_skolem_function_generation = 64 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 333 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 224 total_FactorFindingTime_in_initial_skolem_function_generation = 5 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 2316 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 0 total-time-in-initial-skolem-function-generation-without-size-computation-time = 2316 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 1790 milliseconds total-time-without-size-computation-time = 4172 milliseconds total-time-in-interpolant-computation = 2231 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 114 total time in compute-support = 3 total time in initialization of skolem function generator-without-size-computation-time = 0 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 = 48 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 66 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 = 114 milliseconds compose-in-reverse-substitution = 120 time-in-reverse-substitution = 1774 final-skolem-function-sizes = 102204, 1, 102122, 102092, 102015, 101954, 101532, 101488, 99361, 1, 99345, 99316, 97799, 23646, 74567, 74556,