benchmark type = generated benchmark name = ../benchmarks/min/16.v problem = variable_elimination machine = prolient number of factors = 5 number of variables to eliminate = 16 number of variables = 48 aig sizes of factors = 92, 92, 3, 3, 175, variables in factors = 32, 32, 2, 2, 48, variables to eliminate in factors = 16, 16, 1, 1, 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 3 1 125 258 258 1 255 9 0 49 0 5 0 1,2,5, 92,92,175, 2 i_10 1 4 74 345 345 3 302 3 0 4 0 5 0 5, 255, 3 i_11 1 3 67 428 428 3 345 3 0 4 0 5 0 5, 302, 4 i_12 1 4 52 507 507 4 377 3 0 4 0 5 0 5, 345, 5 i_13 1 4 41 561 561 3 402 3 0 4 0 5 1 5, 377, 6 i_14 1 6 23 606 606 6 414 3 0 4 0 5 0 5, 402, 7 i_15 1 6 10 631 631 6 416 3 0 4 0 5 0 5, 414, 8 i_2 1 8 267 501 501 8 626 3 0 4 0 5 0 5, 416, 9 i_3 1 7 208 901 901 7 788 3 0 4 0 5 0 5, 626, 10 i_4 1 7 197 1206 1206 6 942 3 1 4 0 5 0 5, 788, 11 i_5 1 11 186 1497 1497 6 1089 3 5 4 0 5 0 5, 942, 12 i_6 1 9 178 1777 1777 8 1232 3 1 4 0 5 0 5, 1089, 13 i_7 1 12 264 2047 2047 11 1464 3 1 4 0 5 0 5, 1232, 14 i_8 1 13 147 2477 2477 12 1583 3 1 4 0 5 0 5, 1464, 15 i_9 1 19 134 2714 2714 18 1694 3 0 4 0 5 0 5, 1583, 16 i_16 3 37 3 2914 2918 34 1694 6 1 41 0 5 0 3,4,5, 3,3,1694, total_number_of_compose_operations_in_initial_skolem_function_generation = 57 total_ComposeTime_in_initial_skolem_function_generation = 10 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 146 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 80 total_FactorFindingTime_in_initial_skolem_function_generation = 1 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 153 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 3 total-time-in-initial-skolem-function-generation-without-size-computation-time = 153 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 6 milliseconds total-time-without-size-computation-time = 159 milliseconds total-time-in-interpolant-computation = 136 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 3 milliseconds total time in compute-size = 4 total time in compute-support = 1 total time in initialization of skolem function generator-without-size-computation-time = 3 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 = 4 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 0 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 = 4 milliseconds compose-in-reverse-substitution = 120 time-in-reverse-substitution = 2 final-skolem-function-sizes = 1568, 192, 141, 93, 57, 26, 10, 1335, 1118, 952, 794, 642, 495, 258, 134, 3,