benchmark type = generated benchmark name = ../benchmarks/avgceiling/16.v problem = variable_elimination machine = prolient number of factors = 1 number of variables to eliminate = 16 number of variables = 48 aig sizes of factors = 325, variables in factors = 48, variables to eliminate in factors = 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 1 2 14 376 376 1 331 3 0 4 0 1 0 1, 325, 2 i_10 1 1 41 360 360 1 362 3 0 4 0 1 0 1, 331, 3 i_11 1 1 43 387 387 1 390 3 0 4 0 1 0 1, 362, 4 i_12 1 1 53 411 411 1 423 3 0 4 0 1 0 1, 390, 5 i_13 1 2 86 440 440 2 482 3 0 4 0 1 0 1, 423, 6 i_14 1 3 128 495 495 3 580 3 0 4 0 1 0 1, 482, 7 i_15 1 2 81 590 590 2 630 3 0 4 0 1 0 1, 580, 8 i_16 1 3 85 645 645 2 674 3 1 4 0 1 0 1, 630, 9 i_2 1 2 33 727 727 2 691 3 0 4 0 1 0 1, 674, 10 i_3 1 2 46 741 741 2 718 3 0 4 0 1 0 1, 691, 11 i_4 1 3 80 765 765 2 775 3 1 4 0 1 0 1, 718, 12 i_5 1 3 104 819 819 2 851 3 1 4 0 1 0 1, 775, 13 i_6 1 4 109 892 892 4 930 3 0 4 0 1 0 1, 851, 14 i_7 1 4 193 968 968 4 1086 3 0 4 0 1 0 1, 930, 15 i_8 1 6 145 1121 1121 5 1187 3 0 4 0 1 0 1, 1086, 16 i_9 1 7 159 1554 1554 7 1187 2 0 4 0 1 0 1, 1187, total_number_of_compose_operations_in_initial_skolem_function_generation = 47 total_ComposeTime_in_initial_skolem_function_generation = 3 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 64 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 16 total_FactorFindingTime_in_initial_skolem_function_generation = 0 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 45 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 = 45 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 1 milliseconds total-time-without-size-computation-time = 46 milliseconds total-time-in-interpolant-computation = 41 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 2 total time in compute-support = 0 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 = 2 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 = 2 milliseconds compose-in-reverse-substitution = 120 time-in-reverse-substitution = 1 final-skolem-function-sizes = 14, 195, 197, 207, 240, 282, 292, 239, 33, 46, 80, 104, 109, 193, 145, 159,