benchmark type = generated benchmark name = ../benchmarks/decomposition/16.v problem = variable_elimination machine = prolient number of factors = 30 number of variables to eliminate = 32 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 = 28, 30, 30, 26, 26, 24, 24, 22, 22, 20, 20, 18, 18, 16, 16, 14, 14, 12, 12, 4, 6, 4, 8, 8, 2, 6, 10, 10, 32, 32, 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_16 2 2 270 108 108 1 305 6 0 50 0 30 0 29,30, 97,97, 2 i_2_16 1 4 117 309 309 4 392 3 0 4 0 30 0 30, 305, 3 i_1_15 3 8 204 425 425 7 543 9 0 45 0 30 1 2,3,30, 91,91,392, 4 i_2_15 1 9 1 595 595 9 521 3 0 4 0 30 0 30, 543, 5 i_1_14 2 8 154 599 599 8 603 6 0 21 0 30 0 1,30, 87,521, 6 i_2_14 1 23 488 682 682 23 1027 3 0 4 0 30 0 30, 603, 7 i_1_13 3 5 176 1359 1359 5 1154 9 0 45 0 30 0 4,5,30, 79,79,1027, 8 i_2_13 1 48 1 1490 1490 48 1010 3 0 4 0 30 0 30, 1154, 9 i_1_12 3 15 127 1341 1341 15 1091 9 0 45 0 30 0 6,7,30, 73,73,1010, 10 i_2_12 1 36 1234 1430 1430 34 2274 3 0 4 0 30 0 30, 1091, 11 i_1_11 3 22 113 2991 2991 20 2347 9 2 45 0 30 0 8,9,30, 67,67,2274, 12 i_2_11 1 147 7895 3085 3085 144 10085 3 3 4 0 30 0 30, 2347, 13 i_1_10 3 79 141 12298 12298 66 10186 9 12 45 0 30 1 10,11,30, 61,61,10085, 14 i_2_10 1 692 2773 12638 12638 674 12810 3 7 4 0 30 1 30, 10186, 15 i_1_9 3 105 116 16573 16573 83 12893 9 12 45 0 30 0 12,13,30, 55,55,12810, 16 i_2_9 1 1117 2900 16783 16783 1104 15652 3 5 4 0 30 1 30, 12893, 17 i_1_8 3 154 94 20989 20989 139 15713 9 9 45 0 30 1 14,15,30, 49,49,15652, 18 i_2_8 1 1510 5056 21299 21299 1496 20495 3 11 4 0 30 1 30, 15713, 19 i_1_7 3 167 72 26018 26018 145 20539 9 13 45 0 30 0 16,17,30, 43,43,20495, 20 i_2_7 1 5966 1 26150 26150 5947 19718 3 16 4 0 30 0 30, 20539, 21 i_1_6 3 306 110 25897 25897 269 19805 9 22 45 0 30 1 18,19,30, 37,37,19718, 22 i_2_6 1 3148 1 25855 25855 3121 19466 3 17 4 0 30 1 30, 19805, 23 i_1_5 3 419 57 25535 25535 338 19507 9 68 45 1 30 1 27,28,30, 31,31,19466, 24 i_2_5 1 2053 5480 25970 25970 2024 24827 3 17 4 0 30 1 30, 19507, 25 i_1_4 3 378 60 35856 35856 348 24875 9 25 45 0 30 1 23,24,30, 25,25,24827, 26 i_2_4 1 6380 1 35828 35828 6342 24676 3 32 4 0 30 1 30, 24875, 27 i_1_3 3 818 66 34926 34926 774 24740 9 27 45 0 30 1 21,26,30, 19,19,24676, 28 i_2_3 1 6423 1 34945 34945 6385 24045 3 28 4 0 30 1 30, 24740, 29 i_1_2 3 662 26 33387 33387 624 24074 9 34 45 0 30 1 20,22,30, 13,13,24045, 30 i_2_2 1 2021 1 33667 33667 1981 23082 3 32 4 0 30 1 30, 24074, 31 i_1_1 2 575 9 33440 33440 535 23095 6 28 21 0 30 8 25,30, 9,23082, 32 i_2_1 1 9488 233608 33425 33425 9476 23095 2 9 4 0 30 1 30, 23095, total_number_of_compose_operations_in_initial_skolem_function_generation = 182 total_ComposeTime_in_initial_skolem_function_generation = 429 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 741 total_BooleanOpTime_in_initial_skolem_function_generation = 1 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 960 total_FactorFindingTime_in_initial_skolem_function_generation = 25 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 42701 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 2 total-time-in-initial-skolem-function-generation-without-size-computation-time = 42701 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 29873 milliseconds total-time-without-size-computation-time = 72574 milliseconds total-time-in-interpolant-computation = 42189 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 315 total time in compute-support = 10 total time in initialization of skolem function generator-without-size-computation-time = 2 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 = 113 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 202 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 = 315 milliseconds compose-in-reverse-substitution = 496 time-in-reverse-substitution = 29844 final-skolem-function-sizes = 256272, 256125, 256080, 1, 256001, 255947, 255696, 1, 255624, 255577, 254554, 254505, 247308, 247240, 244856, 244815, 242491, 242456, 238556, 1, 238538, 1, 238501, 238480, 233651, 1, 233633, 1, 233624, 1, 233616, 233608,