benchmark type = generated benchmark name = ../benchmarks/max/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 = 91, 91, 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 3 111 262 262 2 240 9 1 49 0 5 0 1,2,5, 91,91,175, 2 i_10 1 3 86 315 315 3 292 3 0 4 0 5 0 5, 240, 3 i_11 1 1 69 422 422 1 332 3 0 4 0 5 0 5, 292, 4 i_12 1 8 56 504 504 4 364 3 1 4 0 5 0 5, 332, 5 i_13 1 2 42 576 576 2 387 3 0 4 0 5 0 5, 364, 6 i_14 1 5 24 624 624 4 398 3 0 4 0 5 0 5, 387, 7 i_15 1 9 13 654 654 9 403 3 0 4 0 5 0 5, 398, 8 i_2 1 15 226 456 456 15 571 3 0 4 0 5 0 5, 403, 9 i_3 1 9 213 775 775 8 729 3 0 4 0 5 1 5, 571, 10 i_4 1 35 200 1097 1097 33 879 3 0 4 0 5 1 5, 729, 11 i_5 1 19 185 1392 1392 18 1019 3 0 4 0 5 0 5, 879, 12 i_6 1 14 170 1671 1671 13 1151 3 1 4 0 5 0 5, 1019, 13 i_7 1 23 171 1931 1931 20 1289 3 0 4 0 5 0 5, 1151, 14 i_8 1 29 149 2203 2203 27 1411 3 2 4 0 5 0 5, 1289, 15 i_9 1 21 128 2439 2439 20 1516 3 1 4 0 5 0 5, 1411, 16 i_16 3 30 4 2680 2676 28 1516 6 1 41 0 5 0 3,4,5, 3,3,1516, total_number_of_compose_operations_in_initial_skolem_function_generation = 57 total_ComposeTime_in_initial_skolem_function_generation = 7 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 = 2 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 225 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 = 225 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 10 milliseconds total-time-without-size-computation-time = 236 milliseconds total-time-in-interpolant-computation = 207 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 = 1 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 = 3 final-skolem-function-sizes = 1398, 201, 143, 97, 59, 30, 14, 1177, 1005, 841, 685, 538, 400, 256, 129, 4,