benchmark type = generated benchmark name = ../benchmarks/subtraction/32.v problem = variable_elimination machine = prolient number of factors = 62 number of variables to eliminate = 32 number of variables = 96 aig sizes of factors = 193, 193, 183, 187, 187, 175, 175, 169, 169, 163, 163, 157, 157, 151, 151, 145, 145, 139, 139, 133, 133, 127, 127, 121, 121, 115, 115, 109, 109, 103, 103, 97, 97, 91, 91, 85, 85, 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, variables in factors = 65, 65, 61, 63, 63, 59, 59, 57, 57, 55, 55, 53, 53, 51, 51, 49, 49, 47, 47, 45, 45, 43, 43, 41, 41, 39, 39, 37, 37, 35, 35, 33, 33, 31, 31, 29, 29, 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, variables to eliminate in factors = 32, 32, 30, 31, 31, 29, 29, 28, 28, 27, 27, 26, 26, 25, 25, 24, 24, 23, 23, 22, 22, 21, 21, 20, 20, 19, 19, 18, 18, 17, 17, 16, 16, 15, 15, 14, 14, 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, 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_32 2 4 410 204 204 2 479 6 0 82 0 62 1 1,2, 193,193, 2 i_31 3 16 472 530 530 7 833 9 0 45 0 62 2 2,4,5, 479,187,187, 3 i_30 2 19 411 934 934 17 1116 6 0 21 0 62 1 3,5, 183,833, 4 i_29 3 17 522 1333 1333 16 1516 9 0 45 0 62 1 5,6,7, 1116,175,175, 5 i_28 3 25 327 1991 1991 22 1732 9 1 45 0 62 1 7,8,9, 1516,169,169, 6 i_27 3 38 398 2259 2259 31 2021 9 1 45 0 62 1 9,10,11, 1732,163,163, 7 i_26 3 29 274 2663 2663 27 2189 9 1 45 0 62 1 11,12,13, 2021,157,157, 8 i_25 3 36 387 2929 2929 34 2480 9 0 45 0 62 1 13,14,15, 2189,151,151, 9 i_24 3 35 601 3356 3356 33 2975 9 1 45 0 62 1 15,16,17, 2480,145,145, 10 i_23 3 45 311 4295 4295 38 3187 9 3 45 0 62 1 17,18,19, 2975,139,139, 11 i_22 3 73 674 4677 4677 68 3756 9 2 45 0 62 1 19,20,21, 3187,133,133, 12 i_21 3 74 311 5539 5539 62 3977 9 6 45 0 62 1 21,22,23, 3756,127,127, 13 i_20 3 98 257 5984 5984 89 4142 9 3 45 0 62 1 23,24,25, 3977,121,121, 14 i_19 3 95 265 6271 6271 92 4327 9 2 45 0 62 1 25,26,27, 4142,115,115, 15 i_18 3 92 341 6662 6662 88 4591 9 2 45 0 62 1 27,28,29, 4327,109,109, 16 i_17 3 104 252 7097 7097 101 4768 9 2 45 0 62 0 29,30,31, 4591,103,103, 17 i_16 3 123 195 7381 7381 114 4899 9 2 45 0 62 1 31,32,33, 4768,97,97, 18 i_15 3 143 176 7731 7731 123 5013 9 13 45 0 62 1 33,34,35, 4899,91,91, 19 i_14 3 144 247 8016 8016 136 5197 9 3 45 0 62 1 35,36,37, 5013,85,85, 20 i_13 3 162 122 8426 8426 158 5264 9 2 45 0 62 1 37,38,39, 5197,79,79, 21 i_12 3 160 126 8699 8699 155 5349 9 3 45 0 62 1 39,40,41, 5264,73,73, 22 i_11 3 205 139 8966 8966 200 5440 9 3 45 0 62 1 41,42,43, 5349,67,67, 23 i_10 3 253 136 9315 9315 246 5537 9 6 45 0 62 0 43,44,45, 5440,61,61, 24 i_9 3 191 226 9685 9685 183 5726 9 3 45 0 62 5 45,46,47, 5537,55,55, 25 i_8 3 245 79 10120 10120 237 5778 9 3 45 0 62 0 47,48,49, 5726,49,49, 26 i_7 3 307 201 10398 10398 294 5953 9 3 45 0 62 0 49,50,51, 5778,43,43, 27 i_6 3 290 169 10770 10770 279 6101 9 8 45 0 62 0 51,52,53, 5953,37,37, 28 i_5 3 302 100 11198 11198 291 6173 9 5 45 0 62 0 53,61,62, 6101,31,31, 29 i_4 3 324 49 11531 11531 318 6207 9 5 45 0 62 0 57,58,62, 25,25,6173, 30 i_3 3 393 24 11675 11675 372 6228 9 6 45 0 62 1 55,60,62, 19,19,6207, 31 i_2 3 357 27 11904 11904 341 6258 9 13 45 0 62 1 54,56,62, 13,13,6228, 32 i_1 2 406 8 12083 12083 401 6258 4 4 20 0 62 1 59,62, 9,6258, total_number_of_compose_operations_in_initial_skolem_function_generation = 277 total_ComposeTime_in_initial_skolem_function_generation = 106 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 1428 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 1984 total_FactorFindingTime_in_initial_skolem_function_generation = 30 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 4778 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 9 total-time-in-initial-skolem-function-generation-without-size-computation-time = 4778 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 325 milliseconds total-time-without-size-computation-time = 5103 milliseconds total-time-in-interpolant-computation = 4575 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 40 total time in compute-support = 25 total time in initialization of skolem function generator-without-size-computation-time = 9 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 = 37 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 3 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 = 40 milliseconds compose-in-reverse-substitution = 496 time-in-reverse-substitution = 238 final-skolem-function-sizes = 5967, 5707, 5383, 5110, 4727, 4516, 4229, 4066, 3795, 3306, 3096, 2530, 2310, 2137, 1949, 1688, 1508, 1379, 1266, 1075, 1002, 920, 828, 732, 543, 495, 319, 172, 91, 52, 33, 8,