benchmark type = generated benchmark name = ../benchmarks/intermediate/8.v problem = variable_elimination machine = prolient number of factors = 1 number of variables to eliminate = 8 number of variables = 24 aig sizes of factors = 119, variables in factors = 24, variables to eliminate in factors = 8, 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 31 138 140 140 30 211 3 0 4 0 1 0 1, 119, 2 i_2 1 12 395 305 305 11 558 3 0 4 0 1 0 1, 211, 3 i_3 1 14 1159 745 745 13 1675 3 0 4 0 1 0 1, 558, 4 i_4 1 22 1032 2227 2227 22 2654 3 0 4 0 1 0 1, 1675, 5 i_5 1 20 444 3740 3740 17 3066 3 2 4 0 1 1 1, 2654, 6 i_6 1 19 226 4078 4078 18 3273 3 1 4 0 1 0 1, 3066, 7 i_7 1 22 111 4243 4243 20 3375 3 1 4 0 1 1 1, 3273, 8 i_8 1 64 55 3796 3796 59 3375 2 4 4 0 1 0 1, 3375, total_number_of_compose_operations_in_initial_skolem_function_generation = 23 total_ComposeTime_in_initial_skolem_function_generation = 8 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 32 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 8 total_FactorFindingTime_in_initial_skolem_function_generation = 2 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 229 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 23 total-time-in-initial-skolem-function-generation-without-size-computation-time = 229 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 3 milliseconds total-time-without-size-computation-time = 245 milliseconds total-time-in-interpolant-computation = 190 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 = 2 total time in initialization of skolem function generator-without-size-computation-time = 23 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 = 1 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 = 2 milliseconds compose-in-reverse-substitution = 28 time-in-reverse-substitution = 3 final-skolem-function-sizes = 3359, 3269, 2915, 1808, 806, 379, 162, 55,