benchmark type = generated benchmark name = ../benchmarks/subtraction/8.v problem = variable_elimination machine = prolient number of factors = 14 number of variables to eliminate = 8 number of variables = 24 aig sizes of factors = 39, 43, 43, 13, 19, 13, 25, 25, 9, 19, 31, 31, 49, 49, variables in factors = 13, 15, 15, 5, 7, 5, 9, 9, 3, 7, 11, 11, 17, 17, variables to eliminate in factors = 6, 7, 7, 2, 3, 2, 4, 4, 1, 3, 5, 5, 8, 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_8 2 2 156 60 60 1 173 6 0 34 0 14 1 13,14, 49,49, 2 i_7 3 5 121 244 244 4 275 9 1 45 0 14 0 2,3,14, 43,43,173, 3 i_6 2 2 79 378 378 1 333 6 0 21 0 14 0 1,14, 39,275, 4 i_5 3 10 90 508 508 10 410 9 0 45 0 14 0 11,12,14, 31,31,333, 5 i_4 3 8 35 653 653 8 435 9 0 45 0 14 0 7,8,14, 25,25,410, 6 i_3 3 12 29 726 726 4 459 9 1 45 0 14 0 5,10,14, 19,19,435, 7 i_2 3 4 27 839 839 3 488 9 1 45 0 14 0 4,6,14, 13,13,459, 8 i_1 2 7 12 907 907 7 488 4 0 20 0 14 0 9,14, 9,488, total_number_of_compose_operations_in_initial_skolem_function_generation = 61 total_ComposeTime_in_initial_skolem_function_generation = 3 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 300 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 112 total_FactorFindingTime_in_initial_skolem_function_generation = 1 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 49 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 = 49 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 0 milliseconds total-time-without-size-computation-time = 49 milliseconds total-time-in-interpolant-computation = 38 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 = 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 = 0 final-skolem-function-sizes = 433, 310, 216, 158, 82, 60, 37, 12,