benchmark type = generated benchmark name = ../benchmarks/intermediate/32.v problem = variable_elimination machine = prolient number of factors = 1 number of variables to eliminate = 32 number of variables = 96 aig sizes of factors = 503, variables in factors = 96, variables to eliminate in factors = 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 1 45 1169 620 620 45 1468 3 0 4 0 1 0 1, 503, 2 i_10 1 58 2083 2036 2036 58 3351 3 0 4 0 1 0 1, 1468, 3 i_11 1 217 3865 5095 5095 210 6980 3 1 4 0 1 0 1, 3351, 4 i_12 1 380 3455 11059 11059 372 10227 3 7 4 0 1 0 1, 6980, 5 i_13 1 470 1622 16968 16968 463 11652 3 5 4 0 1 1 1, 10227, 6 i_14 1 502 1445 18737 18737 490 12912 3 10 4 0 1 1 1, 11652, 7 i_15 1 547 1417 21610 21610 531 14139 3 13 4 0 1 1 1, 12912, 8 i_16 1 747 2061 24567 24567 725 16026 3 14 4 0 1 0 1, 14139, 9 i_17 1 1004 1480 27851 27851 982 17328 3 19 4 0 1 1 1, 16026, 10 i_18 1 1255 1590 30185 30185 1223 18738 3 19 4 0 1 0 1, 17328, 11 i_19 1 1229 1012 32504 32504 1187 19556 3 37 4 0 1 1 1, 18738, 12 i_2 1 17847 54045 36163 36163 17685 73393 3 141 4 0 1 1 1, 19556, 13 i_20 1 7498 1271 130320 130320 7349 74496 3 104 4 0 1 7 1, 73393, 14 i_21 1 6852 1216 135507 135507 6691 75547 3 127 4 0 1 3 1, 74496, 15 i_22 1 8492 1815 137993 137993 8305 77201 3 152 4 0 1 3 1, 75547, 16 i_23 1 5373 1144 141346 141346 5170 78174 3 168 4 0 1 4 1, 77201, 17 i_24 1 6413 958 143492 143492 5849 78991 3 536 4 0 1 3 1, 78174, 18 i_25 1 6470 1618 144841 144841 6313 80462 3 122 4 0 1 3 1, 78991, 19 i_26 1 5027 904 148561 148561 4865 81210 3 126 4 0 1 3 1, 80462, 20 i_27 1 4262 825 150160 150160 4083 81890 3 136 4 0 1 6 1, 81210, 21 i_28 1 5043 1799 151049 151049 4860 83504 3 138 4 0 1 3 1, 81890, 22 i_29 1 5067 1671 152787 152787 4871 85033 3 156 4 0 1 3 1, 83504, 23 i_3 1 183975 132190 166626 166626 183761 217015 3 162 4 0 1 4 1, 85033, 24 i_30 1 11952 1478 398177 398177 11400 218392 3 436 4 0 1 22 1, 217015, 25 i_31 1 7825 679 397808 397808 7220 218984 3 481 4 0 1 22 1, 218392, 26 i_32 1 6924 2987 404385 404385 6250 221865 3 530 4 0 1 25 1, 218984, 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 = 1432634 milliseconds total-time-in-interpolant-computation = 1427118 algorithm-used = monolithic_compositionqe_interpolantskf_cofactorone ordering-used = least-occurring-first total time in ordering = 0 milliseconds total time in compute-size = 802 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 = 802 milliseconds compose-in-reverse-substitution = 2 time-in-reverse-substitution = 1698 final-skolem-function-sizes =