benchmark type = generated benchmark name = ../benchmarks/max/32.v problem = variable_elimination machine = prolient number of factors = 5 number of variables to eliminate = 32 number of variables = 96 aig sizes of factors = 187, 187, 3, 3, 351, variables in factors = 64, 64, 2, 2, 96, variables to eliminate in factors = 32, 32, 1, 1, 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 3 5 223 504 504 3 480 9 0 49 0 5 1 1,2,5, 187,187,351, 2 i_10 1 3 300 609 609 2 666 3 1 4 0 5 0 5, 480, 3 i_11 1 11 285 984 984 4 842 3 1 4 0 5 0 5, 666, 4 i_12 1 9 270 1338 1338 8 1008 3 1 4 0 5 0 5, 842, 5 i_13 1 14 266 1678 1678 12 1175 3 1 4 0 5 0 5, 1008, 6 i_14 1 20 257 2014 2014 19 1337 3 0 4 0 5 0 5, 1175, 7 i_15 1 24 232 2351 2351 22 1480 3 1 4 0 5 0 5, 1337, 8 i_16 1 22 221 2649 2649 16 1617 3 2 4 0 5 0 5, 1480, 9 i_17 1 31 212 2936 2936 24 1750 3 6 4 0 5 0 5, 1617, 10 i_18 1 34 195 3201 3201 34 1871 3 0 4 0 5 0 5, 1750, 11 i_19 1 37 179 3457 3457 35 1981 3 2 4 0 5 0 5, 1871, 12 i_2 1 45 533 2069 2069 43 2389 3 1 4 0 5 0 5, 1981, 13 i_20 1 51 164 4254 4254 45 2489 3 2 4 0 5 0 5, 2389, 14 i_21 1 62 155 4458 4458 55 2585 3 2 4 0 5 1 5, 2489, 15 i_22 1 60 137 4651 4651 59 2668 3 1 4 0 5 0 5, 2585, 16 i_23 1 68 121 4835 4835 65 2740 3 1 4 0 5 1 5, 2668, 17 i_24 1 91 111 4973 4973 86 2807 3 5 4 0 5 0 5, 2740, 18 i_25 1 92 102 5114 5114 89 2870 3 2 4 0 5 1 5, 2807, 19 i_26 1 98 85 5242 5242 94 2921 3 2 4 0 5 1 5, 2870, 20 i_27 1 102 69 5360 5360 98 2961 3 3 4 0 5 0 5, 2921, 21 i_28 1 103 56 5435 5435 100 2993 3 2 4 0 5 0 5, 2961, 22 i_29 1 110 43 5512 5512 108 3017 3 2 4 0 5 0 5, 2993, 23 i_3 1 114 538 3487 3487 112 3464 3 1 4 0 5 1 5, 3017, 24 i_30 1 149 24 6254 6254 145 3475 3 2 4 0 5 1 5, 3464, 25 i_31 1 124 13 6289 6289 120 3480 3 3 4 0 5 1 5, 3475, 26 i_4 1 180 516 4359 4359 177 3914 3 2 4 0 5 0 5, 3480, 27 i_5 1 164 505 5182 5182 159 4342 3 3 4 0 5 0 5, 3914, 28 i_6 1 179 507 6005 6005 174 4779 3 3 4 0 5 0 5, 4342, 29 i_7 1 146 497 6831 6831 142 5211 3 3 4 0 5 0 5, 4779, 30 i_8 1 149 475 7652 7652 144 5627 3 3 4 0 5 0 5, 5211, 31 i_9 1 164 464 8439 8439 158 6036 3 3 4 0 5 0 5, 5627, 32 i_32 3 182 4 11090 11086 177 6036 6 2 41 0 5 0 3,4,5, 3,3,6036, total_number_of_compose_operations_in_initial_skolem_function_generation = 105 total_ComposeTime_in_initial_skolem_function_generation = 63 milliseconds total_number_of_boolean_operations_in_initial_skolem_function_generation = 210 total_BooleanOpTime_in_initial_skolem_function_generation = 0 milliseconds total_number_of_support_operations_in_initial_skolem_function_generation = 160 total_FactorFindingTime_in_initial_skolem_function_generation = 8 milliseconds total-time-in-initial-skolem-function-generation-without-size-computation-time = 2632 milliseconds total time in initialization of skolem function generator-without-size-computation-time = 1 total-time-in-initial-skolem-function-generation-without-size-computation-time = 2632 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 133 milliseconds total-time-without-size-computation-time = 2765 milliseconds total-time-in-interpolant-computation = 2529 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 17 total time in compute-support = 1 total time in initialization of skolem function generator-without-size-computation-time = 1 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 = 16 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 = 17 milliseconds compose-in-reverse-substitution = 496 time-in-reverse-substitution = 81 final-skolem-function-sizes = 5806, 2279, 2087, 1905, 1733, 1560, 1392, 1243, 1100, 961, 834, 4195, 718, 612, 510, 421, 343, 270, 201, 144, 98, 60, 3115, 30, 14, 2642, 2202, 1767, 1324, 886, 465, 4,