benchmark type = generated benchmark name = ../benchmarks/equalization/16.v problem = variable_elimination machine = prolient number of factors = 21 number of variables to eliminate = 32 number of variables = 64 aig sizes of factors = 189, 191, 191, 181, 167, 167, 157, 133, 143, 143, 121, 109, 97, 85, 73, 61, 49, 37, 25, 11, 11, variables in factors = 64, 64, 64, 60, 56, 56, 52, 44, 48, 48, 40, 36, 32, 28, 24, 20, 16, 12, 8, 4, 4, variables to eliminate in factors = 32, 32, 32, 30, 28, 28, 26, 22, 24, 24, 20, 18, 16, 14, 12, 10, 8, 6, 4, 2, 2, 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 3 3 282 220 220 2 357 9 0 65 0 21 1 1,2,3, 189,191,191, 2 i_2_16 1 16 337 395 395 14 604 3 0 4 0 21 0 3, 357, 3 i_1_15 2 17 402 771 771 16 892 6 0 21 0 21 1 3,4, 604,181, 4 i_2_15 1 129 3141 1103 1103 123 3940 3 0 4 0 21 0 4, 892, 5 i_1_14 3 101 415 5742 5742 98 4251 9 1 45 0 21 0 4,5,6, 3940,167,167, 6 i_2_14 1 613 21487 6418 6418 605 25566 3 3 4 0 21 0 6, 4251, 7 i_1_13 2 367 364 31929 31929 339 25819 6 14 21 0 21 1 6,7, 25566,157, 8 i_2_13 1 11032 70784 32725 32725 10988 96294 3 39 4 0 21 1 7, 25819, 9 i_1_12 3 1205 307 114316 114316 1063 96502 9 107 45 0 21 5 7,9,10, 96294,143,143, 10 i_2_12 1 49997 797 116044 116044 49761 97195 3 198 4 0 21 13 10, 96502, 11 i_1_11 2 1483 409 126556 126556 1309 97511 6 133 21 1 21 4 8,10, 133,97195, 12 i_2_11 1 68747 21896 167778 167778 68551 119174 3 157 4 0 21 5 10, 97511, 13 i_1_10 2 5039 324 195273 195273 4774 119405 6 223 21 0 21 9 10,11, 119174,121, 14 i_2_10 1 169987 551032 201909 201909 169403 670008 3 504 4 0 21 16 11, 119405, 15 i_1_9 2 9825 302 986821 986821 8769 670238 6 876 21 0 21 77 11,12, 670008,109, total-time-in-initial-skolem-function-generation-without-size-computation-time = 0 milliseconds total-time-in-reverse-substitution-without-size-computation-time = 0 milliseconds total-time-without-size-computation-time = 1818898 milliseconds total-time-in-interpolant-computation = 1815654 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 638 total time in compute-support = 30 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 = 0 milliseconds size_computation_time_in_reverse_substitution_in_cegar = 0 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 = 638 milliseconds compose-in-reverse-substitution = 2 time-in-reverse-substitution = 873 final-skolem-function-sizes =