benchmark type = generated benchmark name = ../benchmarks/equalization/32.v problem = variable_elimination machine = prolient number of factors = 37 number of variables to eliminate = 64 number of variables = 128 aig sizes of factors = 381, 383, 383, 373, 359, 359, 349, 325, 335, 335, 313, 301, 289, 277, 265, 253, 241, 229, 217, 205, 193, 181, 169, 157, 145, 133, 121, 109, 97, 85, 73, 61, 49, 37, 25, 11, 11, variables in factors = 128, 128, 128, 124, 120, 120, 116, 108, 112, 112, 104, 100, 96, 92, 88, 84, 80, 76, 72, 68, 64, 60, 56, 52, 48, 44, 40, 36, 32, 28, 24, 20, 16, 12, 8, 4, 4, variables to eliminate in factors = 64, 64, 64, 62, 60, 60, 58, 54, 56, 56, 52, 50, 48, 46, 44, 42, 40, 38, 36, 34, 32, 30, 28, 26, 24, 22, 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_32 3 11 593 412 412 5 751 9 0 81 0 37 6 1,2,3, 381,383,383, 2 i_2_32 1 35 926 776 776 29 1426 3 0 4 0 37 1 3, 751, 3 i_1_31 2 32 875 1636 1636 29 2060 6 2 21 0 37 1 3,4, 1426,373, 4 i_2_31 1 69 672 2374 2374 67 2480 3 1 4 0 37 1 4, 2060, 5 i_1_30 3 55 1073 3018 3018 51 3310 9 0 45 0 37 3 4,5,6, 2480,359,359, 6 i_2_30 1 707 16304 4139 4139 703 19315 3 1 4 0 37 1 6, 3310, 7 i_1_29 2 1044 1112 27577 27577 1017 20170 6 13 21 0 37 7 6,7, 19315,349, 8 i_2_29 1 11340 71296 29914 29914 11309 91035 3 16 4 0 37 2 7, 20170, 9 i_1_28 3 3346 750 133664 133664 3200 91534 9 110 45 0 37 6 7,9,10, 91035,335,335, 10 i_2_28 1 116606 157879 133047 133047 116399 248769 3 141 4 0 37 10 10, 91534, 11 i_1_27 2 5749 718 302436 302436 5319 249260 6 314 21 0 37 37 8,10, 325,248769, 12 i_2_27 1 648001 884040 335714 335714 647371 1132643 3 413 4 0 37 37 10, 249260, 13 i_1_26 2 315913 1499 1776042 1776042 200604 1133899 6 114792 21 0 37 101 10,11, 1132643,313,