benchmark type = generated benchmark name = ../benchmarks/subtraction/16.v problem = variable_elimination machine = prolient number of factors = 30 number of variables to eliminate = 16 number of variables = 48 aig sizes of factors = 87, 91, 91, 79, 79, 73, 73, 67, 67, 61, 61, 55, 55, 49, 49, 43, 43, 37, 37, 13, 19, 13, 25, 25, 9, 19, 31, 31, 97, 97, variables in factors = 29, 31, 31, 27, 27, 25, 25, 23, 23, 21, 21, 19, 19, 17, 17, 15, 15, 13, 13, 5, 7, 5, 9, 9, 3, 7, 11, 11, 33, 33, variables to eliminate in factors = 14, 15, 15, 13, 13, 12, 12, 11, 11, 10, 10, 9, 9, 8, 8, 7, 7, 6, 6, 2, 3, 2, 4, 4, 1, 3, 5, 5, 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_16 2 2 270 108 108 2 305 6 0 50 0 30 0 29,30, 97,97, 2 i_15 3 6 185 361 361 6 438 9 0 45 0 30 0 2,3,30, 91,91,305, 3 i_14 2 5 155 530 530 4 542 6 1 21 0 30 0 1,30, 87,438, 4 i_13 3 9 121 693 693 7 615 9 1 45 0 30 0 4,5,30, 79,79,542, 5 i_12 3 5 171 829 829 4 737 9 0 45 0 30 0 6,7,30, 73,73,615, 6 i_11 3 6 177 1036 1036 5 873 9 0 45 0 30 1 8,9,30, 67,67,737, 7 i_10 3 9 256 1253 1253 7 1095 9 0 45 0 30 1 10,11,30, 61,61,873, 8 i_9 3 26 89 1680 1680 25 1150 9 1 45 0 30 0 12,13,30, 55,55,1095, 9 i_8 3 24 168 1816 1816 22 1274 9 1 45 0 30 0 14,15,30, 49,49,1150, 10 i_7 3 22 104 2042 2042 18 1354 9 2 45 0 30 0 16,17,30, 43,43,1274, 11 i_6 3 29 74 2216 2216 28 1408 9 1 45 0 30 0 18,19,30, 37,37,1354, 12 i_5 3 32 55 2393 2393 31 1448 9 0 45 0 30 0 27,28,30, 31,31,1408, 13 i_4 3 48 72 2551 2551 41 1507 9 1 45 0 30 0 23,24,30, 25,25,1448, 14 i_3 3 33 30 2694 2694 31 1533 9 1 45 0 30 1 21,26,30, 19,19,1507, 15 i_2 3 46 25 2731 2731 45 1561 9 1 45 0 30 0 20,22,30, 13,13,1533, 16 i_1 2 35 12 2947 2947 34 1561 4 0 20 0 30 0 25,30, 9,1561, total_number_of_compose_operations_in_initial_skolem_function_generation = 133 total_ComposeTime_in_initial_skolem_function_generation = 10 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 676 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 480 total_FactorFindingTime_in_initial_skolem_function_generation = 3 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 340 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 5 total-time-in-initial-skolem-function-generation-without-size-computation-time = 340 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 11 milliseconds total-time-without-size-computation-time = 351 milliseconds total-time-in-interpolant-computation = 310 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 4 milliseconds total time in compute-size = 6 total time in compute-support = 1 total time in initialization of skolem function generator-without-size-computation-time = 5 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 = 5 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 = 6 milliseconds compose-in-reverse-substitution = 120 time-in-reverse-substitution = 5 final-skolem-function-sizes = 1430, 1232, 1115, 1018, 950, 834, 701, 486, 434, 296, 216, 161, 122, 60, 35, 12,